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	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
Assertion	efcvgfsum	⊢ ( 𝐴 ∈ ℂ → 𝐹 ⇝ ( exp ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		efcvgfsum.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
2		oveq2	⊢ ( 𝑛 = 𝑗 → ( 0 ... 𝑛 ) = ( 0 ... 𝑗 ) )
3	2	sumeq1d	⊢ ( 𝑛 = 𝑗 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑗 ) ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
4		sumex	⊢ Σ 𝑘 ∈ ( 0 ... 𝑗 ) ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ V
5	3 1 4	fvmpt	⊢ ( 𝑗 ∈ ℕ0 → ( 𝐹 ‘ 𝑗 ) = Σ 𝑘 ∈ ( 0 ... 𝑗 ) ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
6	5	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑗 ) = Σ 𝑘 ∈ ( 0 ... 𝑗 ) ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
7		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑗 ) → 𝑘 ∈ ℕ0 )
8	7	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) → 𝑘 ∈ ℕ0 )
9		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
10	9	eftval	⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
11	8 10	syl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
12		simpr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) → 𝑗 ∈ ℕ0 )
13		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
14	12 13	eleqtrdi	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) → 𝑗 ∈ ( ℤ≥ ‘ 0 ) )
15		simpll	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) → 𝐴 ∈ ℂ )
16		eftcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
17	15 8 16	syl2anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
18	11 14 17	fsumser	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... 𝑗 ) ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) )
19	6 18	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑗 ) = ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) )
20	19	ralrimiva	⊢ ( 𝐴 ∈ ℂ → ∀ 𝑗 ∈ ℕ0 ( 𝐹 ‘ 𝑗 ) = ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) )
21		sumex	⊢ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ V
22	21 1	fnmpti	⊢ 𝐹 Fn ℕ0
23		0z	⊢ 0 ∈ ℤ
24		seqfn	⊢ ( 0 ∈ ℤ → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) Fn ( ℤ≥ ‘ 0 ) )
25	23 24	ax-mp	⊢ seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) Fn ( ℤ≥ ‘ 0 )
26	13	fneq2i	⊢ ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) Fn ℕ0 ↔ seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) Fn ( ℤ≥ ‘ 0 ) )
27	25 26	mpbir	⊢ seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) Fn ℕ0
28		eqfnfv	⊢ ( ( 𝐹 Fn ℕ0 ∧ seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) Fn ℕ0 ) → ( 𝐹 = seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ↔ ∀ 𝑗 ∈ ℕ0 ( 𝐹 ‘ 𝑗 ) = ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) ) )
29	22 27 28	mp2an	⊢ ( 𝐹 = seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ↔ ∀ 𝑗 ∈ ℕ0 ( 𝐹 ‘ 𝑗 ) = ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 𝑗 ) )
30	20 29	sylibr	⊢ ( 𝐴 ∈ ℂ → 𝐹 = seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) )
31	9	efcvg	⊢ ( 𝐴 ∈ ℂ → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ⇝ ( exp ‘ 𝐴 ) )
32	30 31	eqbrtrd	⊢ ( 𝐴 ∈ ℂ → 𝐹 ⇝ ( exp ‘ 𝐴 ) )