Theorem 8t4e32

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

	Ref	Expression
Assertion	8t4e32	$$⊢8\cdot 4=32$$

Proof

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