Theorem 6t6e36

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

	Ref	Expression
Assertion	6t6e36	$$⊢6\cdot 6=36$$

Proof

Step	Hyp	Ref	Expression
1		6nn0	$$⊢6\in {\mathbb{N}}_0$$
2		5nn0	$$⊢5\in {\mathbb{N}}_0$$
3		df-6	$$⊢6=5+1$$
4		6t5e30	$$⊢6\cdot 5=30$$
5		3nn0	$$⊢3\in {\mathbb{N}}_0$$
6	5	dec0u	$$⊢10\cdot 3=30$$
7	4 6	eqtr4i	$$⊢6\cdot 5=10\cdot 3$$
8		dfdec10	$$⊢36=10\cdot 3+6$$
9	8	eqcomi	$$⊢10\cdot 3+6=36$$
10	1 2 3 7 9	4t3lem	$$⊢6\cdot 6=36$$