Theorem 5t5e25

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

	Ref	Expression
Assertion	5t5e25	$$⊢5\cdot 5=25$$

Proof

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