Nuprl Lemma : fun-converges-to-cosine

lim n→∞{-1^i (x^2 i)/(2 i)! 0≤i≤n} = λx.cosine(x) for x ∈ (-∞, ∞)


Proof




Definitions occuring in Statement :  fun-converges-to: lim n→∞.f[n; x] = λy.g[y] for x ∈ I riiint: (-∞, ∞) cosine: cosine(x) rsum: Σ{x[k] n≤k≤m} rnexp: x^k1 int-rdiv: (a)/k1 int-rmul: k1 a fastexp: i^n fact: (n)! multiply: m minus: -n natural_number: $n
Definitions unfolded in proof :  all: x:A. B[x] so_lambda: λ2y.t[x; y] member: t ∈ T uall: [x:A]. B[x] nat: ge: i ≥  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 and: P ∧ Q prop: subtype_rel: A ⊆B so_apply: x[s1;s2] nat_plus: + uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) rneq: x ≠ y guard: {T} iff: ⇐⇒ Q rev_implies:  Q less_than: a < b squash: T less_than': less_than'(a;b) true: True cand: c∧ B le: A ≤ B int_upper: {i...} rless: x < y sq_exists: x:A [B[x]] so_lambda: λ2x.t[x] so_apply: x[s] series-sum: Σn.x[n] a sq_stable: SqStable(P) real: top: Top subtract: m rdiv: (x/y) req_int_terms: t1 ≡ t2 sq_type: SQType(T) rge: x ≥ y

Latex:
lim  n\mrightarrow{}\minfty{}.\mSigma{}\{-1\^{}i  *  (x\^{}2  *  i)/(2  *  i)!  |  0\mleq{}i\mleq{}n\}  =  \mlambda{}x.cosine(x)  for  x  \mmember{}  (-\minfty{},  \minfty{})



Date html generated: 2020_05_20-PM-01_09_05
Last ObjectModification: 2020_01_03-AM-00_23_30

Theory : reals


Home Index