Theorem 6t5e30

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

	Ref	Expression
Assertion	6t5e30	$$⊢6\cdot 5=30$$

Proof

Step	Hyp	Ref	Expression
1		6nn0	$$⊢6\in {\mathbb{N}}_0$$
2		4nn0	$$⊢4\in {\mathbb{N}}_0$$
3		df-5	$$⊢5=4+1$$
4		6t4e24	$$⊢6\cdot 4=24$$
5		2nn0	$$⊢2\in {\mathbb{N}}_0$$
6		eqid	$$⊢24=24$$
7		2p1e3	$$⊢2+1=3$$
8		6cn	$$⊢6\in ℂ$$
9		4cn	$$⊢4\in ℂ$$
10		6p4e10	$$⊢6+4=10$$
11	8 9 10	addcomli	$$⊢4+6=10$$
12	5 2 1 6 7 11	decaddci2	$$⊢24+6=30$$
13	1 2 3 4 12	4t3lem	$$⊢6\cdot 5=30$$