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

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