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 · 2 ) = ; 1 0

Proof

Step	Hyp	Ref	Expression
1		5nn0	⊢ 5 ∈ ℕ0
2		1nn0	⊢ 1 ∈ ℕ0
3		df-2	⊢ 2 = ( 1 + 1 )
4		5cn	⊢ 5 ∈ ℂ
5	4	mulid1i	⊢ ( 5 · 1 ) = 5
6		5p5e10	⊢ ( 5 + 5 ) = ; 1 0
7	1 2 3 5 6	4t3lem	⊢ ( 5 · 2 ) = ; 1 0