Metamath Proof Explorer

Theorem abelthlem6

Description: Lemma for abelth . (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Hypotheses abelth.1 ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
abelth.2 ⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ∈ dom ⇝ )
abelth.3 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
abelth.4 ⊢ ( 𝜑 → 0 ≤ 𝑀 )
abelth.5 ⊢ 𝑆 = { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) }
abelth.6 ⊢ 𝐹 = ( 𝑥 ∈ 𝑆 ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) )
abelth.7 ⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ⇝ 0 )
abelthlem6.1 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑆 ∖ { 1 } ) )
Assertion abelthlem6 ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) )

Proof

Step Hyp Ref Expression
1 abelth.1 ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
2 abelth.2 ⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ∈ dom ⇝ )
3 abelth.3 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
4 abelth.4 ⊢ ( 𝜑 → 0 ≤ 𝑀 )
5 abelth.5 ⊢ 𝑆 = { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) }
6 abelth.6 ⊢ 𝐹 = ( 𝑥 ∈ 𝑆 ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) )
7 abelth.7 ⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ⇝ 0 )
8 abelthlem6.1 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑆 ∖ { 1 } ) )
9 8 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
10 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ↑ 𝑛 ) = ( 𝑋 ↑ 𝑛 ) )
11 10 oveq2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) = ( ( 𝐴 ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) )
12 11 sumeq2sdv ⊢ ( 𝑥 = 𝑋 → Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) = Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) )
13 sumex ⊢ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ∈ V
14 12 6 13 fvmpt ⊢ ( 𝑋 ∈ 𝑆 → ( 𝐹 ‘ 𝑋 ) = Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) )
15 9 14 syl ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) )
16 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
17 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
18 fveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑛 ) )
19 oveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝑋 ↑ 𝑘 ) = ( 𝑋 ↑ 𝑛 ) )
20 18 19 oveq12d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) )
21 eqid ⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) )
22 ovex ⊢ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ∈ V
23 20 21 22 fvmpt ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( ( 𝐴 ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) )
24 23 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( ( 𝐴 ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) )
25 1 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑛 ) ∈ ℂ )
26 5 ssrab3 ⊢ 𝑆 ⊆ ℂ
27 26 9 sselid ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
28 expcl ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( 𝑋 ↑ 𝑛 ) ∈ ℂ )
29 27 28 sylan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑋 ↑ 𝑛 ) ∈ ℂ )
30 25 29 mulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ∈ ℂ )
31 fveq2 ⊢ ( 𝑘 = 𝑛 → ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) = ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) )
32 31 19 oveq12d ⊢ ( 𝑘 = 𝑛 → ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) = ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) )
33 eqid ⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) )
34 ovex ⊢ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ∈ V
35 32 33 34 fvmpt ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) )
36 35 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) )
37 16 17 25 serf ⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) : ℕ0 ⟶ ℂ )
38 37 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ∈ ℂ )
39 38 29 mulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ∈ ℂ )
40 1 2 3 4 5 abelthlem2 ⊢ ( 𝜑 → ( 1 ∈ 𝑆 ∧ ( 𝑆 ∖ { 1 } ) ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) )
41 40 simprd ⊢ ( 𝜑 → ( 𝑆 ∖ { 1 } ) ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) )
42 41 8 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) )
43 1 2 3 4 5 6 7 abelthlem5 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ∈ dom ⇝ )
44 42 43 mpdan ⊢ ( 𝜑 → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ∈ dom ⇝ )
45 16 17 36 39 44 isumclim2 ⊢ ( 𝜑 → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ⇝ Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) )
46 seqex ⊢ seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ∈ V
47 46 a1i ⊢ ( 𝜑 → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ∈ V )
48 0nn0 ⊢ 0 ∈ ℕ0
49 48 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
50 oveq1 ⊢ ( 𝑘 = 𝑖 → ( 𝑘 − 1 ) = ( 𝑖 − 1 ) )
51 50 oveq2d ⊢ ( 𝑘 = 𝑖 → ( 0 ... ( 𝑘 − 1 ) ) = ( 0 ... ( 𝑖 − 1 ) ) )
52 51 sumeq1d ⊢ ( 𝑘 = 𝑖 → Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) = Σ 𝑚 ∈ ( 0 ... ( 𝑖 − 1 ) ) ( 𝐴 ‘ 𝑚 ) )
53 oveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝑋 ↑ 𝑘 ) = ( 𝑋 ↑ 𝑖 ) )
54 52 53 oveq12d ⊢ ( 𝑘 = 𝑖 → ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) = ( Σ 𝑚 ∈ ( 0 ... ( 𝑖 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑖 ) ) )
55 eqid ⊢ ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) )
56 ovex ⊢ ( Σ 𝑚 ∈ ( 0 ... ( 𝑖 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑖 ) ) ∈ V
57 54 55 56 fvmpt ⊢ ( 𝑖 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑖 ) = ( Σ 𝑚 ∈ ( 0 ... ( 𝑖 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑖 ) ) )
58 57 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑖 ) = ( Σ 𝑚 ∈ ( 0 ... ( 𝑖 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑖 ) ) )
59 fzfid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 0 ... ( 𝑖 − 1 ) ) ∈ Fin )
60 1 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝐴 : ℕ0 ⟶ ℂ )
61 elfznn0 ⊢ ( 𝑚 ∈ ( 0 ... ( 𝑖 − 1 ) ) → 𝑚 ∈ ℕ0 )
62 ffvelrn ⊢ ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 𝑚 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑚 ) ∈ ℂ )
63 60 61 62 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑚 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) → ( 𝐴 ‘ 𝑚 ) ∈ ℂ )
64 59 63 fsumcl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → Σ 𝑚 ∈ ( 0 ... ( 𝑖 − 1 ) ) ( 𝐴 ‘ 𝑚 ) ∈ ℂ )
65 expcl ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑖 ∈ ℕ0 ) → ( 𝑋 ↑ 𝑖 ) ∈ ℂ )
66 27 65 sylan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑋 ↑ 𝑖 ) ∈ ℂ )
67 64 66 mulcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( Σ 𝑚 ∈ ( 0 ... ( 𝑖 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑖 ) ) ∈ ℂ )
68 58 67 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑖 ) ∈ ℂ )
69 17 peano2zd ⊢ ( 𝜑 → ( 0 + 1 ) ∈ ℤ )
70 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
71 1e0p1 ⊢ 1 = ( 0 + 1 )
72 71 fveq2i ⊢ ( ℤ≥ ‘ 1 ) = ( ℤ≥ ‘ ( 0 + 1 ) )
73 70 72 eqtri ⊢ ℕ = ( ℤ≥ ‘ ( 0 + 1 ) )
74 73 eleq2i ⊢ ( 𝑛 ∈ ℕ ↔ 𝑛 ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) )
75 nnm1nn0 ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 − 1 ) ∈ ℕ0 )
76 75 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 − 1 ) ∈ ℕ0 )
77 fveq2 ⊢ ( 𝑘 = ( 𝑛 − 1 ) → ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) = ( seq 0 ( + , 𝐴 ) ‘ ( 𝑛 − 1 ) ) )
78 oveq2 ⊢ ( 𝑘 = ( 𝑛 − 1 ) → ( 𝑋 ↑ 𝑘 ) = ( 𝑋 ↑ ( 𝑛 − 1 ) ) )
79 77 78 oveq12d ⊢ ( 𝑘 = ( 𝑛 − 1 ) → ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) = ( ( seq 0 ( + , 𝐴 ) ‘ ( 𝑛 − 1 ) ) · ( 𝑋 ↑ ( 𝑛 − 1 ) ) ) )
80 79 oveq2d ⊢ ( 𝑘 = ( 𝑛 − 1 ) → ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) = ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ ( 𝑛 − 1 ) ) · ( 𝑋 ↑ ( 𝑛 − 1 ) ) ) ) )
81 eqid ⊢ ( 𝑘 ∈ ℕ0 ↦ ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) )
82 ovex ⊢ ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ ( 𝑛 − 1 ) ) · ( 𝑋 ↑ ( 𝑛 − 1 ) ) ) ) ∈ V
83 80 81 82 fvmpt ⊢ ( ( 𝑛 − 1 ) ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ ( 𝑛 − 1 ) ) = ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ ( 𝑛 − 1 ) ) · ( 𝑋 ↑ ( 𝑛 − 1 ) ) ) ) )
84 76 83 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ ( 𝑛 − 1 ) ) = ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ ( 𝑛 − 1 ) ) · ( 𝑋 ↑ ( 𝑛 − 1 ) ) ) ) )
85 ax-1cn ⊢ 1 ∈ ℂ
86 nncn ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
87 86 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℂ )
88 nn0ex ⊢ ℕ0 ∈ V
89 88 mptex ⊢ ( 𝑘 ∈ ℕ0 ↦ ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ∈ V
90 89 shftval ⊢ ( ( 1 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) shift 1 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ ( 𝑛 − 1 ) ) )
91 85 87 90 sylancr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) shift 1 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ ( 𝑛 − 1 ) ) )
92 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ) → ( 𝐴 ‘ 𝑚 ) = ( 𝐴 ‘ 𝑚 ) )
93 76 16 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
94 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 : ℕ0 ⟶ ℂ )
95 elfznn0 ⊢ ( 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) → 𝑚 ∈ ℕ0 )
96 94 95 62 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ) → ( 𝐴 ‘ 𝑚 ) ∈ ℂ )
97 92 93 96 fsumser ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 ‘ 𝑚 ) = ( seq 0 ( + , 𝐴 ) ‘ ( 𝑛 − 1 ) ) )
98 expm1t ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ ) → ( 𝑋 ↑ 𝑛 ) = ( ( 𝑋 ↑ ( 𝑛 − 1 ) ) · 𝑋 ) )
99 27 98 sylan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑋 ↑ 𝑛 ) = ( ( 𝑋 ↑ ( 𝑛 − 1 ) ) · 𝑋 ) )
100 27 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑋 ∈ ℂ )
101 expcl ⊢ ( ( 𝑋 ∈ ℂ ∧ ( 𝑛 − 1 ) ∈ ℕ0 ) → ( 𝑋 ↑ ( 𝑛 − 1 ) ) ∈ ℂ )
102 27 75 101 syl2an ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑋 ↑ ( 𝑛 − 1 ) ) ∈ ℂ )
103 100 102 mulcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑋 · ( 𝑋 ↑ ( 𝑛 − 1 ) ) ) = ( ( 𝑋 ↑ ( 𝑛 − 1 ) ) · 𝑋 ) )
104 99 103 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑋 ↑ 𝑛 ) = ( 𝑋 · ( 𝑋 ↑ ( 𝑛 − 1 ) ) ) )
105 97 104 oveq12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑛 ) ) = ( ( seq 0 ( + , 𝐴 ) ‘ ( 𝑛 − 1 ) ) · ( 𝑋 · ( 𝑋 ↑ ( 𝑛 − 1 ) ) ) ) )
106 nnnn0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
107 106 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ0 )
108 oveq1 ⊢ ( 𝑘 = 𝑛 → ( 𝑘 − 1 ) = ( 𝑛 − 1 ) )
109 108 oveq2d ⊢ ( 𝑘 = 𝑛 → ( 0 ... ( 𝑘 − 1 ) ) = ( 0 ... ( 𝑛 − 1 ) ) )
110 109 sumeq1d ⊢ ( 𝑘 = 𝑛 → Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) = Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 ‘ 𝑚 ) )
111 110 19 oveq12d ⊢ ( 𝑘 = 𝑛 → ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) = ( Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑛 ) ) )
112 ovex ⊢ ( Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑛 ) ) ∈ V
113 111 55 112 fvmpt ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑛 ) ) )
114 107 113 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑛 ) ) )
115 ffvelrn ⊢ ( ( seq 0 ( + , 𝐴 ) : ℕ0 ⟶ ℂ ∧ ( 𝑛 − 1 ) ∈ ℕ0 ) → ( seq 0 ( + , 𝐴 ) ‘ ( 𝑛 − 1 ) ) ∈ ℂ )
116 37 75 115 syl2an ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( seq 0 ( + , 𝐴 ) ‘ ( 𝑛 − 1 ) ) ∈ ℂ )
117 100 116 102 mul12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ ( 𝑛 − 1 ) ) · ( 𝑋 ↑ ( 𝑛 − 1 ) ) ) ) = ( ( seq 0 ( + , 𝐴 ) ‘ ( 𝑛 − 1 ) ) · ( 𝑋 · ( 𝑋 ↑ ( 𝑛 − 1 ) ) ) ) )
118 105 114 117 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ ( 𝑛 − 1 ) ) · ( 𝑋 ↑ ( 𝑛 − 1 ) ) ) ) )
119 84 91 118 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) shift 1 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) )
120 74 119 sylan2br ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) ) → ( ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) shift 1 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) )
121 69 120 seqfeq ⊢ ( 𝜑 → seq ( 0 + 1 ) ( + , ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) shift 1 ) ) = seq ( 0 + 1 ) ( + , ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) )
122 fveq2 ⊢ ( 𝑘 = 𝑖 → ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) = ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) )
123 122 53 oveq12d ⊢ ( 𝑘 = 𝑖 → ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) = ( ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) · ( 𝑋 ↑ 𝑖 ) ) )
124 ovex ⊢ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) · ( 𝑋 ↑ 𝑖 ) ) ∈ V
125 123 33 124 fvmpt ⊢ ( 𝑖 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑖 ) = ( ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) · ( 𝑋 ↑ 𝑖 ) ) )
126 125 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑖 ) = ( ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) · ( 𝑋 ↑ 𝑖 ) ) )
127 37 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) ∈ ℂ )
128 127 66 mulcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) · ( 𝑋 ↑ 𝑖 ) ) ∈ ℂ )
129 126 128 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑖 ) ∈ ℂ )
130 123 oveq2d ⊢ ( 𝑘 = 𝑖 → ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) = ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) · ( 𝑋 ↑ 𝑖 ) ) ) )
131 ovex ⊢ ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) · ( 𝑋 ↑ 𝑖 ) ) ) ∈ V
132 130 81 131 fvmpt ⊢ ( 𝑖 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) · ( 𝑋 ↑ 𝑖 ) ) ) )
133 132 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) · ( 𝑋 ↑ 𝑖 ) ) ) )
134 126 oveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑋 · ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑖 ) ) = ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑖 ) · ( 𝑋 ↑ 𝑖 ) ) ) )
135 133 134 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( 𝑋 · ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑖 ) ) )
136 16 17 27 45 129 135 isermulc2 ⊢ ( 𝜑 → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ) ⇝ ( 𝑋 · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) )
137 0z ⊢ 0 ∈ ℤ
138 1z ⊢ 1 ∈ ℤ
139 89 isershft ⊢ ( ( 0 ∈ ℤ ∧ 1 ∈ ℤ ) → ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ) ⇝ ( 𝑋 · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ↔ seq ( 0 + 1 ) ( + , ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) shift 1 ) ) ⇝ ( 𝑋 · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) )
140 137 138 139 mp2an ⊢ ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ) ⇝ ( 𝑋 · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ↔ seq ( 0 + 1 ) ( + , ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) shift 1 ) ) ⇝ ( 𝑋 · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) )
141 136 140 sylib ⊢ ( 𝜑 → seq ( 0 + 1 ) ( + , ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑋 · ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) shift 1 ) ) ⇝ ( 𝑋 · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) )
142 121 141 eqbrtrrd ⊢ ( 𝜑 → seq ( 0 + 1 ) ( + , ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ⇝ ( 𝑋 · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) )
143 16 49 68 142 clim2ser2 ⊢ ( 𝜑 → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ⇝ ( ( 𝑋 · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) + ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ 0 ) ) )
144 seq1 ⊢ ( 0 ∈ ℤ → ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ 0 ) = ( ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 0 ) )
145 137 144 ax-mp ⊢ ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ 0 ) = ( ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 0 )
146 oveq1 ⊢ ( 𝑘 = 0 → ( 𝑘 − 1 ) = ( 0 − 1 ) )
147 146 oveq2d ⊢ ( 𝑘 = 0 → ( 0 ... ( 𝑘 − 1 ) ) = ( 0 ... ( 0 − 1 ) ) )
148 risefall0lem ⊢ ( 0 ... ( 0 − 1 ) ) = ∅
149 147 148 eqtrdi ⊢ ( 𝑘 = 0 → ( 0 ... ( 𝑘 − 1 ) ) = ∅ )
150 149 sumeq1d ⊢ ( 𝑘 = 0 → Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) = Σ 𝑚 ∈ ∅ ( 𝐴 ‘ 𝑚 ) )
151 sum0 ⊢ Σ 𝑚 ∈ ∅ ( 𝐴 ‘ 𝑚 ) = 0
152 150 151 eqtrdi ⊢ ( 𝑘 = 0 → Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) = 0 )
153 oveq2 ⊢ ( 𝑘 = 0 → ( 𝑋 ↑ 𝑘 ) = ( 𝑋 ↑ 0 ) )
154 152 153 oveq12d ⊢ ( 𝑘 = 0 → ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) = ( 0 · ( 𝑋 ↑ 0 ) ) )
155 ovex ⊢ ( 0 · ( 𝑋 ↑ 0 ) ) ∈ V
156 154 55 155 fvmpt ⊢ ( 0 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 0 ) = ( 0 · ( 𝑋 ↑ 0 ) ) )
157 48 156 ax-mp ⊢ ( ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 0 ) = ( 0 · ( 𝑋 ↑ 0 ) )
158 145 157 eqtri ⊢ ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ 0 ) = ( 0 · ( 𝑋 ↑ 0 ) )
159 expcl ⊢ ( ( 𝑋 ∈ ℂ ∧ 0 ∈ ℕ0 ) → ( 𝑋 ↑ 0 ) ∈ ℂ )
160 27 48 159 sylancl ⊢ ( 𝜑 → ( 𝑋 ↑ 0 ) ∈ ℂ )
161 160 mul02d ⊢ ( 𝜑 → ( 0 · ( 𝑋 ↑ 0 ) ) = 0 )
162 158 161 syl5eq ⊢ ( 𝜑 → ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ 0 ) = 0 )
163 162 oveq2d ⊢ ( 𝜑 → ( ( 𝑋 · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) + ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ 0 ) ) = ( ( 𝑋 · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) + 0 ) )
164 16 17 36 39 44 isumcl ⊢ ( 𝜑 → Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ∈ ℂ )
165 27 164 mulcld ⊢ ( 𝜑 → ( 𝑋 · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ∈ ℂ )
166 165 addid1d ⊢ ( 𝜑 → ( ( 𝑋 · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) + 0 ) = ( 𝑋 · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) )
167 163 166 eqtrd ⊢ ( 𝜑 → ( ( 𝑋 · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) + ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ 0 ) ) = ( 𝑋 · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) )
168 143 167 breqtrd ⊢ ( 𝜑 → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ⇝ ( 𝑋 · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) )
169 16 17 129 serf ⊢ ( 𝜑 → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) : ℕ0 ⟶ ℂ )
170 169 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ 𝑖 ) ∈ ℂ )
171 16 17 68 serf ⊢ ( 𝜑 → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) : ℕ0 ⟶ ℂ )
172 171 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ 𝑖 ) ∈ ℂ )
173 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑖 ∈ ℕ0 )
174 173 16 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑖 ∈ ( ℤ≥ ‘ 0 ) )
175 simpl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝜑 )
176 elfznn0 ⊢ ( 𝑛 ∈ ( 0 ... 𝑖 ) → 𝑛 ∈ ℕ0 )
177 36 39 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) ∈ ℂ )
178 175 176 177 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ... 𝑖 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) ∈ ℂ )
179 113 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑛 ) ) )
180 fzfid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 0 ... ( 𝑛 − 1 ) ) ∈ Fin )
181 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝐴 : ℕ0 ⟶ ℂ )
182 181 95 62 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ) → ( 𝐴 ‘ 𝑚 ) ∈ ℂ )
183 180 182 fsumcl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 ‘ 𝑚 ) ∈ ℂ )
184 183 29 mulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑛 ) ) ∈ ℂ )
185 179 184 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) ∈ ℂ )
186 175 176 185 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ... 𝑖 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) ∈ ℂ )
187 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑚 ∈ ( 0 ... 𝑛 ) ) → ( 𝐴 ‘ 𝑚 ) = ( 𝐴 ‘ 𝑚 ) )
188 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
189 188 16 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ( ℤ≥ ‘ 0 ) )
190 elfznn0 ⊢ ( 𝑚 ∈ ( 0 ... 𝑛 ) → 𝑚 ∈ ℕ0 )
191 181 190 62 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑚 ∈ ( 0 ... 𝑛 ) ) → ( 𝐴 ‘ 𝑚 ) ∈ ℂ )
192 187 189 191 fsumser ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( 𝐴 ‘ 𝑚 ) = ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) )
193 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝐴 ‘ 𝑚 ) = ( 𝐴 ‘ 𝑛 ) )
194 189 191 193 fsumm1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → Σ 𝑚 ∈ ( 0 ... 𝑛 ) ( 𝐴 ‘ 𝑚 ) = ( Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 ‘ 𝑚 ) + ( 𝐴 ‘ 𝑛 ) ) )
195 192 194 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) = ( Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 ‘ 𝑚 ) + ( 𝐴 ‘ 𝑛 ) ) )
196 195 oveq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) − Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 ‘ 𝑚 ) ) = ( ( Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 ‘ 𝑚 ) + ( 𝐴 ‘ 𝑛 ) ) − Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 ‘ 𝑚 ) ) )
197 183 25 pncan2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 ‘ 𝑚 ) + ( 𝐴 ‘ 𝑛 ) ) − Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 ‘ 𝑚 ) ) = ( 𝐴 ‘ 𝑛 ) )
198 196 197 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑛 ) = ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) − Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 ‘ 𝑚 ) ) )
199 198 oveq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) = ( ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) − Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 ‘ 𝑚 ) ) · ( 𝑋 ↑ 𝑛 ) ) )
200 38 183 29 subdird ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) − Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 ‘ 𝑚 ) ) · ( 𝑋 ↑ 𝑛 ) ) = ( ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) − ( Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑛 ) ) ) )
201 199 200 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) = ( ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) − ( Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑛 ) ) ) )
202 36 179 oveq12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) − ( ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) ) = ( ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) − ( Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑛 ) ) ) )
203 201 24 202 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) − ( ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) ) )
204 175 176 203 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ... 𝑖 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) − ( ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) ) )
205 174 178 186 204 sersub ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ 𝑖 ) − ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( Σ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝐴 ‘ 𝑚 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ 𝑖 ) ) )
206 16 17 45 47 168 170 172 205 climsub ⊢ ( 𝜑 → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ⇝ ( Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) − ( 𝑋 · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) )
207 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
208 207 27 164 subdird ⊢ ( 𝜑 → ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) = ( ( 1 · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) − ( 𝑋 · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) )
209 164 mulid2d ⊢ ( 𝜑 → ( 1 · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) = Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) )
210 209 oveq1d ⊢ ( 𝜑 → ( ( 1 · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) − ( 𝑋 · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) = ( Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) − ( 𝑋 · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) )
211 208 210 eqtrd ⊢ ( 𝜑 → ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) = ( Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) − ( 𝑋 · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) )
212 206 211 breqtrrd ⊢ ( 𝜑 → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ⇝ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) )
213 16 17 24 30 212 isumclim ⊢ ( 𝜑 → Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) = ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) )
214 15 213 eqtrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) )