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 ∈ ℤ
2		4z	⊢ 4 ∈ ℤ
3		2z	⊢ 2 ∈ ℤ
4	1 2 3	3pm3.2i	⊢ ( 0 ∈ ℤ ∧ 4 ∈ ℤ ∧ 2 ∈ ℤ )
5		0le2	⊢ 0 ≤ 2
6		2re	⊢ 2 ∈ ℝ
7		4re	⊢ 4 ∈ ℝ
8		2lt4	⊢ 2 < 4
9	6 7 8	ltleii	⊢ 2 ≤ 4
10	5 9	pm3.2i	⊢ ( 0 ≤ 2 ∧ 2 ≤ 4 )
11		elfz4	⊢ ( ( ( 0 ∈ ℤ ∧ 4 ∈ ℤ ∧ 2 ∈ ℤ ) ∧ ( 0 ≤ 2 ∧ 2 ≤ 4 ) ) → 2 ∈ ( 0 ... 4 ) )
12	4 10 11	mp2an	⊢ 2 ∈ ( 0 ... 4 )
13		bcval2	⊢ ( 2 ∈ ( 0 ... 4 ) → ( 4 C 2 ) = ( ( ! ‘ 4 ) / ( ( ! ‘ ( 4 − 2 ) ) · ( ! ‘ 2 ) ) ) )
14	12 13	ax-mp	⊢ ( 4 C 2 ) = ( ( ! ‘ 4 ) / ( ( ! ‘ ( 4 − 2 ) ) · ( ! ‘ 2 ) ) )
15		3nn0	⊢ 3 ∈ ℕ0
16		facp1	⊢ ( 3 ∈ ℕ0 → ( ! ‘ ( 3 + 1 ) ) = ( ( ! ‘ 3 ) · ( 3 + 1 ) ) )
17	15 16	ax-mp	⊢ ( ! ‘ ( 3 + 1 ) ) = ( ( ! ‘ 3 ) · ( 3 + 1 ) )
18		df-4	⊢ 4 = ( 3 + 1 )
19	18	fveq2i	⊢ ( ! ‘ 4 ) = ( ! ‘ ( 3 + 1 ) )
20	18	oveq2i	⊢ ( ( ! ‘ 3 ) · 4 ) = ( ( ! ‘ 3 ) · ( 3 + 1 ) )
21	17 19 20	3eqtr4i	⊢ ( ! ‘ 4 ) = ( ( ! ‘ 3 ) · 4 )
22		4cn	⊢ 4 ∈ ℂ
23		2cn	⊢ 2 ∈ ℂ
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 ) ) · ( ! ‘ 2 ) ) = ( 2 · 2 )
30		2t2e4	⊢ ( 2 · 2 ) = 4
31	29 30	eqtri	⊢ ( ( ! ‘ ( 4 − 2 ) ) · ( ! ‘ 2 ) ) = 4
32	21 31	oveq12i	⊢ ( ( ! ‘ 4 ) / ( ( ! ‘ ( 4 − 2 ) ) · ( ! ‘ 2 ) ) ) = ( ( ( ! ‘ 3 ) · 4 ) / 4 )
33		faccl	⊢ ( 3 ∈ ℕ0 → ( ! ‘ 3 ) ∈ ℕ )
34	15 33	ax-mp	⊢ ( ! ‘ 3 ) ∈ ℕ
35	34	nncni	⊢ ( ! ‘ 3 ) ∈ ℂ
36		4ne0	⊢ 4 ≠ 0
37	35 22 36	divcan4i	⊢ ( ( ( ! ‘ 3 ) · 4 ) / 4 ) = ( ! ‘ 3 )
38		fac3	⊢ ( ! ‘ 3 ) = 6
39	37 38	eqtri	⊢ ( ( ( ! ‘ 3 ) · 4 ) / 4 ) = 6
40	32 39	eqtri	⊢ ( ( ! ‘ 4 ) / ( ( ! ‘ ( 4 − 2 ) ) · ( ! ‘ 2 ) ) ) = 6
41	14 40	eqtri	⊢ ( 4 C 2 ) = 6