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