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 e. ZZ /\ N e. ZZ ) -> ( ( abs ` M ) lcm ( abs ` N ) ) = ( M lcm N ) )

Proof

Step Hyp Ref Expression
1 zre 
 |-  ( M e. ZZ -> M e. RR )
2 zre 
 |-  ( N e. ZZ -> N e. RR )
3 absor 
 |-  ( M e. RR -> ( ( abs ` M ) = M \/ ( abs ` M ) = -u M ) )
4 absor 
 |-  ( N e. RR -> ( ( abs ` N ) = N \/ ( abs ` N ) = -u N ) )
5 3 4 anim12i 
 |-  ( ( M e. RR /\ N e. RR ) -> ( ( ( abs ` M ) = M \/ ( abs ` M ) = -u M ) /\ ( ( abs ` N ) = N \/ ( abs ` N ) = -u N ) ) )
6 1 2 5 syl2an 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( abs ` M ) = M \/ ( abs ` M ) = -u M ) /\ ( ( abs ` N ) = N \/ ( abs ` N ) = -u N ) ) )
7 oveq12 
 |-  ( ( ( abs ` M ) = M /\ ( abs ` N ) = N ) -> ( ( abs ` M ) lcm ( abs ` N ) ) = ( M lcm N ) )
8 7 a1i 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( abs ` M ) = M /\ ( abs ` N ) = N ) -> ( ( abs ` M ) lcm ( abs ` N ) ) = ( M lcm N ) ) )
9 oveq12 
 |-  ( ( ( abs ` M ) = -u M /\ ( abs ` N ) = N ) -> ( ( abs ` M ) lcm ( abs ` N ) ) = ( -u M lcm N ) )
10 neglcm 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( -u M lcm N ) = ( M lcm N ) )
11 9 10 sylan9eqr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( ( abs ` M ) = -u M /\ ( abs ` N ) = N ) ) -> ( ( abs ` M ) lcm ( abs ` N ) ) = ( M lcm N ) )
12 11 ex 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( abs ` M ) = -u M /\ ( abs ` N ) = N ) -> ( ( abs ` M ) lcm ( abs ` N ) ) = ( M lcm N ) ) )
13 oveq12 
 |-  ( ( ( abs ` M ) = M /\ ( abs ` N ) = -u N ) -> ( ( abs ` M ) lcm ( abs ` N ) ) = ( M lcm -u N ) )
14 lcmneg 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm -u N ) = ( M lcm N ) )
15 13 14 sylan9eqr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( ( abs ` M ) = M /\ ( abs ` N ) = -u N ) ) -> ( ( abs ` M ) lcm ( abs ` N ) ) = ( M lcm N ) )
16 15 ex 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( abs ` M ) = M /\ ( abs ` N ) = -u N ) -> ( ( abs ` M ) lcm ( abs ` N ) ) = ( M lcm N ) ) )
17 oveq12 
 |-  ( ( ( abs ` M ) = -u M /\ ( abs ` N ) = -u N ) -> ( ( abs ` M ) lcm ( abs ` N ) ) = ( -u M lcm -u N ) )
18 znegcl 
 |-  ( M e. ZZ -> -u M e. ZZ )
19 lcmneg 
 |-  ( ( -u M e. ZZ /\ N e. ZZ ) -> ( -u M lcm -u N ) = ( -u M lcm N ) )
20 18 19 sylan 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( -u M lcm -u N ) = ( -u M lcm N ) )
21 20 10 eqtrd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( -u M lcm -u N ) = ( M lcm N ) )
22 17 21 sylan9eqr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( ( abs ` M ) = -u M /\ ( abs ` N ) = -u N ) ) -> ( ( abs ` M ) lcm ( abs ` N ) ) = ( M lcm N ) )
23 22 ex 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( abs ` M ) = -u M /\ ( abs ` N ) = -u N ) -> ( ( abs ` M ) lcm ( abs ` N ) ) = ( M lcm N ) ) )
24 8 12 16 23 ccased 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( ( abs ` M ) = M \/ ( abs ` M ) = -u M ) /\ ( ( abs ` N ) = N \/ ( abs ` N ) = -u N ) ) -> ( ( abs ` M ) lcm ( abs ` N ) ) = ( M lcm N ) ) )
25 6 24 mpd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( abs ` M ) lcm ( abs ` N ) ) = ( M lcm N ) )