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\cdot 4=20$$

Proof

Step	Hyp	Ref	Expression
1		5nn0	$$⊢5\in {\mathbb{N}}_0$$
2		3nn0	$$⊢3\in {\mathbb{N}}_0$$
3		df-4	$$⊢4=3+1$$
4		5t3e15	$$⊢5\cdot 3=15$$
5		1nn0	$$⊢1\in {\mathbb{N}}_0$$
6		eqid	$$⊢15=15$$
7		1p1e2	$$⊢1+1=2$$
8		5p5e10	$$⊢5+5=10$$
9	5 1 1 6 7 8	decaddci2	$$⊢15+5=20$$
10	1 2 3 4 9	4t3lem	$$⊢5\cdot 4=20$$