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

Metamath Proof Explorer

Theorem 4bc2eq6

Proof