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