Metamath Proof Explorer

Theorem binomcxplemnn0

Description: Lemma for binomcxp . When C is a nonnegative integer, the binomial's finite sum value by the standard binomial theorem binom equals this generalized infinite sum: the generalized binomial coefficient and exponentiation operators give exactly the same values in the standard index set ( 0 ... C ) , and when the index set is widened beyond C the additional values are just zeroes. (Contributed by Steve Rodriguez, 22-Apr-2020)

Ref Expression
Hypotheses binomcxp.a 
|- ( ph -> A e. RR+ )
binomcxp.b 
|- ( ph -> B e. RR )
binomcxp.lt 
|- ( ph -> ( abs ` B ) < ( abs ` A ) )
binomcxp.c 
|- ( ph -> C e. CC )
Assertion binomcxplemnn0 
|- ( ( ph /\ C e. NN0 ) -> ( ( A + B ) ^c C ) = sum_ k e. NN0 ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) )

Proof

Step Hyp Ref Expression
1 binomcxp.a 
 |-  ( ph -> A e. RR+ )
2 binomcxp.b 
 |-  ( ph -> B e. RR )
3 binomcxp.lt 
 |-  ( ph -> ( abs ` B ) < ( abs ` A ) )
4 binomcxp.c 
 |-  ( ph -> C e. CC )
5 1 rpcnd 
 |-  ( ph -> A e. CC )
6 2 recnd 
 |-  ( ph -> B e. CC )
7 binom 
 |-  ( ( A e. CC /\ B e. CC /\ C e. NN0 ) -> ( ( A + B ) ^ C ) = sum_ k e. ( 0 ... C ) ( ( C _C k ) x. ( ( A ^ ( C - k ) ) x. ( B ^ k ) ) ) )
8 7 3expia 
 |-  ( ( A e. CC /\ B e. CC ) -> ( C e. NN0 -> ( ( A + B ) ^ C ) = sum_ k e. ( 0 ... C ) ( ( C _C k ) x. ( ( A ^ ( C - k ) ) x. ( B ^ k ) ) ) ) )
9 5 6 8 syl2anc 
 |-  ( ph -> ( C e. NN0 -> ( ( A + B ) ^ C ) = sum_ k e. ( 0 ... C ) ( ( C _C k ) x. ( ( A ^ ( C - k ) ) x. ( B ^ k ) ) ) ) )
10 9 imp 
 |-  ( ( ph /\ C e. NN0 ) -> ( ( A + B ) ^ C ) = sum_ k e. ( 0 ... C ) ( ( C _C k ) x. ( ( A ^ ( C - k ) ) x. ( B ^ k ) ) ) )
11 5 adantr 
 |-  ( ( ph /\ C e. NN0 ) -> A e. CC )
12 6 adantr 
 |-  ( ( ph /\ C e. NN0 ) -> B e. CC )
13 11 12 addcld 
 |-  ( ( ph /\ C e. NN0 ) -> ( A + B ) e. CC )
14 simpr 
 |-  ( ( ph /\ C e. NN0 ) -> C e. NN0 )
15 cxpexp 
 |-  ( ( ( A + B ) e. CC /\ C e. NN0 ) -> ( ( A + B ) ^c C ) = ( ( A + B ) ^ C ) )
16 13 14 15 syl2anc 
 |-  ( ( ph /\ C e. NN0 ) -> ( ( A + B ) ^c C ) = ( ( A + B ) ^ C ) )
17 elfznn0 
 |-  ( k e. ( 0 ... C ) -> k e. NN0 )
18 simplr 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) -> C e. NN0 )
19 simpr 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) -> k e. NN0 )
20 18 19 bccbc 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) -> ( C _Cc k ) = ( C _C k ) )
21 17 20 sylan2 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( 0 ... C ) ) -> ( C _Cc k ) = ( C _C k ) )
22 5 ad2antrr 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( 0 ... C ) ) -> A e. CC )
23 elfzle2 
 |-  ( k e. ( 0 ... C ) -> k <_ C )
24 23 adantl 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( 0 ... C ) ) -> k <_ C )
25 nn0sub 
 |-  ( ( k e. NN0 /\ C e. NN0 ) -> ( k <_ C <-> ( C - k ) e. NN0 ) )
26 25 ancoms 
 |-  ( ( C e. NN0 /\ k e. NN0 ) -> ( k <_ C <-> ( C - k ) e. NN0 ) )
27 26 adantll 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) -> ( k <_ C <-> ( C - k ) e. NN0 ) )
28 17 27 sylan2 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( 0 ... C ) ) -> ( k <_ C <-> ( C - k ) e. NN0 ) )
29 24 28 mpbid 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( 0 ... C ) ) -> ( C - k ) e. NN0 )
30 cxpexp 
 |-  ( ( A e. CC /\ ( C - k ) e. NN0 ) -> ( A ^c ( C - k ) ) = ( A ^ ( C - k ) ) )
31 22 29 30 syl2anc 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( 0 ... C ) ) -> ( A ^c ( C - k ) ) = ( A ^ ( C - k ) ) )
32 31 oveq1d 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( 0 ... C ) ) -> ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) = ( ( A ^ ( C - k ) ) x. ( B ^ k ) ) )
33 21 32 oveq12d 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( 0 ... C ) ) -> ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) = ( ( C _C k ) x. ( ( A ^ ( C - k ) ) x. ( B ^ k ) ) ) )
34 33 sumeq2dv 
 |-  ( ( ph /\ C e. NN0 ) -> sum_ k e. ( 0 ... C ) ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) = sum_ k e. ( 0 ... C ) ( ( C _C k ) x. ( ( A ^ ( C - k ) ) x. ( B ^ k ) ) ) )
35 10 16 34 3eqtr4d 
 |-  ( ( ph /\ C e. NN0 ) -> ( ( A + B ) ^c C ) = sum_ k e. ( 0 ... C ) ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) )
36 4 adantr 
 |-  ( ( ph /\ C e. NN0 ) -> C e. CC )
37 13 36 cxpcld 
 |-  ( ( ph /\ C e. NN0 ) -> ( ( A + B ) ^c C ) e. CC )
38 35 37 eqeltrrd 
 |-  ( ( ph /\ C e. NN0 ) -> sum_ k e. ( 0 ... C ) ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) e. CC )
39 38 addid1d 
 |-  ( ( ph /\ C e. NN0 ) -> ( sum_ k e. ( 0 ... C ) ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) + 0 ) = sum_ k e. ( 0 ... C ) ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) )
40 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
41 eqid 
 |-  ( ZZ>= ` ( C + 1 ) ) = ( ZZ>= ` ( C + 1 ) )
42 1nn0 
 |-  1 e. NN0
43 42 a1i 
 |-  ( ( ph /\ C e. NN0 ) -> 1 e. NN0 )
44 14 43 nn0addcld 
 |-  ( ( ph /\ C e. NN0 ) -> ( C + 1 ) e. NN0 )
45 eqidd 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) -> ( j e. NN0 |-> ( ( C _Cc j ) x. ( ( A ^c ( C - j ) ) x. ( B ^ j ) ) ) ) = ( j e. NN0 |-> ( ( C _Cc j ) x. ( ( A ^c ( C - j ) ) x. ( B ^ j ) ) ) ) )
46 simpr 
 |-  ( ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) /\ j = k ) -> j = k )
47 46 oveq2d 
 |-  ( ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) /\ j = k ) -> ( C _Cc j ) = ( C _Cc k ) )
48 46 oveq2d 
 |-  ( ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) /\ j = k ) -> ( C - j ) = ( C - k ) )
49 48 oveq2d 
 |-  ( ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) /\ j = k ) -> ( A ^c ( C - j ) ) = ( A ^c ( C - k ) ) )
50 46 oveq2d 
 |-  ( ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) /\ j = k ) -> ( B ^ j ) = ( B ^ k ) )
51 49 50 oveq12d 
 |-  ( ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) /\ j = k ) -> ( ( A ^c ( C - j ) ) x. ( B ^ j ) ) = ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) )
52 47 51 oveq12d 
 |-  ( ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) /\ j = k ) -> ( ( C _Cc j ) x. ( ( A ^c ( C - j ) ) x. ( B ^ j ) ) ) = ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) )
53 4 ad2antrr 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) -> C e. CC )
54 53 19 bcccl 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) -> ( C _Cc k ) e. CC )
55 5 ad2antrr 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) -> A e. CC )
56 19 nn0cnd 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) -> k e. CC )
57 53 56 subcld 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) -> ( C - k ) e. CC )
58 55 57 cxpcld 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) -> ( A ^c ( C - k ) ) e. CC )
59 6 ad2antrr 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) -> B e. CC )
60 59 19 expcld 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) -> ( B ^ k ) e. CC )
61 58 60 mulcld 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) -> ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) e. CC )
62 54 61 mulcld 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) -> ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) e. CC )
63 45 52 19 62 fvmptd 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) -> ( ( j e. NN0 |-> ( ( C _Cc j ) x. ( ( A ^c ( C - j ) ) x. ( B ^ j ) ) ) ) ` k ) = ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) )
64 peano2nn0 
 |-  ( C e. NN0 -> ( C + 1 ) e. NN0 )
65 64 adantl 
 |-  ( ( ph /\ C e. NN0 ) -> ( C + 1 ) e. NN0 )
66 c0ex 
 |-  0 e. _V
67 66 fconst 
 |-  ( NN0 X. { 0 } ) : NN0 --> { 0 }
68 67 a1i 
 |-  ( ( ph /\ C e. NN0 ) -> ( NN0 X. { 0 } ) : NN0 --> { 0 } )
69 0red 
 |-  ( ( ph /\ C e. NN0 ) -> 0 e. RR )
70 69 snssd 
 |-  ( ( ph /\ C e. NN0 ) -> { 0 } C_ RR )
71 68 70 fssd 
 |-  ( ( ph /\ C e. NN0 ) -> ( NN0 X. { 0 } ) : NN0 --> RR )
72 71 ffvelrnda 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) -> ( ( NN0 X. { 0 } ) ` k ) e. RR )
73 63 62 eqeltrd 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) -> ( ( j e. NN0 |-> ( ( C _Cc j ) x. ( ( A ^c ( C - j ) ) x. ( B ^ j ) ) ) ) ` k ) e. CC )
74 climrel 
 |-  Rel ~~>
75 40 xpeq1i 
 |-  ( NN0 X. { 0 } ) = ( ( ZZ>= ` 0 ) X. { 0 } )
76 seqeq3 
 |-  ( ( NN0 X. { 0 } ) = ( ( ZZ>= ` 0 ) X. { 0 } ) -> seq 0 ( + , ( NN0 X. { 0 } ) ) = seq 0 ( + , ( ( ZZ>= ` 0 ) X. { 0 } ) ) )
77 75 76 ax-mp 
 |-  seq 0 ( + , ( NN0 X. { 0 } ) ) = seq 0 ( + , ( ( ZZ>= ` 0 ) X. { 0 } ) )
78 0z 
 |-  0 e. ZZ
79 serclim0 
 |-  ( 0 e. ZZ -> seq 0 ( + , ( ( ZZ>= ` 0 ) X. { 0 } ) ) ~~> 0 )
80 78 79 ax-mp 
 |-  seq 0 ( + , ( ( ZZ>= ` 0 ) X. { 0 } ) ) ~~> 0
81 77 80 eqbrtri 
 |-  seq 0 ( + , ( NN0 X. { 0 } ) ) ~~> 0
82 releldm 
 |-  ( ( Rel ~~> /\ seq 0 ( + , ( NN0 X. { 0 } ) ) ~~> 0 ) -> seq 0 ( + , ( NN0 X. { 0 } ) ) e. dom ~~> )
83 74 81 82 mp2an 
 |-  seq 0 ( + , ( NN0 X. { 0 } ) ) e. dom ~~>
84 83 a1i 
 |-  ( ( ph /\ C e. NN0 ) -> seq 0 ( + , ( NN0 X. { 0 } ) ) e. dom ~~> )
85 eluznn0 
 |-  ( ( ( C + 1 ) e. NN0 /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> k e. NN0 )
86 65 85 sylan 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> k e. NN0 )
87 86 63 syldan 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> ( ( j e. NN0 |-> ( ( C _Cc j ) x. ( ( A ^c ( C - j ) ) x. ( B ^ j ) ) ) ) ` k ) = ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) )
88 0zd 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> 0 e. ZZ )
89 86 nn0zd 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> k e. ZZ )
90 1zzd 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> 1 e. ZZ )
91 89 90 zsubcld 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> ( k - 1 ) e. ZZ )
92 14 nn0zd 
 |-  ( ( ph /\ C e. NN0 ) -> C e. ZZ )
93 92 adantr 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> C e. ZZ )
94 14 nn0ge0d 
 |-  ( ( ph /\ C e. NN0 ) -> 0 <_ C )
95 94 adantr 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> 0 <_ C )
96 eluzle 
 |-  ( k e. ( ZZ>= ` ( C + 1 ) ) -> ( C + 1 ) <_ k )
97 96 adantl 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> ( C + 1 ) <_ k )
98 93 zred 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> C e. RR )
99 1red 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> 1 e. RR )
100 86 nn0red 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> k e. RR )
101 leaddsub 
 |-  ( ( C e. RR /\ 1 e. RR /\ k e. RR ) -> ( ( C + 1 ) <_ k <-> C <_ ( k - 1 ) ) )
102 98 99 100 101 syl3anc 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> ( ( C + 1 ) <_ k <-> C <_ ( k - 1 ) ) )
103 97 102 mpbid 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> C <_ ( k - 1 ) )
104 elfz4 
 |-  ( ( ( 0 e. ZZ /\ ( k - 1 ) e. ZZ /\ C e. ZZ ) /\ ( 0 <_ C /\ C <_ ( k - 1 ) ) ) -> C e. ( 0 ... ( k - 1 ) ) )
105 88 91 93 95 103 104 syl32anc 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> C e. ( 0 ... ( k - 1 ) ) )
106 4 ad2antrr 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> C e. CC )
107 106 86 bcc0 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> ( ( C _Cc k ) = 0 <-> C e. ( 0 ... ( k - 1 ) ) ) )
108 105 107 mpbird 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> ( C _Cc k ) = 0 )
109 108 oveq1d 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) = ( 0 x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) )
110 5 ad2antrr 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> A e. CC )
111 eluzelcn 
 |-  ( k e. ( ZZ>= ` ( C + 1 ) ) -> k e. CC )
112 111 adantl 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> k e. CC )
113 106 112 subcld 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> ( C - k ) e. CC )
114 110 113 cxpcld 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> ( A ^c ( C - k ) ) e. CC )
115 6 ad2antrr 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> B e. CC )
116 115 86 expcld 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> ( B ^ k ) e. CC )
117 114 116 mulcld 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) e. CC )
118 117 mul02d 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> ( 0 x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) = 0 )
119 109 118 eqtrd 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) = 0 )
120 87 119 eqtrd 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> ( ( j e. NN0 |-> ( ( C _Cc j ) x. ( ( A ^c ( C - j ) ) x. ( B ^ j ) ) ) ) ` k ) = 0 )
121 120 abs00bd 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> ( abs ` ( ( j e. NN0 |-> ( ( C _Cc j ) x. ( ( A ^c ( C - j ) ) x. ( B ^ j ) ) ) ) ` k ) ) = 0 )
122 0re 
 |-  0 e. RR
123 121 122 eqeltrdi 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> ( abs ` ( ( j e. NN0 |-> ( ( C _Cc j ) x. ( ( A ^c ( C - j ) ) x. ( B ^ j ) ) ) ) ` k ) ) e. RR )
124 eqle 
 |-  ( ( ( abs ` ( ( j e. NN0 |-> ( ( C _Cc j ) x. ( ( A ^c ( C - j ) ) x. ( B ^ j ) ) ) ) ` k ) ) e. RR /\ ( abs ` ( ( j e. NN0 |-> ( ( C _Cc j ) x. ( ( A ^c ( C - j ) ) x. ( B ^ j ) ) ) ) ` k ) ) = 0 ) -> ( abs ` ( ( j e. NN0 |-> ( ( C _Cc j ) x. ( ( A ^c ( C - j ) ) x. ( B ^ j ) ) ) ) ` k ) ) <_ 0 )
125 123 121 124 syl2anc 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> ( abs ` ( ( j e. NN0 |-> ( ( C _Cc j ) x. ( ( A ^c ( C - j ) ) x. ( B ^ j ) ) ) ) ` k ) ) <_ 0 )
126 72 recnd 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. NN0 ) -> ( ( NN0 X. { 0 } ) ` k ) e. CC )
127 86 126 syldan 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> ( ( NN0 X. { 0 } ) ` k ) e. CC )
128 127 mul02d 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> ( 0 x. ( ( NN0 X. { 0 } ) ` k ) ) = 0 )
129 125 128 breqtrrd 
 |-  ( ( ( ph /\ C e. NN0 ) /\ k e. ( ZZ>= ` ( C + 1 ) ) ) -> ( abs ` ( ( j e. NN0 |-> ( ( C _Cc j ) x. ( ( A ^c ( C - j ) ) x. ( B ^ j ) ) ) ) ` k ) ) <_ ( 0 x. ( ( NN0 X. { 0 } ) ` k ) ) )
130 40 65 72 73 84 69 129 cvgcmpce 
 |-  ( ( ph /\ C e. NN0 ) -> seq 0 ( + , ( j e. NN0 |-> ( ( C _Cc j ) x. ( ( A ^c ( C - j ) ) x. ( B ^ j ) ) ) ) ) e. dom ~~> )
131 40 41 44 63 62 130 isumsplit 
 |-  ( ( ph /\ C e. NN0 ) -> sum_ k e. NN0 ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) = ( sum_ k e. ( 0 ... ( ( C + 1 ) - 1 ) ) ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) + sum_ k e. ( ZZ>= ` ( C + 1 ) ) ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) ) )
132 1cnd 
 |-  ( ( ph /\ C e. NN0 ) -> 1 e. CC )
133 36 132 pncand 
 |-  ( ( ph /\ C e. NN0 ) -> ( ( C + 1 ) - 1 ) = C )
134 133 oveq2d 
 |-  ( ( ph /\ C e. NN0 ) -> ( 0 ... ( ( C + 1 ) - 1 ) ) = ( 0 ... C ) )
135 134 sumeq1d 
 |-  ( ( ph /\ C e. NN0 ) -> sum_ k e. ( 0 ... ( ( C + 1 ) - 1 ) ) ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) = sum_ k e. ( 0 ... C ) ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) )
136 135 oveq1d 
 |-  ( ( ph /\ C e. NN0 ) -> ( sum_ k e. ( 0 ... ( ( C + 1 ) - 1 ) ) ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) + sum_ k e. ( ZZ>= ` ( C + 1 ) ) ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) ) = ( sum_ k e. ( 0 ... C ) ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) + sum_ k e. ( ZZ>= ` ( C + 1 ) ) ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) ) )
137 119 sumeq2dv 
 |-  ( ( ph /\ C e. NN0 ) -> sum_ k e. ( ZZ>= ` ( C + 1 ) ) ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) = sum_ k e. ( ZZ>= ` ( C + 1 ) ) 0 )
138 ssid 
 |-  ( ZZ>= ` ( C + 1 ) ) C_ ( ZZ>= ` ( C + 1 ) )
139 138 orci 
 |-  ( ( ZZ>= ` ( C + 1 ) ) C_ ( ZZ>= ` ( C + 1 ) ) \/ ( ZZ>= ` ( C + 1 ) ) e. Fin )
140 sumz 
 |-  ( ( ( ZZ>= ` ( C + 1 ) ) C_ ( ZZ>= ` ( C + 1 ) ) \/ ( ZZ>= ` ( C + 1 ) ) e. Fin ) -> sum_ k e. ( ZZ>= ` ( C + 1 ) ) 0 = 0 )
141 139 140 ax-mp 
 |-  sum_ k e. ( ZZ>= ` ( C + 1 ) ) 0 = 0
142 137 141 eqtrdi 
 |-  ( ( ph /\ C e. NN0 ) -> sum_ k e. ( ZZ>= ` ( C + 1 ) ) ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) = 0 )
143 142 oveq2d 
 |-  ( ( ph /\ C e. NN0 ) -> ( sum_ k e. ( 0 ... C ) ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) + sum_ k e. ( ZZ>= ` ( C + 1 ) ) ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) ) = ( sum_ k e. ( 0 ... C ) ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) + 0 ) )
144 131 136 143 3eqtrd 
 |-  ( ( ph /\ C e. NN0 ) -> sum_ k e. NN0 ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) = ( sum_ k e. ( 0 ... C ) ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) + 0 ) )
145 39 144 35 3eqtr4rd 
 |-  ( ( ph /\ C e. NN0 ) -> ( ( A + B ) ^c C ) = sum_ k e. NN0 ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) )