Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Arithmetic theorems
4t5e20
Next ⟩
sq9
Metamath Proof Explorer
Ascii
Unicode
Theorem
4t5e20
Description:
4 times 5 equals 20.
(Contributed by
SN
, 30-Mar-2025)
Ref
Expression
Assertion
4t5e20
⊢
4
⋅
5
=
20
Proof
Step
Hyp
Ref
Expression
1
5cn
⊢
5
∈
ℂ
2
4cn
⊢
4
∈
ℂ
3
5t4e20
⊢
5
⋅
4
=
20
4
1
2
3
mulcomli
⊢
4
⋅
5
=
20