### Nuprl Lemma : rmul-nonzero

`∀x,y:ℝ.  (x * y ≠ r0 `⇐⇒` x ≠ r0 ∧ y ≠ r0)`

Proof

Definitions occuring in Statement :  rneq: `x ≠ y` rmul: `a * b` int-to-real: `r(n)` real: `ℝ` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` rneq: `x ≠ y` or: `P ∨ Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` guard: `{T}` rev_implies: `P `` Q` uimplies: `b supposing a` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` true: `True` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)`
Lemmas referenced :  rmul-one-both rdiv-zero rmul-rdiv-cancel rmul-ac req_transitivity rmul_comm rmul_functionality rmul-assoc req_inversion req_functionality uiff_transitivity rmul-int-rdiv rmul-rdiv-cancel2 rmul-zero-both rless_functionality req_weakening req_wf rless-int rmul_reverses_rless rdiv_wf rmul_reverses_rless_iff real_wf and_wf rmul-neq-zero rmul_wf rneq_wf rmul-is-positive int-to-real_wf rless_wf rmul-is-negative
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation sqequalHypSubstitution unionElimination thin cut lemma_by_obid dependent_functionElimination hypothesisEquality independent_functionElimination hypothesis inlFormation isectElimination natural_numberEquality productElimination sqequalRule inrFormation because_Cache independent_isectElimination introduction imageMemberEquality baseClosed multiplyEquality addLevel promote_hyp

Latex:
\mforall{}x,y:\mBbbR{}.    (x  *  y  \mneq{}  r0  \mLeftarrow{}{}\mRightarrow{}  x  \mneq{}  r0  \mwedge{}  y  \mneq{}  r0)

Date html generated: 2016_05_18-AM-07_33_46
Last ObjectModification: 2016_01_17-AM-02_02_16

Theory : reals

Home Index