This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem binomlem

Description: Lemma for binom (binomial theorem). Inductive step. (Contributed by NM, 6-Dec-2005) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses binomlem.1 
|- ( ph -> A e. CC )
binomlem.2 
|- ( ph -> B e. CC )
binomlem.3 
|- ( ph -> N e. NN0 )
binomlem.4 
|- ( ps -> ( ( A + B ) ^ N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) )
Assertion binomlem 
|- ( ( ph /\ ps ) -> ( ( A + B ) ^ ( N + 1 ) ) = sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( N + 1 ) _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) )

Proof

Step Hyp Ref Expression
1 binomlem.1 
 |-  ( ph -> A e. CC )
2 binomlem.2 
 |-  ( ph -> B e. CC )
3 binomlem.3 
 |-  ( ph -> N e. NN0 )
4 binomlem.4 
 |-  ( ps -> ( ( A + B ) ^ N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) )
5 4 adantl 
 |-  ( ( ph /\ ps ) -> ( ( A + B ) ^ N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) )
6 5 oveq1d 
 |-  ( ( ph /\ ps ) -> ( ( ( A + B ) ^ N ) x. A ) = ( sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) x. A ) )
7 fzfid 
 |-  ( ph -> ( 0 ... N ) e. Fin )
8 fzelp1 
 |-  ( k e. ( 0 ... N ) -> k e. ( 0 ... ( N + 1 ) ) )
9 elfzelz 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> k e. ZZ )
10 bccl 
 |-  ( ( N e. NN0 /\ k e. ZZ ) -> ( N _C k ) e. NN0 )
11 3 9 10 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( N _C k ) e. NN0 )
12 11 nn0cnd 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( N _C k ) e. CC )
13 8 12 sylan2 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( N _C k ) e. CC )
14 fznn0sub 
 |-  ( k e. ( 0 ... N ) -> ( N - k ) e. NN0 )
15 expcl 
 |-  ( ( A e. CC /\ ( N - k ) e. NN0 ) -> ( A ^ ( N - k ) ) e. CC )
16 1 14 15 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( A ^ ( N - k ) ) e. CC )
17 elfznn0 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> k e. NN0 )
18 expcl 
 |-  ( ( B e. CC /\ k e. NN0 ) -> ( B ^ k ) e. CC )
19 2 17 18 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( B ^ k ) e. CC )
20 8 19 sylan2 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( B ^ k ) e. CC )
21 16 20 mulcld 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) e. CC )
22 13 21 mulcld 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) e. CC )
23 7 1 22 fsummulc1 
 |-  ( ph -> ( sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) x. A ) = sum_ k e. ( 0 ... N ) ( ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) x. A ) )
24 1 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> A e. CC )
25 13 21 24 mulassd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) x. A ) = ( ( N _C k ) x. ( ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) x. A ) ) )
26 3 nn0cnd 
 |-  ( ph -> N e. CC )
27 26 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> N e. CC )
28 1cnd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> 1 e. CC )
29 elfzelz 
 |-  ( k e. ( 0 ... N ) -> k e. ZZ )
30 29 adantl 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> k e. ZZ )
31 30 zcnd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> k e. CC )
32 27 28 31 addsubd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( N + 1 ) - k ) = ( ( N - k ) + 1 ) )
33 32 oveq2d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( A ^ ( ( N + 1 ) - k ) ) = ( A ^ ( ( N - k ) + 1 ) ) )
34 expp1 
 |-  ( ( A e. CC /\ ( N - k ) e. NN0 ) -> ( A ^ ( ( N - k ) + 1 ) ) = ( ( A ^ ( N - k ) ) x. A ) )
35 1 14 34 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( A ^ ( ( N - k ) + 1 ) ) = ( ( A ^ ( N - k ) ) x. A ) )
36 33 35 eqtrd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( A ^ ( ( N + 1 ) - k ) ) = ( ( A ^ ( N - k ) ) x. A ) )
37 36 oveq1d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) = ( ( ( A ^ ( N - k ) ) x. A ) x. ( B ^ k ) ) )
38 16 24 20 mul32d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( A ^ ( N - k ) ) x. A ) x. ( B ^ k ) ) = ( ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) x. A ) )
39 37 38 eqtrd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) = ( ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) x. A ) )
40 39 oveq2d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) = ( ( N _C k ) x. ( ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) x. A ) ) )
41 25 40 eqtr4d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) x. A ) = ( ( N _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) )
42 41 sumeq2dv 
 |-  ( ph -> sum_ k e. ( 0 ... N ) ( ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) x. A ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) )
43 fzssp1 
 |-  ( 0 ... N ) C_ ( 0 ... ( N + 1 ) )
44 43 a1i 
 |-  ( ph -> ( 0 ... N ) C_ ( 0 ... ( N + 1 ) ) )
45 fznn0sub 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> ( ( N + 1 ) - k ) e. NN0 )
46 expcl 
 |-  ( ( A e. CC /\ ( ( N + 1 ) - k ) e. NN0 ) -> ( A ^ ( ( N + 1 ) - k ) ) e. CC )
47 1 45 46 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( A ^ ( ( N + 1 ) - k ) ) e. CC )
48 47 19 mulcld 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) e. CC )
49 12 48 mulcld 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) e. CC )
50 8 49 sylan2 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) e. CC )
51 3 adantr 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( 0 ... N ) ) ) -> N e. NN0 )
52 eldifi 
 |-  ( k e. ( ( 0 ... ( N + 1 ) ) \ ( 0 ... N ) ) -> k e. ( 0 ... ( N + 1 ) ) )
53 52 9 syl 
 |-  ( k e. ( ( 0 ... ( N + 1 ) ) \ ( 0 ... N ) ) -> k e. ZZ )
54 53 adantl 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( 0 ... N ) ) ) -> k e. ZZ )
55 eldifn 
 |-  ( k e. ( ( 0 ... ( N + 1 ) ) \ ( 0 ... N ) ) -> -. k e. ( 0 ... N ) )
56 55 adantl 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( 0 ... N ) ) ) -> -. k e. ( 0 ... N ) )
57 bcval3 
 |-  ( ( N e. NN0 /\ k e. ZZ /\ -. k e. ( 0 ... N ) ) -> ( N _C k ) = 0 )
58 51 54 56 57 syl3anc 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( 0 ... N ) ) ) -> ( N _C k ) = 0 )
59 58 oveq1d 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( 0 ... N ) ) ) -> ( ( N _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) = ( 0 x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) )
60 48 mul02d 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( 0 x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) = 0 )
61 52 60 sylan2 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( 0 ... N ) ) ) -> ( 0 x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) = 0 )
62 59 61 eqtrd 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( 0 ... N ) ) ) -> ( ( N _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) = 0 )
63 fzssuz 
 |-  ( 0 ... ( N + 1 ) ) C_ ( ZZ>= ` 0 )
64 63 a1i 
 |-  ( ph -> ( 0 ... ( N + 1 ) ) C_ ( ZZ>= ` 0 ) )
65 44 50 62 64 sumss 
 |-  ( ph -> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) = sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) )
66 23 42 65 3eqtrd 
 |-  ( ph -> ( sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) x. A ) = sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) )
67 66 adantr 
 |-  ( ( ph /\ ps ) -> ( sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) x. A ) = sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) )
68 6 67 eqtrd 
 |-  ( ( ph /\ ps ) -> ( ( ( A + B ) ^ N ) x. A ) = sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) )
69 4 oveq1d 
 |-  ( ps -> ( ( ( A + B ) ^ N ) x. B ) = ( sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) x. B ) )
70 7 2 22 fsummulc1 
 |-  ( ph -> ( sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) x. B ) = sum_ k e. ( 0 ... N ) ( ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) x. B ) )
71 1zzd 
 |-  ( ph -> 1 e. ZZ )
72 0z 
 |-  0 e. ZZ
73 72 a1i 
 |-  ( ph -> 0 e. ZZ )
74 3 nn0zd 
 |-  ( ph -> N e. ZZ )
75 2 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> B e. CC )
76 22 75 mulcld 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) x. B ) e. CC )
77 oveq2 
 |-  ( k = ( j - 1 ) -> ( N _C k ) = ( N _C ( j - 1 ) ) )
78 oveq2 
 |-  ( k = ( j - 1 ) -> ( N - k ) = ( N - ( j - 1 ) ) )
79 78 oveq2d 
 |-  ( k = ( j - 1 ) -> ( A ^ ( N - k ) ) = ( A ^ ( N - ( j - 1 ) ) ) )
80 oveq2 
 |-  ( k = ( j - 1 ) -> ( B ^ k ) = ( B ^ ( j - 1 ) ) )
81 79 80 oveq12d 
 |-  ( k = ( j - 1 ) -> ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) = ( ( A ^ ( N - ( j - 1 ) ) ) x. ( B ^ ( j - 1 ) ) ) )
82 77 81 oveq12d 
 |-  ( k = ( j - 1 ) -> ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) = ( ( N _C ( j - 1 ) ) x. ( ( A ^ ( N - ( j - 1 ) ) ) x. ( B ^ ( j - 1 ) ) ) ) )
83 82 oveq1d 
 |-  ( k = ( j - 1 ) -> ( ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) x. B ) = ( ( ( N _C ( j - 1 ) ) x. ( ( A ^ ( N - ( j - 1 ) ) ) x. ( B ^ ( j - 1 ) ) ) ) x. B ) )
84 71 73 74 76 83 fsumshft 
 |-  ( ph -> sum_ k e. ( 0 ... N ) ( ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) x. B ) = sum_ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( ( N _C ( j - 1 ) ) x. ( ( A ^ ( N - ( j - 1 ) ) ) x. ( B ^ ( j - 1 ) ) ) ) x. B ) )
85 oveq1 
 |-  ( j = k -> ( j - 1 ) = ( k - 1 ) )
86 85 oveq2d 
 |-  ( j = k -> ( N _C ( j - 1 ) ) = ( N _C ( k - 1 ) ) )
87 85 oveq2d 
 |-  ( j = k -> ( N - ( j - 1 ) ) = ( N - ( k - 1 ) ) )
88 87 oveq2d 
 |-  ( j = k -> ( A ^ ( N - ( j - 1 ) ) ) = ( A ^ ( N - ( k - 1 ) ) ) )
89 85 oveq2d 
 |-  ( j = k -> ( B ^ ( j - 1 ) ) = ( B ^ ( k - 1 ) ) )
90 88 89 oveq12d 
 |-  ( j = k -> ( ( A ^ ( N - ( j - 1 ) ) ) x. ( B ^ ( j - 1 ) ) ) = ( ( A ^ ( N - ( k - 1 ) ) ) x. ( B ^ ( k - 1 ) ) ) )
91 86 90 oveq12d 
 |-  ( j = k -> ( ( N _C ( j - 1 ) ) x. ( ( A ^ ( N - ( j - 1 ) ) ) x. ( B ^ ( j - 1 ) ) ) ) = ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( N - ( k - 1 ) ) ) x. ( B ^ ( k - 1 ) ) ) ) )
92 91 oveq1d 
 |-  ( j = k -> ( ( ( N _C ( j - 1 ) ) x. ( ( A ^ ( N - ( j - 1 ) ) ) x. ( B ^ ( j - 1 ) ) ) ) x. B ) = ( ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( N - ( k - 1 ) ) ) x. ( B ^ ( k - 1 ) ) ) ) x. B ) )
93 92 cbvsumv 
 |-  sum_ j e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( ( N _C ( j - 1 ) ) x. ( ( A ^ ( N - ( j - 1 ) ) ) x. ( B ^ ( j - 1 ) ) ) ) x. B ) = sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( N - ( k - 1 ) ) ) x. ( B ^ ( k - 1 ) ) ) ) x. B )
94 84 93 eqtrdi 
 |-  ( ph -> sum_ k e. ( 0 ... N ) ( ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) x. B ) = sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( N - ( k - 1 ) ) ) x. ( B ^ ( k - 1 ) ) ) ) x. B ) )
95 26 adantr 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> N e. CC )
96 elfzelz 
 |-  ( k e. ( ( 0 + 1 ) ... ( N + 1 ) ) -> k e. ZZ )
97 96 adantl 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> k e. ZZ )
98 97 zcnd 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> k e. CC )
99 1cnd 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> 1 e. CC )
100 95 98 99 subsub3d 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( N - ( k - 1 ) ) = ( ( N + 1 ) - k ) )
101 100 oveq2d 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( A ^ ( N - ( k - 1 ) ) ) = ( A ^ ( ( N + 1 ) - k ) ) )
102 101 oveq1d 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( A ^ ( N - ( k - 1 ) ) ) x. ( B ^ ( k - 1 ) ) ) = ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ ( k - 1 ) ) ) )
103 102 oveq2d 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( N - ( k - 1 ) ) ) x. ( B ^ ( k - 1 ) ) ) ) = ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ ( k - 1 ) ) ) ) )
104 103 oveq1d 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( N - ( k - 1 ) ) ) x. ( B ^ ( k - 1 ) ) ) ) x. B ) = ( ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ ( k - 1 ) ) ) ) x. B ) )
105 fzp1ss 
 |-  ( 0 e. ZZ -> ( ( 0 + 1 ) ... ( N + 1 ) ) C_ ( 0 ... ( N + 1 ) ) )
106 72 105 ax-mp 
 |-  ( ( 0 + 1 ) ... ( N + 1 ) ) C_ ( 0 ... ( N + 1 ) )
107 106 sseli 
 |-  ( k e. ( ( 0 + 1 ) ... ( N + 1 ) ) -> k e. ( 0 ... ( N + 1 ) ) )
108 9 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> k e. ZZ )
109 peano2zm 
 |-  ( k e. ZZ -> ( k - 1 ) e. ZZ )
110 108 109 syl 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( k - 1 ) e. ZZ )
111 bccl 
 |-  ( ( N e. NN0 /\ ( k - 1 ) e. ZZ ) -> ( N _C ( k - 1 ) ) e. NN0 )
112 3 110 111 syl2an2r 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( N _C ( k - 1 ) ) e. NN0 )
113 112 nn0cnd 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( N _C ( k - 1 ) ) e. CC )
114 107 113 sylan2 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( N _C ( k - 1 ) ) e. CC )
115 107 47 sylan2 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( A ^ ( ( N + 1 ) - k ) ) e. CC )
116 2 adantr 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> B e. CC )
117 elfznn 
 |-  ( k e. ( 1 ... ( N + 1 ) ) -> k e. NN )
118 0p1e1 
 |-  ( 0 + 1 ) = 1
119 118 oveq1i 
 |-  ( ( 0 + 1 ) ... ( N + 1 ) ) = ( 1 ... ( N + 1 ) )
120 117 119 eleq2s 
 |-  ( k e. ( ( 0 + 1 ) ... ( N + 1 ) ) -> k e. NN )
121 120 adantl 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> k e. NN )
122 nnm1nn0 
 |-  ( k e. NN -> ( k - 1 ) e. NN0 )
123 121 122 syl 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( k - 1 ) e. NN0 )
124 116 123 expcld 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( B ^ ( k - 1 ) ) e. CC )
125 115 124 mulcld 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ ( k - 1 ) ) ) e. CC )
126 114 125 116 mulassd 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ ( k - 1 ) ) ) ) x. B ) = ( ( N _C ( k - 1 ) ) x. ( ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ ( k - 1 ) ) ) x. B ) ) )
127 115 124 116 mulassd 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ ( k - 1 ) ) ) x. B ) = ( ( A ^ ( ( N + 1 ) - k ) ) x. ( ( B ^ ( k - 1 ) ) x. B ) ) )
128 expm1t 
 |-  ( ( B e. CC /\ k e. NN ) -> ( B ^ k ) = ( ( B ^ ( k - 1 ) ) x. B ) )
129 2 120 128 syl2an 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( B ^ k ) = ( ( B ^ ( k - 1 ) ) x. B ) )
130 129 oveq2d 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) = ( ( A ^ ( ( N + 1 ) - k ) ) x. ( ( B ^ ( k - 1 ) ) x. B ) ) )
131 127 130 eqtr4d 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ ( k - 1 ) ) ) x. B ) = ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) )
132 131 oveq2d 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( N _C ( k - 1 ) ) x. ( ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ ( k - 1 ) ) ) x. B ) ) = ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) )
133 104 126 132 3eqtrd 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( N - ( k - 1 ) ) ) x. ( B ^ ( k - 1 ) ) ) ) x. B ) = ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) )
134 133 sumeq2dv 
 |-  ( ph -> sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( N - ( k - 1 ) ) ) x. ( B ^ ( k - 1 ) ) ) ) x. B ) = sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) )
135 106 a1i 
 |-  ( ph -> ( ( 0 + 1 ) ... ( N + 1 ) ) C_ ( 0 ... ( N + 1 ) ) )
136 113 48 mulcld 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) e. CC )
137 107 136 sylan2 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) e. CC )
138 3 adantr 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( ( 0 + 1 ) ... ( N + 1 ) ) ) ) -> N e. NN0 )
139 eldifi 
 |-  ( k e. ( ( 0 ... ( N + 1 ) ) \ ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> k e. ( 0 ... ( N + 1 ) ) )
140 139 adantl 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( ( 0 + 1 ) ... ( N + 1 ) ) ) ) -> k e. ( 0 ... ( N + 1 ) ) )
141 140 9 syl 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( ( 0 + 1 ) ... ( N + 1 ) ) ) ) -> k e. ZZ )
142 141 109 syl 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( ( 0 + 1 ) ... ( N + 1 ) ) ) ) -> ( k - 1 ) e. ZZ )
143 eldifn 
 |-  ( k e. ( ( 0 ... ( N + 1 ) ) \ ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> -. k e. ( ( 0 + 1 ) ... ( N + 1 ) ) )
144 143 adantl 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( ( 0 + 1 ) ... ( N + 1 ) ) ) ) -> -. k e. ( ( 0 + 1 ) ... ( N + 1 ) ) )
145 72 a1i 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( ( 0 + 1 ) ... ( N + 1 ) ) ) ) -> 0 e. ZZ )
146 138 nn0zd 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( ( 0 + 1 ) ... ( N + 1 ) ) ) ) -> N e. ZZ )
147 1zzd 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( ( 0 + 1 ) ... ( N + 1 ) ) ) ) -> 1 e. ZZ )
148 fzaddel 
 |-  ( ( ( 0 e. ZZ /\ N e. ZZ ) /\ ( ( k - 1 ) e. ZZ /\ 1 e. ZZ ) ) -> ( ( k - 1 ) e. ( 0 ... N ) <-> ( ( k - 1 ) + 1 ) e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) )
149 145 146 142 147 148 syl22anc 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( ( 0 + 1 ) ... ( N + 1 ) ) ) ) -> ( ( k - 1 ) e. ( 0 ... N ) <-> ( ( k - 1 ) + 1 ) e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) )
150 141 zcnd 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( ( 0 + 1 ) ... ( N + 1 ) ) ) ) -> k e. CC )
151 ax-1cn 
 |-  1 e. CC
152 npcan 
 |-  ( ( k e. CC /\ 1 e. CC ) -> ( ( k - 1 ) + 1 ) = k )
153 150 151 152 sylancl 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( ( 0 + 1 ) ... ( N + 1 ) ) ) ) -> ( ( k - 1 ) + 1 ) = k )
154 153 eleq1d 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( ( 0 + 1 ) ... ( N + 1 ) ) ) ) -> ( ( ( k - 1 ) + 1 ) e. ( ( 0 + 1 ) ... ( N + 1 ) ) <-> k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) )
155 149 154 bitrd 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( ( 0 + 1 ) ... ( N + 1 ) ) ) ) -> ( ( k - 1 ) e. ( 0 ... N ) <-> k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) )
156 144 155 mtbird 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( ( 0 + 1 ) ... ( N + 1 ) ) ) ) -> -. ( k - 1 ) e. ( 0 ... N ) )
157 bcval3 
 |-  ( ( N e. NN0 /\ ( k - 1 ) e. ZZ /\ -. ( k - 1 ) e. ( 0 ... N ) ) -> ( N _C ( k - 1 ) ) = 0 )
158 138 142 156 157 syl3anc 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( ( 0 + 1 ) ... ( N + 1 ) ) ) ) -> ( N _C ( k - 1 ) ) = 0 )
159 158 oveq1d 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( ( 0 + 1 ) ... ( N + 1 ) ) ) ) -> ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) = ( 0 x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) )
160 139 60 sylan2 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( ( 0 + 1 ) ... ( N + 1 ) ) ) ) -> ( 0 x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) = 0 )
161 159 160 eqtrd 
 |-  ( ( ph /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( ( 0 + 1 ) ... ( N + 1 ) ) ) ) -> ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) = 0 )
162 135 137 161 64 sumss 
 |-  ( ph -> sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) = sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) )
163 94 134 162 3eqtrd 
 |-  ( ph -> sum_ k e. ( 0 ... N ) ( ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) x. B ) = sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) )
164 70 163 eqtrd 
 |-  ( ph -> ( sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) x. B ) = sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) )
165 69 164 sylan9eqr 
 |-  ( ( ph /\ ps ) -> ( ( ( A + B ) ^ N ) x. B ) = sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) )
166 68 165 oveq12d 
 |-  ( ( ph /\ ps ) -> ( ( ( ( A + B ) ^ N ) x. A ) + ( ( ( A + B ) ^ N ) x. B ) ) = ( sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) + sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) ) )
167 1 2 addcld 
 |-  ( ph -> ( A + B ) e. CC )
168 167 3 expp1d 
 |-  ( ph -> ( ( A + B ) ^ ( N + 1 ) ) = ( ( ( A + B ) ^ N ) x. ( A + B ) ) )
169 167 3 expcld 
 |-  ( ph -> ( ( A + B ) ^ N ) e. CC )
170 169 1 2 adddid 
 |-  ( ph -> ( ( ( A + B ) ^ N ) x. ( A + B ) ) = ( ( ( ( A + B ) ^ N ) x. A ) + ( ( ( A + B ) ^ N ) x. B ) ) )
171 168 170 eqtrd 
 |-  ( ph -> ( ( A + B ) ^ ( N + 1 ) ) = ( ( ( ( A + B ) ^ N ) x. A ) + ( ( ( A + B ) ^ N ) x. B ) ) )
172 171 adantr 
 |-  ( ( ph /\ ps ) -> ( ( A + B ) ^ ( N + 1 ) ) = ( ( ( ( A + B ) ^ N ) x. A ) + ( ( ( A + B ) ^ N ) x. B ) ) )
173 bcpasc 
 |-  ( ( N e. NN0 /\ k e. ZZ ) -> ( ( N _C k ) + ( N _C ( k - 1 ) ) ) = ( ( N + 1 ) _C k ) )
174 3 9 173 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N _C k ) + ( N _C ( k - 1 ) ) ) = ( ( N + 1 ) _C k ) )
175 174 oveq1d 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( N _C k ) + ( N _C ( k - 1 ) ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) = ( ( ( N + 1 ) _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) )
176 12 113 48 adddird 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( N _C k ) + ( N _C ( k - 1 ) ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) = ( ( ( N _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) + ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) ) )
177 175 176 eqtr3d 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( N + 1 ) _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) = ( ( ( N _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) + ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) ) )
178 177 sumeq2dv 
 |-  ( ph -> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( N + 1 ) _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) = sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( N _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) + ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) ) )
179 fzfid 
 |-  ( ph -> ( 0 ... ( N + 1 ) ) e. Fin )
180 179 49 136 fsumadd 
 |-  ( ph -> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( N _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) + ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) ) = ( sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) + sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) ) )
181 178 180 eqtrd 
 |-  ( ph -> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( N + 1 ) _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) = ( sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) + sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) ) )
182 181 adantr 
 |-  ( ( ph /\ ps ) -> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( N + 1 ) _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) = ( sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) + sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) ) )
183 166 172 182 3eqtr4d 
 |-  ( ( ph /\ ps ) -> ( ( A + B ) ^ ( N + 1 ) ) = sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( N + 1 ) _C k ) x. ( ( A ^ ( ( N + 1 ) - k ) ) x. ( B ^ k ) ) ) )