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