Theorem bcxmas 7076

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

Assertion

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

Distinct variable group:   j,N

Proof of Theorem bcxmas

Step	Hyp	Ref	Expression
1		bcxmaslem1 7074	. . . . 5 |- (m = 0 -> (((N + 1) + m) C. m) = (((N + 1) + 0) C. 0))
2		opreq2 3969	. . . . . 6 |- (m = 0 -> (0...m) = (0...0))
3	2	sumeq1d 6990	. . . . 5 |- (m = 0 -> sum_j e. (0...m)((N + j) C. j) = sum_j e. (0...0)((N + j) C. j))
4	1, 3	eqeq12d 1489	. . . 4 |- (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	4	imbi2d 612	. . 3 |- (m = 0 -> ((N e. NN0 -> (((N + 1) + m) C. m) = sum_j e. (0...m)((N + j) C. j)) <-> (N e. NN0 -> (((N + 1) + 0) C. 0) = sum_j e. (0...0)((N + j) C. j))))
6		bcxmaslem1 7074	. . . . 5 |- (m = k -> (((N + 1) + m) C. m) = (((N + 1) + k) C. k))
7		opreq2 3969	. . . . . 6 |- (m = k -> (0...m) = (0...k))
8	7	sumeq1d 6990	. . . . 5 |- (m = k -> sum_j e. (0...m)((N + j) C. j) = sum_j e. (0...k)((N + j) C. j))
9	6, 8	eqeq12d 1489	. . . 4 |- (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)))
10	9	imbi2d 612	. . 3 |- (m = k -> ((N e. NN0 -> (((N + 1) + m) C. m) = sum_j e. (0...m)((N + j) C. j)) <-> (N e. NN0 -> (((N + 1) + k) C. k) = sum_j e. (0...k)((N + j) C. j))))
11		bcxmaslem1 7074	. . . . 5 |- (m = (k + 1) -> (((N + 1) + m) C. m) = (((N + 1) + (k + 1)) C. (k + 1)))
12		opreq2 3969	. . . . . 6 |- (m = (k + 1) -> (0...m) = (0...(k + 1)))
13	12	sumeq1d 6990	. . . . 5 |- (m = (k + 1) -> sum_j e. (0...m)((N + j) C. j) = sum_j e. (0...(k + 1))((N + j) C. j))
14	11, 13	eqeq12d 1489	. . . 4 |- (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)))
15	14	imbi2d 612	. . 3 |- (m = (k + 1) -> ((N e. NN0 -> (((N + 1) + m) C. m) = sum_j e. (0...m)((N + j) C. j)) <-> (N e. NN0 -> (((N + 1) + (k + 1)) C. (k + 1)) = sum_j e. (0...(k + 1))((N + j) C. j))))
16		bcxmaslem1 7074	. . . . 5 |- (m = M -> (((N + 1) + m) C. m) = (((N + 1) + M) C. M))
17		opreq2 3969	. . . . . 6 |- (m = M -> (0...m) = (0...M))
18	17	sumeq1d 6990	. . . . 5 |- (m = M -> sum_j e. (0...m)((N + j) C. j) = sum_j e. (0...M)((N + j) C. j))
19	16, 18	eqeq12d 1489	. . . 4 |- (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)))
20	19	imbi2d 612	. . 3 |- (m = M -> ((N e. NN0 -> (((N + 1) + m) C. m) = sum_j e. (0...m)((N + j) C. j)) <-> (N e. NN0 -> (((N + 1) + M) C. M) = sum_j e. (0...M)((N + j) C. j))))
21		0nn0 6113	. . . . 5 |- 0 e. NN0
22		nn0addclt 6120	. . . . . 6 |- ((N e. NN0 /\ 0 e. NN0) -> (N + 0) e. NN0)
23		bcn0t 6963	. . . . . 6 |- ((N + 0) e. NN0 -> ((N + 0) C. 0) = 1)
24	22, 23	syl 10	. . . . 5 |- ((N e. NN0 /\ 0 e. NN0) -> ((N + 0) C. 0) = 1)
25	21, 24	mpan2 696	. . . 4 |- (N e. NN0 -> ((N + 0) C. 0) = 1)
26		bcxmaslem1 7074	. . . . . 6 |- (j = 0 -> ((N + j) C. j) = ((N + 0) C. 0))
27	26	fsum1 7005	. . . . 5 |- ((((N + 0) C. 0) e. NN0 /\ 0 e. ZZ) -> sum_j e. (0...0)((N + j) C. j) = ((N + 0) C. 0))
28		1nn0 6114	. . . . . 6 |- 1 e. NN0
29	25, 28	syl6eqel 1556	. . . . 5 |- (N e. NN0 -> ((N + 0) C. 0) e. NN0)
30		0z 6146	. . . . . 6 |- 0 e. ZZ
31	30	a1i 8	. . . . 5 |- (N e. NN0 -> 0 e. ZZ)
32	27, 29, 31	sylanc 471	. . . 4 |- (N e. NN0 -> sum_j e. (0...0)((N + j) C. j) = ((N + 0) C. 0))
33		peano2nn0 6124	. . . . . 6 |- (N e. NN0 -> (N + 1) e. NN0)
34	33, 21	jctir 293	. . . . 5 |- (N e. NN0 -> ((N + 1) e. NN0 /\ 0 e. NN0))
35		nn0addclt 6120	. . . . 5 |- (((N + 1) e. NN0 /\ 0 e. NN0) -> ((N + 1) + 0) e. NN0)
36		bcn0t 6963	. . . . 5 |- (((N + 1) + 0) e. NN0 -> (((N + 1) + 0) C. 0) = 1)
37	34, 35, 36	3syl 20	. . . 4 |- (N e. NN0 -> (((N + 1) + 0) C. 0) = 1)
38	25, 32, 37	3eqtr4rd 1518	. . 3 |- (N e. NN0 -> (((N + 1) + 0) C. 0) = sum_j e. (0...0)((N + j) C. j))
39		pm3.27 323	. . . . . . . . . . 11 |- ((N e. NN0 /\ k e. NN0) -> k e. NN0)
40		elnn0uz 6441	. . . . . . . . . . 11 |- (k e. NN0 <-> k e. (ZZ>` 0))
41	39, 40	sylib 198	. . . . . . . . . 10 |- ((N e. NN0 /\ k e. NN0) -> k e. (ZZ>` 0))
42		oprex 3983	. . . . . . . . . . 11 |- ((N + j) C. j) e. V
43		oprex 3983	. . . . . . . . . . 11 |- ((N + (k + 1)) C. (k + 1)) e. V
44		bcxmaslem1 7074	. . . . . . . . . . 11 |- (j = (k + 1) -> ((N + j) C. j) = ((N + (k + 1)) C. (k + 1)))
45	42, 43, 44	fsump1 7006	. . . . . . . . . 10 |- (k e. (ZZ>` 0) -> 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))))
46	41, 45	syl 10	. . . . . . . . 9 |- ((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))))
47		bcxmaslem2 7075	. . . . . . . . . . . 12 |- ((N e. CC /\ k e. CC /\ 1 e. CC) -> (N + (k + 1)) = ((N + 1) + k))
48		nn0cnt 6109	. . . . . . . . . . . . 13 |- (N e. NN0 -> N e. CC)
49	48	adantr 389	. . . . . . . . . . . 12 |- ((N e. NN0 /\ k e. NN0) -> N e. CC)
50		nn0cnt 6109	. . . . . . . . . . . . 13 |- (k e. NN0 -> k e. CC)
51	50	adantl 388	. . . . . . . . . . . 12 |- ((N e. NN0 /\ k e. NN0) -> k e. CC)
52		ax1cn 5269	. . . . . . . . . . . . 13 |- 1 e. CC
53	52	a1i 8	. . . . . . . . . . . 12 |- ((N e. NN0 /\ k e. NN0) -> 1 e. CC)
54	47, 49, 51, 53	syl3anc 858	. . . . . . . . . . 11 |- ((N e. NN0 /\ k e. NN0) -> (N + (k + 1)) = ((N + 1) + k))
55	54	opreq1d 3975	. . . . . . . . . 10 |- ((N e. NN0 /\ k e. NN0) -> ((N + (k + 1)) C. (k + 1)) = (((N + 1) + k) C. (k + 1)))
56	55	opreq2d 3976	. . . . . . . . 9 |- ((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	46, 56	eqtrd 1507	. . . . . . . 8 |- ((N e. NN0 /\ k e. NN0) -> sum_j e. (0...(k