### Nuprl Lemma : rneq-iff-rabs

`∀x,y:ℝ.  (x ≠ y `⇐⇒` r0 < |x - y|)`

Proof

Definitions occuring in Statement :  rneq: `x ≠ y` rless: `x < y` rabs: `|x|` rsub: `x - y` int-to-real: `r(n)` real: `ℝ` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` rev_implies: `P `` Q` top: `Top` rneq: `x ≠ y` or: `P ∨ Q` guard: `{T}` uimplies: `b supposing a` itermConstant: `"const"` req_int_terms: `t1 ≡ t2` false: `False` not: `¬A` uiff: `uiff(P;Q)`
Lemmas referenced :  rneq_wf rless_wf int-to-real_wf rabs_wf rsub_wf real_wf rabs-as-rmax rmax_strict_ub rminus_wf rless-implies-rless real_term_polynomial itermSubtract_wf itermVar_wf itermMinus_wf itermConstant_wf real_term_value_const_lemma real_term_value_sub_lemma real_term_value_var_lemma real_term_value_minus_lemma req-iff-rsub-is-0 rneq-if-rabs
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis natural_numberEquality sqequalRule isect_memberEquality voidElimination voidEquality dependent_functionElimination productElimination independent_functionElimination unionElimination inrFormation independent_isectElimination computeAll lambdaEquality int_eqEquality intEquality inlFormation because_Cache

Latex:
\mforall{}x,y:\mBbbR{}.    (x  \mneq{}  y  \mLeftarrow{}{}\mRightarrow{}  r0  <  |x  -  y|)

Date html generated: 2017_10_03-AM-08_31_12
Last ObjectModification: 2017_07_28-AM-07_26_59

Theory : reals

Home Index