Theorem bcpasc 6922

Description: Pascal's rule for the binomial coefficient, generalized to all integers K. Equation 2 of [Gleason] p. 295.

Hypotheses

Ref	Expression
bcpasc.1	|- N e. NN0
bcpasc.2	|- K e. ZZ

Assertion

Ref	Expression
bcpasc	|- ((N C. K) + (N C. (K - 1))) = ((N + 1) C. K)

Proof of Theorem bcpasc

Step	Hyp	Ref	Expression
1		bcpasc.1	. . . . 5 |- N e. NN0
2		elnn0 6058	. . . . 5 |- (N e. NN0 <-> (N e. NN \/ N = 0))
3	1, 2	mpbi 189	. . . 4 |- (N e. NN \/ N = 0)
4	3	ori 230	. . 3 |- (-. N e. NN -> N = 0)
5		ax1cn 5252	. . . . . . 7 |- 1 e. CC
6	5	addid1 5313	. . . . . 6 |- (1 + 0) = 1
7		opreq2 3964	. . . . . . . 8 |- (K = 0 -> (0 C. K) = (0 C. 0))
8		0nn0 6070	. . . . . . . . 9 |- 0 e. NN0
9		bcn0t 6916	. . . . . . . . 9 |- (0 e. NN0 -> (0 C. 0) = 1)
10	8, 9	ax-mp 7	. . . . . . . 8 |- (0 C. 0) = 1
11	7, 10	syl6eq 1521	. . . . . . 7 |- (K = 0 -> (0 C. K) = 1)
12		opreq1 3963	. . . . . . . . . 10 |- (K = 0 -> (K - 1) = (0 - 1))
13		df-neg 5341	. . . . . . . . . 10 |- -u1 = (0 - 1)
14	12, 13	syl6eqr 1523	. . . . . . . . 9 |- (K = 0 -> (K - 1) = -u1)
15	14	opreq2d 3971	. . . . . . . 8 |- (K = 0 -> (0 C. (K - 1)) = (0 C. -u1))
16		1z 6116	. . . . . . . . . 10 |- 1 e. ZZ
17		znegclt 6120	. . . . . . . . . 10 |- (1 e. ZZ -> -u1 e. ZZ)
18	16, 17	ax-mp 7	. . . . . . . . 9 |- -u1 e. ZZ
19		lt01 5663	. . . . . . . . . . 11 |- 0 < 1
20		1re 5418	. . . . . . . . . . . 12 |- 1 e. RR
21		lt0neg2t 5652	. . . . . . . . . . . 12 |- (1 e. RR -> (0 < 1 <-> -u1 < 0))
22	20, 21	ax-mp 7	. . . . . . . . . . 11 |- (0 < 1 <-> -u1 < 0)
23	19, 22	mpbi 189	. . . . . . . . . 10 |- -u1 < 0
24	23	orci 270	. . . . . . . . 9 |- (-u1 < 0 \/ 0 < -u1)
25		bcval4t 6914	. . . . . . . . 9 |- ((0 e. NN0 /\ -u1 e. ZZ /\ (-u1 < 0 \/ 0 < -u1)) -> (0 C. -u1) = 0)
26	8, 18, 24, 25	mp3an 915	. . . . . . . 8 |- (0 C. -u1) = 0
27	15, 26	syl6eq 1521	. . . . . . 7 |- (K = 0 -> (0 C. (K - 1)) = 0)
28	11, 27	opreq12d 3973	. . . . . 6 |- (K = 0 -> ((0 C. K) + (0 C. (K - 1))) = (1 + 0))
29		opreq2 3964	. . . . . . 7 |- (K = 0 -> (1 C. K) = (1 C. 0))
30		1nn0 6071	. . . . . . . 8 |- 1 e. NN0
31		bcn0t 6916	. . . . . . . 8 |- (1 e. NN0 -> (1 C. 0) = 1)
32	30, 31	ax-mp 7	. . . . . . 7 |- (1 C. 0) = 1
33	29, 32	syl6eq 1521	. . . . . 6 |- (K = 0 -> (1 C. K) = 1)
34	6, 28, 33	3eqtr4a 1530	. . . . 5 |- (K = 0 -> ((0 C. K) + (0 C. (K - 1))) = (1 C. K))
35		bcpasc.2	. . . . . . . 8 |- K e. ZZ
36	35	zre 6098	. . . . . . 7 |- K e. RR
37		0re 5423	. . . . . . 7 |- 0 e. RR
38	36, 37	lttri2 5555	. . . . . 6 |- (K =/= 0 <-> (K < 0 \/ 0 < K))
39		0cn 5311	. . . . . . . . 9 |- 0 e. CC
40	39	addid1 5313	. . . . . . . 8 |- (0 + 0) = 0
41		bcval4t 6914	. . . . . . . . . . 11 |- ((0 e. NN0 /\ K e. ZZ /\ (K < 0 \/ 0 < K)) -> (0 C. K) = 0)
42	8, 35, 41	mp3an12 905	. . . . . . . . . 10 |- ((K < 0 \/ 0 < K) -> (0 C. K) = 0)
43	42	orcs 274	. . . . . . . . 9 |- (K < 0 -> (0 C. K) = 0)
44	36	leid 5594	. . . . . . . . . . . 12 |- K <_ K
45		zlem1ltt 6140	. . . . . . . . . . . . 13 |- ((K e. ZZ /\ K e. ZZ) -> (K <_ K <-> (K - 1) < K))
46	35, 35, 45	mp2an 696	. . . . . . . . . . . 12 |- (K <_ K <-> (K - 1) < K)
47	44, 46	mpbi 189	. . . . . . . . . . 11 |- (K - 1) < K
48	36, 20	resubcl 5422	. . . . . . . . . . . 12 |- (K - 1) e. RR
49	48, 36, 37	lttr 5569	. . . . . . . . . . 11 |- (((K - 1) < K /\ K < 0) -> (K - 1) < 0)
50	47, 49	mpan 694	. . . . . . . . . 10 |- (K < 0 -> (K - 1) < 0)
51		orc 269	. . . . . . . . . 10 |- ((K - 1) < 0 -> ((K - 1) < 0 \/ 0 < (K - 1)))
52		zsubclt 6125	. . . . . . . . . . . 12 |- ((K e. ZZ /\ 1 e. ZZ) -> (K - 1) e. ZZ)
53	35, 16, 52	mp2an 696	. . . . . . . . . . 11 |- (K - 1) e. ZZ
54		bcval4t 6914	. . . . . . . . . . 11 |- ((0 e. NN0 /\ (K - 1) e. ZZ /\ ((K - 1) < 0 \/ 0 < (K - 1))) -> (0 C. (K - 1)) = 0)
55	8, 53, 54	mp3an12 905	. . . . . . . . . 10 |- (((K - 1) < 0 \/ 0 < (K - 1)) -> (0 C. (K - 1)) = 0)
56	50, 51, 55	3syl 20	. . . . . . . . 9 |- (K < 0 -> (0 C. (K - 1)) = 0)
57	43, 56	opreq12d 3973	. . . . . . . 8 |- (K < 0 -> ((0 C. K) + (0 C. (K - 1))) = (0 + 0))
58		bcval4t 6914	. . . . . . . . . 10 |- ((1 e. NN0 /\ K e. ZZ /\ (K < 0 \/ 1 < K)) -> (1 C. K) = 0)
59	30, 35, 58	mp3an12 905	. . . . . . . . 9 |- ((K < 0 \/ 1 < K) -> (1 C. K) = 0)
60	59	orcs 274	. . . . . . . 8 |- (K < 0 -> (1 C. K) = 0)
61	40, 57, 60	3eqtr4a 1530	. . . . . . 7 |- (K < 0 -> ((0 C. K) + (0 C. (K - 1))) = (1 C. K))
62	42	olcs 275	. . . . . . . . 9 |- (0 < K -> (0 C. K) = 0)
63	62	opreq1d 3970	. . . . . . . 8 |- (0 < K -> ((0 C. K) + (0 C. (K - 1))) = (0 + (0 C. (K - 1))))
64		0z 6103	. . . . . . . . . . 11 |- 0 e. ZZ
65		zltp1let 6138	. . . . . . . . . . 11 |- ((0 e. ZZ /\ K e. ZZ) -> (0 < K <-> (0 + 1) <_ K))
66	64, 35, 65	mp2an 696	. . . . . . . . . 10 |- (0 < K <-> (0 + 1) <_ K)
67	5	addid2 5314	. . . . . . . . . . 11 |- (0 + 1) = 1
68	67	breq1i 2622	. . . . . . . . . 10 |- ((0 + 1) <_ K <-> 1 <_ K)
69	20, 36	leloe 5558	. . . . . . . . . 10 |- (1 <_ K <-> (1 < K \/ 1 = K))
70	66, 68, 69	3bitr 177	. . . . . . . . 9 |- (0 < K <-> (1 < K \/ 1 = K))
71	59	olcs 275	. . . . . . . . . . 11 |- (1 < K -> (1 C. K) = 0)
72	20, 36	posdif 5648	. . . . . . . . . . . . . . . 16 |- (1 < K <-> 0 < (K - 1))
73		olc 268	. . . . . . . . . . . . . . . 16 |- (0 < (K - 1) -> ((K - 1) < 0 \/ 0 < (K - 1)))
74	72, 73	sylbi 199	. . . . . . . . . . . . . . 15 |- (1 < K -> ((K - 1) < 0 \/ 0 < (K - 1)))
75	74, 55	syl 10	. . . . . . . . . . . . . 14 |- (1 < K -> (0 C. (K - 1)) = 0)
76	75	eqcomd 1478	. . . . . . . . . . . . 13 |- (1 < K -> 0 = (0 C. (K - 1)))
77	76	opreq2d 3971	. . . . . . . . . . . 12 |- (1 < K -> (0 + 0) = (0 + (0 C. (K - 1))))
78	77, 40	syl5eqr 1519	. . . . . . . . . . 11 |- (1 < K -> 0 = (0 + (0 C. (K - 1))))
79	71, 78	eqtr2d 1506	. . . . . . . . . 10 |- (1 < K -> (0 + (0 C. (K - 1))) = (1 C. K))
80		opreq1 3963	. . . . . . . . . . . . . . . 16 |- (1 = K -> (1 - 1) = (K - 1))
81	5	subid 5374	. . . . . . . . . . . . . . . 16 |- (1 - 1) = 0
82	80, 81	syl5eqr 1519	. . . . . . . . . . . . . . 15 |- (1 = K -> 0 = (K - 1))
83	82	opreq2d 3971	. . . . . . . . . . . . . 14 |- (1 = K -> (0 C. 0) = (0 C. (K - 1)))
84	83, 10	syl5eqr 1519	. . . . . . . . . . . . 13 |- (1 = K -> 1 = (0 C. (K - 1)))
85	84	opreq2d 3971	. . . . . . . . . . . 12 |- (1 = K -> (0 + 1) = (0 + (0 C. (K - 1))))
86	85, 67	syl5eqr 1519	. . . . . . . . . . 11 |- (1 = K -> 1 = (0 + (0 C. (K - 1))))
87		opreq2 3964	. . . . . . . . . . . 12 |- (1 = K -> (1 C. 1) = (1 C. K))
88		bcnnt 6917	. . . . . . . . . . . . 13 |- (1 e. NN0 -> (1 C. 1) = 1)
89	30, 88	ax-mp 7	. . . . . . . . . . . 12 |- (1 C. 1) = 1
90	87, 89	syl5eqr 1519	. . . . . . . . . . 11 |- (1 = K -> 1 = (1 C. K))
91	86, 90	eqtr3d 1507	. . . . . . . . . 10 |- (1 = K -> (0 + (0 C. (K - 1))) = (1 C. K))
92	79, 91	jaoi 341	. . . . . . . . 9 |- ((1 < K \/ 1 = K) -> (0 + (0 C. (K - 1))) = (1 C. K))
93	70, 92	sylbi 199	. . . . . . . 8 |- (0 < K -> (0 + (0 C. (K - 1))) = (1 C. K))
94	63, 93	eqtrd 1505	. . . . . . 7 |- (0 < K -> ((0 C. K) + (0 C. (K - 1))) = (1 C. K))
95	61, 94	jaoi 341	. . . . . 6 |- ((K < 0 \/ 0 < K) -> ((0 C. K) + (0 C. (K - 1))) = (1 C. K))
96	38, 95	sylbi 199	. . . . 5 |- (K =/= 0 -> ((0 C. K) + (0 C. (K - 1))) = (1 C. K))
97	34, 96	pm2.61ine 1632	. . . 4 |- ((0 C. K) + (0 C. (K - 1))) = (1 C. K)
98		opreq1 3963	. . . . 5 |- (N = 0 -> (N C. K) = (0 C. K))
99		opreq1 3963	. . . . 5 |- (N = 0 -> (N C. (K - 1)) = (0 C. (K - 1)))
100	98, 99	opreq12d 3973	. . . 4 |- (N = 0 -> ((N C. K) + (N C. (K - 1))) = ((0 C. K) + (0 C. (K - 1))))
101		opreq1 3963	. . . . . 6 |- (N = 0 -> (N + 1) = (0 + 1))
102	101, 67	syl6eq 1521	. . . . 5 |- (N = 0 -> (N + 1) = 1)
103	102	opreq1d 3970	. . . 4 |- (N = 0 -> ((N + 1) C. K) = (1 C. K))
104	97, 100, 103	3eqtr4a 1530	. . 3 |- (N = 0 -> ((N C. K) + (N C. (K - 1)))