Nuprl Lemma : cosine-approx-lemma

a:{2...}. ∀N:ℕ+.  (∃k:ℕ [(N ≤ (a^((2 k) 2) ((2 k) 2)!))])


Proof




Definitions occuring in Statement :  fact: (n)! exp: i^n int_upper: {i...} nat_plus: + nat: le: A ≤ B all: x:A. B[x] sq_exists: x:A [B[x]] multiply: m add: m natural_number: $n
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T uall: [x:A]. B[x] int_upper: {i...} nat: nat_plus: + decidable: Dec(P) or: P ∨ Q uimplies: supposing a not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False top: Top and: P ∧ Q prop: so_lambda: λ2x.t[x] so_apply: x[s] squash: T label: ...$L... t guard: {T} true: True subtype_rel: A ⊆B iff: ⇐⇒ Q le: A ≤ B less_than': less_than'(a;b) rev_uimplies: rev_uimplies(P;Q) ge: i ≥  sq_exists: x:A [B[x]] sq_type: SQType(T) rev_implies:  Q lt_int: i <j bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  bfalse: ff bnot: ¬bb assert: b subtract: m less_than: a < b fact: (n)! primrec: primrec(n;b;c) primtailrec: primtailrec(n;i;b;f)
Lemmas referenced :  int_upper_wf int_upper_properties mul_preserves_le nat_plus_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf istype-le itermMultiply_wf int_term_value_mul_lemma set-value-type equal_wf le_wf int-value-type squash_wf true_wf istype-universe exp2 decidable__equal_int intformeq_wf int_formula_prop_eq_lemma subtype_rel_self iff_weakening_equal nat_plus_wf istype-int_upper genfact-inv_wf itermAdd_wf intformless_wf int_term_value_add_lemma int_formula_prop_less_lemma mul_preserves_le2 decidable__lt istype-less_than nat_plus_subtype_nat upper_subtype_nat istype-false less_than_functionality le_weakening multiply_functionality_wrt_le exp_wf2 nat_properties fact_wf subtype_base_sq set_subtype_base int_subtype_base ge_wf genfact-step btrue_wf eqtt_to_assert assert_of_lt_int eqff_to_assert lt_int_wf bool_cases_sqequal bool_wf bool_subtype_base assert-bnot iff_weakening_uiff assert_wf less_than_wf subtract-1-ge-0 mul-commutes fact_unroll subtract_wf itermSubtract_wf int_term_value_subtract_lemma istype-nat exp-positive exp_add
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality hypothesis hypothesisEquality setElimination rename dependent_set_memberEquality_alt multiplyEquality because_Cache dependent_functionElimination unionElimination independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt int_eqEquality isect_memberEquality_alt voidElimination sqequalRule independent_pairFormation universeIsType cutEval equalityTransitivity equalitySymmetry equalityIstype inhabitedIsType intEquality applyEquality imageElimination instantiate universeEquality applyLambdaEquality imageMemberEquality baseClosed productElimination addEquality cumulativity intWeakElimination axiomSqEquality functionIsTypeImplies sqequalIntensionalEquality baseApply closedConclusion equalityElimination promote_hyp

Latex:
\mforall{}a:\{2...\}.  \mforall{}N:\mBbbN{}\msupplus{}.    (\mexists{}k:\mBbbN{}  [(N  \mleq{}  (a\^{}((2  *  k)  +  2)  *  ((2  *  k)  +  2)!))])



Date html generated: 2019_10_29-AM-10_33_29
Last ObjectModification: 2019_02_08-PM-01_37_57

Theory : reals


Home Index