Metamath Proof Explorer


Theorem nn0mulcom

Description: Multiplication is commutative for nonnegative integers. Proven without ax-mulcom . (Contributed by SN, 25-Jan-2025)

Ref Expression
Assertion nn0mulcom ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )

Proof

Step Hyp Ref Expression
1 elnn0 ( 𝐵 ∈ ℕ0 ↔ ( 𝐵 ∈ ℕ ∨ 𝐵 = 0 ) )
2 elnn0 ( 𝐴 ∈ ℕ0 ↔ ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) )
3 nnmulcom ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
4 nnre ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
5 remul02 ( 𝐵 ∈ ℝ → ( 0 · 𝐵 ) = 0 )
6 remul01 ( 𝐵 ∈ ℝ → ( 𝐵 · 0 ) = 0 )
7 5 6 eqtr4d ( 𝐵 ∈ ℝ → ( 0 · 𝐵 ) = ( 𝐵 · 0 ) )
8 4 7 syl ( 𝐵 ∈ ℕ → ( 0 · 𝐵 ) = ( 𝐵 · 0 ) )
9 oveq1 ( 𝐴 = 0 → ( 𝐴 · 𝐵 ) = ( 0 · 𝐵 ) )
10 oveq2 ( 𝐴 = 0 → ( 𝐵 · 𝐴 ) = ( 𝐵 · 0 ) )
11 9 10 eqeq12d ( 𝐴 = 0 → ( ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) ↔ ( 0 · 𝐵 ) = ( 𝐵 · 0 ) ) )
12 8 11 syl5ibrcom ( 𝐵 ∈ ℕ → ( 𝐴 = 0 → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) ) )
13 12 impcom ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
14 3 13 jaoian ( ( ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) ∧ 𝐵 ∈ ℕ ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
15 2 14 sylanb ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
16 nn0re ( 𝐴 ∈ ℕ0𝐴 ∈ ℝ )
17 remul01 ( 𝐴 ∈ ℝ → ( 𝐴 · 0 ) = 0 )
18 remul02 ( 𝐴 ∈ ℝ → ( 0 · 𝐴 ) = 0 )
19 17 18 eqtr4d ( 𝐴 ∈ ℝ → ( 𝐴 · 0 ) = ( 0 · 𝐴 ) )
20 16 19 syl ( 𝐴 ∈ ℕ0 → ( 𝐴 · 0 ) = ( 0 · 𝐴 ) )
21 oveq2 ( 𝐵 = 0 → ( 𝐴 · 𝐵 ) = ( 𝐴 · 0 ) )
22 oveq1 ( 𝐵 = 0 → ( 𝐵 · 𝐴 ) = ( 0 · 𝐴 ) )
23 21 22 eqeq12d ( 𝐵 = 0 → ( ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) ↔ ( 𝐴 · 0 ) = ( 0 · 𝐴 ) ) )
24 20 23 syl5ibrcom ( 𝐴 ∈ ℕ0 → ( 𝐵 = 0 → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) ) )
25 24 imp ( ( 𝐴 ∈ ℕ0𝐵 = 0 ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
26 15 25 jaodan ( ( 𝐴 ∈ ℕ0 ∧ ( 𝐵 ∈ ℕ ∨ 𝐵 = 0 ) ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
27 1 26 sylan2b ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )