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 ∈ ℤ → -M lcm N = M lcm N

Proof

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