Nuprl Lemma : sine-is-limit

x:ℝ. Σi.-1^i (x^(2 i) 1)/((2 i) 1)! sine(x)


Proof




Definitions occuring in Statement :  sine: sine(x) series-sum: Σn.x[n] a rnexp: x^k1 int-rdiv: (a)/k1 int-rmul: k1 a real: all: x:A. B[x] multiply: m add: m minus: -n natural_number: $n fastexp: i^n fact: (n)!
Definitions unfolded in proof :  all: x:A. B[x] sine: sine(x) member: t ∈ T subtype_rel: A ⊆B uall: [x:A]. B[x] so_lambda: λ2x.t[x] nat: ge: i ≥  decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False implies:  Q not: ¬A top: Top and: P ∧ Q prop: nat_plus: + int_nzero: -o so_apply: x[s] nequal: a ≠ b ∈  guard: {T} pi1: fst(t)
Lemmas referenced :  sine-exists-ext all_wf exists_wf series-sum_wf int-rmul_wf int-rdiv_wf fact_wf nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermAdd_wf itermMultiply_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_mul_lemma int_term_value_var_lemma int_formula_prop_wf le_wf subtype_rel_sets less_than_wf nequal_wf nat_plus_properties intformeq_wf intformless_wf int_formula_prop_eq_lemma int_formula_prop_less_lemma equal-wf-base int_subtype_base rnexp_wf nat_wf equal_wf real_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut applyEquality thin instantiate extract_by_obid hypothesis lambdaEquality sqequalHypSubstitution sqequalRule hypothesisEquality introduction isectElimination because_Cache dependent_set_memberEquality addEquality multiplyEquality natural_numberEquality setElimination rename dependent_functionElimination unionElimination independent_isectElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll setEquality equalityTransitivity equalitySymmetry Error :applyLambdaEquality,  baseClosed independent_functionElimination productElimination

Latex:
\mforall{}x:\mBbbR{}.  \mSigma{}i.-1\^{}i  *  (x\^{}(2  *  i)  +  1)/((2  *  i)  +  1)!  =  sine(x)



Date html generated: 2016_10_26-AM-09_24_22
Last ObjectModification: 2016_08_25-PM-11_38_00

Theory : reals


Home Index