Metamath Proof Explorer

Theorem lcmabs

Description: The lcm of two integers is the same as that of their absolute values. (Contributed by Steve Rodriguez, 20-Jan-2020)

Ref Expression
Assertion lcmabs ⊢M∈ℤ∧N∈ℤ→MlcmN=MlcmN

Proof

Step Hyp Ref Expression
1 zre ⊢M∈ℤ→M∈ℝ
2 zre ⊢N∈ℤ→N∈ℝ
3 absor ⊢M∈ℝ→M=M∨M=−M
4 absor ⊢N∈ℝ→N=N∨N=−N
5 3 4 anim12i ⊢M∈ℝ∧N∈ℝ→M=M∨M=−M∧N=N∨N=−N
6 1 2 5 syl2an ⊢M∈ℤ∧N∈ℤ→M=M∨M=−M∧N=N∨N=−N
7 oveq12 ⊢M=M∧N=N→MlcmN=MlcmN
8 7 a1i ⊢M∈ℤ∧N∈ℤ→M=M∧N=N→MlcmN=MlcmN
9 oveq12 ⊢M=−M∧N=N→MlcmN=- MlcmN
10 neglcm ⊢M∈ℤ∧N∈ℤ→- MlcmN=MlcmN
11 9 10 sylan9eqr ⊢M∈ℤ∧N∈ℤ∧M=−M∧N=N→MlcmN=MlcmN
12 11 ex ⊢M∈ℤ∧N∈ℤ→M=−M∧N=N→MlcmN=MlcmN
13 oveq12 ⊢M=M∧N=−N→MlcmN=Mlcm- N
14 lcmneg ⊢M∈ℤ∧N∈ℤ→Mlcm- N=MlcmN
15 13 14 sylan9eqr ⊢M∈ℤ∧N∈ℤ∧M=M∧N=−N→MlcmN=MlcmN
16 15 ex ⊢M∈ℤ∧N∈ℤ→M=M∧N=−N→MlcmN=MlcmN
17 oveq12 ⊢M=−M∧N=−N→MlcmN=- Mlcm- N
18 znegcl ⊢M∈ℤ→−M∈ℤ
19 lcmneg ⊢−M∈ℤ∧N∈ℤ→- Mlcm- N=- MlcmN
20 18 19 sylan ⊢M∈ℤ∧N∈ℤ→- Mlcm- N=- MlcmN
21 20 10 eqtrd ⊢M∈ℤ∧N∈ℤ→- Mlcm- N=MlcmN
22 17 21 sylan9eqr ⊢M∈ℤ∧N∈ℤ∧M=−M∧N=−N→MlcmN=MlcmN
23 22 ex ⊢M∈ℤ∧N∈ℤ→M=−M∧N=−N→MlcmN=MlcmN
24 8 12 16 23 ccased ⊢M∈ℤ∧N∈ℤ→M=M∨M=−M∧N=N∨N=−N→MlcmN=MlcmN
25 6 24 mpd ⊢M∈ℤ∧N∈ℤ→MlcmN=MlcmN