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

Metamath Proof Explorer

Theorem zaddcom

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

Ref Expression
Assertion zaddcom ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )

Proof

Step Hyp Ref Expression
1 reelznn0nn ⊢ ( 𝐴 ∈ ℤ ↔ ( 𝐴 ∈ ℕ0 ∨ ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ) )
2 reelznn0nn ⊢ ( 𝐵 ∈ ℤ ↔ ( 𝐵 ∈ ℕ0 ∨ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) )
3 nn0addcom ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )
4 zaddcomlem ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )
5 zaddcomlem ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ∧ 𝐴 ∈ ℕ0 ) → ( 𝐵 + 𝐴 ) = ( 𝐴 + 𝐵 ) )
6 5 eqcomd ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ∧ 𝐴 ∈ ℕ0 ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )
7 6 ancoms ⊢ ( ( 𝐴 ∈ ℕ0 ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )
8 renegid2 ⊢ ( 𝐵 ∈ ℝ → ( ( 0 −ℝ 𝐵 ) + 𝐵 ) = 0 )
9 8 ad2antrl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( ( 0 −ℝ 𝐵 ) + 𝐵 ) = 0 )
10 renegid2 ⊢ ( 𝐴 ∈ ℝ → ( ( 0 −ℝ 𝐴 ) + 𝐴 ) = 0 )
11 10 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( ( 0 −ℝ 𝐴 ) + 𝐴 ) = 0 )
12 11 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( ( ( 0 −ℝ 𝐴 ) + 𝐴 ) + 𝐵 ) = ( 0 + 𝐵 ) )
13 simplr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( 0 −ℝ 𝐴 ) ∈ ℕ )
14 13 nncnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( 0 −ℝ 𝐴 ) ∈ ℂ )
15 simpll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → 𝐴 ∈ ℝ )
16 15 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → 𝐴 ∈ ℂ )
17 simprl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → 𝐵 ∈ ℝ )
18 17 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → 𝐵 ∈ ℂ )
19 14 16 18 addassd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( ( ( 0 −ℝ 𝐴 ) + 𝐴 ) + 𝐵 ) = ( ( 0 −ℝ 𝐴 ) + ( 𝐴 + 𝐵 ) ) )
20 readdlid ⊢ ( 𝐵 ∈ ℝ → ( 0 + 𝐵 ) = 𝐵 )
21 20 ad2antrl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( 0 + 𝐵 ) = 𝐵 )
22 12 19 21 3eqtr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( ( 0 −ℝ 𝐴 ) + ( 𝐴 + 𝐵 ) ) = 𝐵 )
23 22 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( ( 0 −ℝ 𝐵 ) + ( ( 0 −ℝ 𝐴 ) + ( 𝐴 + 𝐵 ) ) ) = ( ( 0 −ℝ 𝐵 ) + 𝐵 ) )
24 9 23 11 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( ( 0 −ℝ 𝐵 ) + ( ( 0 −ℝ 𝐴 ) + ( 𝐴 + 𝐵 ) ) ) = ( ( 0 −ℝ 𝐴 ) + 𝐴 ) )
25 simprr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( 0 −ℝ 𝐵 ) ∈ ℕ )
26 25 nncnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( 0 −ℝ 𝐵 ) ∈ ℂ )
27 16 18 addcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( 𝐴 + 𝐵 ) ∈ ℂ )
28 26 14 27 addassd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( ( ( 0 −ℝ 𝐵 ) + ( 0 −ℝ 𝐴 ) ) + ( 𝐴 + 𝐵 ) ) = ( ( 0 −ℝ 𝐵 ) + ( ( 0 −ℝ 𝐴 ) + ( 𝐴 + 𝐵 ) ) ) )
29 9 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( ( ( 0 −ℝ 𝐵 ) + 𝐵 ) + 𝐴 ) = ( 0 + 𝐴 ) )
30 26 18 16 addassd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( ( ( 0 −ℝ 𝐵 ) + 𝐵 ) + 𝐴 ) = ( ( 0 −ℝ 𝐵 ) + ( 𝐵 + 𝐴 ) ) )
31 readdlid ⊢ ( 𝐴 ∈ ℝ → ( 0 + 𝐴 ) = 𝐴 )
32 31 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( 0 + 𝐴 ) = 𝐴 )
33 29 30 32 3eqtr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( ( 0 −ℝ 𝐵 ) + ( 𝐵 + 𝐴 ) ) = 𝐴 )
34 33 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( ( 0 −ℝ 𝐴 ) + ( ( 0 −ℝ 𝐵 ) + ( 𝐵 + 𝐴 ) ) ) = ( ( 0 −ℝ 𝐴 ) + 𝐴 ) )
35 24 28 34 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( ( ( 0 −ℝ 𝐵 ) + ( 0 −ℝ 𝐴 ) ) + ( 𝐴 + 𝐵 ) ) = ( ( 0 −ℝ 𝐴 ) + ( ( 0 −ℝ 𝐵 ) + ( 𝐵 + 𝐴 ) ) ) )
36 nnaddcom ⊢ ( ( ( 0 −ℝ 𝐴 ) ∈ ℕ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) → ( ( 0 −ℝ 𝐴 ) + ( 0 −ℝ 𝐵 ) ) = ( ( 0 −ℝ 𝐵 ) + ( 0 −ℝ 𝐴 ) ) )
37 36 ad2ant2l ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( ( 0 −ℝ 𝐴 ) + ( 0 −ℝ 𝐵 ) ) = ( ( 0 −ℝ 𝐵 ) + ( 0 −ℝ 𝐴 ) ) )
38 37 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( ( ( 0 −ℝ 𝐴 ) + ( 0 −ℝ 𝐵 ) ) + ( 𝐴 + 𝐵 ) ) = ( ( ( 0 −ℝ 𝐵 ) + ( 0 −ℝ 𝐴 ) ) + ( 𝐴 + 𝐵 ) ) )
39 18 16 addcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( 𝐵 + 𝐴 ) ∈ ℂ )
40 14 26 39 addassd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( ( ( 0 −ℝ 𝐴 ) + ( 0 −ℝ 𝐵 ) ) + ( 𝐵 + 𝐴 ) ) = ( ( 0 −ℝ 𝐴 ) + ( ( 0 −ℝ 𝐵 ) + ( 𝐵 + 𝐴 ) ) ) )
41 35 38 40 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( ( ( 0 −ℝ 𝐴 ) + ( 0 −ℝ 𝐵 ) ) + ( 𝐴 + 𝐵 ) ) = ( ( ( 0 −ℝ 𝐴 ) + ( 0 −ℝ 𝐵 ) ) + ( 𝐵 + 𝐴 ) ) )
42 13 25 nnaddcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( ( 0 −ℝ 𝐴 ) + ( 0 −ℝ 𝐵 ) ) ∈ ℕ )
43 42 nncnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( ( 0 −ℝ 𝐴 ) + ( 0 −ℝ 𝐵 ) ) ∈ ℂ )
44 43 27 39 sn-addcand ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( ( ( ( 0 −ℝ 𝐴 ) + ( 0 −ℝ 𝐵 ) ) + ( 𝐴 + 𝐵 ) ) = ( ( ( 0 −ℝ 𝐴 ) + ( 0 −ℝ 𝐵 ) ) + ( 𝐵 + 𝐴 ) ) ↔ ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) ) )
45 41 44 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )
46 3 4 7 45 ccase ⊢ ( ( ( 𝐴 ∈ ℕ0 ∨ ( 𝐴 ∈ ℝ ∧ ( 0 −ℝ 𝐴 ) ∈ ℕ ) ) ∧ ( 𝐵 ∈ ℕ0 ∨ ( 𝐵 ∈ ℝ ∧ ( 0 −ℝ 𝐵 ) ∈ ℕ ) ) ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )
47 1 2 46 syl2anb ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )