Theorem 8t3e24

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

	Ref	Expression
Assertion	8t3e24	$$⊢8\cdot 3=24$$

Proof

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