This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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