Metamath Proof Explorer

Theorem 7t6e42

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

Ref Expression
Assertion 7t6e42 
|- ( 7 x. 6 ) = ; 4 2

Proof

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