Metamath Proof Explorer

Theorem bcxmas

Description: Parallel summation (Christmas Stocking) theorem for Pascal's Triangle. (Contributed by Paul Chapman, 18-May-2007) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Assertion bcxmas 
|- ( ( N e. NN0 /\ M e. NN0 ) -> ( ( ( N + 1 ) + M ) _C M ) = sum_ j e. ( 0 ... M ) ( ( N + j ) _C j ) )

Proof

Step Hyp Ref Expression
1 bcxmaslem1 
 |-  ( m = 0 -> ( ( ( N + 1 ) + m ) _C m ) = ( ( ( N + 1 ) + 0 ) _C 0 ) )
2 oveq2 
 |-  ( m = 0 -> ( 0 ... m ) = ( 0 ... 0 ) )
3 2 sumeq1d 
 |-  ( m = 0 -> sum_ j e. ( 0 ... m ) ( ( N + j ) _C j ) = sum_ j e. ( 0 ... 0 ) ( ( N + j ) _C j ) )
4 1 3 eqeq12d 
 |-  ( m = 0 -> ( ( ( ( N + 1 ) + m ) _C m ) = sum_ j e. ( 0 ... m ) ( ( N + j ) _C j ) <-> ( ( ( N + 1 ) + 0 ) _C 0 ) = sum_ j e. ( 0 ... 0 ) ( ( N + j ) _C j ) ) )
5 bcxmaslem1 
 |-  ( m = k -> ( ( ( N + 1 ) + m ) _C m ) = ( ( ( N + 1 ) + k ) _C k ) )
6 oveq2 
 |-  ( m = k -> ( 0 ... m ) = ( 0 ... k ) )
7 6 sumeq1d 
 |-  ( m = k -> sum_ j e. ( 0 ... m ) ( ( N + j ) _C j ) = sum_ j e. ( 0 ... k ) ( ( N + j ) _C j ) )
8 5 7 eqeq12d 
 |-  ( m = k -> ( ( ( ( N + 1 ) + m ) _C m ) = sum_ j e. ( 0 ... m ) ( ( N + j ) _C j ) <-> ( ( ( N + 1 ) + k ) _C k ) = sum_ j e. ( 0 ... k ) ( ( N + j ) _C j ) ) )
9 bcxmaslem1 
 |-  ( m = ( k + 1 ) -> ( ( ( N + 1 ) + m ) _C m ) = ( ( ( N + 1 ) + ( k + 1 ) ) _C ( k + 1 ) ) )
10 oveq2 
 |-  ( m = ( k + 1 ) -> ( 0 ... m ) = ( 0 ... ( k + 1 ) ) )
11 10 sumeq1d 
 |-  ( m = ( k + 1 ) -> sum_ j e. ( 0 ... m ) ( ( N + j ) _C j ) = sum_ j e. ( 0 ... ( k + 1 ) ) ( ( N + j ) _C j ) )
12 9 11 eqeq12d 
 |-  ( m = ( k + 1 ) -> ( ( ( ( N + 1 ) + m ) _C m ) = sum_ j e. ( 0 ... m ) ( ( N + j ) _C j ) <-> ( ( ( N + 1 ) + ( k + 1 ) ) _C ( k + 1 ) ) = sum_ j e. ( 0 ... ( k + 1 ) ) ( ( N + j ) _C j ) ) )
13 bcxmaslem1 
 |-  ( m = M -> ( ( ( N + 1 ) + m ) _C m ) = ( ( ( N + 1 ) + M ) _C M ) )
14 oveq2 
 |-  ( m = M -> ( 0 ... m ) = ( 0 ... M ) )
15 14 sumeq1d 
 |-  ( m = M -> sum_ j e. ( 0 ... m ) ( ( N + j ) _C j ) = sum_ j e. ( 0 ... M ) ( ( N + j ) _C j ) )
16 13 15 eqeq12d 
 |-  ( m = M -> ( ( ( ( N + 1 ) + m ) _C m ) = sum_ j e. ( 0 ... m ) ( ( N + j ) _C j ) <-> ( ( ( N + 1 ) + M ) _C M ) = sum_ j e. ( 0 ... M ) ( ( N + j ) _C j ) ) )
17 0nn0 
 |-  0 e. NN0
18 nn0addcl 
 |-  ( ( N e. NN0 /\ 0 e. NN0 ) -> ( N + 0 ) e. NN0 )
19 bcn0 
 |-  ( ( N + 0 ) e. NN0 -> ( ( N + 0 ) _C 0 ) = 1 )
20 18 19 syl 
 |-  ( ( N e. NN0 /\ 0 e. NN0 ) -> ( ( N + 0 ) _C 0 ) = 1 )
21 17 20 mpan2 
 |-  ( N e. NN0 -> ( ( N + 0 ) _C 0 ) = 1 )
22 0z 
 |-  0 e. ZZ
23 1nn0 
 |-  1 e. NN0
24 21 23 eqeltrdi 
 |-  ( N e. NN0 -> ( ( N + 0 ) _C 0 ) e. NN0 )
25 24 nn0cnd 
 |-  ( N e. NN0 -> ( ( N + 0 ) _C 0 ) e. CC )
26 bcxmaslem1 
 |-  ( j = 0 -> ( ( N + j ) _C j ) = ( ( N + 0 ) _C 0 ) )
27 26 fsum1 
 |-  ( ( 0 e. ZZ /\ ( ( N + 0 ) _C 0 ) e. CC ) -> sum_ j e. ( 0 ... 0 ) ( ( N + j ) _C j ) = ( ( N + 0 ) _C 0 ) )
28 22 25 27 sylancr 
 |-  ( N e. NN0 -> sum_ j e. ( 0 ... 0 ) ( ( N + j ) _C j ) = ( ( N + 0 ) _C 0 ) )
29 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
30 nn0addcl 
 |-  ( ( ( N + 1 ) e. NN0 /\ 0 e. NN0 ) -> ( ( N + 1 ) + 0 ) e. NN0 )
31 29 17 30 sylancl 
 |-  ( N e. NN0 -> ( ( N + 1 ) + 0 ) e. NN0 )
32 bcn0 
 |-  ( ( ( N + 1 ) + 0 ) e. NN0 -> ( ( ( N + 1 ) + 0 ) _C 0 ) = 1 )
33 31 32 syl 
 |-  ( N e. NN0 -> ( ( ( N + 1 ) + 0 ) _C 0 ) = 1 )
34 21 28 33 3eqtr4rd 
 |-  ( N e. NN0 -> ( ( ( N + 1 ) + 0 ) _C 0 ) = sum_ j e. ( 0 ... 0 ) ( ( N + j ) _C j ) )
35 elnn0uz 
 |-  ( k e. NN0 <-> k e. ( ZZ>= ` 0 ) )
36 35 bilani 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> k e. ( ZZ>= ` 0 ) )
37 simpl 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> N e. NN0 )
38 elfznn0 
 |-  ( j e. ( 0 ... ( k + 1 ) ) -> j e. NN0 )
39 nn0addcl 
 |-  ( ( N e. NN0 /\ j e. NN0 ) -> ( N + j ) e. NN0 )
40 37 38 39 syl2an 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ j e. ( 0 ... ( k + 1 ) ) ) -> ( N + j ) e. NN0 )
41 elfzelz 
 |-  ( j e. ( 0 ... ( k + 1 ) ) -> j e. ZZ )
42 41 adantl 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ j e. ( 0 ... ( k + 1 ) ) ) -> j e. ZZ )
43 bccl 
 |-  ( ( ( N + j ) e. NN0 /\ j e. ZZ ) -> ( ( N + j ) _C j ) e. NN0 )
44 40 42 43 syl2anc 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ j e. ( 0 ... ( k + 1 ) ) ) -> ( ( N + j ) _C j ) e. NN0 )
45 44 nn0cnd 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ j e. ( 0 ... ( k + 1 ) ) ) -> ( ( N + j ) _C j ) e. CC )
46 bcxmaslem1 
 |-  ( j = ( k + 1 ) -> ( ( N + j ) _C j ) = ( ( N + ( k + 1 ) ) _C ( k + 1 ) ) )
47 36 45 46 fsump1 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> sum_ j e. ( 0 ... ( k + 1 ) ) ( ( N + j ) _C j ) = ( sum_ j e. ( 0 ... k ) ( ( N + j ) _C j ) + ( ( N + ( k + 1 ) ) _C ( k + 1 ) ) ) )
48 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
49 48 adantr 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> N e. CC )
50 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
51 50 adantl 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> k e. CC )
52 1cnd 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> 1 e. CC )
53 add32r 
 |-  ( ( N e. CC /\ k e. CC /\ 1 e. CC ) -> ( N + ( k + 1 ) ) = ( ( N + 1 ) + k ) )
54 49 51 52 53 syl3anc 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( N + ( k + 1 ) ) = ( ( N + 1 ) + k ) )
55 54 oveq1d 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( N + ( k + 1 ) ) _C ( k + 1 ) ) = ( ( ( N + 1 ) + k ) _C ( k + 1 ) ) )
56 55 oveq2d 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( sum_ j e. ( 0 ... k ) ( ( N + j ) _C j ) + ( ( N + ( k + 1 ) ) _C ( k + 1 ) ) ) = ( sum_ j e. ( 0 ... k ) ( ( N + j ) _C j ) + ( ( ( N + 1 ) + k ) _C ( k + 1 ) ) ) )
57 47 56 eqtrd 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> sum_ j e. ( 0 ... ( k + 1 ) ) ( ( N + j ) _C j ) = ( sum_ j e. ( 0 ... k ) ( ( N + j ) _C j ) + ( ( ( N + 1 ) + k ) _C ( k + 1 ) ) ) )
58 57 adantr 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ ( ( ( N + 1 ) + k ) _C k ) = sum_ j e. ( 0 ... k ) ( ( N + j ) _C j ) ) -> sum_ j e. ( 0 ... ( k + 1 ) ) ( ( N + j ) _C j ) = ( sum_ j e. ( 0 ... k ) ( ( N + j ) _C j ) + ( ( ( N + 1 ) + k ) _C ( k + 1 ) ) ) )
59 oveq1 
 |-  ( ( ( ( N + 1 ) + k ) _C k ) = sum_ j e. ( 0 ... k ) ( ( N + j ) _C j ) -> ( ( ( ( N + 1 ) + k ) _C k ) + ( ( ( N + 1 ) + k ) _C ( k + 1 ) ) ) = ( sum_ j e. ( 0 ... k ) ( ( N + j ) _C j ) + ( ( ( N + 1 ) + k ) _C ( k + 1 ) ) ) )
60 59 adantl 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ ( ( ( N + 1 ) + k ) _C k ) = sum_ j e. ( 0 ... k ) ( ( N + j ) _C j ) ) -> ( ( ( ( N + 1 ) + k ) _C k ) + ( ( ( N + 1 ) + k ) _C ( k + 1 ) ) ) = ( sum_ j e. ( 0 ... k ) ( ( N + j ) _C j ) + ( ( ( N + 1 ) + k ) _C ( k + 1 ) ) ) )
61 ax-1cn 
 |-  1 e. CC
62 pncan 
 |-  ( ( k e. CC /\ 1 e. CC ) -> ( ( k + 1 ) - 1 ) = k )
63 51 61 62 sylancl 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( k + 1 ) - 1 ) = k )
64 63 oveq2d 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ( N + 1 ) + k ) _C ( ( k + 1 ) - 1 ) ) = ( ( ( N + 1 ) + k ) _C k ) )
65 64 oveq2d 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ( ( N + 1 ) + k ) _C ( k + 1 ) ) + ( ( ( N + 1 ) + k ) _C ( ( k + 1 ) - 1 ) ) ) = ( ( ( ( N + 1 ) + k ) _C ( k + 1 ) ) + ( ( ( N + 1 ) + k ) _C k ) ) )
66 nn0addcl 
 |-  ( ( ( N + 1 ) e. NN0 /\ k e. NN0 ) -> ( ( N + 1 ) + k ) e. NN0 )
67 29 66 sylan 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( N + 1 ) + k ) e. NN0 )
68 nn0p1nn 
 |-  ( k e. NN0 -> ( k + 1 ) e. NN )
69 68 adantl 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( k + 1 ) e. NN )
70 69 nnzd 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( k + 1 ) e. ZZ )
71 bcpasc 
 |-  ( ( ( ( N + 1 ) + k ) e. NN0 /\ ( k + 1 ) e. ZZ ) -> ( ( ( ( N + 1 ) + k ) _C ( k + 1 ) ) + ( ( ( N + 1 ) + k ) _C ( ( k + 1 ) - 1 ) ) ) = ( ( ( ( N + 1 ) + k ) + 1 ) _C ( k + 1 ) ) )
72 67 70 71 syl2anc 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ( ( N + 1 ) + k ) _C ( k + 1 ) ) + ( ( ( N + 1 ) + k ) _C ( ( k + 1 ) - 1 ) ) ) = ( ( ( ( N + 1 ) + k ) + 1 ) _C ( k + 1 ) ) )
73 65 72 eqtr3d 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ( ( N + 1 ) + k ) _C ( k + 1 ) ) + ( ( ( N + 1 ) + k ) _C k ) ) = ( ( ( ( N + 1 ) + k ) + 1 ) _C ( k + 1 ) ) )
74 nn0p1nn 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN )
75 nnnn0addcl 
 |-  ( ( ( N + 1 ) e. NN /\ k e. NN0 ) -> ( ( N + 1 ) + k ) e. NN )
76 74 75 sylan 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( N + 1 ) + k ) e. NN )
77 76 nnnn0d 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( N + 1 ) + k ) e. NN0 )
78 bccl 
 |-  ( ( ( ( N + 1 ) + k ) e. NN0 /\ ( k + 1 ) e. ZZ ) -> ( ( ( N + 1 ) + k ) _C ( k + 1 ) ) e. NN0 )
79 77 70 78 syl2anc 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ( N + 1 ) + k ) _C ( k + 1 ) ) e. NN0 )
80 79 nn0cnd 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ( N + 1 ) + k ) _C ( k + 1 ) ) e. CC )
81 nn0z 
 |-  ( k e. NN0 -> k e. ZZ )
82 81 adantl 
 |-  ( ( ( N + 1 ) e. NN0 /\ k e. NN0 ) -> k e. ZZ )
83 bccl 
 |-  ( ( ( ( N + 1 ) + k ) e. NN0 /\ k e. ZZ ) -> ( ( ( N + 1 ) + k ) _C k ) e. NN0 )
84 66 82 83 syl2anc 
 |-  ( ( ( N + 1 ) e. NN0 /\ k e. NN0 ) -> ( ( ( N + 1 ) + k ) _C k ) e. NN0 )
85 29 84 sylan 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ( N + 1 ) + k ) _C k ) e. NN0 )
86 85 nn0cnd 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ( N + 1 ) + k ) _C k ) e. CC )
87 80 86 addcomd 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ( ( N + 1 ) + k ) _C ( k + 1 ) ) + ( ( ( N + 1 ) + k ) _C k ) ) = ( ( ( ( N + 1 ) + k ) _C k ) + ( ( ( N + 1 ) + k ) _C ( k + 1 ) ) ) )
88 peano2cn 
 |-  ( N e. CC -> ( N + 1 ) e. CC )
89 48 88 syl 
 |-  ( N e. NN0 -> ( N + 1 ) e. CC )
90 89 adantr 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( N + 1 ) e. CC )
91 90 51 52 addassd 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ( N + 1 ) + k ) + 1 ) = ( ( N + 1 ) + ( k + 1 ) ) )
92 91 oveq1d 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ( ( N + 1 ) + k ) + 1 ) _C ( k + 1 ) ) = ( ( ( N + 1 ) + ( k + 1 ) ) _C ( k + 1 ) ) )
93 73 87 92 3eqtr3d 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ( ( N + 1 ) + k ) _C k ) + ( ( ( N + 1 ) + k ) _C ( k + 1 ) ) ) = ( ( ( N + 1 ) + ( k + 1 ) ) _C ( k + 1 ) ) )
94 93 adantr 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ ( ( ( N + 1 ) + k ) _C k ) = sum_ j e. ( 0 ... k ) ( ( N + j ) _C j ) ) -> ( ( ( ( N + 1 ) + k ) _C k ) + ( ( ( N + 1 ) + k ) _C ( k + 1 ) ) ) = ( ( ( N + 1 ) + ( k + 1 ) ) _C ( k + 1 ) ) )
95 58 60 94 3eqtr2rd 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ ( ( ( N + 1 ) + k ) _C k ) = sum_ j e. ( 0 ... k ) ( ( N + j ) _C j ) ) -> ( ( ( N + 1 ) + ( k + 1 ) ) _C ( k + 1 ) ) = sum_ j e. ( 0 ... ( k + 1 ) ) ( ( N + j ) _C j ) )
96 4 8 12 16 34 95 nn0indd 
 |-  ( ( N e. NN0 /\ M e. NN0 ) -> ( ( ( N + 1 ) + M ) _C M ) = sum_ j e. ( 0 ... M ) ( ( N + j ) _C j ) )