Theorem bccl2t 6909

Description: A binomial coefficient, in its standard domain, is a natural number.

Assertion

Ref	Expression
bccl2t	|- ((N e. NN0 /\ K e. (0...N)) -> (N C. K) e. NN)

Proof of Theorem bccl2t

Step	Hyp	Ref	Expression
1		breq1 2612	. . . . . . . . 9 |- (k = K -> (k <_ N <-> K <_ N))
2		opreq2 3954	. . . . . . . . . 10 |- (k = K -> (N C. k) = (N C. K))
3	2	eleq1d 1532	. . . . . . . . 9 |- (k = K -> ((N C. k) e. NN <-> (N C. K) e. NN))
4	1, 3	imbi12d 624	. . . . . . . 8 |- (k = K -> ((k <_ N -> (N C. k) e. NN) <-> (K <_ N -> (N C. K) e. NN)))
5	4	rcla4v 1864	. . . . . . 7 |- (K e. NN -> (A.k e. NN (k <_ N -> (N C. k) e. NN) -> (K <_ N -> (N C. K) e. NN)))
6		breq2 2613	. . . . . . . . . 10 |- (n = 1 -> (k <_ n <-> k <_ 1))
7		opreq1 3953	. . . . . . . . . . 11 |- (n = 1 -> (n C. k) = (1 C. k))
8	7	eleq1d 1532	. . . . . . . . . 10 |- (n = 1 -> ((n C. k) e. NN <-> (1 C. k) e. NN))
9	6, 8	imbi12d 624	. . . . . . . . 9 |- (n = 1 -> ((k <_ n -> (n C. k) e. NN) <-> (k <_ 1 -> (1 C. k) e. NN)))
10	9	ralbidv 1655	. . . . . . . 8 |- (n = 1 -> (A.k e. NN (k <_ n -> (n C. k) e. NN) <-> A.k e. NN (k <_ 1 -> (1 C. k) e. NN)))
11		breq2 2613	. . . . . . . . . 10 |- (n = j -> (k <_ n <-> k <_ j))
12		opreq1 3953	. . . . . . . . . . 11 |- (n = j -> (n C. k) = (j C. k))
13	12	eleq1d 1532	. . . . . . . . . 10 |- (n = j -> ((n C. k) e. NN <-> (j C. k) e. NN))
14	11, 13	imbi12d 624	. . . . . . . . 9 |- (n = j -> ((k <_ n -> (n C. k) e. NN) <-> (k <_ j -> (j C. k) e. NN)))
15	14	ralbidv 1655	. . . . . . . 8 |- (n = j -> (A.k e. NN (k <_ n -> (n C. k) e. NN) <-> A.k e. NN (k <_ j -> (j C. k) e. NN)))
16		breq2 2613	. . . . . . . . . 10 |- (n = (j + 1) -> (k <_ n <-> k <_ (j + 1)))
17		opreq1 3953	. . . . . . . . . . 11 |- (n = (j + 1) -> (n C. k) = ((j + 1) C. k))
18	17	eleq1d 1532	. . . . . . . . . 10 |- (n = (j + 1) -> ((n C. k) e. NN <-> ((j + 1) C. k) e. NN))
19	16, 18	imbi12d 624	. . . . . . . . 9 |- (n = (j + 1) -> ((k <_ n -> (n C. k) e. NN) <-> (k <_ (j + 1) -> ((j + 1) C. k) e. NN)))
20	19	ralbidv 1655	. . . . . . . 8 |- (n = (j + 1) -> (A.k e. NN (k <_ n -> (n C. k) e. NN) <-> A.k e. NN (k <_ (j + 1) -> ((j + 1) C. k) e. NN)))
21		breq2 2613	. . . . . . . . . 10 |- (n = N -> (k <_ n <-> k <_ N))
22		opreq1 3953	. . . . . . . . . . 11 |- (n = N -> (n C. k) = (N C. k))
23	22	eleq1d 1532	. . . . . . . . . 10 |- (n = N -> ((n C. k) e. NN <-> (N C. k) e. NN))
24	21, 23	imbi12d 624	. . . . . . . . 9 |- (n = N -> ((k <_ n -> (n C. k) e. NN) <-> (k <_ N -> (N C. k) e. NN)))
25	24	ralbidv 1655	. . . . . . . 8 |- (n = N -> (A.k e. NN (k <_ n -> (n C. k) e. NN) <-> A.k e. NN (k <_ N -> (N C. k) e. NN)))
26		nnle1eq1t 5893	. . . . . . . . . 10 |- (k e. NN -> (k <_ 1 <-> k = 1))
27		opreq2 3954	. . . . . . . . . . 11 |- (k = 1 -> (1 C. k) = (1 C. 1))
28		1nn0 6061	. . . . . . . . . . . . 13 |- 1 e. NN0
29		bcnnt 6902	. . . . . . . . . . . . 13 |- (1 e. NN0 -> (1 C. 1) = 1)
30	28, 29	ax-mp 7	. . . . . . . . . . . 12 |- (1 C. 1) = 1
31		1nn 5882	. . . . . . . . . . . 12 |- 1 e. NN
32	30, 31	eqeltr 1536	. . . . . . . . . . 11 |- (1 C. 1) e. NN
33	27, 32	syl6eqel 1548	. . . . . . . . . 10 |- (k = 1 -> (1 C. k) e. NN)
34	26, 33	syl6bi 214	. . . . . . . . 9 |- (k e. NN -> (k <_ 1 -> (1 C. k) e. NN))
35	34	rgen 1690	. . . . . . . 8 |- A.k e. NN (k <_ 1 -> (1 C. k) e. NN)
36		ax-17 968	. . . . . . . . 9 |- (j e. NN -> A.k j e. NN)
37		hbra1 1679	. . . . . . . . 9 |- (A.k e. NN (k <_ j -> (j C. k) e. NN) -> A.kA.k e. NN (k <_ j -> (j C. k) e. NN))
38		leloet 5491	. . . . . . . . . . . . . . 15 |- ((k e. RR /\ (j + 1) e. RR) -> (k <_ (j + 1) <-> (k < (j + 1) \/ k = (j + 1))))
39		nnret 5877	. . . . . . . . . . . . . . 15 |- (k e. NN -> k e. RR)
40		peano2nn 5883	. . . . . . . . . . . . . . . 16 |- (j e. NN -> (j + 1) e. NN)
41		nnret 5877	. . . . . . . . . . . . . . . 16 |- ((j + 1) e. NN -> (j + 1) e. RR)
42	40, 41	syl 10	. . . . . . . . . . . . . . 15 |- (j e. NN -> (j + 1) e. RR)
43	38, 39, 42	syl2an 454	. . . . . . . . . . . . . 14 |- ((k e. NN /\ j e. NN) -> (k <_ (j + 1) <-> (k < (j + 1) \/ k = (j + 1))))
44		nnleltp1t 5901	. . . . . . . . . . . . . . 15 |- ((k e. NN /\ j e. NN) -> (k <_ j <-> k < (j + 1)))
45	44	orbi1d 613	. . . . . . . . . . . . . 14 |- ((k e. NN /\ j e. NN) -> ((k <_ j \/ k = (j + 1)) <-> (k < (j + 1) \/ k = (j + 1))))
46	43, 45	bitr4d 529	. . . . . . . . . . . . 13 |- ((k e. NN /\ j e. NN) -> (k <_ (j + 1) <-> (k <_ j \/ k = (j + 1))))
47		nnge1t 5891	. . . . . . . . . . . . . . . 16 |- (k e. NN -> 1 <_ k)
48		1re 5407	. . . . . . . . . . . . . . . . . 18 |- 1 e. RR
49		leloet 5491	. . . . . . . . . . . . . . . . . 18 |- ((1 e. RR /\ k e. RR) -> (1 <_ k <-> (1 < k \/ 1 = k)))
50	48, 49	mpan 693	. . . . . . . . . . . . . . . . 17 |- (k e. RR -> (1 <_ k <-> (1 < k \/ 1 = k)))
51	39, 50	syl 10	. . . . . . . . . . . . . . . 16 |- (k e. NN -> (1 <_ k <-> (1 < k \/ 1 = k)))
52	47, 51	mpbid 195	. . . . . . . . . . . . . . 15 |- (k e. NN -> (1 < k \/ 1 = k))
53	52	adantr 389	. . . . . . . . . . . . . 14 |- ((k e. NN /\ j e. NN) -> (1 < k \/ 1 = k))
54		nnaddclt 5888	. . . . . . . . . . . . . . . . . . . 20 |- (((j C. k) e. NN /\ (j C. (k - 1)) e. NN) -> ((j C. k) + (j C. (k - 1))) e. NN)
55		ra4 1686	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (A.k e. NN (k <_ j -> (j C. k) e. NN) -> (k e. NN -> (k <_ j -> (j C. k) e. NN)))
56	55	imp32 363	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A.k e. NN (k <_ j -> (j C. k) e. NN) /\ (k e. NN /\ k <_ j)) -> (j C. k) e. NN)
57	56	ancoms 436	. . . . . . . . . . . . . . . . . . . . . 22 |- (((k e. NN /\ k <_ j) /\ A.k e. NN (k <_ j -> (j C. k) e. NN)) -> (j C. k) e. NN)
58	57	adantllr 397	. . . . . . . . . . . . . . . . . . . . 21 |- ((((k e. NN /\ j e. NN) /\ k <_ j) /\ A.k e. NN (k <_ j -> (j C. k) e. NN)) -> (j C. k) e. NN)
59	58	adantlrl 398	. . . . . . . . . . . . . . . . . . . 20 |- ((((k e. NN /\ j e. NN) /\ (1 < k /\ k <_ j)) /\ A.k e. NN (k <_ j -> (j C. k) e. NN)) -> (j C. k) e. NN)
60		nnzt 6100	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (k e. NN -> k e. ZZ)
61		peano2zm 6116	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (k e. ZZ -> (k - 1) e. ZZ)
62	60, 61	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (k e. NN -> (k - 1) e. ZZ)
63		nnltlem1t 6134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((1 e. NN /\ k e. NN) -> (1 < k <-> 1 <_ (k - 1)))
64	31, 63	mpan 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (k e. NN -> (1 < k <-> 1 <_ (k - 1)))
65	64	biimpd 153	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (k e. NN -> (1 < k -> 1 <_ (k - 1)))
66	65	anim2d 559	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (k e. NN -> (((k - 1) e. ZZ /\ 1 < k) -> ((k - 1) e. ZZ /\ 1 <_ (k - 1))))
67		elnnz1 6102	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((k - 1) e. NN <-> ((k - 1) e. ZZ /\ 1 <_ (k - 1)))
68	66, 67	syl6ibr 213	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (k e. NN -> (((k - 1) e. ZZ /\ 1 < k) -> (k - 1) e. NN))
69	62, 68	mpand 699	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (k e. NN -> (1 < k -> (k - 1) e. NN))
70		breq1 2612	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (n = (k - 1) -> (n <_ j <-> (k - 1) <_ j))
71		opreq2 3954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (n = (k - 1) -> (j C. n) = (j C. (k - 1)))
72	71	eleq1d 1532	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (n = (k - 1) -> ((j C. n) e. NN <-> (j C. (k - 1)) e. NN))
73	70, 72	imbi12d 624	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (n = (k - 1) -> ((n <_ j -> (j C. n) e. NN) <-> ((k - 1) <_ j -> (j C. (k - 1)) e. NN)))
74	73	rcla4v 1864	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((k - 1) e. NN -> (A.