Theorem 7t3e21

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

	Ref	Expression
Assertion	7t3e21	$$⊢7\cdot 3=21$$

Proof

Step	Hyp	Ref	Expression
1		7nn0	$$⊢7\in {\mathbb{N}}_0$$
2		2nn0	$$⊢2\in {\mathbb{N}}_0$$
3		df-3	$$⊢3=2+1$$
4		7t2e14	$$⊢7\cdot 2=14$$
5		1nn0	$$⊢1\in {\mathbb{N}}_0$$
6		4nn0	$$⊢4\in {\mathbb{N}}_0$$
7		eqid	$$⊢14=14$$
8		1p1e2	$$⊢1+1=2$$
9	1	nn0cni	$$⊢7\in ℂ$$
10	6	nn0cni	$$⊢4\in ℂ$$
11		7p4e11	$$⊢7+4=11$$
12	9 10 11	addcomli	$$⊢4+7=11$$
13	5 6 1 7 8 5 12	decaddci	$$⊢14+7=21$$
14	1 2 3 4 13	4t3lem	$$⊢7\cdot 3=21$$