Metamath Proof Explorer


Theorem zmulcom

Description: Multiplication is commutative for integers. Proven without ax-mulcom . From this result and grpcominv1 , we can show that rationals commute under multiplication without using ax-mulcom . (Contributed by SN, 25-Jan-2025)

Ref Expression
Assertion zmulcom ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )

Proof

Step Hyp Ref Expression
1 reelznn0nn ( 𝐴 ∈ ℤ ↔ ( 𝐴 ∈ ℕ0 ∨ ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ) )
2 reelznn0nn ( 𝐵 ∈ ℤ ↔ ( 𝐵 ∈ ℕ0 ∨ ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ) )
3 nn0mulcom ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ0 ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
4 zmulcomlem ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
5 zmulcomlem ( ( ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ∧ 𝐴 ∈ ℕ0 ) → ( 𝐵 · 𝐴 ) = ( 𝐴 · 𝐵 ) )
6 5 eqcomd ( ( ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ∧ 𝐴 ∈ ℕ0 ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
7 6 ancoms ( ( 𝐴 ∈ ℕ0 ∧ ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
8 nnmulcom ( ( ( 0 − 𝐴 ) ∈ ℕ ∧ ( 0 − 𝐵 ) ∈ ℕ ) → ( ( 0 − 𝐴 ) · ( 0 − 𝐵 ) ) = ( ( 0 − 𝐵 ) · ( 0 − 𝐴 ) ) )
9 8 ad2ant2l ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ) → ( ( 0 − 𝐴 ) · ( 0 − 𝐵 ) ) = ( ( 0 − 𝐵 ) · ( 0 − 𝐴 ) ) )
10 9 oveq2d ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ) → ( 0 − ( ( 0 − 𝐴 ) · ( 0 − 𝐵 ) ) ) = ( 0 − ( ( 0 − 𝐵 ) · ( 0 − 𝐴 ) ) ) )
11 rernegcl ( 𝐴 ∈ ℝ → ( 0 − 𝐴 ) ∈ ℝ )
12 11 ad2antrr ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ) → ( 0 − 𝐴 ) ∈ ℝ )
13 simprr ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ) → ( 0 − 𝐵 ) ∈ ℕ )
14 12 13 renegmulnnass ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ) → ( ( 0 − ( 0 − 𝐴 ) ) · ( 0 − 𝐵 ) ) = ( 0 − ( ( 0 − 𝐴 ) · ( 0 − 𝐵 ) ) ) )
15 rernegcl ( 𝐵 ∈ ℝ → ( 0 − 𝐵 ) ∈ ℝ )
16 15 ad2antrl ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ) → ( 0 − 𝐵 ) ∈ ℝ )
17 simplr ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ) → ( 0 − 𝐴 ) ∈ ℕ )
18 16 17 renegmulnnass ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ) → ( ( 0 − ( 0 − 𝐵 ) ) · ( 0 − 𝐴 ) ) = ( 0 − ( ( 0 − 𝐵 ) · ( 0 − 𝐴 ) ) ) )
19 10 14 18 3eqtr4d ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ) → ( ( 0 − ( 0 − 𝐴 ) ) · ( 0 − 𝐵 ) ) = ( ( 0 − ( 0 − 𝐵 ) ) · ( 0 − 𝐴 ) ) )
20 19 oveq2d ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ) → ( 0 − ( ( 0 − ( 0 − 𝐴 ) ) · ( 0 − 𝐵 ) ) ) = ( 0 − ( ( 0 − ( 0 − 𝐵 ) ) · ( 0 − 𝐴 ) ) ) )
21 rernegcl ( ( 0 − 𝐴 ) ∈ ℝ → ( 0 − ( 0 − 𝐴 ) ) ∈ ℝ )
22 11 21 syl ( 𝐴 ∈ ℝ → ( 0 − ( 0 − 𝐴 ) ) ∈ ℝ )
23 22 ad2antrr ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ) → ( 0 − ( 0 − 𝐴 ) ) ∈ ℝ )
24 23 16 remulneg2d ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ) → ( ( 0 − ( 0 − 𝐴 ) ) · ( 0 − ( 0 − 𝐵 ) ) ) = ( 0 − ( ( 0 − ( 0 − 𝐴 ) ) · ( 0 − 𝐵 ) ) ) )
25 rernegcl ( ( 0 − 𝐵 ) ∈ ℝ → ( 0 − ( 0 − 𝐵 ) ) ∈ ℝ )
26 15 25 syl ( 𝐵 ∈ ℝ → ( 0 − ( 0 − 𝐵 ) ) ∈ ℝ )
27 26 ad2antrl ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ) → ( 0 − ( 0 − 𝐵 ) ) ∈ ℝ )
28 27 12 remulneg2d ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ) → ( ( 0 − ( 0 − 𝐵 ) ) · ( 0 − ( 0 − 𝐴 ) ) ) = ( 0 − ( ( 0 − ( 0 − 𝐵 ) ) · ( 0 − 𝐴 ) ) ) )
29 20 24 28 3eqtr4d ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ) → ( ( 0 − ( 0 − 𝐴 ) ) · ( 0 − ( 0 − 𝐵 ) ) ) = ( ( 0 − ( 0 − 𝐵 ) ) · ( 0 − ( 0 − 𝐴 ) ) ) )
30 renegneg ( 𝐴 ∈ ℝ → ( 0 − ( 0 − 𝐴 ) ) = 𝐴 )
31 30 ad2antrr ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ) → ( 0 − ( 0 − 𝐴 ) ) = 𝐴 )
32 renegneg ( 𝐵 ∈ ℝ → ( 0 − ( 0 − 𝐵 ) ) = 𝐵 )
33 32 ad2antrl ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ) → ( 0 − ( 0 − 𝐵 ) ) = 𝐵 )
34 31 33 oveq12d ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ) → ( ( 0 − ( 0 − 𝐴 ) ) · ( 0 − ( 0 − 𝐵 ) ) ) = ( 𝐴 · 𝐵 ) )
35 33 31 oveq12d ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ) → ( ( 0 − ( 0 − 𝐵 ) ) · ( 0 − ( 0 − 𝐴 ) ) ) = ( 𝐵 · 𝐴 ) )
36 29 34 35 3eqtr3d ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
37 3 4 7 36 ccase ( ( ( 𝐴 ∈ ℕ0 ∨ ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ) ∧ ( 𝐵 ∈ ℕ0 ∨ ( 𝐵 ∈ ℝ ∧ ( 0 − 𝐵 ) ∈ ℕ ) ) ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
38 1 2 37 syl2anb ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )