Description: Commutative law for multiplication. (Contributed by metakunt, 25-Apr-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mulcomnni.1 | ⊢ 𝐴 ∈ ℕ | |
mulcomnni.2 | ⊢ 𝐵 ∈ ℕ | ||
Assertion | mulcomnni | ⊢ ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mulcomnni.1 | ⊢ 𝐴 ∈ ℕ | |
2 | mulcomnni.2 | ⊢ 𝐵 ∈ ℕ | |
3 | 1 | nncni | ⊢ 𝐴 ∈ ℂ |
4 | 2 | nncni | ⊢ 𝐵 ∈ ℂ |
5 | 3 4 | mulcomi | ⊢ ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) |