Theorem 4bc2eq6

Description: The value of four choose two. (Contributed by Scott Fenton, 9-Jan-2017)

	Ref	Expression
Assertion	4bc2eq6	|- ( 4 _C 2 ) = 6

Proof

Step	Hyp	Ref	Expression
1		0z	|- 0 e. ZZ
2		4z	|- 4 e. ZZ
3		2z	|- 2 e. ZZ
4	1 2 3	3pm3.2i	|- ( 0 e. ZZ /\ 4 e. ZZ /\ 2 e. ZZ )
5		0le2	|- 0 <_ 2
6		2re	|- 2 e. RR
7		4re	|- 4 e. RR
8		2lt4	|- 2 < 4
9	6 7 8	ltleii	|- 2 <_ 4
10	5 9	pm3.2i	|- ( 0 <_ 2 /\ 2 <_ 4 )
11		elfz4	|- ( ( ( 0 e. ZZ /\ 4 e. ZZ /\ 2 e. ZZ ) /\ ( 0 <_ 2 /\ 2 <_ 4 ) ) -> 2 e. ( 0 ... 4 ) )
12	4 10 11	mp2an	|- 2 e. ( 0 ... 4 )
13		bcval2	|- ( 2 e. ( 0 ... 4 ) -> ( 4 _C 2 ) = ( ( ! ` 4 ) / ( ( ! ` ( 4 - 2 ) ) x. ( ! ` 2 ) ) ) )
14	12 13	ax-mp	|- ( 4 _C 2 ) = ( ( ! ` 4 ) / ( ( ! ` ( 4 - 2 ) ) x. ( ! ` 2 ) ) )
15		3nn0	|- 3 e. NN0
16		facp1	|- ( 3 e. NN0 -> ( ! ` ( 3 + 1 ) ) = ( ( ! ` 3 ) x. ( 3 + 1 ) ) )
17	15 16	ax-mp	|- ( ! ` ( 3 + 1 ) ) = ( ( ! ` 3 ) x. ( 3 + 1 ) )
18		df-4	|- 4 = ( 3 + 1 )
19	18	fveq2i	|- ( ! ` 4 ) = ( ! ` ( 3 + 1 ) )
20	18	oveq2i	|- ( ( ! ` 3 ) x. 4 ) = ( ( ! ` 3 ) x. ( 3 + 1 ) )
21	17 19 20	3eqtr4i	|- ( ! ` 4 ) = ( ( ! ` 3 ) x. 4 )
22		4cn	|- 4 e. CC
23		2cn	|- 2 e. CC
24		2p2e4	|- ( 2 + 2 ) = 4
25	22 23 23 24	subaddrii	|- ( 4 - 2 ) = 2
26	25	fveq2i	|- ( ! ` ( 4 - 2 ) ) = ( ! ` 2 )
27		fac2	|- ( ! ` 2 ) = 2
28	26 27	eqtri	|- ( ! ` ( 4 - 2 ) ) = 2
29	28 27	oveq12i	|- ( ( ! ` ( 4 - 2 ) ) x. ( ! ` 2 ) ) = ( 2 x. 2 )
30		2t2e4	|- ( 2 x. 2 ) = 4
31	29 30	eqtri	|- ( ( ! ` ( 4 - 2 ) ) x. ( ! ` 2 ) ) = 4
32	21 31	oveq12i	|- ( ( ! ` 4 ) / ( ( ! ` ( 4 - 2 ) ) x. ( ! ` 2 ) ) ) = ( ( ( ! ` 3 ) x. 4 ) / 4 )
33		faccl	|- ( 3 e. NN0 -> ( ! ` 3 ) e. NN )
34	15 33	ax-mp	|- ( ! ` 3 ) e. NN
35	34	nncni	|- ( ! ` 3 ) e. CC
36		4ne0	|- 4 =/= 0
37	35 22 36	divcan4i	|- ( ( ( ! ` 3 ) x. 4 ) / 4 ) = ( ! ` 3 )
38		fac3	|- ( ! ` 3 ) = 6
39	37 38	eqtri	|- ( ( ( ! ` 3 ) x. 4 ) / 4 ) = 6
40	32 39	eqtri	|- ( ( ! ` 4 ) / ( ( ! ` ( 4 - 2 ) ) x. ( ! ` 2 ) ) ) = 6
41	14 40	eqtri	|- ( 4 _C 2 ) = 6