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 e. NN0 /\ A e. CC /\ B e. CC ) -> ( ( A ^ N ) - ( B ^ N ) ) = ( ( A - B ) x. sum_ k e. ( 0 ..^ N ) ( ( A ^ k ) x. ( B ^ ( ( N - k ) - 1 ) ) ) ) )

Proof

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