Metamath Proof Explorer


Theorem 4t5e20

Description: 4 times 5 equals 20. (Contributed by SN, 30-Mar-2025)

Ref Expression
Assertion 4t5e20 ( 4 · 5 ) = 2 0

Proof

Step Hyp Ref Expression
1 5cn 5 ∈ ℂ
2 4cn 4 ∈ ℂ
3 5t4e20 ( 5 · 4 ) = 2 0
4 1 2 3 mulcomli ( 4 · 5 ) = 2 0