Metamath Proof Explorer

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 e. NN0
2 2z 
 |-  2 e. ZZ
3 bcpasc 
 |-  ( ( 4 e. NN0 /\ 2 e. ZZ ) -> ( ( 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 e. NN0 -> ( 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