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 N0M0(N+1+MM)=j=0M(N+jj)

Proof

Step Hyp Ref Expression
1 bcxmaslem1 m=0(N+1+mm)=(N+1+00)
2 oveq2 m=00m=00
3 2 sumeq1d m=0j=0m(N+jj)=j=00(N+jj)
4 1 3 eqeq12d m=0(N+1+mm)=j=0m(N+jj)(N+1+00)=j=00(N+jj)
5 bcxmaslem1 m=k(N+1+mm)=(N+1+kk)
6 oveq2 m=k0m=0k
7 6 sumeq1d m=kj=0m(N+jj)=j=0k(N+jj)
8 5 7 eqeq12d m=k(N+1+mm)=j=0m(N+jj)(N+1+kk)=j=0k(N+jj)
9 bcxmaslem1 m=k+1(N+1+mm)=(N+1+k+1k+1)
10 oveq2 m=k+10m=0k+1
11 10 sumeq1d m=k+1j=0m(N+jj)=j=0k+1(N+jj)
12 9 11 eqeq12d m=k+1(N+1+mm)=j=0m(N+jj)(N+1+k+1k+1)=j=0k+1(N+jj)
13 bcxmaslem1 m=M(N+1+mm)=(N+1+MM)
14 oveq2 m=M0m=0M
15 14 sumeq1d m=Mj=0m(N+jj)=j=0M(N+jj)
16 13 15 eqeq12d m=M(N+1+mm)=j=0m(N+jj)(N+1+MM)=j=0M(N+jj)
17 0nn0 00
18 nn0addcl N000N+00
19 bcn0 N+00(N+00)=1
20 18 19 syl N000(N+00)=1
21 17 20 mpan2 N0(N+00)=1
22 0z 0
23 1nn0 10
24 21 23 eqeltrdi N0(N+00)0
25 24 nn0cnd N0(N+00)
26 bcxmaslem1 j=0(N+jj)=(N+00)
27 26 fsum1 0(N+00)j=00(N+jj)=(N+00)
28 22 25 27 sylancr N0j=00(N+jj)=(N+00)
29 peano2nn0 N0N+10
30 nn0addcl N+1000N+1+00
31 29 17 30 sylancl N0N+1+00
32 bcn0 N+1+00(N+1+00)=1
33 31 32 syl N0(N+1+00)=1
34 21 28 33 3eqtr4rd N0(N+1+00)=j=00(N+jj)
35 simpr N0k0k0
36 elnn0uz k0k0
37 35 36 sylib N0k0k0
38 simpl N0k0N0
39 elfznn0 j0k+1j0
40 nn0addcl N0j0N+j0
41 38 39 40 syl2an N0k0j0k+1N+j0
42 elfzelz j0k+1j
43 42 adantl N0k0j0k+1j
44 bccl N+j0j(N+jj)0
45 41 43 44 syl2anc N0k0j0k+1(N+jj)0
46 45 nn0cnd N0k0j0k+1(N+jj)
47 bcxmaslem1 j=k+1(N+jj)=(N+k+1k+1)
48 37 46 47 fsump1 N0k0j=0k+1(N+jj)=j=0k(N+jj)+(N+k+1k+1)
49 nn0cn N0N
50 49 adantr N0k0N
51 nn0cn k0k
52 51 adantl N0k0k
53 1cnd N0k01
54 add32r Nk1N+k+1=N+1+k
55 50 52 53 54 syl3anc N0k0N+k+1=N+1+k
56 55 oveq1d N0k0(N+k+1k+1)=(N+1+kk+1)
57 56 oveq2d N0k0j=0k(N+jj)+(N+k+1k+1)=j=0k(N+jj)+(N+1+kk+1)
58 48 57 eqtrd N0k0j=0k+1(N+jj)=j=0k(N+jj)+(N+1+kk+1)
59 58 adantr N0k0(N+1+kk)=j=0k(N+jj)j=0k+1(N+jj)=j=0k(N+jj)+(N+1+kk+1)
60 oveq1 (N+1+kk)=j=0k(N+jj)(N+1+kk)+(N+1+kk+1)=j=0k(N+jj)+(N+1+kk+1)
61 60 adantl N0k0(N+1+kk)=j=0k(N+jj)(N+1+kk)+(N+1+kk+1)=j=0k(N+jj)+(N+1+kk+1)
62 ax-1cn 1
63 pncan k1k+1-1=k
64 52 62 63 sylancl N0k0k+1-1=k
65 64 oveq2d N0k0(N+1+kk+1-1)=(N+1+kk)
66 65 oveq2d N0k0(N+1+kk+1)+(N+1+kk+1-1)=(N+1+kk+1)+(N+1+kk)
67 nn0addcl N+10k0N+1+k0
68 29 67 sylan N0k0N+1+k0
69 nn0p1nn k0k+1
70 69 adantl N0k0k+1
71 70 nnzd N0k0k+1
72 bcpasc N+1+k0k+1(N+1+kk+1)+(N+1+kk+1-1)=(N+1+k+1k+1)
73 68 71 72 syl2anc N0k0(N+1+kk+1)+(N+1+kk+1-1)=(N+1+k+1k+1)
74 66 73 eqtr3d N0k0(N+1+kk+1)+(N+1+kk)=(N+1+k+1k+1)
75 nn0p1nn N0N+1
76 nnnn0addcl N+1k0N+1+k
77 75 76 sylan N0k0N+1+k
78 77 nnnn0d N0k0N+1+k0
79 bccl N+1+k0k+1(N+1+kk+1)0
80 78 71 79 syl2anc N0k0(N+1+kk+1)0
81 80 nn0cnd N0k0(N+1+kk+1)
82 nn0z k0k
83 82 adantl N+10k0k
84 bccl N+1+k0k(N+1+kk)0
85 67 83 84 syl2anc N+10k0(N+1+kk)0
86 29 85 sylan N0k0(N+1+kk)0
87 86 nn0cnd N0k0(N+1+kk)
88 81 87 addcomd N0k0(N+1+kk+1)+(N+1+kk)=(N+1+kk)+(N+1+kk+1)
89 peano2cn NN+1
90 49 89 syl N0N+1
91 90 adantr N0k0N+1
92 91 52 53 addassd N0k0N+1+k+1=N+1+k+1
93 92 oveq1d N0k0(N+1+k+1k+1)=(N+1+k+1k+1)
94 74 88 93 3eqtr3d N0k0(N+1+kk)+(N+1+kk+1)=(N+1+k+1k+1)
95 94 adantr N0k0(N+1+kk)=j=0k(N+jj)(N+1+kk)+(N+1+kk+1)=(N+1+k+1k+1)
96 59 61 95 3eqtr2rd N0k0(N+1+kk)=j=0k(N+jj)(N+1+k+1k+1)=j=0k+1(N+jj)
97 4 8 12 16 34 96 nn0indd N0M0(N+1+MM)=j=0M(N+jj)