This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( 𝑛 ∈ ℕ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 ‘ 𝐴 ) )