### Nuprl Lemma : rinverse-nonzero

`∀x:ℝ. (x ≠ r0 `` (r1/x) ≠ r0)`

Proof

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

Latex:
\mforall{}x:\mBbbR{}.  (x  \mneq{}  r0  {}\mRightarrow{}  (r1/x)  \mneq{}  r0)

Date html generated: 2016_05_18-AM-07_24_29
Last ObjectModification: 2016_01_17-AM-01_57_01

Theory : reals

Home Index