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 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) lcm ( abs ‘ 𝑁 ) ) = ( 𝑀 lcm 𝑁 ) )

Proof

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