Metamath Proof Explorer


Theorem nn0addcom

Description: Addition is commutative for nonnegative integers. Proven without ax-mulcom . (Contributed by SN, 1-Feb-2025)

Ref Expression
Assertion nn0addcom ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )

Proof

Step Hyp Ref Expression
1 elnn0 ( 𝐵 ∈ ℕ0 ↔ ( 𝐵 ∈ ℕ ∨ 𝐵 = 0 ) )
2 elnn0 ( 𝐴 ∈ ℕ0 ↔ ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) )
3 nnaddcom ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )
4 nnre ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
5 readdlid ( 𝐵 ∈ ℝ → ( 0 + 𝐵 ) = 𝐵 )
6 readdrid ( 𝐵 ∈ ℝ → ( 𝐵 + 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 readdrid ( 𝐴 ∈ ℝ → ( 𝐴 + 0 ) = 𝐴 )
18 readdlid ( 𝐴 ∈ ℝ → ( 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 ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )