Metamath Proof Explorer

Theorem altgsumbcALT

Description: Alternate proof of altgsumbc , using Pascal's rule ( bcpascm1 ) instead of the binomial theorem ( binom ). (Contributed by AV, 8-Sep-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion altgsumbcALT 
|- ( N e. NN -> sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) x. ( N _C k ) ) = 0 )

Proof

Step Hyp Ref Expression
1 elfzelz 
 |-  ( k e. ( 0 ... N ) -> k e. ZZ )
2 bcpascm1 
 |-  ( ( N e. NN /\ k e. ZZ ) -> ( ( ( N - 1 ) _C k ) + ( ( N - 1 ) _C ( k - 1 ) ) ) = ( N _C k ) )
3 1 2 sylan2 
 |-  ( ( N e. NN /\ k e. ( 0 ... N ) ) -> ( ( ( N - 1 ) _C k ) + ( ( N - 1 ) _C ( k - 1 ) ) ) = ( N _C k ) )
4 3 eqcomd 
 |-  ( ( N e. NN /\ k e. ( 0 ... N ) ) -> ( N _C k ) = ( ( ( N - 1 ) _C k ) + ( ( N - 1 ) _C ( k - 1 ) ) ) )
5 4 oveq2d 
 |-  ( ( N e. NN /\ k e. ( 0 ... N ) ) -> ( ( -u 1 ^ k ) x. ( N _C k ) ) = ( ( -u 1 ^ k ) x. ( ( ( N - 1 ) _C k ) + ( ( N - 1 ) _C ( k - 1 ) ) ) ) )
6 ax-1cn 
 |-  1 e. CC
7 negcl 
 |-  ( 1 e. CC -> -u 1 e. CC )
8 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
9 expcl 
 |-  ( ( -u 1 e. CC /\ k e. NN0 ) -> ( -u 1 ^ k ) e. CC )
10 7 8 9 syl2an 
 |-  ( ( 1 e. CC /\ k e. ( 0 ... N ) ) -> ( -u 1 ^ k ) e. CC )
11 6 10 mpan 
 |-  ( k e. ( 0 ... N ) -> ( -u 1 ^ k ) e. CC )
12 11 adantl 
 |-  ( ( N e. NN /\ k e. ( 0 ... N ) ) -> ( -u 1 ^ k ) e. CC )
13 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
14 bccl 
 |-  ( ( ( N - 1 ) e. NN0 /\ k e. ZZ ) -> ( ( N - 1 ) _C k ) e. NN0 )
15 14 nn0cnd 
 |-  ( ( ( N - 1 ) e. NN0 /\ k e. ZZ ) -> ( ( N - 1 ) _C k ) e. CC )
16 13 1 15 syl2an 
 |-  ( ( N e. NN /\ k e. ( 0 ... N ) ) -> ( ( N - 1 ) _C k ) e. CC )
17 peano2zm 
 |-  ( k e. ZZ -> ( k - 1 ) e. ZZ )
18 1 17 syl 
 |-  ( k e. ( 0 ... N ) -> ( k - 1 ) e. ZZ )
19 bccl 
 |-  ( ( ( N - 1 ) e. NN0 /\ ( k - 1 ) e. ZZ ) -> ( ( N - 1 ) _C ( k - 1 ) ) e. NN0 )
20 19 nn0cnd 
 |-  ( ( ( N - 1 ) e. NN0 /\ ( k - 1 ) e. ZZ ) -> ( ( N - 1 ) _C ( k - 1 ) ) e. CC )
21 13 18 20 syl2an 
 |-  ( ( N e. NN /\ k e. ( 0 ... N ) ) -> ( ( N - 1 ) _C ( k - 1 ) ) e. CC )
22 12 16 21 adddid 
 |-  ( ( N e. NN /\ k e. ( 0 ... N ) ) -> ( ( -u 1 ^ k ) x. ( ( ( N - 1 ) _C k ) + ( ( N - 1 ) _C ( k - 1 ) ) ) ) = ( ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C k ) ) + ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) )
23 5 22 eqtrd 
 |-  ( ( N e. NN /\ k e. ( 0 ... N ) ) -> ( ( -u 1 ^ k ) x. ( N _C k ) ) = ( ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C k ) ) + ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) )
24 23 sumeq2dv 
 |-  ( N e. NN -> sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) x. ( N _C k ) ) = sum_ k e. ( 0 ... N ) ( ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C k ) ) + ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) )
25 fzfid 
 |-  ( N e. NN -> ( 0 ... N ) e. Fin )
26 neg1cn 
 |-  -u 1 e. CC
27 26 a1i 
 |-  ( N e. NN -> -u 1 e. CC )
28 27 8 9 syl2an 
 |-  ( ( N e. NN /\ k e. ( 0 ... N ) ) -> ( -u 1 ^ k ) e. CC )
29 28 16 mulcld 
 |-  ( ( N e. NN /\ k e. ( 0 ... N ) ) -> ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C k ) ) e. CC )
30 1z 
 |-  1 e. ZZ
31 30 a1i 
 |-  ( k e. ( 0 ... N ) -> 1 e. ZZ )
32 1 31 zsubcld 
 |-  ( k e. ( 0 ... N ) -> ( k - 1 ) e. ZZ )
33 13 32 20 syl2an 
 |-  ( ( N e. NN /\ k e. ( 0 ... N ) ) -> ( ( N - 1 ) _C ( k - 1 ) ) e. CC )
34 28 33 mulcld 
 |-  ( ( N e. NN /\ k e. ( 0 ... N ) ) -> ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) e. CC )
35 25 29 34 fsumadd 
 |-  ( N e. NN -> sum_ k e. ( 0 ... N ) ( ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C k ) ) + ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) = ( sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C k ) ) + sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) )
36 30 a1i 
 |-  ( N e. NN -> 1 e. ZZ )
37 0zd 
 |-  ( N e. NN -> 0 e. ZZ )
38 nnz 
 |-  ( N e. NN -> N e. ZZ )
39 oveq2 
 |-  ( k = ( j - 1 ) -> ( -u 1 ^ k ) = ( -u 1 ^ ( j - 1 ) ) )
40 oveq2 
 |-  ( k = ( j - 1 ) -> ( ( N - 1 ) _C k ) = ( ( N - 1 ) _C ( j - 1 ) ) )
41 39 40 oveq12d 
 |-  ( k = ( j - 1 ) -> ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C k ) ) = ( ( -u 1 ^ ( j - 1 ) ) x. ( ( N - 1 ) _C ( j - 1 ) ) ) )
42 36 37 38 29 41 fsumshft 
 |-  ( N e. NN -> sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C k ) ) = sum_ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( -u 1 ^ ( j - 1 ) ) x. ( ( N - 1 ) _C ( j - 1 ) ) ) )
43 0p1e1 
 |-  ( 0 + 1 ) = 1
44 43 oveq1i 
 |-  ( ( 0 + 1 ) ... ( N + 1 ) ) = ( 1 ... ( N + 1 ) )
45 44 a1i 
 |-  ( N e. NN -> ( ( 0 + 1 ) ... ( N + 1 ) ) = ( 1 ... ( N + 1 ) ) )
46 45 sumeq1d 
 |-  ( N e. NN -> sum_ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( -u 1 ^ ( j - 1 ) ) x. ( ( N - 1 ) _C ( j - 1 ) ) ) = sum_ j e. ( 1 ... ( N + 1 ) ) ( ( -u 1 ^ ( j - 1 ) ) x. ( ( N - 1 ) _C ( j - 1 ) ) ) )
47 elnnuz 
 |-  ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
48 47 biimpi 
 |-  ( N e. NN -> N e. ( ZZ>= ` 1 ) )
49 26 a1i 
 |-  ( ( N e. NN /\ j e. ( 1 ... ( N + 1 ) ) ) -> -u 1 e. CC )
50 elfznn 
 |-  ( j e. ( 1 ... ( N + 1 ) ) -> j e. NN )
51 nnm1nn0 
 |-  ( j e. NN -> ( j - 1 ) e. NN0 )
52 50 51 syl 
 |-  ( j e. ( 1 ... ( N + 1 ) ) -> ( j - 1 ) e. NN0 )
53 52 adantl 
 |-  ( ( N e. NN /\ j e. ( 1 ... ( N + 1 ) ) ) -> ( j - 1 ) e. NN0 )
54 49 53 expcld 
 |-  ( ( N e. NN /\ j e. ( 1 ... ( N + 1 ) ) ) -> ( -u 1 ^ ( j - 1 ) ) e. CC )
55 elfzelz 
 |-  ( j e. ( 1 ... ( N + 1 ) ) -> j e. ZZ )
56 elfzel1 
 |-  ( j e. ( 1 ... ( N + 1 ) ) -> 1 e. ZZ )
57 55 56 zsubcld 
 |-  ( j e. ( 1 ... ( N + 1 ) ) -> ( j - 1 ) e. ZZ )
58 bccl 
 |-  ( ( ( N - 1 ) e. NN0 /\ ( j - 1 ) e. ZZ ) -> ( ( N - 1 ) _C ( j - 1 ) ) e. NN0 )
59 58 nn0cnd 
 |-  ( ( ( N - 1 ) e. NN0 /\ ( j - 1 ) e. ZZ ) -> ( ( N - 1 ) _C ( j - 1 ) ) e. CC )
60 13 57 59 syl2an 
 |-  ( ( N e. NN /\ j e. ( 1 ... ( N + 1 ) ) ) -> ( ( N - 1 ) _C ( j - 1 ) ) e. CC )
61 54 60 mulcld 
 |-  ( ( N e. NN /\ j e. ( 1 ... ( N + 1 ) ) ) -> ( ( -u 1 ^ ( j - 1 ) ) x. ( ( N - 1 ) _C ( j - 1 ) ) ) e. CC )
62 oveq1 
 |-  ( j = ( N + 1 ) -> ( j - 1 ) = ( ( N + 1 ) - 1 ) )
63 62 oveq2d 
 |-  ( j = ( N + 1 ) -> ( -u 1 ^ ( j - 1 ) ) = ( -u 1 ^ ( ( N + 1 ) - 1 ) ) )
64 62 oveq2d 
 |-  ( j = ( N + 1 ) -> ( ( N - 1 ) _C ( j - 1 ) ) = ( ( N - 1 ) _C ( ( N + 1 ) - 1 ) ) )
65 63 64 oveq12d 
 |-  ( j = ( N + 1 ) -> ( ( -u 1 ^ ( j - 1 ) ) x. ( ( N - 1 ) _C ( j - 1 ) ) ) = ( ( -u 1 ^ ( ( N + 1 ) - 1 ) ) x. ( ( N - 1 ) _C ( ( N + 1 ) - 1 ) ) ) )
66 48 61 65 fsump1 
 |-  ( N e. NN -> sum_ j e. ( 1 ... ( N + 1 ) ) ( ( -u 1 ^ ( j - 1 ) ) x. ( ( N - 1 ) _C ( j - 1 ) ) ) = ( sum_ j e. ( 1 ... N ) ( ( -u 1 ^ ( j - 1 ) ) x. ( ( N - 1 ) _C ( j - 1 ) ) ) + ( ( -u 1 ^ ( ( N + 1 ) - 1 ) ) x. ( ( N - 1 ) _C ( ( N + 1 ) - 1 ) ) ) ) )
67 nncn 
 |-  ( N e. NN -> N e. CC )
68 pncan1 
 |-  ( N e. CC -> ( ( N + 1 ) - 1 ) = N )
69 67 68 syl 
 |-  ( N e. NN -> ( ( N + 1 ) - 1 ) = N )
70 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
71 69 70 eqeltrd 
 |-  ( N e. NN -> ( ( N + 1 ) - 1 ) e. NN0 )
72 71 nn0zd 
 |-  ( N e. NN -> ( ( N + 1 ) - 1 ) e. ZZ )
73 nnre 
 |-  ( N e. NN -> N e. RR )
74 ltm1 
 |-  ( N e. RR -> ( N - 1 ) < N )
75 73 74 syl 
 |-  ( N e. NN -> ( N - 1 ) < N )
76 75 69 breqtrrd 
 |-  ( N e. NN -> ( N - 1 ) < ( ( N + 1 ) - 1 ) )
77 76 olcd 
 |-  ( N e. NN -> ( ( ( N + 1 ) - 1 ) < 0 \/ ( N - 1 ) < ( ( N + 1 ) - 1 ) ) )
78 bcval4 
 |-  ( ( ( N - 1 ) e. NN0 /\ ( ( N + 1 ) - 1 ) e. ZZ /\ ( ( ( N + 1 ) - 1 ) < 0 \/ ( N - 1 ) < ( ( N + 1 ) - 1 ) ) ) -> ( ( N - 1 ) _C ( ( N + 1 ) - 1 ) ) = 0 )
79 13 72 77 78 syl3anc 
 |-  ( N e. NN -> ( ( N - 1 ) _C ( ( N + 1 ) - 1 ) ) = 0 )
80 79 oveq2d 
 |-  ( N e. NN -> ( ( -u 1 ^ ( ( N + 1 ) - 1 ) ) x. ( ( N - 1 ) _C ( ( N + 1 ) - 1 ) ) ) = ( ( -u 1 ^ ( ( N + 1 ) - 1 ) ) x. 0 ) )
81 27 71 expcld 
 |-  ( N e. NN -> ( -u 1 ^ ( ( N + 1 ) - 1 ) ) e. CC )
82 81 mul01d 
 |-  ( N e. NN -> ( ( -u 1 ^ ( ( N + 1 ) - 1 ) ) x. 0 ) = 0 )
83 80 82 eqtrd 
 |-  ( N e. NN -> ( ( -u 1 ^ ( ( N + 1 ) - 1 ) ) x. ( ( N - 1 ) _C ( ( N + 1 ) - 1 ) ) ) = 0 )
84 83 oveq2d 
 |-  ( N e. NN -> ( sum_ j e. ( 1 ... N ) ( ( -u 1 ^ ( j - 1 ) ) x. ( ( N - 1 ) _C ( j - 1 ) ) ) + ( ( -u 1 ^ ( ( N + 1 ) - 1 ) ) x. ( ( N - 1 ) _C ( ( N + 1 ) - 1 ) ) ) ) = ( sum_ j e. ( 1 ... N ) ( ( -u 1 ^ ( j - 1 ) ) x. ( ( N - 1 ) _C ( j - 1 ) ) ) + 0 ) )
85 oveq1 
 |-  ( j = k -> ( j - 1 ) = ( k - 1 ) )
86 85 oveq2d 
 |-  ( j = k -> ( -u 1 ^ ( j - 1 ) ) = ( -u 1 ^ ( k - 1 ) ) )
87 85 oveq2d 
 |-  ( j = k -> ( ( N - 1 ) _C ( j - 1 ) ) = ( ( N - 1 ) _C ( k - 1 ) ) )
88 86 87 oveq12d 
 |-  ( j = k -> ( ( -u 1 ^ ( j - 1 ) ) x. ( ( N - 1 ) _C ( j - 1 ) ) ) = ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) )
89 88 cbvsumv 
 |-  sum_ j e. ( 1 ... N ) ( ( -u 1 ^ ( j - 1 ) ) x. ( ( N - 1 ) _C ( j - 1 ) ) ) = sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) )
90 89 a1i 
 |-  ( N e. NN -> sum_ j e. ( 1 ... N ) ( ( -u 1 ^ ( j - 1 ) ) x. ( ( N - 1 ) _C ( j - 1 ) ) ) = sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) )
91 90 oveq1d 
 |-  ( N e. NN -> ( sum_ j e. ( 1 ... N ) ( ( -u 1 ^ ( j - 1 ) ) x. ( ( N - 1 ) _C ( j - 1 ) ) ) + 0 ) = ( sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) + 0 ) )
92 fzfid 
 |-  ( N e. NN -> ( 1 ... N ) e. Fin )
93 26 a1i 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> -u 1 e. CC )
94 elfznn 
 |-  ( k e. ( 1 ... N ) -> k e. NN )
95 nnm1nn0 
 |-  ( k e. NN -> ( k - 1 ) e. NN0 )
96 94 95 syl 
 |-  ( k e. ( 1 ... N ) -> ( k - 1 ) e. NN0 )
97 96 adantl 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( k - 1 ) e. NN0 )
98 93 97 expcld 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( -u 1 ^ ( k - 1 ) ) e. CC )
99 elfzelz 
 |-  ( k e. ( 1 ... N ) -> k e. ZZ )
100 elfzel1 
 |-  ( k e. ( 1 ... N ) -> 1 e. ZZ )
101 99 100 zsubcld 
 |-  ( k e. ( 1 ... N ) -> ( k - 1 ) e. ZZ )
102 13 101 19 syl2an 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( ( N - 1 ) _C ( k - 1 ) ) e. NN0 )
103 102 nn0cnd 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( ( N - 1 ) _C ( k - 1 ) ) e. CC )
104 98 103 mulcld 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) e. CC )
105 92 104 fsumcl 
 |-  ( N e. NN -> sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) e. CC )
106 105 addridd 
 |-  ( N e. NN -> ( sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) + 0 ) = sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) )
107 91 106 eqtrd 
 |-  ( N e. NN -> ( sum_ j e. ( 1 ... N ) ( ( -u 1 ^ ( j - 1 ) ) x. ( ( N - 1 ) _C ( j - 1 ) ) ) + 0 ) = sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) )
108 66 84 107 3eqtrd 
 |-  ( N e. NN -> sum_ j e. ( 1 ... ( N + 1 ) ) ( ( -u 1 ^ ( j - 1 ) ) x. ( ( N - 1 ) _C ( j - 1 ) ) ) = sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) )
109 42 46 108 3eqtrd 
 |-  ( N e. NN -> sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C k ) ) = sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) )
110 elnn0uz 
 |-  ( N e. NN0 <-> N e. ( ZZ>= ` 0 ) )
111 70 110 sylib 
 |-  ( N e. NN -> N e. ( ZZ>= ` 0 ) )
112 oveq2 
 |-  ( k = 0 -> ( -u 1 ^ k ) = ( -u 1 ^ 0 ) )
113 oveq1 
 |-  ( k = 0 -> ( k - 1 ) = ( 0 - 1 ) )
114 113 oveq2d 
 |-  ( k = 0 -> ( ( N - 1 ) _C ( k - 1 ) ) = ( ( N - 1 ) _C ( 0 - 1 ) ) )
115 112 114 oveq12d 
 |-  ( k = 0 -> ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) = ( ( -u 1 ^ 0 ) x. ( ( N - 1 ) _C ( 0 - 1 ) ) ) )
116 111 34 115 fsum1p 
 |-  ( N e. NN -> sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) = ( ( ( -u 1 ^ 0 ) x. ( ( N - 1 ) _C ( 0 - 1 ) ) ) + sum_ k e. ( ( 0 + 1 ) ... N ) ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) )
117 27 exp0d 
 |-  ( N e. NN -> ( -u 1 ^ 0 ) = 1 )
118 0z 
 |-  0 e. ZZ
119 zsubcl 
 |-  ( ( 0 e. ZZ /\ 1 e. ZZ ) -> ( 0 - 1 ) e. ZZ )
120 118 30 119 mp2an 
 |-  ( 0 - 1 ) e. ZZ
121 120 a1i 
 |-  ( N e. NN -> ( 0 - 1 ) e. ZZ )
122 0re 
 |-  0 e. RR
123 ltm1 
 |-  ( 0 e. RR -> ( 0 - 1 ) < 0 )
124 122 123 mp1i 
 |-  ( N e. NN -> ( 0 - 1 ) < 0 )
125 124 orcd 
 |-  ( N e. NN -> ( ( 0 - 1 ) < 0 \/ ( N - 1 ) < ( 0 - 1 ) ) )
126 bcval4 
 |-  ( ( ( N - 1 ) e. NN0 /\ ( 0 - 1 ) e. ZZ /\ ( ( 0 - 1 ) < 0 \/ ( N - 1 ) < ( 0 - 1 ) ) ) -> ( ( N - 1 ) _C ( 0 - 1 ) ) = 0 )
127 13 121 125 126 syl3anc 
 |-  ( N e. NN -> ( ( N - 1 ) _C ( 0 - 1 ) ) = 0 )
128 117 127 oveq12d 
 |-  ( N e. NN -> ( ( -u 1 ^ 0 ) x. ( ( N - 1 ) _C ( 0 - 1 ) ) ) = ( 1 x. 0 ) )
129 6 a1i 
 |-  ( N e. NN -> 1 e. CC )
130 129 mul01d 
 |-  ( N e. NN -> ( 1 x. 0 ) = 0 )
131 128 130 eqtrd 
 |-  ( N e. NN -> ( ( -u 1 ^ 0 ) x. ( ( N - 1 ) _C ( 0 - 1 ) ) ) = 0 )
132 43 a1i 
 |-  ( N e. NN -> ( 0 + 1 ) = 1 )
133 132 oveq1d 
 |-  ( N e. NN -> ( ( 0 + 1 ) ... N ) = ( 1 ... N ) )
134 99 zcnd 
 |-  ( k e. ( 1 ... N ) -> k e. CC )
135 npcan1 
 |-  ( k e. CC -> ( ( k - 1 ) + 1 ) = k )
136 135 eqcomd 
 |-  ( k e. CC -> k = ( ( k - 1 ) + 1 ) )
137 134 136 syl 
 |-  ( k e. ( 1 ... N ) -> k = ( ( k - 1 ) + 1 ) )
138 137 adantl 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> k = ( ( k - 1 ) + 1 ) )
139 138 oveq2d 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( -u 1 ^ k ) = ( -u 1 ^ ( ( k - 1 ) + 1 ) ) )
140 expp1 
 |-  ( ( -u 1 e. CC /\ ( k - 1 ) e. NN0 ) -> ( -u 1 ^ ( ( k - 1 ) + 1 ) ) = ( ( -u 1 ^ ( k - 1 ) ) x. -u 1 ) )
141 27 96 140 syl2an 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( -u 1 ^ ( ( k - 1 ) + 1 ) ) = ( ( -u 1 ^ ( k - 1 ) ) x. -u 1 ) )
142 139 141 eqtrd 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( -u 1 ^ k ) = ( ( -u 1 ^ ( k - 1 ) ) x. -u 1 ) )
143 142 oveq1d 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) = ( ( ( -u 1 ^ ( k - 1 ) ) x. -u 1 ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) )
144 98 93 mulcomd 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( ( -u 1 ^ ( k - 1 ) ) x. -u 1 ) = ( -u 1 x. ( -u 1 ^ ( k - 1 ) ) ) )
145 144 oveq1d 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( ( ( -u 1 ^ ( k - 1 ) ) x. -u 1 ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) = ( ( -u 1 x. ( -u 1 ^ ( k - 1 ) ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) )
146 93 98 103 mulassd 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( ( -u 1 x. ( -u 1 ^ ( k - 1 ) ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) = ( -u 1 x. ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) )
147 143 145 146 3eqtrd 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) = ( -u 1 x. ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) )
148 133 147 sumeq12rdv 
 |-  ( N e. NN -> sum_ k e. ( ( 0 + 1 ) ... N ) ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) = sum_ k e. ( 1 ... N ) ( -u 1 x. ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) )
149 92 27 104 fsummulc2 
 |-  ( N e. NN -> ( -u 1 x. sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) = sum_ k e. ( 1 ... N ) ( -u 1 x. ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) )
150 148 149 eqtr4d 
 |-  ( N e. NN -> sum_ k e. ( ( 0 + 1 ) ... N ) ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) = ( -u 1 x. sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) )
151 131 150 oveq12d 
 |-  ( N e. NN -> ( ( ( -u 1 ^ 0 ) x. ( ( N - 1 ) _C ( 0 - 1 ) ) ) + sum_ k e. ( ( 0 + 1 ) ... N ) ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) = ( 0 + ( -u 1 x. sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) ) )
152 27 105 mulcld 
 |-  ( N e. NN -> ( -u 1 x. sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) e. CC )
153 152 addlidd 
 |-  ( N e. NN -> ( 0 + ( -u 1 x. sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) ) = ( -u 1 x. sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) )
154 116 151 153 3eqtrd 
 |-  ( N e. NN -> sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) = ( -u 1 x. sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) )
155 109 154 oveq12d 
 |-  ( N e. NN -> ( sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C k ) ) + sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) = ( sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) + ( -u 1 x. sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) ) )
156 35 155 eqtrd 
 |-  ( N e. NN -> sum_ k e. ( 0 ... N ) ( ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C k ) ) + ( ( -u 1 ^ k ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) = ( sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) + ( -u 1 x. sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) ) )
157 105 mulm1d 
 |-  ( N e. NN -> ( -u 1 x. sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) = -u sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) )
158 157 oveq2d 
 |-  ( N e. NN -> ( sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) + ( -u 1 x. sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) ) = ( sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) + -u sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) )
159 105 negidd 
 |-  ( N e. NN -> ( sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) + -u sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) = 0 )
160 158 159 eqtrd 
 |-  ( N e. NN -> ( sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) + ( -u 1 x. sum_ k e. ( 1 ... N ) ( ( -u 1 ^ ( k - 1 ) ) x. ( ( N - 1 ) _C ( k - 1 ) ) ) ) ) = 0 )
161 24 156 160 3eqtrd 
 |-  ( N e. NN -> sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) x. ( N _C k ) ) = 0 )