Nuprl Lemma : exp-exists-ext
∀x:ℝ. ∃a:ℝ. Σn.(x^n)/(n)! = a
Proof
Definitions occuring in Statement :
series-sum: Σn.x[n] = a,
rnexp: x^k1,
int-rdiv: (a)/k1,
real: ℝ,
fact: (n)!,
all: ∀x:A. B[x],
exists: ∃x:A. B[x]
Definitions unfolded in proof :
canonical-bound-property,
rmul_preserves_rleq,
r-archimedean,
ratio-test-ext,
rleq_functionality,
r-archimedean2,
iff_weakening_equal,
exp-series-converges,
exp-exists,
guard: {T},
implies: P ⇒ Q,
all: ∀x:A. B[x],
sq_type: SQType(T),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
reg-seq-mul: reg-seq-mul(x;y),
bnot: ¬bb,
le_int: i ≤z j,
reg-seq-adjust: reg-seq-adjust(n;x),
reg-seq-inv: reg-seq-inv(x),
canonical-bound: canonical-bound(r),
imax: imax(a;b),
accelerate: accelerate(k;f),
eq_int: (i =z j),
btrue: tt,
bfalse: ff,
mu-ge: mu-ge(f;n),
rinv: rinv(x),
int-to-real: r(n),
rmul: a * b,
rdiv: (x/y),
absval: |i|,
lt_int: i <z j,
ifthenelse: if b then t else f fi ,
quick-find: quick-find(p;n),
rlessw: rlessw(x;y),
rminus: -(x),
so_lambda: λ2x.t[x],
member: t ∈ T
Lemmas referenced :
int_subtype_base,
subtype_base_sq,
exp-exists,
canonical-bound-property,
rmul_preserves_rleq,
r-archimedean,
ratio-test-ext,
rleq_functionality,
r-archimedean2,
iff_weakening_equal,
exp-series-converges
Rules used in proof :
independent_functionElimination,
dependent_functionElimination,
natural_numberEquality,
independent_isectElimination,
intEquality,
cumulativity,
isectElimination,
equalitySymmetry,
equalityTransitivity,
sqequalHypSubstitution,
thin,
sqequalRule,
hypothesis,
extract_by_obid,
instantiate,
cut,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
introduction
Latex:
\mforall{}x:\mBbbR{}. \mexists{}a:\mBbbR{}. \mSigma{}n.(x\^{}n)/(n)! = a
Date html generated:
2018_05_22-PM-02_04_08
Last ObjectModification:
2018_05_21-AM-00_16_53
Theory : reals
Home
Index