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

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 simpr 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> k e. NN0 )
36 elnn0uz 
 |-  ( k e. NN0 <-> k e. ( ZZ>= ` 0 ) )
37 35 36 sylib 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> k e. ( ZZ>= ` 0 ) )
38 simpl 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> N e. NN0 )
39 elfznn0 
 |-  ( j e. ( 0 ... ( k + 1 ) ) -> j e. NN0 )
40 nn0addcl 
 |-  ( ( N e. NN0 /\ j e. NN0 ) -> ( N + j ) e. NN0 )
41 38 39 40 syl2an 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ j e. ( 0 ... ( k + 1 ) ) ) -> ( N + j ) e. NN0 )
42 elfzelz 
 |-  ( j e. ( 0 ... ( k + 1 ) ) -> j e. ZZ )
43 42 adantl 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ j e. ( 0 ... ( k + 1 ) ) ) -> j e. ZZ )
44 bccl 
 |-  ( ( ( N + j ) e. NN0 /\ j e. ZZ ) -> ( ( N + j ) _C j ) e. NN0 )
45 41 43 44 syl2anc 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ j e. ( 0 ... ( k + 1 ) ) ) -> ( ( N + j ) _C j ) e. NN0 )
46 45 nn0cnd 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ j e. ( 0 ... ( k + 1 ) ) ) -> ( ( N + j ) _C j ) e. CC )
47 bcxmaslem1 
 |-  ( j = ( k + 1 ) -> ( ( N + j ) _C j ) = ( ( N + ( k + 1 ) ) _C ( k + 1 ) ) )
48 37 46 47 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 ) ) ) )
49 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
50 49 adantr 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> N e. CC )
51 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
52 51 adantl 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> k e. CC )
53 1cnd 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> 1 e. CC )
54 add32r 
 |-  ( ( N e. CC /\ k e. CC /\ 1 e. CC ) -> ( N + ( k + 1 ) ) = ( ( N + 1 ) + k ) )
55 50 52 53 54 syl3anc 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( N + ( k + 1 ) ) = ( ( N + 1 ) + k ) )
56 55 oveq1d 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( N + ( k + 1 ) ) _C ( k + 1 ) ) = ( ( ( N + 1 ) + k ) _C ( k + 1 ) ) )
57 56 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 ) ) ) )
58 48 57 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 ) ) ) )
59 58 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 ) ) ) )
60 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 ) ) ) )
61 60 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 ) ) ) )
62 ax-1cn 
 |-  1 e. CC
63 pncan 
 |-  ( ( k e. CC /\ 1 e. CC ) -> ( ( k + 1 ) - 1 ) = k )
64 52 62 63 sylancl 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( k + 1 ) - 1 ) = k )
65 64 oveq2d 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ( N + 1 ) + k ) _C ( ( k + 1 ) - 1 ) ) = ( ( ( N + 1 ) + k ) _C k ) )
66 65 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 ) ) )
67 nn0addcl 
 |-  ( ( ( N + 1 ) e. NN0 /\ k e. NN0 ) -> ( ( N + 1 ) + k ) e. NN0 )
68 29 67 sylan 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( N + 1 ) + k ) e. NN0 )
69 nn0p1nn 
 |-  ( k e. NN0 -> ( k + 1 ) e. NN )
70 69 adantl 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( k + 1 ) e. NN )
71 70 nnzd 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( k + 1 ) e. ZZ )
72 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 ) ) )
73 68 71 72 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 ) ) )
74 66 73 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 ) ) )
75 nn0p1nn 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN )
76 nnnn0addcl 
 |-  ( ( ( N + 1 ) e. NN /\ k e. NN0 ) -> ( ( N + 1 ) + k ) e. NN )
77 75 76 sylan 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( N + 1 ) + k ) e. NN )
78 77 nnnn0d 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( N + 1 ) + k ) e. NN0 )
79 bccl 
 |-  ( ( ( ( N + 1 ) + k ) e. NN0 /\ ( k + 1 ) e. ZZ ) -> ( ( ( N + 1 ) + k ) _C ( k + 1 ) ) e. NN0 )
80 78 71 79 syl2anc 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ( N + 1 ) + k ) _C ( k + 1 ) ) e. NN0 )
81 80 nn0cnd 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ( N + 1 ) + k ) _C ( k + 1 ) ) e. CC )
82 nn0z 
 |-  ( k e. NN0 -> k e. ZZ )
83 82 adantl 
 |-  ( ( ( N + 1 ) e. NN0 /\ k e. NN0 ) -> k e. ZZ )
84 bccl 
 |-  ( ( ( ( N + 1 ) + k ) e. NN0 /\ k e. ZZ ) -> ( ( ( N + 1 ) + k ) _C k ) e. NN0 )
85 67 83 84 syl2anc 
 |-  ( ( ( N + 1 ) e. NN0 /\ k e. NN0 ) -> ( ( ( N + 1 ) + k ) _C k ) e. NN0 )
86 29 85 sylan 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ( N + 1 ) + k ) _C k ) e. NN0 )
87 86 nn0cnd 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ( N + 1 ) + k ) _C k ) e. CC )
88 81 87 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 ) ) ) )
89 peano2cn 
 |-  ( N e. CC -> ( N + 1 ) e. CC )
90 49 89 syl 
 |-  ( N e. NN0 -> ( N + 1 ) e. CC )
91 90 adantr 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( N + 1 ) e. CC )
92 91 52 53 addassd 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ( N + 1 ) + k ) + 1 ) = ( ( N + 1 ) + ( k + 1 ) ) )
93 92 oveq1d 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ( ( N + 1 ) + k ) + 1 ) _C ( k + 1 ) ) = ( ( ( N + 1 ) + ( k + 1 ) ) _C ( k + 1 ) ) )
94 74 88 93 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 ) ) )
95 94 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 ) ) )
96 59 61 95 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 ) )
97 4 8 12 16 34 96 nn0indd 
 |-  ( ( N e. NN0 /\ M e. NN0 ) -> ( ( ( N + 1 ) + M ) _C M ) = sum_ j e. ( 0 ... M ) ( ( N + j ) _C j ) )