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 = (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} (\frac{A^{k}}{k!}))$
	Assertion	efcvgfsum	$⊢ A \in ℂ \to F ⇝ e^{A}$

Proof

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

Metamath Proof Explorer

Theorem efcvgfsum

Proof