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

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 → M lcm N = M lcm N
8 7 a1i ⊢ M ∈ ℤ ∧ N ∈ ℤ → M = M ∧ N = N → M lcm N = M lcm N
9 oveq12 ⊢ M = − M ∧ N = N → M lcm N = -M lcm N
10 neglcm ⊢ M ∈ ℤ ∧ N ∈ ℤ → -M lcm N = M lcm N
11 9 10 sylan9eqr ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M = − M ∧ N = N → M lcm N = M lcm N
12 11 ex ⊢ M ∈ ℤ ∧ N ∈ ℤ → M = − M ∧ N = N → M lcm N = M lcm N
13 oveq12 ⊢ M = M ∧ N = − N → M lcm N = M lcm -N
14 lcmneg ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm -N = M lcm N
15 13 14 sylan9eqr ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M = M ∧ N = − N → M lcm N = M lcm N
16 15 ex ⊢ M ∈ ℤ ∧ N ∈ ℤ → M = M ∧ N = − N → M lcm N = M lcm N
17 oveq12 ⊢ M = − M ∧ N = − N → M lcm N = -M lcm -N
18 znegcl ⊢ M ∈ ℤ → − M ∈ ℤ
19 lcmneg ⊢ − M ∈ ℤ ∧ N ∈ ℤ → -M lcm -N = -M lcm N
20 18 19 sylan ⊢ M ∈ ℤ ∧ N ∈ ℤ → -M lcm -N = -M lcm N
21 20 10 eqtrd ⊢ M ∈ ℤ ∧ N ∈ ℤ → -M lcm -N = M lcm N
22 17 21 sylan9eqr ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M = − M ∧ N = − N → M lcm N = M lcm N
23 22 ex ⊢ M ∈ ℤ ∧ N ∈ ℤ → M = − M ∧ N = − N → M lcm N = M lcm N
24 8 12 16 23 ccased ⊢ M ∈ ℤ ∧ N ∈ ℤ → M = M ∨ M = − M ∧ N = N ∨ N = − N → M lcm N = M lcm N
25 6 24 mpd ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm N = M lcm N