Metamath Proof Explorer

Theorem 9t9e81

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

Ref Expression
Assertion 9t9e81 
|- ( 9 x. 9 ) = ; 8 1

Proof

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