Metamath Proof Explorer

Theorem 9t3e27

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

Ref Expression
Assertion 9t3e27 
|- ( 9 x. 3 ) = ; 2 7

Proof

Step Hyp Ref Expression
1 9nn0 
 |-  9 e. NN0
2 2nn0 
 |-  2 e. NN0
3 df-3 
 |-  3 = ( 2 + 1 )
4 9t2e18 
 |-  ( 9 x. 2 ) = ; 1 8
5 1nn0 
 |-  1 e. NN0
6 8nn0 
 |-  8 e. NN0
7 eqid 
 |-  ; 1 8 = ; 1 8
8 1p1e2 
 |-  ( 1 + 1 ) = 2
9 7nn0 
 |-  7 e. NN0
10 1 nn0cni 
 |-  9 e. CC
11 6 nn0cni 
 |-  8 e. CC
12 9p8e17 
 |-  ( 9 + 8 ) = ; 1 7
13 10 11 12 addcomli 
 |-  ( 8 + 9 ) = ; 1 7
14 5 6 1 7 8 9 13 decaddci 
 |-  ( ; 1 8 + 9 ) = ; 2 7
15 1 2 3 4 14 4t3lem 
 |-  ( 9 x. 3 ) = ; 2 7