### Nuprl Lemma : rinv_preserves_rneq

`∀a,b:ℝ.  (a ≠ r0 `` b ≠ r0 `` a ≠ b `` (r1/a) ≠ (r1/b))`

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` prop: `ℙ` uall: `∀[x:A]. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` true: `True` uimplies: `b supposing a` itermConstant: `"const"` req_int_terms: `t1 ≡ t2` false: `False` not: `¬A` top: `Top` uiff: `uiff(P;Q)` guard: `{T}` rdiv: `(x/y)` cand: `A c∧ B`
Lemmas referenced :  rneq_wf int-to-real_wf real_wf rmul_reverses_rless rless-int rless_wf rmul_wf rless_functionality rminus_wf real_term_polynomial itermSubtract_wf itermMultiply_wf itermVar_wf itermConstant_wf itermMinus_wf real_term_value_const_lemma real_term_value_sub_lemma real_term_value_mul_lemma real_term_value_var_lemma real_term_value_minus_lemma req-iff-rsub-is-0 rinv_preserves_rless rless-implies-rless rsub_wf rdiv_wf rmul_reverses_rless_iff rinv_wf2 req_transitivity rminus_functionality rinv-as-rdiv rneq-symmetry rminus-neq-zero rminus-rdiv2 rmul-rinv rmul_preserves_rless rless_transitivity2 rleq_weakening_rless
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution unionElimination thin cut introduction extract_by_obid isectElimination hypothesisEquality hypothesis natural_numberEquality dependent_functionElimination minusEquality independent_functionElimination productElimination sqequalRule independent_pairFormation imageMemberEquality baseClosed independent_isectElimination computeAll lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality because_Cache inrFormation inlFormation

Latex:
\mforall{}a,b:\mBbbR{}.    (a  \mneq{}  r0  {}\mRightarrow{}  b  \mneq{}  r0  {}\mRightarrow{}  a  \mneq{}  b  {}\mRightarrow{}  (r1/a)  \mneq{}  (r1/b))

Date html generated: 2017_10_03-AM-08_36_54
Last ObjectModification: 2017_07_28-AM-07_29_44

Theory : reals

Home Index