Theorem 8t5e40

Description: 8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015) (Revised by AV, 6-Sep-2021)

	Ref	Expression
Assertion	8t5e40	$$⊢8\cdot 5=40$$

Proof

Step	Hyp	Ref	Expression
1		8nn0	$$⊢8\in {\mathbb{N}}_0$$
2		4nn0	$$⊢4\in {\mathbb{N}}_0$$
3		df-5	$$⊢5=4+1$$
4		8t4e32	$$⊢8\cdot 4=32$$
5		3nn0	$$⊢3\in {\mathbb{N}}_0$$
6		2nn0	$$⊢2\in {\mathbb{N}}_0$$
7		eqid	$$⊢32=32$$
8		3p1e4	$$⊢3+1=4$$
9		8cn	$$⊢8\in ℂ$$
10		2cn	$$⊢2\in ℂ$$
11		8p2e10	$$⊢8+2=10$$
12	9 10 11	addcomli	$$⊢2+8=10$$
13	5 6 1 7 8 12	decaddci2	$$⊢32+8=40$$
14	1 2 3 4 13	4t3lem	$$⊢8\cdot 5=40$$