# Metamath Proof Explorer

## Theorem efcvgfsum

Description: Exponential function convergence in terms of a sequence of partial finite sums. (Contributed by NM, 10-Jan-2006) (Revised by Mario Carneiro, 28-Apr-2014)

Ref Expression
Hypothesis efcvgfsum.1 ${⊢}{F}=\left({n}\in {ℕ}_{0}⟼\sum _{{k}=0}^{{n}}\left(\frac{{{A}}^{{k}}}{{k}!}\right)\right)$
Assertion efcvgfsum ${⊢}{A}\in ℂ\to {F}⇝{\mathrm{e}}^{{A}}$

### Proof

Step Hyp Ref Expression
1 efcvgfsum.1 ${⊢}{F}=\left({n}\in {ℕ}_{0}⟼\sum _{{k}=0}^{{n}}\left(\frac{{{A}}^{{k}}}{{k}!}\right)\right)$
2 oveq2 ${⊢}{n}={j}\to \left(0\dots {n}\right)=\left(0\dots {j}\right)$
3 2 sumeq1d ${⊢}{n}={j}\to \sum _{{k}=0}^{{n}}\left(\frac{{{A}}^{{k}}}{{k}!}\right)=\sum _{{k}=0}^{{j}}\left(\frac{{{A}}^{{k}}}{{k}!}\right)$
4 sumex ${⊢}\sum _{{k}=0}^{{j}}\left(\frac{{{A}}^{{k}}}{{k}!}\right)\in \mathrm{V}$
5 3 1 4 fvmpt ${⊢}{j}\in {ℕ}_{0}\to {F}\left({j}\right)=\sum _{{k}=0}^{{j}}\left(\frac{{{A}}^{{k}}}{{k}!}\right)$
6 5 adantl ${⊢}\left({A}\in ℂ\wedge {j}\in {ℕ}_{0}\right)\to {F}\left({j}\right)=\sum _{{k}=0}^{{j}}\left(\frac{{{A}}^{{k}}}{{k}!}\right)$
7 elfznn0 ${⊢}{k}\in \left(0\dots {j}\right)\to {k}\in {ℕ}_{0}$
8 7 adantl ${⊢}\left(\left({A}\in ℂ\wedge {j}\in {ℕ}_{0}\right)\wedge {k}\in \left(0\dots {j}\right)\right)\to {k}\in {ℕ}_{0}$
9 eqid ${⊢}\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)=\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)$
10 9 eftval ${⊢}{k}\in {ℕ}_{0}\to \left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)\left({k}\right)=\frac{{{A}}^{{k}}}{{k}!}$
11 8 10 syl ${⊢}\left(\left({A}\in ℂ\wedge {j}\in {ℕ}_{0}\right)\wedge {k}\in \left(0\dots {j}\right)\right)\to \left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)\left({k}\right)=\frac{{{A}}^{{k}}}{{k}!}$
12 simpr ${⊢}\left({A}\in ℂ\wedge {j}\in {ℕ}_{0}\right)\to {j}\in {ℕ}_{0}$
13 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
14 12 13 eleqtrdi ${⊢}\left({A}\in ℂ\wedge {j}\in {ℕ}_{0}\right)\to {j}\in {ℤ}_{\ge 0}$
15 simpll ${⊢}\left(\left({A}\in ℂ\wedge {j}\in {ℕ}_{0}\right)\wedge {k}\in \left(0\dots {j}\right)\right)\to {A}\in ℂ$
16 eftcl ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to \frac{{{A}}^{{k}}}{{k}!}\in ℂ$
17 15 8 16 syl2anc ${⊢}\left(\left({A}\in ℂ\wedge {j}\in {ℕ}_{0}\right)\wedge {k}\in \left(0\dots {j}\right)\right)\to \frac{{{A}}^{{k}}}{{k}!}\in ℂ$
18 11 14 17 fsumser ${⊢}\left({A}\in ℂ\wedge {j}\in {ℕ}_{0}\right)\to \sum _{{k}=0}^{{j}}\left(\frac{{{A}}^{{k}}}{{k}!}\right)=seq0\left(+,\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)\right)\left({j}\right)$
19 6 18 eqtrd ${⊢}\left({A}\in ℂ\wedge {j}\in {ℕ}_{0}\right)\to {F}\left({j}\right)=seq0\left(+,\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)\right)\left({j}\right)$
20 19 ralrimiva ${⊢}{A}\in ℂ\to \forall {j}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)=seq0\left(+,\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)\right)\left({j}\right)$
21 sumex ${⊢}\sum _{{k}=0}^{{n}}\left(\frac{{{A}}^{{k}}}{{k}!}\right)\in \mathrm{V}$
22 21 1 fnmpti ${⊢}{F}Fn{ℕ}_{0}$
23 0z ${⊢}0\in ℤ$
24 seqfn ${⊢}0\in ℤ\to seq0\left(+,\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)\right)Fn{ℤ}_{\ge 0}$
25 23 24 ax-mp ${⊢}seq0\left(+,\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)\right)Fn{ℤ}_{\ge 0}$
26 13 fneq2i ${⊢}seq0\left(+,\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)\right)Fn{ℕ}_{0}↔seq0\left(+,\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)\right)Fn{ℤ}_{\ge 0}$
27 25 26 mpbir ${⊢}seq0\left(+,\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)\right)Fn{ℕ}_{0}$
28 eqfnfv ${⊢}\left({F}Fn{ℕ}_{0}\wedge seq0\left(+,\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)\right)Fn{ℕ}_{0}\right)\to \left({F}=seq0\left(+,\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)\right)↔\forall {j}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)=seq0\left(+,\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)\right)\left({j}\right)\right)$
29 22 27 28 mp2an ${⊢}{F}=seq0\left(+,\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)\right)↔\forall {j}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)=seq0\left(+,\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)\right)\left({j}\right)$
30 20 29 sylibr ${⊢}{A}\in ℂ\to {F}=seq0\left(+,\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)\right)$
31 9 efcvg ${⊢}{A}\in ℂ\to seq0\left(+,\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)\right)⇝{\mathrm{e}}^{{A}}$
32 30 31 eqbrtrd ${⊢}{A}\in ℂ\to {F}⇝{\mathrm{e}}^{{A}}$