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 mulid2d ( 𝜑 → ( 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 syl5bi ( 𝜑 → ( 𝑙 ∈ ( ( 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 addid1d ( 𝜑 → ( ( ( - 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 ↑ 𝑘 ) · ( 𝐴𝑘 ) ) ) )