Metamath Proof Explorer

Theorem 9t8e72

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

Ref Expression
Assertion 9t8e72 
|- ( 9 x. 8 ) = ; 7 2

Proof

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