### Nuprl Lemma : req-iff-rabs-rleq

`∀x,y:ℝ.  (x = y `⇐⇒` ∀m:ℕ+. (|x - y| ≤ (r1/r(m))))`

Proof

Definitions occuring in Statement :  rdiv: `(x/y)` rleq: `x ≤ y` rabs: `|x|` rsub: `x - y` req: `x = y` int-to-real: `r(n)` real: `ℝ` nat_plus: `ℕ+` 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` so_lambda: `λ2x.t[x]` nat_plus: `ℕ+` uimplies: `b supposing a` rneq: `x ≠ y` guard: `{T}` or: `P ∨ Q` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` top: `Top` so_apply: `x[s]` subtype_rel: `A ⊆r B` true: `True` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)` absval: `|i|` itermConstant: `"const"` req_int_terms: `t1 ≡ t2` rdiv: `(x/y)` squash: `↓T` sq_exists: `∃x:{A| B[x]}` rless: `x < y`
Lemmas referenced :  nat_plus_wf req_wf all_wf rleq_wf rabs_wf rsub_wf rdiv_wf int-to-real_wf rless-int nat_plus_properties decidable__lt satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf rless_wf real_wf absval_wf rinv_wf2 rmul_wf rleq-int-fractions2 decidable__le intformle_wf itermMultiply_wf int_formula_prop_le_lemma int_term_value_mul_lemma rleq_functionality rabs_functionality rsub_functionality req_weakening uiff_transitivity2 real_term_polynomial itermSubtract_wf real_term_value_const_lemma real_term_value_sub_lemma real_term_value_var_lemma req-iff-rsub-is-0 req_transitivity real_term_value_mul_lemma rinv-as-rdiv squash_wf true_wf rabs-int rless_transitivity1 rless_irreflexivity small-reciprocal-real req-iff-not-rneq rneq-iff-rabs rneq_wf not_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation cut introduction extract_by_obid hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule lambdaEquality natural_numberEquality setElimination rename because_Cache independent_isectElimination inrFormation dependent_functionElimination productElimination independent_functionElimination unionElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality computeAll applyEquality minusEquality multiplyEquality imageElimination equalityTransitivity equalitySymmetry imageMemberEquality baseClosed impliesFunctionality addLevel lemma_by_obid dependent_set_memberEquality

Latex:
\mforall{}x,y:\mBbbR{}.    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \mforall{}m:\mBbbN{}\msupplus{}.  (|x  -  y|  \mleq{}  (r1/r(m))))

Date html generated: 2017_10_03-AM-09_06_12
Last ObjectModification: 2017_07_28-AM-07_41_59

Theory : reals

Home Index