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

Metamath Proof Explorer

Theorem 8t6e48

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

		Ref	Expression
	Assertion	8t6e48	$⊢ 8 \cdot 6 = 48$

Step	Hyp	Ref	Expression
1		8nn0	$⊢ 8 \in ℕ_{0}$
2		5nn0	$⊢ 5 \in ℕ_{0}$
3		df-6	$⊢ 6 = 5 + 1$
4		8t5e40	$⊢ 8 \cdot 5 = 40$
5		4nn0	$⊢ 4 \in ℕ_{0}$
6	5	dec0u	$⊢ 10 \cdot 4 = 40$
7	4 6	eqtr4i	$⊢ 8 \cdot 5 = 10 \cdot 4$
8		dfdec10	$⊢ 48 = 10 \cdot 4 + 8$
9	8	eqcomi	$⊢ 10 \cdot 4 + 8 = 48$
10	1 2 3 7 9	4t3lem	$⊢ 8 \cdot 6 = 48$