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 ⊢ A ∈ ℤ ∧ B ∈ ℤ → A ⁢ B = B ⁢ A

Proof

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