Metamath Proof Explorer


Theorem mulcomnni

Description: Commutative law for multiplication. (Contributed by metakunt, 25-Apr-2024)

Ref Expression
Hypotheses mulcomnni.1 𝐴 ∈ ℕ
mulcomnni.2 𝐵 ∈ ℕ
Assertion mulcomnni ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 )

Proof

Step Hyp Ref Expression
1 mulcomnni.1 𝐴 ∈ ℕ
2 mulcomnni.2 𝐵 ∈ ℕ
3 1 nncni 𝐴 ∈ ℂ
4 2 nncni 𝐵 ∈ ℂ
5 3 4 mulcomi ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 )