Theorem ex-bc

Description: Example for df-bc . (Contributed by AV, 4-Sep-2021)

	Ref	Expression
Assertion	ex-bc	⊢ ( 5 C 3 ) = ; 1 0

Proof

Step	Hyp	Ref	Expression
1		df-5	⊢ 5 = ( 4 + 1 )
2	1	oveq1i	⊢ ( 5 C 3 ) = ( ( 4 + 1 ) C 3 )
3		4bc3eq4	⊢ ( 4 C 3 ) = 4
4		3m1e2	⊢ ( 3 − 1 ) = 2
5	4	oveq2i	⊢ ( 4 C ( 3 − 1 ) ) = ( 4 C 2 )
6		4bc2eq6	⊢ ( 4 C 2 ) = 6
7	5 6	eqtri	⊢ ( 4 C ( 3 − 1 ) ) = 6
8	3 7	oveq12i	⊢ ( ( 4 C 3 ) + ( 4 C ( 3 − 1 ) ) ) = ( 4 + 6 )
9		4nn0	⊢ 4 ∈ ℕ0
10		3z	⊢ 3 ∈ ℤ
11		bcpasc	⊢ ( ( 4 ∈ ℕ0 ∧ 3 ∈ ℤ ) → ( ( 4 C 3 ) + ( 4 C ( 3 − 1 ) ) ) = ( ( 4 + 1 ) C 3 ) )
12	9 10 11	mp2an	⊢ ( ( 4 C 3 ) + ( 4 C ( 3 − 1 ) ) ) = ( ( 4 + 1 ) C 3 )
13		6cn	⊢ 6 ∈ ℂ
14		4cn	⊢ 4 ∈ ℂ
15		6p4e10	⊢ ( 6 + 4 ) = ; 1 0
16	13 14 15	addcomli	⊢ ( 4 + 6 ) = ; 1 0
17	8 12 16	3eqtr3i	⊢ ( ( 4 + 1 ) C 3 ) = ; 1 0
18	2 17	eqtri	⊢ ( 5 C 3 ) = ; 1 0