Theorem 5bc2eq10

Description: The value of 5 choose 2. (Contributed by metakunt, 8-Jun-2024)

	Ref	Expression
Assertion	5bc2eq10	⊢ ( 5 C 2 ) = ; 1 0

Proof

Step	Hyp	Ref	Expression
1		4nn0	⊢ 4 ∈ ℕ0
2		2z	⊢ 2 ∈ ℤ
3		bcpasc	⊢ ( ( 4 ∈ ℕ0 ∧ 2 ∈ ℤ ) → ( ( 4 C 2 ) + ( 4 C ( 2 − 1 ) ) ) = ( ( 4 + 1 ) C 2 ) )
4	1 2 3	mp2an	⊢ ( ( 4 C 2 ) + ( 4 C ( 2 − 1 ) ) ) = ( ( 4 + 1 ) C 2 )
5		4p1e5	⊢ ( 4 + 1 ) = 5
6	5	oveq1i	⊢ ( ( 4 + 1 ) C 2 ) = ( 5 C 2 )
7	4 6	eqtri	⊢ ( ( 4 C 2 ) + ( 4 C ( 2 − 1 ) ) ) = ( 5 C 2 )
8	7	eqcomi	⊢ ( 5 C 2 ) = ( ( 4 C 2 ) + ( 4 C ( 2 − 1 ) ) )
9		2m1e1	⊢ ( 2 − 1 ) = 1
10	9	oveq2i	⊢ ( 4 C ( 2 − 1 ) ) = ( 4 C 1 )
11	10	oveq2i	⊢ ( ( 4 C 2 ) + ( 4 C ( 2 − 1 ) ) ) = ( ( 4 C 2 ) + ( 4 C 1 ) )
12		4bc2eq6	⊢ ( 4 C 2 ) = 6
13		bcn1	⊢ ( 4 ∈ ℕ0 → ( 4 C 1 ) = 4 )
14	1 13	ax-mp	⊢ ( 4 C 1 ) = 4
15	12 14	oveq12i	⊢ ( ( 4 C 2 ) + ( 4 C 1 ) ) = ( 6 + 4 )
16	11 15	eqtri	⊢ ( ( 4 C 2 ) + ( 4 C ( 2 − 1 ) ) ) = ( 6 + 4 )
17		6p4e10	⊢ ( 6 + 4 ) = ; 1 0
18	8 16 17	3eqtri	⊢ ( 5 C 2 ) = ; 1 0