### Nuprl Lemma : rdiv-factorial-lemma2

x:ℝ. ∀b:ℕ.  (((x x) ≤ r(b b))  (∀n:ℕ(((b ÷ 2) ≤ n)  ((x x) ≤ (r((2 (n 1))!)/r((2 n)!))))))

Proof

Definitions occuring in Statement :  rdiv: (x/y) rleq: x ≤ y rmul: b int-to-real: r(n) real: nat: le: A ≤ B all: x:A. B[x] implies:  Q divide: n ÷ m multiply: m add: m natural_number: \$n fact: (n)!
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q uall: [x:A]. B[x] member: t ∈ T nat: int_nzero: -o true: True nequal: a ≠ b ∈  not: ¬A uimplies: supposing a sq_type: SQType(T) guard: {T} false: False prop: nat_plus: + less_than: a < b squash: T less_than': less_than'(a;b) and: P ∧ Q ge: i ≥  decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top subtype_rel: A ⊆B iff: ⇐⇒ Q rev_implies:  Q uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) rge: x ≥ y le: A ≤ B
Lemmas referenced :  int_formula_prop_eq_lemma int_formula_prop_less_lemma intformeq_wf intformless_wf mul_preserves_le rleq_weakening_equal rleq_functionality_wrt_implies rleq-int req_weakening rleq_functionality fact-non-zero rneq-int nat_plus_wf int_formula_prop_wf int_term_value_var_lemma int_term_value_add_lemma int_term_value_mul_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermAdd_wf itermMultiply_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le nat_properties fact_wf rdiv_wf real_wf int-to-real_wf rmul_wf rleq_wf nat_wf le_wf rdiv-factorial-lemma1 less_than_wf rem_bounds_1 nequal_wf true_wf equal_wf int_subtype_base subtype_base_sq div_rem_sum
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality dependent_set_memberEquality natural_numberEquality addLevel instantiate cumulativity intEquality independent_isectElimination hypothesis dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination voidElimination because_Cache sqequalRule independent_pairFormation introduction imageMemberEquality baseClosed divideEquality multiplyEquality productElimination addEquality unionElimination dependent_pairFormation lambdaEquality int_eqEquality isect_memberEquality voidEquality computeAll applyEquality imageElimination

Latex:
\mforall{}x:\mBbbR{}.  \mforall{}b:\mBbbN{}.
(((x  *  x)  \mleq{}  r(b  *  b))  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  (((b  \mdiv{}  2)  \mleq{}  n)  {}\mRightarrow{}  ((x  *  x)  \mleq{}  (r((2  *  (n  +  1))!)/r((2  *  n)!))))))

Date html generated: 2016_05_18-AM-08_04_46
Last ObjectModification: 2016_01_17-AM-02_19_57

Theory : reals

Home Index