Theorem 5t2e10

Description: 5 times 2 equals 10. (Contributed by NM, 5-Feb-2007) (Revised by AV, 4-Sep-2021)

	Ref	Expression
Assertion	5t2e10	$$⊢5\cdot 2=10$$

Proof

Step	Hyp	Ref	Expression
1		5nn0	$$⊢5\in {\mathbb{N}}_0$$
2		1nn0	$$⊢1\in {\mathbb{N}}_0$$
3		df-2	$$⊢2=1+1$$
4		5cn	$$⊢5\in ℂ$$
5	4	mulid1i	$$⊢5\cdot 1=5$$
6		5p5e10	$$⊢5+5=10$$
7	1 2 3 5 6	4t3lem	$$⊢5\cdot 2=10$$