Theorem 7t4e28

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

	Ref	Expression
Assertion	7t4e28	$$⊢7\cdot 4=28$$

Proof

Step	Hyp	Ref	Expression
1		7nn0	$$⊢7\in {\mathbb{N}}_0$$
2		3nn0	$$⊢3\in {\mathbb{N}}_0$$
3		df-4	$$⊢4=3+1$$
4		7t3e21	$$⊢7\cdot 3=21$$
5		2nn0	$$⊢2\in {\mathbb{N}}_0$$
6		1nn0	$$⊢1\in {\mathbb{N}}_0$$
7		eqid	$$⊢21=21$$
8		7cn	$$⊢7\in ℂ$$
9		ax-1cn	$$⊢1\in ℂ$$
10		7p1e8	$$⊢7+1=8$$
11	8 9 10	addcomli	$$⊢1+7=8$$
12	5 6 1 7 11	decaddi	$$⊢21+7=28$$
13	1 2 3 4 12	4t3lem	$$⊢7\cdot 4=28$$