Metamath Proof Explorer


Theorem 9t6e54

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

Ref Expression
Assertion 9t6e54
|- ( 9 x. 6 ) = ; 5 4

Proof

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