Theorem 4bc2eq6

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

	Ref	Expression
Assertion	4bc2eq6	$$⊢\left(\genfrac{}{}{0ex}{}{4}{2}\right)=6$$

Proof

Step	Hyp	Ref	Expression
1		0z	$$⊢0\in \mathbb{Z}$$
2		4z	$$⊢4\in \mathbb{Z}$$
3		2z	$$⊢2\in \mathbb{Z}$$
4	1 2 3	3pm3.2i	$$⊢\left(0\in \mathbb{Z}\wedge 4\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)$$
5		0le2	$$⊢0\le 2$$
6		2re	$$⊢2\in ℝ$$
7		4re	$$⊢4\in ℝ$$
8		2lt4	$$⊢2<4$$
9	6 7 8	ltleii	$$⊢2\le 4$$
10	5 9	pm3.2i	$$⊢\left(0\le 2\wedge 2\le 4\right)$$
11		elfz4	$$⊢\left(\left(0\in \mathbb{Z}\wedge 4\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)\wedge \left(0\le 2\wedge 2\le 4\right)\right)\to 2\in \left(0\dots 4\right)$$
12	4 10 11	mp2an	$$⊢2\in \left(0\dots 4\right)$$
13		bcval2	$$⊢2\in \left(0\dots 4\right)\to \left(\genfrac{}{}{0ex}{}{4}{2}\right)=\frac{4!}{\left(4-2\right)!2!}$$
14	12 13	ax-mp	$$⊢\left(\genfrac{}{}{0ex}{}{4}{2}\right)=\frac{4!}{\left(4-2\right)!2!}$$
15		3nn0	$$⊢3\in {\mathbb{N}}_0$$
16		facp1	$$⊢3\in {\mathbb{N}}_0\to \left(3+1\right)!=3!\left(3+1\right)$$
17	15 16	ax-mp	$$⊢\left(3+1\right)!=3!\left(3+1\right)$$
18		df-4	$$⊢4=3+1$$
19	18	fveq2i	$$⊢4!=\left(3+1\right)!$$
20	18	oveq2i	$$⊢3!\cdot 4=3!\left(3+1\right)$$
21	17 19 20	3eqtr4i	$$⊢4!=3!\cdot 4$$
22		4cn	$$⊢4\in ℂ$$
23		2cn	$$⊢2\in ℂ$$
24		2p2e4	$$⊢2+2=4$$
25	22 23 23 24	subaddrii	$$⊢4-2=2$$
26	25	fveq2i	$$⊢\left(4-2\right)!=2!$$
27		fac2	$$⊢2!=2$$
28	26 27	eqtri	$$⊢\left(4-2\right)!=2$$
29	28 27	oveq12i	$$⊢\left(4-2\right)!2!=2\cdot 2$$
30		2t2e4	$$⊢2\cdot 2=4$$
31	29 30	eqtri	$$⊢\left(4-2\right)!2!=4$$
32	21 31	oveq12i	$$⊢\frac{4!}{\left(4-2\right)!2!}=\frac{3!\cdot 4}{4}$$
33		faccl	$$⊢3\in {\mathbb{N}}_0\to 3!\in \mathbb{N}$$
34	15 33	ax-mp	$$⊢3!\in \mathbb{N}$$
35	34	nncni	$$⊢3!\in ℂ$$
36		4ne0	$$⊢4\ne 0$$
37	35 22 36	divcan4i	$$⊢\frac{3!\cdot 4}{4}=3!$$
38		fac3	$$⊢3!=6$$
39	37 38	eqtri	$$⊢\frac{3!\cdot 4}{4}=6$$
40	32 39	eqtri	$$⊢\frac{4!}{\left(4-2\right)!2!}=6$$
41	14 40	eqtri	$$⊢\left(\genfrac{}{}{0ex}{}{4}{2}\right)=6$$