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$$

Proof

Step	Hyp	Ref	Expression
1		8nn0	$$⊢8\in {\mathbb{N}}_0$$
2		5nn0	$$⊢5\in {\mathbb{N}}_0$$
3		df-6	$$⊢6=5+1$$
4		8t5e40	$$⊢8\cdot 5=40$$
5		4nn0	$$⊢4\in {\mathbb{N}}_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$$