Metamath Proof Explorer


Theorem 5bc2eq10

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

Ref Expression
Assertion 5bc2eq10 ( 5 2 ) = 10

Proof

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