Theorem 5t4e20

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

	Ref	Expression
Assertion	5t4e20	⊢ ( 5 · 4 ) = ; 2 0

Proof

Step	Hyp	Ref	Expression
1		5nn0	⊢ 5 ∈ ℕ0
2		3nn0	⊢ 3 ∈ ℕ0
3		df-4	⊢ 4 = ( 3 + 1 )
4		5t3e15	⊢ ( 5 · 3 ) = ; 1 5
5		1nn0	⊢ 1 ∈ ℕ0
6		eqid	⊢ ; 1 5 = ; 1 5
7		1p1e2	⊢ ( 1 + 1 ) = 2
8		5p5e10	⊢ ( 5 + 5 ) = ; 1 0
9	5 1 1 6 7 8	decaddci2	⊢ ( ; 1 5 + 5 ) = ; 2 0
10	1 2 3 4 9	4t3lem	⊢ ( 5 · 4 ) = ; 2 0