### Nuprl Lemma : rational-approx-property1

`∀x:ℝ. ∀n:ℕ+.  (x ≤ ((x within 1/n) + (r1/r(n))))`

Proof

Definitions occuring in Statement :  rational-approx: `(x within 1/n)` rdiv: `(x/y)` rleq: `x ≤ y` radd: `a + b` int-to-real: `r(n)` real: `ℝ` nat_plus: `ℕ+` all: `∀x:A. B[x]` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` real: `ℝ` and: `P ∧ Q` nat_plus: `ℕ+` uimplies: `b supposing a` rneq: `x ≠ y` guard: `{T}` or: `P ∨ Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` top: `Top` prop: `ℙ` rge: `x ≥ y` uiff: `uiff(P;Q)` squash: `↓T` true: `True` subtype_rel: `A ⊆r B` rsub: `x - y`
Lemmas referenced :  radd-rminus-assoc req_weakening radd_comm radd_functionality rleq_functionality uiff_transitivity iff_weakening_equal radd_comm_eq true_wf squash_wf rminus_wf radd_wf rleq_wf radd-preserves-rleq rleq_weakening_equal rleq_functionality_wrt_implies rless_wf int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_less_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermConstant_wf intformless_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__lt nat_plus_properties rless-int int-to-real_wf rdiv_wf rabs_wf rational-approx_wf rsub_wf rabs-bounds real_wf nat_plus_wf rational-approx-property-ext
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation hypothesis sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality isectElimination setElimination rename productElimination natural_numberEquality independent_isectElimination sqequalRule inrFormation because_Cache independent_functionElimination unionElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll applyEquality imageElimination equalityTransitivity equalitySymmetry imageMemberEquality baseClosed universeEquality

Latex:
\mforall{}x:\mBbbR{}.  \mforall{}n:\mBbbN{}\msupplus{}.    (x  \mleq{}  ((x  within  1/n)  +  (r1/r(n))))

Date html generated: 2016_05_18-AM-07_30_17
Last ObjectModification: 2016_01_17-AM-02_00_07

Theory : reals

Home Index