Metamath Proof Explorer

Theorem 6t3e18

Description: 6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015)

Ref Expression
Assertion 6t3e18 
|- ( 6 x. 3 ) = ; 1 8

Proof

Step Hyp Ref Expression
1 6nn0 
 |-  6 e. NN0
2 2nn0 
 |-  2 e. NN0
3 df-3 
 |-  3 = ( 2 + 1 )
4 6t2e12 
 |-  ( 6 x. 2 ) = ; 1 2
5 1nn0 
 |-  1 e. NN0
6 eqid 
 |-  ; 1 2 = ; 1 2
7 6cn 
 |-  6 e. CC
8 2cn 
 |-  2 e. CC
9 6p2e8 
 |-  ( 6 + 2 ) = 8
10 7 8 9 addcomli 
 |-  ( 2 + 6 ) = 8
11 5 2 1 6 10 decaddi 
 |-  ( ; 1 2 + 6 ) = ; 1 8
12 1 2 3 4 11 4t3lem 
 |-  ( 6 x. 3 ) = ; 1 8