### Nuprl Lemma : r-archimedean-rabs

`∀x:ℝ. ∃n:ℕ. (|x| ≤ r(n))`

Proof

Definitions occuring in Statement :  rleq: `x ≤ y` rabs: `|x|` int-to-real: `r(n)` real: `ℝ` nat: `ℕ` all: `∀x:A. B[x]` exists: `∃x:A. B[x]`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` exists: `∃x:A. B[x]` uall: `∀[x:A]. B[x]` top: `Top` nat: `ℕ` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` cand: `A c∧ B` prop: `ℙ` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` le: `A ≤ B` less_than': `less_than'(a;b)` false: `False` not: `¬A` true: `True` squash: `↓T` req_int_terms: `t1 ≡ t2`
Lemmas referenced :  r-archimedean rabs-as-rmax rmax_lb rminus_wf int-to-real_wf rleq_wf rabs_wf real_wf rmul_reverses_rleq rleq-int false_wf rmul_wf itermSubtract_wf itermMultiply_wf itermVar_wf itermConstant_wf itermMinus_wf req-iff-rsub-is-0 rminus-rminus rleq_functionality req_transitivity req_weakening squash_wf true_wf rminus-int real_polynomial_null real_term_value_sub_lemma real_term_value_mul_lemma real_term_value_var_lemma real_term_value_const_lemma real_term_value_minus_lemma
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation hypothesis sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality productElimination dependent_pairFormation sqequalRule isectElimination isect_memberEquality voidElimination voidEquality setElimination rename independent_isectElimination independent_pairFormation minusEquality natural_numberEquality independent_functionElimination promote_hyp because_Cache applyEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry imageMemberEquality baseClosed approximateComputation int_eqEquality intEquality

Latex:
\mforall{}x:\mBbbR{}.  \mexists{}n:\mBbbN{}.  (|x|  \mleq{}  r(n))

Date html generated: 2017_10_03-AM-09_22_41
Last ObjectModification: 2017_07_28-AM-07_45_56

Theory : reals

Home Index