Metamath Proof Explorer

Theorem 5t2e10

Description: 5 times 2 equals 10. (Contributed by NM, 5-Feb-2007) (Revised by AV, 4-Sep-2021)

Ref Expression
Assertion 5t2e10 
|- ( 5 x. 2 ) = ; 1 0

Proof

Step Hyp Ref Expression
1 5nn0 
 |-  5 e. NN0
2 1nn0 
 |-  1 e. NN0
3 df-2 
 |-  2 = ( 1 + 1 )
4 5cn 
 |-  5 e. CC
5 4 mulid1i 
 |-  ( 5 x. 1 ) = 5
6 5p5e10 
 |-  ( 5 + 5 ) = ; 1 0
7 1 2 3 5 6 4t3lem 
 |-  ( 5 x. 2 ) = ; 1 0