Metamath Proof Explorer

Theorem pwp1fsum

Description: The n-th power of a number increased by 1 expressed by a product with a finite sum. (Contributed by AV, 15-Aug-2021)

Ref Expression
Hypotheses pwp1fsum.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
pwp1fsum.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion pwp1fsum ( 𝜑 → ( ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) + 1 ) = ( ( 𝐴 + 1 ) · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 pwp1fsum.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 pwp1fsum.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
4 fzfid ⊢ ( 𝜑 → ( 0 ... ( 𝑁 − 1 ) ) ∈ Fin )
5 neg1cn ⊢ - 1 ∈ ℂ
6 5 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → - 1 ∈ ℂ )
7 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℕ0 )
8 7 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℕ0 )
9 6 8 expcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( - 1 ↑ 𝑘 ) ∈ ℂ )
10 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝐴 ∈ ℂ )
11 10 8 expcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
12 9 11 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℂ )
13 4 12 fsumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℂ )
14 1 3 13 adddird ⊢ ( 𝜑 → ( ( 𝐴 + 1 ) · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = ( ( 𝐴 · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) + ( 1 · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) ) )
15 4 1 12 fsummulc2 ⊢ ( 𝜑 → ( 𝐴 · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 · ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) )
16 10 12 mulcomd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝐴 · ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = ( ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) · 𝐴 ) )
17 9 11 10 mulassd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) · 𝐴 ) = ( ( - 1 ↑ 𝑘 ) · ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) ) )
18 expp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) )
19 1 7 18 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) )
20 19 eqcomd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) = ( 𝐴 ↑ ( 𝑘 + 1 ) ) )
21 20 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( - 1 ↑ 𝑘 ) · ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) ) = ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) )
22 16 17 21 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝐴 · ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) )
23 22 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 · ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) )
24 15 23 eqtrd ⊢ ( 𝜑 → ( 𝐴 · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) )
25 13 mullidd ⊢ ( 𝜑 → ( 1 · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) )
26 24 25 oveq12d ⊢ ( 𝜑 → ( ( 𝐴 · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) + ( 1 · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) ) = ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) + Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) )
27 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
28 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
29 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
30 peano2zm ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
31 29 30 syl ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℤ )
32 2 31 syl ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℤ )
33 peano2nn0 ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ0 )
34 7 33 syl ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑘 + 1 ) ∈ ℕ0 )
35 34 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑘 + 1 ) ∈ ℕ0 )
36 10 35 expcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) ∈ ℂ )
37 9 36 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) ∈ ℂ )
38 oveq2 ⊢ ( 𝑘 = ( 𝑙 − 1 ) → ( - 1 ↑ 𝑘 ) = ( - 1 ↑ ( 𝑙 − 1 ) ) )
39 oveq1 ⊢ ( 𝑘 = ( 𝑙 − 1 ) → ( 𝑘 + 1 ) = ( ( 𝑙 − 1 ) + 1 ) )
40 39 oveq2d ⊢ ( 𝑘 = ( 𝑙 − 1 ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( 𝐴 ↑ ( ( 𝑙 − 1 ) + 1 ) ) )
41 38 40 oveq12d ⊢ ( 𝑘 = ( 𝑙 − 1 ) → ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) = ( ( - 1 ↑ ( 𝑙 − 1 ) ) · ( 𝐴 ↑ ( ( 𝑙 − 1 ) + 1 ) ) ) )
42 27 28 32 37 41 fsumshft ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) = Σ 𝑙 ∈ ( ( 0 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) ( ( - 1 ↑ ( 𝑙 − 1 ) ) · ( 𝐴 ↑ ( ( 𝑙 − 1 ) + 1 ) ) ) )
43 elfzelz ⊢ ( 𝑙 ∈ ( ( 0 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) → 𝑙 ∈ ℤ )
44 43 zcnd ⊢ ( 𝑙 ∈ ( ( 0 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) → 𝑙 ∈ ℂ )
45 44 adantl ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( ( 0 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) ) → 𝑙 ∈ ℂ )
46 npcan1 ⊢ ( 𝑙 ∈ ℂ → ( ( 𝑙 − 1 ) + 1 ) = 𝑙 )
47 45 46 syl ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( ( 0 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) ) → ( ( 𝑙 − 1 ) + 1 ) = 𝑙 )
48 47 oveq2d ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( ( 0 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) ) → ( 𝐴 ↑ ( ( 𝑙 − 1 ) + 1 ) ) = ( 𝐴 ↑ 𝑙 ) )
49 48 oveq2d ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( ( 0 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) ) → ( ( - 1 ↑ ( 𝑙 − 1 ) ) · ( 𝐴 ↑ ( ( 𝑙 − 1 ) + 1 ) ) ) = ( ( - 1 ↑ ( 𝑙 − 1 ) ) · ( 𝐴 ↑ 𝑙 ) ) )
50 49 sumeq2dv ⊢ ( 𝜑 → Σ 𝑙 ∈ ( ( 0 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) ( ( - 1 ↑ ( 𝑙 − 1 ) ) · ( 𝐴 ↑ ( ( 𝑙 − 1 ) + 1 ) ) ) = Σ 𝑙 ∈ ( ( 0 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) ( ( - 1 ↑ ( 𝑙 − 1 ) ) · ( 𝐴 ↑ 𝑙 ) ) )
51 2 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
52 npcan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
53 51 52 syl ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
54 0p1e1 ⊢ ( 0 + 1 ) = 1
55 54 fveq2i ⊢ ( ℤ≥ ‘ ( 0 + 1 ) ) = ( ℤ≥ ‘ 1 )
56 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
57 55 56 eqtr4i ⊢ ( ℤ≥ ‘ ( 0 + 1 ) ) = ℕ
58 57 a1i ⊢ ( 𝜑 → ( ℤ≥ ‘ ( 0 + 1 ) ) = ℕ )
59 2 53 58 3eltr4d ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) )
60 54 oveq1i ⊢ ( ( 0 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 1 ... ( ( 𝑁 − 1 ) + 1 ) )
61 60 eleq2i ⊢ ( 𝑙 ∈ ( ( 0 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) ↔ 𝑙 ∈ ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) )
62 5 a1i ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) → - 1 ∈ ℂ )
63 nnm1nn0 ⊢ ( 𝑙 ∈ ℕ → ( 𝑙 − 1 ) ∈ ℕ0 )
64 63 adantl ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) → ( 𝑙 − 1 ) ∈ ℕ0 )
65 62 64 expcld ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) → ( - 1 ↑ ( 𝑙 − 1 ) ) ∈ ℂ )
66 1 adantr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) → 𝐴 ∈ ℂ )
67 nnnn0 ⊢ ( 𝑙 ∈ ℕ → 𝑙 ∈ ℕ0 )
68 67 adantl ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) → 𝑙 ∈ ℕ0 )
69 66 68 expcld ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) → ( 𝐴 ↑ 𝑙 ) ∈ ℂ )
70 65 69 mulcld ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) → ( ( - 1 ↑ ( 𝑙 − 1 ) ) · ( 𝐴 ↑ 𝑙 ) ) ∈ ℂ )
71 70 expcom ⊢ ( 𝑙 ∈ ℕ → ( 𝜑 → ( ( - 1 ↑ ( 𝑙 − 1 ) ) · ( 𝐴 ↑ 𝑙 ) ) ∈ ℂ ) )
72 elfznn ⊢ ( 𝑙 ∈ ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) → 𝑙 ∈ ℕ )
73 71 72 syl11 ⊢ ( 𝜑 → ( 𝑙 ∈ ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) → ( ( - 1 ↑ ( 𝑙 − 1 ) ) · ( 𝐴 ↑ 𝑙 ) ) ∈ ℂ ) )
74 61 73 biimtrid ⊢ ( 𝜑 → ( 𝑙 ∈ ( ( 0 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) → ( ( - 1 ↑ ( 𝑙 − 1 ) ) · ( 𝐴 ↑ 𝑙 ) ) ∈ ℂ ) )
75 74 imp ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( ( 0 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) ) → ( ( - 1 ↑ ( 𝑙 − 1 ) ) · ( 𝐴 ↑ 𝑙 ) ) ∈ ℂ )
76 oveq1 ⊢ ( 𝑙 = ( ( 𝑁 − 1 ) + 1 ) → ( 𝑙 − 1 ) = ( ( ( 𝑁 − 1 ) + 1 ) − 1 ) )
77 76 oveq2d ⊢ ( 𝑙 = ( ( 𝑁 − 1 ) + 1 ) → ( - 1 ↑ ( 𝑙 − 1 ) ) = ( - 1 ↑ ( ( ( 𝑁 − 1 ) + 1 ) − 1 ) ) )
78 oveq2 ⊢ ( 𝑙 = ( ( 𝑁 − 1 ) + 1 ) → ( 𝐴 ↑ 𝑙 ) = ( 𝐴 ↑ ( ( 𝑁 − 1 ) + 1 ) ) )
79 77 78 oveq12d ⊢ ( 𝑙 = ( ( 𝑁 − 1 ) + 1 ) → ( ( - 1 ↑ ( 𝑙 − 1 ) ) · ( 𝐴 ↑ 𝑙 ) ) = ( ( - 1 ↑ ( ( ( 𝑁 − 1 ) + 1 ) − 1 ) ) · ( 𝐴 ↑ ( ( 𝑁 − 1 ) + 1 ) ) ) )
80 59 75 79 fsumm1 ⊢ ( 𝜑 → Σ 𝑙 ∈ ( ( 0 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) ( ( - 1 ↑ ( 𝑙 − 1 ) ) · ( 𝐴 ↑ 𝑙 ) ) = ( Σ 𝑙 ∈ ( ( 0 + 1 ) ... ( ( ( 𝑁 − 1 ) + 1 ) − 1 ) ) ( ( - 1 ↑ ( 𝑙 − 1 ) ) · ( 𝐴 ↑ 𝑙 ) ) + ( ( - 1 ↑ ( ( ( 𝑁 − 1 ) + 1 ) − 1 ) ) · ( 𝐴 ↑ ( ( 𝑁 − 1 ) + 1 ) ) ) ) )
81 32 zcnd ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℂ )
82 pncan1 ⊢ ( ( 𝑁 − 1 ) ∈ ℂ → ( ( ( 𝑁 − 1 ) + 1 ) − 1 ) = ( 𝑁 − 1 ) )
83 81 82 syl ⊢ ( 𝜑 → ( ( ( 𝑁 − 1 ) + 1 ) − 1 ) = ( 𝑁 − 1 ) )
84 83 oveq2d ⊢ ( 𝜑 → ( ( 0 + 1 ) ... ( ( ( 𝑁 − 1 ) + 1 ) − 1 ) ) = ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) )
85 84 sumeq1d ⊢ ( 𝜑 → Σ 𝑙 ∈ ( ( 0 + 1 ) ... ( ( ( 𝑁 − 1 ) + 1 ) − 1 ) ) ( ( - 1 ↑ ( 𝑙 − 1 ) ) · ( 𝐴 ↑ 𝑙 ) ) = Σ 𝑙 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ ( 𝑙 − 1 ) ) · ( 𝐴 ↑ 𝑙 ) ) )
86 oveq1 ⊢ ( 𝑙 = 𝑘 → ( 𝑙 − 1 ) = ( 𝑘 − 1 ) )
87 86 oveq2d ⊢ ( 𝑙 = 𝑘 → ( - 1 ↑ ( 𝑙 − 1 ) ) = ( - 1 ↑ ( 𝑘 − 1 ) ) )
88 oveq2 ⊢ ( 𝑙 = 𝑘 → ( 𝐴 ↑ 𝑙 ) = ( 𝐴 ↑ 𝑘 ) )
89 87 88 oveq12d ⊢ ( 𝑙 = 𝑘 → ( ( - 1 ↑ ( 𝑙 − 1 ) ) · ( 𝐴 ↑ 𝑙 ) ) = ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) )
90 89 cbvsumv ⊢ Σ 𝑙 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ ( 𝑙 − 1 ) ) · ( 𝐴 ↑ 𝑙 ) ) = Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) )
91 85 90 eqtrdi ⊢ ( 𝜑 → Σ 𝑙 ∈ ( ( 0 + 1 ) ... ( ( ( 𝑁 − 1 ) + 1 ) − 1 ) ) ( ( - 1 ↑ ( 𝑙 − 1 ) ) · ( 𝐴 ↑ 𝑙 ) ) = Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) )
92 83 oveq2d ⊢ ( 𝜑 → ( - 1 ↑ ( ( ( 𝑁 − 1 ) + 1 ) − 1 ) ) = ( - 1 ↑ ( 𝑁 − 1 ) ) )
93 53 oveq2d ⊢ ( 𝜑 → ( 𝐴 ↑ ( ( 𝑁 − 1 ) + 1 ) ) = ( 𝐴 ↑ 𝑁 ) )
94 92 93 oveq12d ⊢ ( 𝜑 → ( ( - 1 ↑ ( ( ( 𝑁 − 1 ) + 1 ) − 1 ) ) · ( 𝐴 ↑ ( ( 𝑁 − 1 ) + 1 ) ) ) = ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) )
95 91 94 oveq12d ⊢ ( 𝜑 → ( Σ 𝑙 ∈ ( ( 0 + 1 ) ... ( ( ( 𝑁 − 1 ) + 1 ) − 1 ) ) ( ( - 1 ↑ ( 𝑙 − 1 ) ) · ( 𝐴 ↑ 𝑙 ) ) + ( ( - 1 ↑ ( ( ( 𝑁 − 1 ) + 1 ) − 1 ) ) · ( 𝐴 ↑ ( ( 𝑁 − 1 ) + 1 ) ) ) ) = ( Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) + ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) ) )
96 80 95 eqtrd ⊢ ( 𝜑 → Σ 𝑙 ∈ ( ( 0 + 1 ) ... ( ( 𝑁 − 1 ) + 1 ) ) ( ( - 1 ↑ ( 𝑙 − 1 ) ) · ( 𝐴 ↑ 𝑙 ) ) = ( Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) + ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) ) )
97 42 50 96 3eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) = ( Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) + ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) ) )
98 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
99 elnn0uz ⊢ ( ( 𝑁 − 1 ) ∈ ℕ0 ↔ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
100 98 99 sylib ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
101 2 100 syl ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
102 oveq2 ⊢ ( 𝑘 = 0 → ( - 1 ↑ 𝑘 ) = ( - 1 ↑ 0 ) )
103 exp0 ⊢ ( - 1 ∈ ℂ → ( - 1 ↑ 0 ) = 1 )
104 5 103 ax-mp ⊢ ( - 1 ↑ 0 ) = 1
105 102 104 eqtrdi ⊢ ( 𝑘 = 0 → ( - 1 ↑ 𝑘 ) = 1 )
106 oveq2 ⊢ ( 𝑘 = 0 → ( 𝐴 ↑ 𝑘 ) = ( 𝐴 ↑ 0 ) )
107 105 106 oveq12d ⊢ ( 𝑘 = 0 → ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) = ( 1 · ( 𝐴 ↑ 0 ) ) )
108 101 12 107 fsum1p ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) = ( ( 1 · ( 𝐴 ↑ 0 ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) )
109 1 exp0d ⊢ ( 𝜑 → ( 𝐴 ↑ 0 ) = 1 )
110 109 oveq2d ⊢ ( 𝜑 → ( 1 · ( 𝐴 ↑ 0 ) ) = ( 1 · 1 ) )
111 1t1e1 ⊢ ( 1 · 1 ) = 1
112 110 111 eqtrdi ⊢ ( 𝜑 → ( 1 · ( 𝐴 ↑ 0 ) ) = 1 )
113 112 oveq1d ⊢ ( 𝜑 → ( ( 1 · ( 𝐴 ↑ 0 ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = ( 1 + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) )
114 fzfid ⊢ ( 𝜑 → ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ∈ Fin )
115 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℕ )
116 5 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → - 1 ∈ ℂ )
117 nnnn0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
118 117 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ0 )
119 116 118 expcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( - 1 ↑ 𝑘 ) ∈ ℂ )
120 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ℂ )
121 120 118 expcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
122 119 121 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℂ )
123 122 expcom ⊢ ( 𝑘 ∈ ℕ → ( 𝜑 → ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℂ ) )
124 115 123 syl ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 𝜑 → ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℂ ) )
125 54 oveq1i ⊢ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) = ( 1 ... ( 𝑁 − 1 ) )
126 124 125 eleq2s ⊢ ( 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) → ( 𝜑 → ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℂ ) )
127 126 impcom ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℂ )
128 114 127 fsumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℂ )
129 3 128 addcomd ⊢ ( 𝜑 → ( 1 + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = ( Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) + 1 ) )
130 108 113 129 3eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) = ( Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) + 1 ) )
131 97 130 oveq12d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) + Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = ( ( Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) + ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) ) + ( Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) + 1 ) ) )
132 nnm1nn0 ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 − 1 ) ∈ ℕ0 )
133 132 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑘 − 1 ) ∈ ℕ0 )
134 116 133 expcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( - 1 ↑ ( 𝑘 − 1 ) ) ∈ ℂ )
135 134 121 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℂ )
136 135 expcom ⊢ ( 𝑘 ∈ ℕ → ( 𝜑 → ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℂ ) )
137 115 136 syl ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 𝜑 → ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℂ ) )
138 137 125 eleq2s ⊢ ( 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) → ( 𝜑 → ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℂ ) )
139 138 impcom ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℂ )
140 114 139 fsumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℂ )
141 5 a1i ⊢ ( 𝜑 → - 1 ∈ ℂ )
142 2 98 syl ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℕ0 )
143 141 142 expcld ⊢ ( 𝜑 → ( - 1 ↑ ( 𝑁 − 1 ) ) ∈ ℂ )
144 2 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
145 1 144 expcld ⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
146 143 145 mulcld ⊢ ( 𝜑 → ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) ∈ ℂ )
147 140 146 addcld ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) + ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) ) ∈ ℂ )
148 147 128 3 addassd ⊢ ( 𝜑 → ( ( ( Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) + ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) + 1 ) = ( ( Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) + ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) ) + ( Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) + 1 ) ) )
149 140 146 addcomd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) + ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) ) = ( ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) ) )
150 149 oveq1d ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) + ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = ( ( ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) )
151 146 140 128 addassd ⊢ ( 𝜑 → ( ( ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = ( ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) + ( Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) ) )
152 nncn ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
153 npcan1 ⊢ ( 𝑘 ∈ ℂ → ( ( 𝑘 − 1 ) + 1 ) = 𝑘 )
154 152 153 syl ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑘 − 1 ) + 1 ) = 𝑘 )
155 154 eqcomd ⊢ ( 𝑘 ∈ ℕ → 𝑘 = ( ( 𝑘 − 1 ) + 1 ) )
156 155 oveq2d ⊢ ( 𝑘 ∈ ℕ → ( - 1 ↑ 𝑘 ) = ( - 1 ↑ ( ( 𝑘 − 1 ) + 1 ) ) )
157 5 a1i ⊢ ( 𝑘 ∈ ℕ → - 1 ∈ ℂ )
158 157 132 expp1d ⊢ ( 𝑘 ∈ ℕ → ( - 1 ↑ ( ( 𝑘 − 1 ) + 1 ) ) = ( ( - 1 ↑ ( 𝑘 − 1 ) ) · - 1 ) )
159 157 132 expcld ⊢ ( 𝑘 ∈ ℕ → ( - 1 ↑ ( 𝑘 − 1 ) ) ∈ ℂ )
160 159 157 mulcomd ⊢ ( 𝑘 ∈ ℕ → ( ( - 1 ↑ ( 𝑘 − 1 ) ) · - 1 ) = ( - 1 · ( - 1 ↑ ( 𝑘 − 1 ) ) ) )
161 156 158 160 3eqtrd ⊢ ( 𝑘 ∈ ℕ → ( - 1 ↑ 𝑘 ) = ( - 1 · ( - 1 ↑ ( 𝑘 − 1 ) ) ) )
162 161 oveq2d ⊢ ( 𝑘 ∈ ℕ → ( ( - 1 ↑ ( 𝑘 − 1 ) ) + ( - 1 ↑ 𝑘 ) ) = ( ( - 1 ↑ ( 𝑘 − 1 ) ) + ( - 1 · ( - 1 ↑ ( 𝑘 − 1 ) ) ) ) )
163 159 mulm1d ⊢ ( 𝑘 ∈ ℕ → ( - 1 · ( - 1 ↑ ( 𝑘 − 1 ) ) ) = - ( - 1 ↑ ( 𝑘 − 1 ) ) )
164 163 oveq2d ⊢ ( 𝑘 ∈ ℕ → ( ( - 1 ↑ ( 𝑘 − 1 ) ) + ( - 1 · ( - 1 ↑ ( 𝑘 − 1 ) ) ) ) = ( ( - 1 ↑ ( 𝑘 − 1 ) ) + - ( - 1 ↑ ( 𝑘 − 1 ) ) ) )
165 159 negidd ⊢ ( 𝑘 ∈ ℕ → ( ( - 1 ↑ ( 𝑘 − 1 ) ) + - ( - 1 ↑ ( 𝑘 − 1 ) ) ) = 0 )
166 162 164 165 3eqtrd ⊢ ( 𝑘 ∈ ℕ → ( ( - 1 ↑ ( 𝑘 − 1 ) ) + ( - 1 ↑ 𝑘 ) ) = 0 )
167 166 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( - 1 ↑ ( 𝑘 − 1 ) ) + ( - 1 ↑ 𝑘 ) ) = 0 )
168 167 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( - 1 ↑ ( 𝑘 − 1 ) ) + ( - 1 ↑ 𝑘 ) ) · ( 𝐴 ↑ 𝑘 ) ) = ( 0 · ( 𝐴 ↑ 𝑘 ) ) )
169 134 119 121 adddird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( - 1 ↑ ( 𝑘 − 1 ) ) + ( - 1 ↑ 𝑘 ) ) · ( 𝐴 ↑ 𝑘 ) ) = ( ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) + ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) )
170 121 mul02d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 0 · ( 𝐴 ↑ 𝑘 ) ) = 0 )
171 168 169 170 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) + ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = 0 )
172 171 expcom ⊢ ( 𝑘 ∈ ℕ → ( 𝜑 → ( ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) + ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = 0 ) )
173 115 172 syl ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) → ( 𝜑 → ( ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) + ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = 0 ) )
174 173 125 eleq2s ⊢ ( 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) → ( 𝜑 → ( ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) + ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = 0 ) )
175 174 impcom ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) + ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = 0 )
176 175 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) + ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) 0 )
177 114 139 127 fsumadd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) + ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = ( Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) )
178 114 olcd ⊢ ( 𝜑 → ( ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ⊆ ( ℤ≥ ‘ 1 ) ∨ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ∈ Fin ) )
179 sumz ⊢ ( ( ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ⊆ ( ℤ≥ ‘ 1 ) ∨ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ∈ Fin ) → Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) 0 = 0 )
180 178 179 syl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) 0 = 0 )
181 176 177 180 3eqtr3d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = 0 )
182 181 oveq2d ⊢ ( 𝜑 → ( ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) + ( Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) ) = ( ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) + 0 ) )
183 146 addridd ⊢ ( 𝜑 → ( ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) + 0 ) = ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) )
184 182 183 eqtrd ⊢ ( 𝜑 → ( ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) + ( Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) ) = ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) )
185 150 151 184 3eqtrd ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) + ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) )
186 185 oveq1d ⊢ ( 𝜑 → ( ( ( Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( 𝐴 ↑ 𝑘 ) ) + ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) + 1 ) = ( ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) + 1 ) )
187 131 148 186 3eqtr2d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) + Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = ( ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) + 1 ) )
188 14 26 187 3eqtrd ⊢ ( 𝜑 → ( ( 𝐴 + 1 ) · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = ( ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) + 1 ) )
189 188 eqcomd ⊢ ( 𝜑 → ( ( ( - 1 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 ↑ 𝑁 ) ) + 1 ) = ( ( 𝐴 + 1 ) · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) )