Nuprl Lemma : cosine-exists-ext1

x:ℝ{a:ℝ| Σi.-1^i (x^2 i)/(2 i)! a} 


Proof




Definitions occuring in Statement :  series-sum: Σn.x[n] a rnexp: x^k1 int-rdiv: (a)/k1 int-rmul: k1 a real: all: x:A. B[x] set: {x:A| B[x]}  multiply: m minus: -n natural_number: $n fastexp: i^n fact: (n)!
Definitions unfolded in proof :  decidable__int_equal decidable__equal_int fact-greater-exp expfact-property rdiv-factorial-limit-zero subsequence-converges accelerate: accelerate(k;f) req_functionality rleq_functionality rmul_preserves_rleq r-archimedean r-archimedean-rabs converges-iff-cauchy-ext label: ...$L... t so_apply: x[s] so_lambda: λ2x.t[x] alternating-series-converges iff_weakening_equal so_apply: x[s1;s2] so_lambda: λ2y.t[x; y] squash: T or: P ∨ Q guard: {T} prop: has-value: (a)↓ implies:  Q all: x:A. B[x] and: P ∧ Q strict4: strict4(F) uimplies: supposing a top: Top so_apply: x[s1;s2;s3;s4] so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]) uall: [x:A]. B[x] cosine-exists member: t ∈ T
Lemmas referenced :  decidable__int_equal decidable__equal_int fact-greater-exp expfact-property rdiv-factorial-limit-zero subsequence-converges req_functionality rleq_functionality rmul_preserves_rleq r-archimedean r-archimedean-rabs converges-iff-cauchy-ext alternating-series-converges iff_weakening_equal cosine-exists
Rules used in proof :  decideExceptionCases independent_functionElimination dependent_functionElimination equalityEquality sqleReflexivity unionElimination unionEquality equalitySymmetry equalityTransitivity callbyvalueDecide because_Cache inlFormation exceptionSqequal imageElimination imageMemberEquality inrFormation applyExceptionCases hypothesisEquality closedConclusion baseApply callbyvalueApply lambdaFormation independent_pairFormation independent_isectElimination voidEquality voidElimination isect_memberEquality baseClosed isectElimination sqequalHypSubstitution thin sqequalRule hypothesis extract_by_obid instantiate cut sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution introduction

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



Date html generated: 2016_07_08-PM-05_55_03
Last ObjectModification: 2016_07_05-PM-03_07_28

Theory : reals


Home Index