Metamath Proof Explorer

Theorem neglcm

Description: Negating one operand of the lcm operator does not alter the result. (Contributed by Steve Rodriguez, 20-Jan-2020)

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

Proof

Step Hyp Ref Expression
1 lcmneg ⊢N∈ℤ∧M∈ℤ→Nlcm- M=NlcmM
2 1 ancoms ⊢M∈ℤ∧N∈ℤ→Nlcm- M=NlcmM
3 znegcl ⊢M∈ℤ→−M∈ℤ
4 lcmcom ⊢−M∈ℤ∧N∈ℤ→- MlcmN=Nlcm- M
5 3 4 sylan ⊢M∈ℤ∧N∈ℤ→- MlcmN=Nlcm- M
6 lcmcom ⊢M∈ℤ∧N∈ℤ→MlcmN=NlcmM
7 2 5 6 3eqtr4d ⊢M∈ℤ∧N∈ℤ→- MlcmN=MlcmN