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 e. NN0
10 3z 
 |-  3 e. ZZ
11 bcpasc 
 |-  ( ( 4 e. NN0 /\ 3 e. ZZ ) -> ( ( 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 e. CC
14 4cn 
 |-  4 e. CC
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