Metamath Proof Explorer

Theorem bccolsum

Description: A column-sum rule for binomial coefficients. (Contributed by Scott Fenton, 24-Jun-2020)

Ref Expression
Assertion bccolsum 
|- ( ( N e. NN0 /\ C e. NN0 ) -> sum_ k e. ( 0 ... N ) ( k _C C ) = ( ( N + 1 ) _C ( C + 1 ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( m = 0 -> ( 0 ... m ) = ( 0 ... 0 ) )
2 1 sumeq1d 
 |-  ( m = 0 -> sum_ k e. ( 0 ... m ) ( k _C C ) = sum_ k e. ( 0 ... 0 ) ( k _C C ) )
3 oveq1 
 |-  ( m = 0 -> ( m + 1 ) = ( 0 + 1 ) )
4 0p1e1 
 |-  ( 0 + 1 ) = 1
5 3 4 eqtrdi 
 |-  ( m = 0 -> ( m + 1 ) = 1 )
6 5 oveq1d 
 |-  ( m = 0 -> ( ( m + 1 ) _C ( C + 1 ) ) = ( 1 _C ( C + 1 ) ) )
7 2 6 eqeq12d 
 |-  ( m = 0 -> ( sum_ k e. ( 0 ... m ) ( k _C C ) = ( ( m + 1 ) _C ( C + 1 ) ) <-> sum_ k e. ( 0 ... 0 ) ( k _C C ) = ( 1 _C ( C + 1 ) ) ) )
8 7 imbi2d 
 |-  ( m = 0 -> ( ( C e. NN0 -> sum_ k e. ( 0 ... m ) ( k _C C ) = ( ( m + 1 ) _C ( C + 1 ) ) ) <-> ( C e. NN0 -> sum_ k e. ( 0 ... 0 ) ( k _C C ) = ( 1 _C ( C + 1 ) ) ) ) )
9 oveq2 
 |-  ( m = n -> ( 0 ... m ) = ( 0 ... n ) )
10 9 sumeq1d 
 |-  ( m = n -> sum_ k e. ( 0 ... m ) ( k _C C ) = sum_ k e. ( 0 ... n ) ( k _C C ) )
11 oveq1 
 |-  ( m = n -> ( m + 1 ) = ( n + 1 ) )
12 11 oveq1d 
 |-  ( m = n -> ( ( m + 1 ) _C ( C + 1 ) ) = ( ( n + 1 ) _C ( C + 1 ) ) )
13 10 12 eqeq12d 
 |-  ( m = n -> ( sum_ k e. ( 0 ... m ) ( k _C C ) = ( ( m + 1 ) _C ( C + 1 ) ) <-> sum_ k e. ( 0 ... n ) ( k _C C ) = ( ( n + 1 ) _C ( C + 1 ) ) ) )
14 13 imbi2d 
 |-  ( m = n -> ( ( C e. NN0 -> sum_ k e. ( 0 ... m ) ( k _C C ) = ( ( m + 1 ) _C ( C + 1 ) ) ) <-> ( C e. NN0 -> sum_ k e. ( 0 ... n ) ( k _C C ) = ( ( n + 1 ) _C ( C + 1 ) ) ) ) )
15 oveq2 
 |-  ( m = ( n + 1 ) -> ( 0 ... m ) = ( 0 ... ( n + 1 ) ) )
16 15 sumeq1d 
 |-  ( m = ( n + 1 ) -> sum_ k e. ( 0 ... m ) ( k _C C ) = sum_ k e. ( 0 ... ( n + 1 ) ) ( k _C C ) )
17 oveq1 
 |-  ( m = ( n + 1 ) -> ( m + 1 ) = ( ( n + 1 ) + 1 ) )
18 17 oveq1d 
 |-  ( m = ( n + 1 ) -> ( ( m + 1 ) _C ( C + 1 ) ) = ( ( ( n + 1 ) + 1 ) _C ( C + 1 ) ) )
19 16 18 eqeq12d 
 |-  ( m = ( n + 1 ) -> ( sum_ k e. ( 0 ... m ) ( k _C C ) = ( ( m + 1 ) _C ( C + 1 ) ) <-> sum_ k e. ( 0 ... ( n + 1 ) ) ( k _C C ) = ( ( ( n + 1 ) + 1 ) _C ( C + 1 ) ) ) )
20 19 imbi2d 
 |-  ( m = ( n + 1 ) -> ( ( C e. NN0 -> sum_ k e. ( 0 ... m ) ( k _C C ) = ( ( m + 1 ) _C ( C + 1 ) ) ) <-> ( C e. NN0 -> sum_ k e. ( 0 ... ( n + 1 ) ) ( k _C C ) = ( ( ( n + 1 ) + 1 ) _C ( C + 1 ) ) ) ) )
21 oveq2 
 |-  ( m = N -> ( 0 ... m ) = ( 0 ... N ) )
22 21 sumeq1d 
 |-  ( m = N -> sum_ k e. ( 0 ... m ) ( k _C C ) = sum_ k e. ( 0 ... N ) ( k _C C ) )
23 oveq1 
 |-  ( m = N -> ( m + 1 ) = ( N + 1 ) )
24 23 oveq1d 
 |-  ( m = N -> ( ( m + 1 ) _C ( C + 1 ) ) = ( ( N + 1 ) _C ( C + 1 ) ) )
25 22 24 eqeq12d 
 |-  ( m = N -> ( sum_ k e. ( 0 ... m ) ( k _C C ) = ( ( m + 1 ) _C ( C + 1 ) ) <-> sum_ k e. ( 0 ... N ) ( k _C C ) = ( ( N + 1 ) _C ( C + 1 ) ) ) )
26 25 imbi2d 
 |-  ( m = N -> ( ( C e. NN0 -> sum_ k e. ( 0 ... m ) ( k _C C ) = ( ( m + 1 ) _C ( C + 1 ) ) ) <-> ( C e. NN0 -> sum_ k e. ( 0 ... N ) ( k _C C ) = ( ( N + 1 ) _C ( C + 1 ) ) ) ) )
27 0z 
 |-  0 e. ZZ
28 0nn0 
 |-  0 e. NN0
29 nn0z 
 |-  ( C e. NN0 -> C e. ZZ )
30 bccl 
 |-  ( ( 0 e. NN0 /\ C e. ZZ ) -> ( 0 _C C ) e. NN0 )
31 28 29 30 sylancr 
 |-  ( C e. NN0 -> ( 0 _C C ) e. NN0 )
32 31 nn0cnd 
 |-  ( C e. NN0 -> ( 0 _C C ) e. CC )
33 oveq1 
 |-  ( k = 0 -> ( k _C C ) = ( 0 _C C ) )
34 33 fsum1 
 |-  ( ( 0 e. ZZ /\ ( 0 _C C ) e. CC ) -> sum_ k e. ( 0 ... 0 ) ( k _C C ) = ( 0 _C C ) )
35 27 32 34 sylancr 
 |-  ( C e. NN0 -> sum_ k e. ( 0 ... 0 ) ( k _C C ) = ( 0 _C C ) )
36 elnn0 
 |-  ( C e. NN0 <-> ( C e. NN \/ C = 0 ) )
37 1red 
 |-  ( C e. NN -> 1 e. RR )
38 nnrp 
 |-  ( C e. NN -> C e. RR+ )
39 37 38 ltaddrp2d 
 |-  ( C e. NN -> 1 < ( C + 1 ) )
40 peano2nn 
 |-  ( C e. NN -> ( C + 1 ) e. NN )
41 40 nnred 
 |-  ( C e. NN -> ( C + 1 ) e. RR )
42 37 41 ltnled 
 |-  ( C e. NN -> ( 1 < ( C + 1 ) <-> -. ( C + 1 ) <_ 1 ) )
43 39 42 mpbid 
 |-  ( C e. NN -> -. ( C + 1 ) <_ 1 )
44 elfzle2 
 |-  ( ( C + 1 ) e. ( 0 ... 1 ) -> ( C + 1 ) <_ 1 )
45 43 44 nsyl 
 |-  ( C e. NN -> -. ( C + 1 ) e. ( 0 ... 1 ) )
46 45 iffalsed 
 |-  ( C e. NN -> if ( ( C + 1 ) e. ( 0 ... 1 ) , ( ( ! ` 1 ) / ( ( ! ` ( 1 - ( C + 1 ) ) ) x. ( ! ` ( C + 1 ) ) ) ) , 0 ) = 0 )
47 1nn0 
 |-  1 e. NN0
48 40 nnzd 
 |-  ( C e. NN -> ( C + 1 ) e. ZZ )
49 bcval 
 |-  ( ( 1 e. NN0 /\ ( C + 1 ) e. ZZ ) -> ( 1 _C ( C + 1 ) ) = if ( ( C + 1 ) e. ( 0 ... 1 ) , ( ( ! ` 1 ) / ( ( ! ` ( 1 - ( C + 1 ) ) ) x. ( ! ` ( C + 1 ) ) ) ) , 0 ) )
50 47 48 49 sylancr 
 |-  ( C e. NN -> ( 1 _C ( C + 1 ) ) = if ( ( C + 1 ) e. ( 0 ... 1 ) , ( ( ! ` 1 ) / ( ( ! ` ( 1 - ( C + 1 ) ) ) x. ( ! ` ( C + 1 ) ) ) ) , 0 ) )
51 bc0k 
 |-  ( C e. NN -> ( 0 _C C ) = 0 )
52 46 50 51 3eqtr4rd 
 |-  ( C e. NN -> ( 0 _C C ) = ( 1 _C ( C + 1 ) ) )
53 bcnn 
 |-  ( 0 e. NN0 -> ( 0 _C 0 ) = 1 )
54 28 53 ax-mp 
 |-  ( 0 _C 0 ) = 1
55 bcnn 
 |-  ( 1 e. NN0 -> ( 1 _C 1 ) = 1 )
56 47 55 ax-mp 
 |-  ( 1 _C 1 ) = 1
57 54 56 eqtr4i 
 |-  ( 0 _C 0 ) = ( 1 _C 1 )
58 oveq2 
 |-  ( C = 0 -> ( 0 _C C ) = ( 0 _C 0 ) )
59 oveq1 
 |-  ( C = 0 -> ( C + 1 ) = ( 0 + 1 ) )
60 59 4 eqtrdi 
 |-  ( C = 0 -> ( C + 1 ) = 1 )
61 60 oveq2d 
 |-  ( C = 0 -> ( 1 _C ( C + 1 ) ) = ( 1 _C 1 ) )
62 57 58 61 3eqtr4a 
 |-  ( C = 0 -> ( 0 _C C ) = ( 1 _C ( C + 1 ) ) )
63 52 62 jaoi 
 |-  ( ( C e. NN \/ C = 0 ) -> ( 0 _C C ) = ( 1 _C ( C + 1 ) ) )
64 36 63 sylbi 
 |-  ( C e. NN0 -> ( 0 _C C ) = ( 1 _C ( C + 1 ) ) )
65 35 64 eqtrd 
 |-  ( C e. NN0 -> sum_ k e. ( 0 ... 0 ) ( k _C C ) = ( 1 _C ( C + 1 ) ) )
66 elnn0uz 
 |-  ( n e. NN0 <-> n e. ( ZZ>= ` 0 ) )
67 66 birani 
 |-  ( ( n e. NN0 /\ C e. NN0 ) -> n e. ( ZZ>= ` 0 ) )
68 elfznn0 
 |-  ( k e. ( 0 ... ( n + 1 ) ) -> k e. NN0 )
69 68 adantl 
 |-  ( ( ( n e. NN0 /\ C e. NN0 ) /\ k e. ( 0 ... ( n + 1 ) ) ) -> k e. NN0 )
70 simplr 
 |-  ( ( ( n e. NN0 /\ C e. NN0 ) /\ k e. ( 0 ... ( n + 1 ) ) ) -> C e. NN0 )
71 70 nn0zd 
 |-  ( ( ( n e. NN0 /\ C e. NN0 ) /\ k e. ( 0 ... ( n + 1 ) ) ) -> C e. ZZ )
72 bccl 
 |-  ( ( k e. NN0 /\ C e. ZZ ) -> ( k _C C ) e. NN0 )
73 69 71 72 syl2anc 
 |-  ( ( ( n e. NN0 /\ C e. NN0 ) /\ k e. ( 0 ... ( n + 1 ) ) ) -> ( k _C C ) e. NN0 )
74 73 nn0cnd 
 |-  ( ( ( n e. NN0 /\ C e. NN0 ) /\ k e. ( 0 ... ( n + 1 ) ) ) -> ( k _C C ) e. CC )
75 oveq1 
 |-  ( k = ( n + 1 ) -> ( k _C C ) = ( ( n + 1 ) _C C ) )
76 67 74 75 fsump1 
 |-  ( ( n e. NN0 /\ C e. NN0 ) -> sum_ k e. ( 0 ... ( n + 1 ) ) ( k _C C ) = ( sum_ k e. ( 0 ... n ) ( k _C C ) + ( ( n + 1 ) _C C ) ) )
77 76 adantr 
 |-  ( ( ( n e. NN0 /\ C e. NN0 ) /\ sum_ k e. ( 0 ... n ) ( k _C C ) = ( ( n + 1 ) _C ( C + 1 ) ) ) -> sum_ k e. ( 0 ... ( n + 1 ) ) ( k _C C ) = ( sum_ k e. ( 0 ... n ) ( k _C C ) + ( ( n + 1 ) _C C ) ) )
78 id 
 |-  ( sum_ k e. ( 0 ... n ) ( k _C C ) = ( ( n + 1 ) _C ( C + 1 ) ) -> sum_ k e. ( 0 ... n ) ( k _C C ) = ( ( n + 1 ) _C ( C + 1 ) ) )
79 nn0cn 
 |-  ( C e. NN0 -> C e. CC )
80 79 adantl 
 |-  ( ( n e. NN0 /\ C e. NN0 ) -> C e. CC )
81 1cnd 
 |-  ( ( n e. NN0 /\ C e. NN0 ) -> 1 e. CC )
82 80 81 pncand 
 |-  ( ( n e. NN0 /\ C e. NN0 ) -> ( ( C + 1 ) - 1 ) = C )
83 82 oveq2d 
 |-  ( ( n e. NN0 /\ C e. NN0 ) -> ( ( n + 1 ) _C ( ( C + 1 ) - 1 ) ) = ( ( n + 1 ) _C C ) )
84 83 eqcomd 
 |-  ( ( n e. NN0 /\ C e. NN0 ) -> ( ( n + 1 ) _C C ) = ( ( n + 1 ) _C ( ( C + 1 ) - 1 ) ) )
85 78 84 oveqan12rd 
 |-  ( ( ( n e. NN0 /\ C e. NN0 ) /\ sum_ k e. ( 0 ... n ) ( k _C C ) = ( ( n + 1 ) _C ( C + 1 ) ) ) -> ( sum_ k e. ( 0 ... n ) ( k _C C ) + ( ( n + 1 ) _C C ) ) = ( ( ( n + 1 ) _C ( C + 1 ) ) + ( ( n + 1 ) _C ( ( C + 1 ) - 1 ) ) ) )
86 peano2nn0 
 |-  ( n e. NN0 -> ( n + 1 ) e. NN0 )
87 peano2nn0 
 |-  ( C e. NN0 -> ( C + 1 ) e. NN0 )
88 87 nn0zd 
 |-  ( C e. NN0 -> ( C + 1 ) e. ZZ )
89 bcpasc 
 |-  ( ( ( n + 1 ) e. NN0 /\ ( C + 1 ) e. ZZ ) -> ( ( ( n + 1 ) _C ( C + 1 ) ) + ( ( n + 1 ) _C ( ( C + 1 ) - 1 ) ) ) = ( ( ( n + 1 ) + 1 ) _C ( C + 1 ) ) )
90 86 88 89 syl2an 
 |-  ( ( n e. NN0 /\ C e. NN0 ) -> ( ( ( n + 1 ) _C ( C + 1 ) ) + ( ( n + 1 ) _C ( ( C + 1 ) - 1 ) ) ) = ( ( ( n + 1 ) + 1 ) _C ( C + 1 ) ) )
91 90 adantr 
 |-  ( ( ( n e. NN0 /\ C e. NN0 ) /\ sum_ k e. ( 0 ... n ) ( k _C C ) = ( ( n + 1 ) _C ( C + 1 ) ) ) -> ( ( ( n + 1 ) _C ( C + 1 ) ) + ( ( n + 1 ) _C ( ( C + 1 ) - 1 ) ) ) = ( ( ( n + 1 ) + 1 ) _C ( C + 1 ) ) )
92 77 85 91 3eqtrd 
 |-  ( ( ( n e. NN0 /\ C e. NN0 ) /\ sum_ k e. ( 0 ... n ) ( k _C C ) = ( ( n + 1 ) _C ( C + 1 ) ) ) -> sum_ k e. ( 0 ... ( n + 1 ) ) ( k _C C ) = ( ( ( n + 1 ) + 1 ) _C ( C + 1 ) ) )
93 92 exp31 
 |-  ( n e. NN0 -> ( C e. NN0 -> ( sum_ k e. ( 0 ... n ) ( k _C C ) = ( ( n + 1 ) _C ( C + 1 ) ) -> sum_ k e. ( 0 ... ( n + 1 ) ) ( k _C C ) = ( ( ( n + 1 ) + 1 ) _C ( C + 1 ) ) ) ) )
94 93 a2d 
 |-  ( n e. NN0 -> ( ( C e. NN0 -> sum_ k e. ( 0 ... n ) ( k _C C ) = ( ( n + 1 ) _C ( C + 1 ) ) ) -> ( C e. NN0 -> sum_ k e. ( 0 ... ( n + 1 ) ) ( k _C C ) = ( ( ( n + 1 ) + 1 ) _C ( C + 1 ) ) ) ) )
95 8 14 20 26 65 94 nn0ind 
 |-  ( N e. NN0 -> ( C e. NN0 -> sum_ k e. ( 0 ... N ) ( k _C C ) = ( ( N + 1 ) _C ( C + 1 ) ) ) )
96 95 imp 
 |-  ( ( N e. NN0 /\ C e. NN0 ) -> sum_ k e. ( 0 ... N ) ( k _C C ) = ( ( N + 1 ) _C ( C + 1 ) ) )