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