Nuprl Lemma : neg-approx-of-nonneg-real

∀x:ℝ. ((r0 ≤ x) ⇒ (∀n:ℕ⁺. (((x n) ≤ 0) ⇒ (|x n| ≤ 2))))

Proof

Definitions occuring in Statement : rleq: x ≤ y, int-to-real: r(n), real: ℝ, absval: |i|, nat_plus: ℕ⁺, le: A ≤ B, all: ∀x:A. B[x], implies: P ⇒ Q, apply: f a, natural_number: $n
Definitions unfolded in proof : all: ∀x:A. B[x], implies: P ⇒ Q, member: t ∈ T, uall: ∀[x:A]. B[x], real: ℝ, nat_plus: ℕ⁺, uimplies: b supposing a, rneq: x ≠ y, guard: {T}, or: P ∨ Q, iff: P ⇐⇒ Q, and: P ∧ Q, rev_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: ℙ, rational-approx: (x within 1/n), int_nzero: ℤ^-^o, nequal: a ≠ b ∈ T , subtype_rel: A ⊆r B, le: A ≤ B, uiff: uiff(P;Q), rge: x ≥ y, less_than: a < b, squash: ↓T, less_than': less_than'(a;b), true: True, rleq: x ≤ y, rnonneg: rnonneg(x), 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 : rational-approx-property, rabs-difference-bound-rleq, rational-approx_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, le_wf, nat_plus_wf, rleq_wf, real_wf, radd_wf, int-rdiv_wf, intformeq_wf, itermMultiply_wf, int_formula_prop_eq_lemma, int_term_value_mul_lemma, equal-wf-base, int_subtype_base, nequal_wf, rleq_functionality, req_weakening, radd_functionality, int-rdiv-req, rleq_functionality_wrt_implies, rleq_weakening_equal, req-int-fractions, mul_nat_plus, less_than_wf, decidable__equal_int, rmul_preserves_rleq2, rleq-int, decidable__le, intformle_wf, int_formula_prop_le_lemma, less_than'_wf, rsub_wf, rmul_wf, rinv_wf2, req_transitivity, radd-rdiv, rdiv_functionality, radd-int, real_term_polynomial, itermSubtract_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_functionality, rmul-rinv, absval_unfold, lt_int_wf, bool_wf, eqtt_to_assert, assert_of_lt_int, top_wf, eqff_to_assert, equal_wf, bool_cases_sqequal, subtype_base_sq, bool_subtype_base, assert-bnot, itermMinus_wf, itermAdd_wf, int_term_value_minus_lemma, int_term_value_add_lemma
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, lambdaFormation, cut, introduction, extract_by_obid, sqequalHypSubstitution, dependent_functionElimination, thin, hypothesisEquality, because_Cache, isectElimination, setElimination, rename, hypothesis, natural_numberEquality, independent_isectElimination, sqequalRule, inrFormation, productElimination, independent_functionElimination, unionElimination, dependent_pairFormation, lambdaEquality, int_eqEquality, intEquality, isect_memberEquality, voidElimination, voidEquality, independent_pairFormation, computeAll, applyEquality, dependent_set_memberEquality, multiplyEquality, baseApply, closedConclusion, baseClosed, imageMemberEquality, addEquality, isect_memberFormation, independent_pairEquality, minusEquality, axiomEquality, equalityTransitivity, equalitySymmetry, equalityElimination, lessCases, sqequalAxiom, imageElimination, promote_hyp, instantiate, cumulativity

Latex:
\mforall{}x:\mBbbR{}. ((r0 \mleq{} x) {}\mRightarrow{} (\mforall{}n:\mBbbN{}\msupplus{}. (((x n) \mleq{} 0) {}\mRightarrow{} (|x n| \mleq{} 2)))) Date html generated: 2017_10_03-AM-08_45_26 Last ObjectModification: 2017_07_28-AM-07_32_04 Theory : reals Home Index