Nuprl Lemma : small-ctrex1-bounds

(r1/r(10))≤r(10^1141) small-ctrex1()≤(r1/r(4))


Proof




Definitions occuring in Statement :  small-ctrex1: small-ctrex1() rdiv: (x/y) rbetween: x≤y≤z rmul: b int-to-real: r(n) natural_number: $n fastexp: i^n
Definitions unfolded in proof :  prop: implies:  Q not: ¬A false: False le: A ≤ B nat: uall: [x:A]. B[x] and: P ∧ Q member: t ∈ T true: True efficient-exp-ext fastexp: i^n less_than': less_than'(a;b) squash: T less_than: a < b rational-approx: (x within 1/n) sq_type: SQType(T) nequal: a ≠ b ∈  int_nzero: -o rev_implies:  Q iff: ⇐⇒ Q all: x:A. B[x] or: P ∨ Q guard: {T} rneq: x ≠ y uimplies: supposing a nat_plus: + subtype_rel: A ⊆B uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) top: Top exists: x:A. B[x] satisfiable_int_formula: satisfiable_int_formula(fmla) decidable: Dec(P) label: ...$L... t real: rnonneg: rnonneg(x) rleq: x ≤ y rbetween: x≤y≤z rge: x ≥ y rsub: y
Lemmas referenced :  efficient-exp-ext radd-int-fractions rleq-int-fractions radd-preserves-rleq rminus_wf radd_comm radd-rminus-assoc rleq_weakening_equal rleq_functionality_wrt_implies rmul-rsub-distrib rmul-one-both rmul-assoc req_functionality rmul_functionality req_transitivity uiff_transitivity rmul_preserves_rleq2 rleq-int decidable__le intformle_wf int_formula_prop_le_lemma less_than'_wf rmul-distrib2 rmul_comm rmul-rdiv-cancel req-iff-bdd-diff trivial-bdd-diff rmul-rdiv2 radd_functionality radd_wf rabs-difference-bound-rleq rmul-neq-zero rmul-int rdiv_functionality rmul_wf equal_wf int_entire_a rneq-int decidable__equal_int nat_plus_wf real_wf rleq_wf nat_plus_properties decidable__lt satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermConstant_wf itermMultiply_wf itermVar_wf intformeq_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_mul_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_wf int-rdiv-req req_inversion req_weakening rsub_functionality rabs_functionality rleq_functionality ctrex1-calculation rabs_wf rsub_wf small-ctrex1_wf rdiv_wf int-to-real_wf less_than_wf rless-int rless_wf int-rdiv_wf subtype_base_sq int_subtype_base equal-wf-base true_wf nequal_wf rational-approx-property fastexp_wf false_wf le_wf
Rules used in proof :  cut baseClosed imageMemberEquality introduction hypothesisEquality hypothesis lambdaFormation dependent_set_memberEquality thin isectElimination sqequalHypSubstitution lemma_by_obid natural_numberEquality independent_pairFormation sqequalReflexivity computationStep sqequalTransitivity sqequalRule sqequalSubstitution voidElimination equalitySymmetry equalityTransitivity intEquality cumulativity instantiate addLevel independent_functionElimination productElimination dependent_functionElimination inrFormation independent_isectElimination multiplyEquality because_Cache applyEquality equalityEquality computeAll voidEquality isect_memberEquality int_eqEquality dependent_pairFormation unionElimination setEquality lambdaEquality rename setElimination promote_hyp levelHypothesis axiomEquality minusEquality independent_pairEquality isect_memberFormation functionEquality impliesFunctionality addEquality

Latex:
(r1/r(10))\mleq{}r(10\^{}1141)  *  small-ctrex1()\mleq{}(r1/r(4))



Date html generated: 2016_05_18-AM-10_48_58
Last ObjectModification: 2016_01_17-AM-00_37_10

Theory : reals


Home Index