Theorem bcpasc2 6905

Description: Pascal's rule for the binomial coefficient. Equation 2 of [Gleason] p. 295.

Hypotheses

Ref	Expression
bcpasc2.1	|- N e. NN
bcpasc2.2	|- K e. NN
bcpasc2.3	|- K <_ N

Assertion

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

Proof of Theorem bcpasc2

Step	Hyp	Ref	Expression
1		ax1cn 5241	. . . . . 6 |- 1 e. CC
2		bcpasc2.2	. . . . . . 7 |- K e. NN
3	2	nncn 5880	. . . . . 6 |- K e. CC
4		bcpasc2.1	. . . . . . . . 9 |- N e. NN
5	4	nncn 5880	. . . . . . . 8 |- N e. CC
6	5, 3	subcl 5338	. . . . . . 7 |- (N - K) e. CC
7	6, 1	addcl 5292	. . . . . 6 |- ((N - K) + 1) e. CC
8	2	nnne0 5899	. . . . . 6 |- K =/= 0
9		bcpasc2.3	. . . . . . . . 9 |- K <_ N
10	2	nnnn0 6054	. . . . . . . . . 10 |- K e. NN0
11	4	nnnn0 6054	. . . . . . . . . 10 |- N e. NN0
12		nn0subt 6108	. . . . . . . . . 10 |- ((K e. NN0 /\ N e. NN0) -> (K <_ N <-> (N - K) e. NN0))
13	10, 11, 12	mp2an 695	. . . . . . . . 9 |- (K <_ N <-> (N - K) e. NN0)
14	9, 13	mpbi 189	. . . . . . . 8 |- (N - K) e. NN0
15		nn0p1nnt 6122	. . . . . . . 8 |- ((N - K) e. NN0 -> ((N - K) + 1) e. NN)
16	14, 15	ax-mp 7	. . . . . . 7 |- ((N - K) + 1) e. NN
17	16	nnne0 5899	. . . . . 6 |- ((N - K) + 1) =/= 0
18	1, 3, 1, 7, 8, 17	divadddiv 5744	. . . . 5 |- ((1 / K) + (1 / ((N - K) + 1))) = (((1 x. ((N - K) + 1)) + (K x. 1)) / (K x. ((N - K) + 1)))
19	7	mulid2 5305	. . . . . . . 8 |- (1 x. ((N - K) + 1)) = ((N - K) + 1)
20	3	mulid1 5304	. . . . . . . 8 |- (K x. 1) = K
21	19, 20	opreq12i 3958	. . . . . . 7 |- ((1 x. ((N - K) + 1)) + (K x. 1)) = (((N - K) + 1) + K)
22	6, 1, 3	add23 5313	. . . . . . 7 |- (((N - K) + 1) + K) = (((N - K) + K) + 1)
23		npcant 5371	. . . . . . . . 9 |- ((N e. CC /\ K e. CC) -> ((N - K) + K) = N)
24	5, 3, 23	mp2an 695	. . . . . . . 8 |- ((N - K) + K) = N
25	24	opreq1i 3956	. . . . . . 7 |- (((N - K) + K) + 1) = (N + 1)
26	21, 22, 25	3eqtr 1491	. . . . . 6 |- ((1 x. ((N - K) + 1)) + (K x. 1)) = (N + 1)
27	26	opreq1i 3956	. . . . 5 |- (((1 x. ((N - K) + 1)) + (K x. 1)) / (K x. ((N - K) + 1))) = ((N + 1) / (K x. ((N - K) + 1)))
28	18, 27	eqtr 1487	. . . 4 |- ((1 / K) + (1 / ((N - K) + 1))) = ((N + 1) / (K x. ((N - K) + 1)))
29	28	opreq2i 3957	. . 3 |- (((!` N) / ((!` (K - 1)) x. (!` (N - K)))) x. ((1 / K) + (1 / ((N - K) + 1)))) = (((!` N) / ((!` (K - 1)) x. (!` (N - K)))) x. ((N + 1) / (K x. ((N - K) + 1))))
30		facclt 6877	. . . . . . 7 |- (N e. NN0 -> (!` N) e. NN)
31	11, 30	ax-mp 7	. . . . . 6 |- (!` N) e. NN
32	31	nncn 5880	. . . . 5 |- (!` N) e. CC
33		nnge1t 5891	. . . . . . . . . 10 |- (K e. NN -> 1 <_ K)
34	2, 33	ax-mp 7	. . . . . . . . 9 |- 1 <_ K
35		1nn0 6061	. . . . . . . . . 10 |- 1 e. NN0
36		nn0subt 6108	. . . . . . . . . 10 |- ((1 e. NN0 /\ K e. NN0) -> (1 <_ K <-> (K - 1) e. NN0))
37	35, 10, 36	mp2an 695	. . . . . . . . 9 |- (1 <_ K <-> (K - 1) e. NN0)
38	34, 37	mpbi 189	. . . . . . . 8 |- (K - 1) e. NN0
39		facclt 6877	. . . . . . . 8 |- ((K - 1) e. NN0 -> (!` (K - 1)) e. NN)
40	38, 39	ax-mp 7	. . . . . . 7 |- (!` (K - 1)) e. NN
41		facclt 6877	. . . . . . . 8 |- ((N - K) e. NN0 -> (!` (N - K)) e. NN)
42	14, 41	ax-mp 7	. . . . . . 7 |- (!` (N - K)) e. NN
43		nnmulclt 5889	. . . . . . 7 |- (((!` (K - 1)) e. NN /\ (!` (N - K)) e. NN) -> ((!` (K - 1)) x. (!` (N - K))) e. NN)
44	40, 42, 43	mp2an 695	. . . . . 6 |- ((!` (K - 1)) x. (!` (N - K))) e. NN
45	44	nncn 5880	. . . . 5 |- ((!` (K - 1)) x. (!` (N - K))) e. CC
46	44	nnne0 5899	. . . . 5 |- ((!` (K - 1)) x. (!` (N - K))) =/= 0
47	32, 45, 46	divcl 5679	. . . 4 |- ((!` N) / ((!` (K - 1)) x. (!` (N - K)))) e. CC
48	3, 8	reccl 5682	. . . 4 |- (1 / K) e. CC
49	7, 17	reccl 5682	. . . 4 |- (1 / ((N - K) + 1)) e. CC
50	47, 48, 49	adddi 5298	. . 3 |- (((!` N) / ((!` (K - 1)) x. (!` (N - K)))) x. ((1 / K) + (1 / ((N - K) + 1)))) = ((((!` N) / ((!` (K - 1)) x. (!` (N - K)))) x. (1 / K)) + (((!` N) / ((!` (K - 1)) x. (!` (N - K)))) x. (1 / ((N - K) + 1))))
51	11, 35	nn0addcl 6068	. . . . . 6 |- (N + 1) e. NN0
52	51	nn0cn 6058	. . . . 5 |- (N + 1) e. CC
53	3, 7	mulcl 5293	. . . . 5 |- (K x. ((N - K) + 1)) e. CC
54	3, 7, 8, 17	muln0 5668	. . . . 5 |- (K x. ((N - K) + 1)) =/= 0
55	32, 45, 52, 53, 46, 54	divmuldiv 5742	. . . 4 |- (((!` N) / ((!` (K - 1)) x. (!` (N - K)))) x. ((N + 1) / (K x. ((N - K) + 1)))) = (((!` N) x. (N + 1)) / (((!` (K - 1)) x. (!` (N - K))) x. (K x. ((N - K) + 1))))
56		facp1t 6873	. . . . . 6 |- (N e. NN0 -> (!` (N + 1)) = ((!` N) x. (N + 1)))
57	11, 56	ax-mp 7	. . . . 5 |- (!` (N + 1)) = ((!` N) x. (N + 1))
58	2	nnre 5879	. . . . . . . . . . 11 |- K e. RR
59	51	nn0re 6057	. . . . . . . . . . 11 |- (N + 1) e. RR
60		nnleltp1t 5901	. . . . . . . . . . . . 13 |- ((K e. NN /\ N e. NN) -> (K <_ N <-> K < (N + 1)))
61	2, 4, 60	mp2an 695	. . . . . . . . . . . 12 |- (K <_ N <-> K < (N + 1))
62	9, 61	mpbi 189	. . . . . . . . . . 11 |- K < (N + 1)
63	58, 59, 62	ltlei 5554	. . . . . . . . . 10 |- K <_ (N + 1)
64		nn0subt 6108	. . . . . . . . . . 11 |- ((K e. NN0 /\ (N + 1) e. NN0) -> (K <_ (N + 1) <-> ((N + 1) - K) e. NN0))
65	10, 51, 64	mp2an 695	. . . . . . . . . 10 |- (K <_ (N + 1) <-> ((N + 1) - K) e. NN0)
66	63, 65	mpbi 189	. . . . . . . . 9 |- ((N + 1) - K) e. NN0
67		facclt 6877	. . . . . . . . 9 |- (((N + 1) - K) e. NN0 -> (!` ((N + 1) - K)) e. NN)
68	66, 67	ax-mp 7	. . . . . . . 8 |- (!` ((N + 1) - K)) e. NN
69	68	nncn 5880	. . . . . . 7 |- (!` ((N + 1) - K)) e. CC
70		facclt 6877	. . . . . . . . 9 |- (K e. NN0 -> (!` K) e. NN)
71	10, 70	ax-mp 7	. . . . . . . 8 |- (!` K) e. NN
72	71	nncn 5880	. . . . . . 7 |- (!` K) e. CC
73	69, 72	mulcom 5295	. . . . . 6 |- ((!` ((N + 1) - K)) x. (!` K)) = ((!` K) x. (!` ((N + 1) - K)))
74		facnn2t 6876	. . . . . . . 8 |- (K e. NN -> (!` K) = ((!` (K - 1)) x. K))
75	2, 74	ax-mp 7	. . . . . . 7 |- (!` K) = ((!` (K - 1)) x. K)
76	5, 1, 3	addsub 5360	. . . . . . . . 9 |- ((N + 1) - K) = ((N - K) + 1)
77	76	fveq2i 3712	. . . . . . . 8 |- (!` ((N + 1) - K)) = (!` ((N - K) + 1))
78		facp1t 6873	. . . . . . . . 9 |- ((N - K) e. NN0 -> (!` ((N - K) + 1)) = ((!` (N - K)) x. ((N - K) + 1)))
79	14, 78	ax-mp 7	. . . . . . . 8 |- (!` ((N - K) + 1)) = ((!` (N - K)) x. ((N - K) + 1))
80	77, 79	eqtr 1487	. . . . . . 7 |- (!` ((N + 1) - K)) = ((!` (N - K)) x. ((N - K) + 1))
81	75, 80	opreq12i 3958	. . . . . 6 |- ((!` K) x. (!` ((N + 1) - K))) = (((!` (K - 1)) x. K) x. ((!` (N - K)) x. ((N - K) + 1)))
82	40	nncn 5880	. . . . . . 7 |- (!` (K - 1)) e. CC
83	42	nncn 5880	. . . . . . 7 |- (!` (N - K)) e. CC
84	82, 3, 83, 7	mul4 5397	. . . . . 6 |- (((!` (K - 1)) x. K) x. ((!`