This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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$

Step	Hyp	Ref	Expression
1		5nn0	$⊢ 5 \in ℕ_{0}$
2		3nn0	$⊢ 3 \in ℕ_{0}$
3		df-4	$⊢ 4 = 3 + 1$
4		5t3e15	$⊢ 5 \cdot 3 = 15$
5		1nn0	$⊢ 1 \in ℕ_{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$