Theorem 7t3e21

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

	Ref	Expression
Assertion	7t3e21	⊢ ( 7 · 3 ) = ; 2 1

Proof

Step	Hyp	Ref	Expression
1		7nn0	⊢ 7 ∈ ℕ0
2		2nn0	⊢ 2 ∈ ℕ0
3		df-3	⊢ 3 = ( 2 + 1 )
4		7t2e14	⊢ ( 7 · 2 ) = ; 1 4
5		1nn0	⊢ 1 ∈ ℕ0
6		4nn0	⊢ 4 ∈ ℕ0
7		eqid	⊢ ; 1 4 = ; 1 4
8		1p1e2	⊢ ( 1 + 1 ) = 2
9	1	nn0cni	⊢ 7 ∈ ℂ
10	6	nn0cni	⊢ 4 ∈ ℂ
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 · 3 ) = ; 2 1