This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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$

Step	Hyp	Ref	Expression
1		6nn0	$⊢ 6 \in ℕ_{0}$
2		4nn0	$⊢ 4 \in ℕ_{0}$
3		df-5	$⊢ 5 = 4 + 1$
4		6t4e24	$⊢ 6 \cdot 4 = 24$
5		2nn0	$⊢ 2 \in ℕ_{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$