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 
|- ( ph -> A e. CC )
pwp1fsum.n 
|- ( ph -> N e. NN )
Assertion pwp1fsum 
|- ( ph -> ( ( ( -u 1 ^ ( N - 1 ) ) x. ( A ^ N ) ) + 1 ) = ( ( A + 1 ) x. sum_ k e. ( 0 ... ( N - 1 ) ) ( ( -u 1 ^ k ) x. ( A ^ k ) ) ) )

Proof

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