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

Metamath Proof Explorer

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