This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )