# Metamath Proof Explorer

## Theorem pwdif

Description: The difference of two numbers to the same power is the difference of the two numbers multiplied with a finite sum. Generalization of subsq . See Wikipedia "Fermat number", section "Other theorems about Fermat numbers", https://en.wikipedia.org/wiki/Fermat_number , 5-Aug-2021. (Contributed by AV, 6-Aug-2021) (Revised by AV, 19-Aug-2021)

Ref Expression
Assertion pwdif $⊢ N ∈ ℕ 0 ∧ A ∈ ℂ ∧ B ∈ ℂ → A N − B N = A − B ⁢ ∑ k ∈ 0 ..^ N A k ⁢ B N - k - 1$

### Proof

Step Hyp Ref Expression
1 elnn0 $⊢ N ∈ ℕ 0 ↔ N ∈ ℕ ∨ N = 0$
2 simp2 $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → A ∈ ℂ$
3 simp3 $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → B ∈ ℂ$
4 fzofi $⊢ 0 ..^ N ∈ Fin$
5 4 a1i $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → 0 ..^ N ∈ Fin$
6 2 adantr $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 ..^ N → A ∈ ℂ$
7 elfzonn0 $⊢ k ∈ 0 ..^ N → k ∈ ℕ 0$
8 7 adantl $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 ..^ N → k ∈ ℕ 0$
9 6 8 expcld $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 ..^ N → A k ∈ ℂ$
10 3 adantr $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 ..^ N → B ∈ ℂ$
11 ubmelm1fzo $⊢ k ∈ 0 ..^ N → N - k - 1 ∈ 0 ..^ N$
12 elfzonn0 $⊢ N - k - 1 ∈ 0 ..^ N → N - k - 1 ∈ ℕ 0$
13 11 12 syl $⊢ k ∈ 0 ..^ N → N - k - 1 ∈ ℕ 0$
14 13 adantl $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 ..^ N → N - k - 1 ∈ ℕ 0$
15 10 14 expcld $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 ..^ N → B N - k - 1 ∈ ℂ$
16 9 15 mulcld $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 ..^ N → A k ⁢ B N - k - 1 ∈ ℂ$
17 5 16 fsumcl $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → ∑ k ∈ 0 ..^ N A k ⁢ B N - k - 1 ∈ ℂ$
18 2 3 17 subdird $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → A − B ⁢ ∑ k ∈ 0 ..^ N A k ⁢ B N - k - 1 = A ⁢ ∑ k ∈ 0 ..^ N A k ⁢ B N - k - 1 − B ⁢ ∑ k ∈ 0 ..^ N A k ⁢ B N - k - 1$
19 5 2 16 fsummulc2 $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ ∑ k ∈ 0 ..^ N A k ⁢ B N - k - 1 = ∑ k ∈ 0 ..^ N A ⁢ A k ⁢ B N - k - 1$
20 6 9 15 mulassd $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 ..^ N → A ⁢ A k ⁢ B N - k - 1 = A ⁢ A k ⁢ B N - k - 1$
21 6 9 mulcomd $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 ..^ N → A ⁢ A k = A k ⁢ A$
22 expp1 $⊢ A ∈ ℂ ∧ k ∈ ℕ 0 → A k + 1 = A k ⁢ A$
23 2 7 22 syl2an $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 ..^ N → A k + 1 = A k ⁢ A$
24 21 23 eqtr4d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 ..^ N → A ⁢ A k = A k + 1$
25 24 oveq1d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 ..^ N → A ⁢ A k ⁢ B N - k - 1 = A k + 1 ⁢ B N - k - 1$
26 20 25 eqtr3d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 ..^ N → A ⁢ A k ⁢ B N - k - 1 = A k + 1 ⁢ B N - k - 1$
27 26 sumeq2dv $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → ∑ k ∈ 0 ..^ N A ⁢ A k ⁢ B N - k - 1 = ∑ k ∈ 0 ..^ N A k + 1 ⁢ B N - k - 1$
28 19 27 eqtrd $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ ∑ k ∈ 0 ..^ N A k ⁢ B N - k - 1 = ∑ k ∈ 0 ..^ N A k + 1 ⁢ B N - k - 1$
29 5 3 16 fsummulc2 $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → B ⁢ ∑ k ∈ 0 ..^ N A k ⁢ B N - k - 1 = ∑ k ∈ 0 ..^ N B ⁢ A k ⁢ B N - k - 1$
30 10 16 mulcomd $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 ..^ N → B ⁢ A k ⁢ B N - k - 1 = A k ⁢ B N - k - 1 ⁢ B$
31 9 15 10 mulassd $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 ..^ N → A k ⁢ B N - k - 1 ⁢ B = A k ⁢ B N - k - 1 ⁢ B$
32 expp1 $⊢ B ∈ ℂ ∧ N - k - 1 ∈ ℕ 0 → B N − k - 1 + 1 = B N - k - 1 ⁢ B$
33 32 eqcomd $⊢ B ∈ ℂ ∧ N - k - 1 ∈ ℕ 0 → B N - k - 1 ⁢ B = B N − k - 1 + 1$
34 3 13 33 syl2an $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 ..^ N → B N - k - 1 ⁢ B = B N − k - 1 + 1$
35 nncn $⊢ N ∈ ℕ → N ∈ ℂ$
36 35 3ad2ant1 $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → N ∈ ℂ$
37 36 adantr $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 ..^ N → N ∈ ℂ$
38 elfzoelz $⊢ k ∈ 0 ..^ N → k ∈ ℤ$
39 38 zcnd $⊢ k ∈ 0 ..^ N → k ∈ ℂ$
40 39 adantl $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 ..^ N → k ∈ ℂ$
41 37 40 subcld $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 ..^ N → N − k ∈ ℂ$
42 npcan1 $⊢ N − k ∈ ℂ → N − k - 1 + 1 = N − k$
43 42 oveq2d $⊢ N − k ∈ ℂ → B N − k - 1 + 1 = B N − k$
44 41 43 syl $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 ..^ N → B N − k - 1 + 1 = B N − k$
45 34 44 eqtrd $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 ..^ N → B N - k - 1 ⁢ B = B N − k$
46 45 oveq2d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 ..^ N → A k ⁢ B N - k - 1 ⁢ B = A k ⁢ B N − k$
47 30 31 46 3eqtrd $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 ..^ N → B ⁢ A k ⁢ B N - k - 1 = A k ⁢ B N − k$
48 47 sumeq2dv $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → ∑ k ∈ 0 ..^ N B ⁢ A k ⁢ B N - k - 1 = ∑ k ∈ 0 ..^ N A k ⁢ B N − k$
49 29 48 eqtrd $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → B ⁢ ∑ k ∈ 0 ..^ N A k ⁢ B N - k - 1 = ∑ k ∈ 0 ..^ N A k ⁢ B N − k$
50 28 49 oveq12d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ ∑ k ∈ 0 ..^ N A k ⁢ B N - k - 1 − B ⁢ ∑ k ∈ 0 ..^ N A k ⁢ B N - k - 1 = ∑ k ∈ 0 ..^ N A k + 1 ⁢ B N - k - 1 − ∑ k ∈ 0 ..^ N A k ⁢ B N − k$
51 nnz $⊢ N ∈ ℕ → N ∈ ℤ$
52 51 3ad2ant1 $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → N ∈ ℤ$
53 fzoval $⊢ N ∈ ℤ → 0 ..^ N = 0 … N − 1$
54 52 53 syl $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → 0 ..^ N = 0 … N − 1$
55 54 sumeq1d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → ∑ k ∈ 0 ..^ N A k + 1 ⁢ B N - k - 1 = ∑ k = 0 N − 1 A k + 1 ⁢ B N - k - 1$
56 nnm1nn0 $⊢ N ∈ ℕ → N − 1 ∈ ℕ 0$
57 nn0uz $⊢ ℕ 0 = ℤ ≥ 0$
58 56 57 eleqtrdi $⊢ N ∈ ℕ → N − 1 ∈ ℤ ≥ 0$
59 58 3ad2ant1 $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → N − 1 ∈ ℤ ≥ 0$
60 2 adantr $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 … N − 1 → A ∈ ℂ$
61 elfznn0 $⊢ k ∈ 0 … N − 1 → k ∈ ℕ 0$
62 peano2nn0 $⊢ k ∈ ℕ 0 → k + 1 ∈ ℕ 0$
63 61 62 syl $⊢ k ∈ 0 … N − 1 → k + 1 ∈ ℕ 0$
64 63 adantl $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 … N − 1 → k + 1 ∈ ℕ 0$
65 60 64 expcld $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 … N − 1 → A k + 1 ∈ ℂ$
66 3 adantr $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 … N − 1 → B ∈ ℂ$
67 36 adantr $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 … N − 1 → N ∈ ℂ$
68 61 nn0cnd $⊢ k ∈ 0 … N − 1 → k ∈ ℂ$
69 68 adantl $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 … N − 1 → k ∈ ℂ$
70 1cnd $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 … N − 1 → 1 ∈ ℂ$
71 67 69 70 sub32d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 … N − 1 → N - k - 1 = N - 1 - k$
72 fznn0sub $⊢ k ∈ 0 … N − 1 → N - 1 - k ∈ ℕ 0$
73 72 adantl $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 … N − 1 → N - 1 - k ∈ ℕ 0$
74 71 73 eqeltrd $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 … N − 1 → N - k - 1 ∈ ℕ 0$
75 66 74 expcld $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 … N − 1 → B N - k - 1 ∈ ℂ$
76 65 75 mulcld $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 … N − 1 → A k + 1 ⁢ B N - k - 1 ∈ ℂ$
77 oveq1 $⊢ k = N − 1 → k + 1 = N - 1 + 1$
78 77 oveq2d $⊢ k = N − 1 → A k + 1 = A N - 1 + 1$
79 oveq2 $⊢ k = N − 1 → N − k = N − N − 1$
80 79 oveq1d $⊢ k = N − 1 → N - k - 1 = N - N − 1 - 1$
81 80 oveq2d $⊢ k = N − 1 → B N - k - 1 = B N - N − 1 - 1$
82 78 81 oveq12d $⊢ k = N − 1 → A k + 1 ⁢ B N - k - 1 = A N - 1 + 1 ⁢ B N - N − 1 - 1$
83 59 76 82 fsumm1 $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → ∑ k = 0 N − 1 A k + 1 ⁢ B N - k - 1 = ∑ k = 0 N - 1 - 1 A k + 1 ⁢ B N - k - 1 + A N - 1 + 1 ⁢ B N - N − 1 - 1$
84 55 83 eqtrd $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → ∑ k ∈ 0 ..^ N A k + 1 ⁢ B N - k - 1 = ∑ k = 0 N - 1 - 1 A k + 1 ⁢ B N - k - 1 + A N - 1 + 1 ⁢ B N - N − 1 - 1$
85 54 sumeq1d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → ∑ k ∈ 0 ..^ N A k ⁢ B N − k = ∑ k = 0 N − 1 A k ⁢ B N − k$
86 61 adantl $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 … N − 1 → k ∈ ℕ 0$
87 60 86 expcld $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 … N − 1 → A k ∈ ℂ$
88 54 eleq2d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → k ∈ 0 ..^ N ↔ k ∈ 0 … N − 1$
89 fzonnsub $⊢ k ∈ 0 ..^ N → N − k ∈ ℕ$
90 89 nnnn0d $⊢ k ∈ 0 ..^ N → N − k ∈ ℕ 0$
91 88 90 syl6bir $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → k ∈ 0 … N − 1 → N − k ∈ ℕ 0$
92 91 imp $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 … N − 1 → N − k ∈ ℕ 0$
93 66 92 expcld $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 … N − 1 → B N − k ∈ ℂ$
94 87 93 mulcld $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 0 … N − 1 → A k ⁢ B N − k ∈ ℂ$
95 oveq2 $⊢ k = 0 → A k = A 0$
96 oveq2 $⊢ k = 0 → N − k = N − 0$
97 96 oveq2d $⊢ k = 0 → B N − k = B N − 0$
98 95 97 oveq12d $⊢ k = 0 → A k ⁢ B N − k = A 0 ⁢ B N − 0$
99 59 94 98 fsum1p $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → ∑ k = 0 N − 1 A k ⁢ B N − k = A 0 ⁢ B N − 0 + ∑ k = 0 + 1 N − 1 A k ⁢ B N − k$
100 2 exp0d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → A 0 = 1$
101 36 subid1d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → N − 0 = N$
102 101 oveq2d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → B N − 0 = B N$
103 100 102 oveq12d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → A 0 ⁢ B N − 0 = 1 ⁢ B N$
104 simp1 $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → N ∈ ℕ$
105 104 nnnn0d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → N ∈ ℕ 0$
106 3 105 expcld $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → B N ∈ ℂ$
107 106 mulid2d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → 1 ⁢ B N = B N$
108 103 107 eqtrd $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → A 0 ⁢ B N − 0 = B N$
109 0p1e1 $⊢ 0 + 1 = 1$
110 109 a1i $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → 0 + 1 = 1$
111 110 oveq1d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → 0 + 1 … N − 1 = 1 … N − 1$
112 111 sumeq1d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → ∑ k = 0 + 1 N − 1 A k ⁢ B N − k = ∑ k = 1 N − 1 A k ⁢ B N − k$
113 108 112 oveq12d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → A 0 ⁢ B N − 0 + ∑ k = 0 + 1 N − 1 A k ⁢ B N − k = B N + ∑ k = 1 N − 1 A k ⁢ B N − k$
114 85 99 113 3eqtrd $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → ∑ k ∈ 0 ..^ N A k ⁢ B N − k = B N + ∑ k = 1 N − 1 A k ⁢ B N − k$
115 84 114 oveq12d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → ∑ k ∈ 0 ..^ N A k + 1 ⁢ B N - k - 1 − ∑ k ∈ 0 ..^ N A k ⁢ B N − k = ∑ k = 0 N - 1 - 1 A k + 1 ⁢ B N - k - 1 + A N - 1 + 1 ⁢ B N - N − 1 - 1 - B N + ∑ k = 1 N − 1 A k ⁢ B N − k$
116 fzfid $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → 1 … N − 1 ∈ Fin$
117 2 adantr $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 1 … N − 1 → A ∈ ℂ$
118 elfznn $⊢ k ∈ 1 … N − 1 → k ∈ ℕ$
119 118 nnnn0d $⊢ k ∈ 1 … N − 1 → k ∈ ℕ 0$
120 119 adantl $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 1 … N − 1 → k ∈ ℕ 0$
121 117 120 expcld $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 1 … N − 1 → A k ∈ ℂ$
122 3 adantr $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 1 … N − 1 → B ∈ ℂ$
123 fzoval $⊢ N ∈ ℤ → 1 ..^ N = 1 … N − 1$
124 52 123 syl $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → 1 ..^ N = 1 … N − 1$
125 124 eleq2d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → k ∈ 1 ..^ N ↔ k ∈ 1 … N − 1$
126 fzonnsub $⊢ k ∈ 1 ..^ N → N − k ∈ ℕ$
127 126 nnnn0d $⊢ k ∈ 1 ..^ N → N − k ∈ ℕ 0$
128 125 127 syl6bir $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → k ∈ 1 … N − 1 → N − k ∈ ℕ 0$
129 128 imp $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 1 … N − 1 → N − k ∈ ℕ 0$
130 122 129 expcld $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 1 … N − 1 → B N − k ∈ ℂ$
131 121 130 mulcld $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ k ∈ 1 … N − 1 → A k ⁢ B N − k ∈ ℂ$
132 116 131 fsumcl $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → ∑ k = 1 N − 1 A k ⁢ B N − k ∈ ℂ$
133 2 105 expcld $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → A N ∈ ℂ$
134 oveq1 $⊢ k = l → k + 1 = l + 1$
135 134 oveq2d $⊢ k = l → A k + 1 = A l + 1$
136 oveq2 $⊢ k = l → N − k = N − l$
137 136 oveq1d $⊢ k = l → N - k - 1 = N - l - 1$
138 137 oveq2d $⊢ k = l → B N - k - 1 = B N - l - 1$
139 135 138 oveq12d $⊢ k = l → A k + 1 ⁢ B N - k - 1 = A l + 1 ⁢ B N - l - 1$
140 139 cbvsumv $⊢ ∑ k = 0 N - 1 - 1 A k + 1 ⁢ B N - k - 1 = ∑ l = 0 N - 1 - 1 A l + 1 ⁢ B N - l - 1$
141 1m1e0 $⊢ 1 − 1 = 0$
142 141 eqcomi $⊢ 0 = 1 − 1$
143 142 oveq1i $⊢ 0 … N - 1 - 1 = 1 − 1 … N - 1 - 1$
144 143 a1i $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → 0 … N - 1 - 1 = 1 − 1 … N - 1 - 1$
145 36 adantr $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ l ∈ 0 … N - 1 - 1 → N ∈ ℂ$
146 elfznn0 $⊢ l ∈ 0 … N - 1 - 1 → l ∈ ℕ 0$
147 146 nn0cnd $⊢ l ∈ 0 … N - 1 - 1 → l ∈ ℂ$
148 147 adantl $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ l ∈ 0 … N - 1 - 1 → l ∈ ℂ$
149 1cnd $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ l ∈ 0 … N - 1 - 1 → 1 ∈ ℂ$
150 145 148 149 subsub4d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ l ∈ 0 … N - 1 - 1 → N - l - 1 = N − l + 1$
151 150 oveq2d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ l ∈ 0 … N - 1 - 1 → B N - l - 1 = B N − l + 1$
152 151 oveq2d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ l ∈ 0 … N - 1 - 1 → A l + 1 ⁢ B N - l - 1 = A l + 1 ⁢ B N − l + 1$
153 144 152 sumeq12dv $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → ∑ l = 0 N - 1 - 1 A l + 1 ⁢ B N - l - 1 = ∑ l = 1 − 1 N - 1 - 1 A l + 1 ⁢ B N − l + 1$
154 140 153 syl5eq $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → ∑ k = 0 N - 1 - 1 A k + 1 ⁢ B N - k - 1 = ∑ l = 1 − 1 N - 1 - 1 A l + 1 ⁢ B N − l + 1$
155 1zzd $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → 1 ∈ ℤ$
156 peano2zm $⊢ N ∈ ℤ → N − 1 ∈ ℤ$
157 52 156 syl $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → N − 1 ∈ ℤ$
158 oveq2 $⊢ k = l + 1 → A k = A l + 1$
159 oveq2 $⊢ k = l + 1 → N − k = N − l + 1$
160 159 oveq2d $⊢ k = l + 1 → B N − k = B N − l + 1$
161 158 160 oveq12d $⊢ k = l + 1 → A k ⁢ B N − k = A l + 1 ⁢ B N − l + 1$
162 155 155 157 131 161 fsumshftm $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → ∑ k = 1 N − 1 A k ⁢ B N − k = ∑ l = 1 − 1 N - 1 - 1 A l + 1 ⁢ B N − l + 1$
163 154 162 eqtr4d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → ∑ k = 0 N - 1 - 1 A k + 1 ⁢ B N - k - 1 = ∑ k = 1 N − 1 A k ⁢ B N − k$
164 npcan1 $⊢ N ∈ ℂ → N - 1 + 1 = N$
165 36 164 syl $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → N - 1 + 1 = N$
166 165 oveq2d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → A N - 1 + 1 = A N$
167 peano2cnm $⊢ N ∈ ℂ → N − 1 ∈ ℂ$
168 35 167 syl $⊢ N ∈ ℕ → N − 1 ∈ ℂ$
169 1cnd $⊢ N ∈ ℕ → 1 ∈ ℂ$
170 35 168 169 sub32d $⊢ N ∈ ℕ → N - N − 1 - 1 = N - 1 - N − 1$
171 168 subidd $⊢ N ∈ ℕ → N - 1 - N − 1 = 0$
172 170 171 eqtrd $⊢ N ∈ ℕ → N - N − 1 - 1 = 0$
173 172 3ad2ant1 $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → N - N − 1 - 1 = 0$
174 173 oveq2d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → B N - N − 1 - 1 = B 0$
175 exp0 $⊢ B ∈ ℂ → B 0 = 1$
176 175 3ad2ant3 $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → B 0 = 1$
177 174 176 eqtrd $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → B N - N − 1 - 1 = 1$
178 166 177 oveq12d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → A N - 1 + 1 ⁢ B N - N − 1 - 1 = A N ⋅ 1$
179 133 mulid1d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → A N ⋅ 1 = A N$
180 178 179 eqtrd $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → A N - 1 + 1 ⁢ B N - N − 1 - 1 = A N$
181 163 180 oveq12d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → ∑ k = 0 N - 1 - 1 A k + 1 ⁢ B N - k - 1 + A N - 1 + 1 ⁢ B N - N − 1 - 1 = ∑ k = 1 N − 1 A k ⁢ B N − k + A N$
182 132 133 181 comraddd $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → ∑ k = 0 N - 1 - 1 A k + 1 ⁢ B N - k - 1 + A N - 1 + 1 ⁢ B N - N − 1 - 1 = A N + ∑ k = 1 N − 1 A k ⁢ B N − k$
183 182 oveq1d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → ∑ k = 0 N - 1 - 1 A k + 1 ⁢ B N - k - 1 + A N - 1 + 1 ⁢ B N - N − 1 - 1 - B N + ∑ k = 1 N − 1 A k ⁢ B N − k = A N + ∑ k = 1 N − 1 A k ⁢ B N − k - B N + ∑ k = 1 N − 1 A k ⁢ B N − k$
184 133 106 132 pnpcan2d $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → A N + ∑ k = 1 N − 1 A k ⁢ B N − k - B N + ∑ k = 1 N − 1 A k ⁢ B N − k = A N − B N$
185 115 183 184 3eqtrd $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → ∑ k ∈ 0 ..^ N A k + 1 ⁢ B N - k - 1 − ∑ k ∈ 0 ..^ N A k ⁢ B N − k = A N − B N$
186 18 50 185 3eqtrrd $⊢ N ∈ ℕ ∧ A ∈ ℂ ∧ B ∈ ℂ → A N − B N = A − B ⁢ ∑ k ∈ 0 ..^ N A k ⁢ B N - k - 1$
187 186 3exp $⊢ N ∈ ℕ → A ∈ ℂ → B ∈ ℂ → A N − B N = A − B ⁢ ∑ k ∈ 0 ..^ N A k ⁢ B N - k - 1$
188 simp2 $⊢ N = 0 ∧ A ∈ ℂ ∧ B ∈ ℂ → A ∈ ℂ$
189 simp3 $⊢ N = 0 ∧ A ∈ ℂ ∧ B ∈ ℂ → B ∈ ℂ$
190 188 189 subcld $⊢ N = 0 ∧ A ∈ ℂ ∧ B ∈ ℂ → A − B ∈ ℂ$
191 190 mul01d $⊢ N = 0 ∧ A ∈ ℂ ∧ B ∈ ℂ → A − B ⋅ 0 = 0$
192 oveq2 $⊢ N = 0 → 0 ..^ N = 0 ..^ 0$
193 fzo0 $⊢ 0 ..^ 0 = ∅$
194 192 193 eqtrdi $⊢ N = 0 → 0 ..^ N = ∅$
195 194 sumeq1d $⊢ N = 0 → ∑ k ∈ 0 ..^ N A k ⁢ B N - k - 1 = ∑ k ∈ ∅ A k ⁢ B N - k - 1$
196 195 3ad2ant1 $⊢ N = 0 ∧ A ∈ ℂ ∧ B ∈ ℂ → ∑ k ∈ 0 ..^ N A k ⁢ B N - k - 1 = ∑ k ∈ ∅ A k ⁢ B N - k - 1$
197 sum0 $⊢ ∑ k ∈ ∅ A k ⁢ B N - k - 1 = 0$
198 196 197 eqtrdi $⊢ N = 0 ∧ A ∈ ℂ ∧ B ∈ ℂ → ∑ k ∈ 0 ..^ N A k ⁢ B N - k - 1 = 0$
199 198 oveq2d $⊢ N = 0 ∧ A ∈ ℂ ∧ B ∈ ℂ → A − B ⁢ ∑ k ∈ 0 ..^ N A k ⁢ B N - k - 1 = A − B ⋅ 0$
200 oveq2 $⊢ N = 0 → A N = A 0$
201 200 3ad2ant1 $⊢ N = 0 ∧ A ∈ ℂ ∧ B ∈ ℂ → A N = A 0$
202 exp0 $⊢ A ∈ ℂ → A 0 = 1$
203 202 3ad2ant2 $⊢ N = 0 ∧ A ∈ ℂ ∧ B ∈ ℂ → A 0 = 1$
204 201 203 eqtrd $⊢ N = 0 ∧ A ∈ ℂ ∧ B ∈ ℂ → A N = 1$
205 oveq2 $⊢ N = 0 → B N = B 0$
206 205 3ad2ant1 $⊢ N = 0 ∧ A ∈ ℂ ∧ B ∈ ℂ → B N = B 0$
207 175 3ad2ant3 $⊢ N = 0 ∧ A ∈ ℂ ∧ B ∈ ℂ → B 0 = 1$
208 206 207 eqtrd $⊢ N = 0 ∧ A ∈ ℂ ∧ B ∈ ℂ → B N = 1$
209 204 208 oveq12d $⊢ N = 0 ∧ A ∈ ℂ ∧ B ∈ ℂ → A N − B N = 1 − 1$
210 209 141 eqtrdi $⊢ N = 0 ∧ A ∈ ℂ ∧ B ∈ ℂ → A N − B N = 0$
211 191 199 210 3eqtr4rd $⊢ N = 0 ∧ A ∈ ℂ ∧ B ∈ ℂ → A N − B N = A − B ⁢ ∑ k ∈ 0 ..^ N A k ⁢ B N - k - 1$
212 211 3exp $⊢ N = 0 → A ∈ ℂ → B ∈ ℂ → A N − B N = A − B ⁢ ∑ k ∈ 0 ..^ N A k ⁢ B N - k - 1$
213 187 212 jaoi $⊢ N ∈ ℕ ∨ N = 0 → A ∈ ℂ → B ∈ ℂ → A N − B N = A − B ⁢ ∑ k ∈ 0 ..^ N A k ⁢ B N - k - 1$
214 1 213 sylbi $⊢ N ∈ ℕ 0 → A ∈ ℂ → B ∈ ℂ → A N − B N = A − B ⁢ ∑ k ∈ 0 ..^ N A k ⁢ B N - k - 1$
215 214 3imp $⊢ N ∈ ℕ 0 ∧ A ∈ ℂ ∧ B ∈ ℂ → A N − B N = A − B ⁢ ∑ k ∈ 0 ..^ N A k ⁢ B N - k - 1$