Nuprl Lemma : r-archimedean2

`∀x:ℝ. ∃N:ℕ. ∀n:{N...}. (|(x/r(n + 1))| ≤ (r1/r(2)))`

Proof

Definitions occuring in Statement :  rdiv: `(x/y)` rleq: `x ≤ y` rabs: `|x|` int-to-real: `r(n)` real: `ℝ` int_upper: `{i...}` nat: `ℕ` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` add: `n + m` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` rge: `x ≥ y` top: `Top` not: `¬A` false: `False` satisfiable_int_formula: `satisfiable_int_formula(fmla)` decidable: `Dec(P)` ge: `i ≥ j ` nat: `ℕ` rev_uimplies: `rev_uimplies(P;Q)` uiff: `uiff(P;Q)` true: `True` less_than': `less_than'(a;b)` squash: `↓T` less_than: `a < b` prop: `ℙ` implies: `P `` Q` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` or: `P ∨ Q` guard: `{T}` rneq: `x ≠ y` uimplies: `b supposing a` and: `P ∧ Q` exists: `∃x:A. B[x]` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` int_upper: `{i...}` so_apply: `x[s]` subtype_rel: `A ⊆r B` rdiv: `(x/y)` itermConstant: `"const"` req_int_terms: `t1 ≡ t2` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` bfalse: `ff` sq_type: `SQType(T)` bnot: `¬bb` ifthenelse: `if b then t else f fi ` assert: `↑b`
Lemmas referenced :  real_wf rleq_weakening_equal rleq_functionality_wrt_implies rmul_comm rmul-rdiv-cancel2 req_weakening rleq_functionality uiff_transitivity int_formula_prop_wf int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma itermConstant_wf itermAdd_wf itermVar_wf intformle_wf intformnot_wf satisfiable-full-omega-tt decidable__le nat_properties rleq-int rless_wf rleq_wf rless-int rdiv_wf rmul_preserves_rleq rabs_wf int-to-real_wf rmul_wf r-archimedean int_upper_wf all_wf int_upper_properties decidable__lt intformand_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_less_lemma rneq_wf squash_wf true_wf rabs-int iff_weakening_equal absval_pos le_wf rinv_wf2 absval_wf rneq_functionality rabs-of-nonneg rabs-rdiv rless_functionality req_transitivity real_term_polynomial itermSubtract_wf itermMultiply_wf real_term_value_const_lemma real_term_value_sub_lemma real_term_value_mul_lemma real_term_value_var_lemma req-iff-rsub-is-0 rmul-rinv3 uiff_transitivity2 rinv-mul-as-rdiv absval_unfold lt_int_wf bool_wf eqtt_to_assert assert_of_lt_int top_wf less_than_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid hypothesis equalitySymmetry equalityTransitivity computeAll voidEquality voidElimination isect_memberEquality intEquality int_eqEquality lambdaEquality unionElimination rename setElimination addEquality baseClosed imageMemberEquality independent_pairFormation independent_functionElimination inrFormation sqequalRule independent_isectElimination because_Cache dependent_pairFormation productElimination hypothesisEquality natural_numberEquality isectElimination thin dependent_functionElimination sqequalHypSubstitution applyEquality imageElimination universeEquality dependent_set_memberEquality minusEquality equalityElimination lessCases isect_memberFormation sqequalAxiom promote_hyp instantiate cumulativity

Latex:
\mforall{}x:\mBbbR{}.  \mexists{}N:\mBbbN{}.  \mforall{}n:\{N...\}.  (|(x/r(n  +  1))|  \mleq{}  (r1/r(2)))

Date html generated: 2017_10_03-AM-09_23_03
Last ObjectModification: 2017_07_28-AM-07_46_12

Theory : reals

Home Index