Metamath Proof Explorer

Theorem 7t3e21

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

Ref Expression
Assertion 7t3e21 
|- ( 7 x. 3 ) = ; 2 1

Proof

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