Theorem 5t3e15

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

	Ref	Expression
Assertion	5t3e15	⊢ ( 5 · 3 ) = ; 1 5

Proof

Step	Hyp	Ref	Expression
1		5nn0	⊢ 5 ∈ ℕ0
2		2nn0	⊢ 2 ∈ ℕ0
3		df-3	⊢ 3 = ( 2 + 1 )
4		5t2e10	⊢ ( 5 · 2 ) = ; 1 0
5		dec10p	⊢ ( ; 1 0 + 5 ) = ; 1 5
6	1 2 3 4 5	4t3lem	⊢ ( 5 · 3 ) = ; 1 5