Metamath Proof Explorer

Theorem lcmgcdeq

Description: Two integers' absolute values are equal iff their least common multiple and greatest common divisor are equal. (Contributed by Steve Rodriguez, 20-Jan-2020)

Ref Expression
Assertion lcmgcdeq 
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M lcm N ) = ( M gcd N ) <-> ( abs ` M ) = ( abs ` N ) ) )

Proof

Step Hyp Ref Expression
1 dvdslcm 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || ( M lcm N ) /\ N || ( M lcm N ) ) )
2 1 simpld 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> M || ( M lcm N ) )
3 2 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M lcm N ) = ( M gcd N ) ) -> M || ( M lcm N ) )
4 gcddvds 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) || M /\ ( M gcd N ) || N ) )
5 4 simprd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) || N )
6 breq1 
 |-  ( ( M lcm N ) = ( M gcd N ) -> ( ( M lcm N ) || N <-> ( M gcd N ) || N ) )
7 5 6 syl5ibrcom 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M lcm N ) = ( M gcd N ) -> ( M lcm N ) || N ) )
8 7 imp 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M lcm N ) = ( M gcd N ) ) -> ( M lcm N ) || N )
9 lcmcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) e. NN0 )
10 9 nn0zd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) e. ZZ )
11 dvdstr 
 |-  ( ( M e. ZZ /\ ( M lcm N ) e. ZZ /\ N e. ZZ ) -> ( ( M || ( M lcm N ) /\ ( M lcm N ) || N ) -> M || N ) )
12 10 11 syl3an2 
 |-  ( ( M e. ZZ /\ ( M e. ZZ /\ N e. ZZ ) /\ N e. ZZ ) -> ( ( M || ( M lcm N ) /\ ( M lcm N ) || N ) -> M || N ) )
13 12 3com12 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( M || ( M lcm N ) /\ ( M lcm N ) || N ) -> M || N ) )
14 13 3expb 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( M || ( M lcm N ) /\ ( M lcm N ) || N ) -> M || N ) )
15 14 anidms 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M || ( M lcm N ) /\ ( M lcm N ) || N ) -> M || N ) )
16 15 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M lcm N ) = ( M gcd N ) ) -> ( ( M || ( M lcm N ) /\ ( M lcm N ) || N ) -> M || N ) )
17 3 8 16 mp2and 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M lcm N ) = ( M gcd N ) ) -> M || N )
18 absdvdsb 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> ( abs ` M ) || N ) )
19 zabscl 
 |-  ( M e. ZZ -> ( abs ` M ) e. ZZ )
20 dvdsabsb 
 |-  ( ( ( abs ` M ) e. ZZ /\ N e. ZZ ) -> ( ( abs ` M ) || N <-> ( abs ` M ) || ( abs ` N ) ) )
21 19 20 sylan 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( abs ` M ) || N <-> ( abs ` M ) || ( abs ` N ) ) )
22 18 21 bitrd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> ( abs ` M ) || ( abs ` N ) ) )
23 22 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M lcm N ) = ( M gcd N ) ) -> ( M || N <-> ( abs ` M ) || ( abs ` N ) ) )
24 17 23 mpbid 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M lcm N ) = ( M gcd N ) ) -> ( abs ` M ) || ( abs ` N ) )
25 1 simprd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> N || ( M lcm N ) )
26 25 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M lcm N ) = ( M gcd N ) ) -> N || ( M lcm N ) )
27 4 simpld 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) || M )
28 breq1 
 |-  ( ( M lcm N ) = ( M gcd N ) -> ( ( M lcm N ) || M <-> ( M gcd N ) || M ) )
29 27 28 syl5ibrcom 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M lcm N ) = ( M gcd N ) -> ( M lcm N ) || M ) )
30 29 imp 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M lcm N ) = ( M gcd N ) ) -> ( M lcm N ) || M )
31 dvdstr 
 |-  ( ( N e. ZZ /\ ( M lcm N ) e. ZZ /\ M e. ZZ ) -> ( ( N || ( M lcm N ) /\ ( M lcm N ) || M ) -> N || M ) )
32 10 31 syl3an2 
 |-  ( ( N e. ZZ /\ ( M e. ZZ /\ N e. ZZ ) /\ M e. ZZ ) -> ( ( N || ( M lcm N ) /\ ( M lcm N ) || M ) -> N || M ) )
33 32 3coml 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( N || ( M lcm N ) /\ ( M lcm N ) || M ) -> N || M ) )
34 33 3expb 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( N || ( M lcm N ) /\ ( M lcm N ) || M ) -> N || M ) )
35 34 anidms 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( N || ( M lcm N ) /\ ( M lcm N ) || M ) -> N || M ) )
36 35 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M lcm N ) = ( M gcd N ) ) -> ( ( N || ( M lcm N ) /\ ( M lcm N ) || M ) -> N || M ) )
37 26 30 36 mp2and 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M lcm N ) = ( M gcd N ) ) -> N || M )
38 absdvdsb 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( N || M <-> ( abs ` N ) || M ) )
39 zabscl 
 |-  ( N e. ZZ -> ( abs ` N ) e. ZZ )
40 dvdsabsb 
 |-  ( ( ( abs ` N ) e. ZZ /\ M e. ZZ ) -> ( ( abs ` N ) || M <-> ( abs ` N ) || ( abs ` M ) ) )
41 39 40 sylan 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( ( abs ` N ) || M <-> ( abs ` N ) || ( abs ` M ) ) )
42 38 41 bitrd 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( N || M <-> ( abs ` N ) || ( abs ` M ) ) )
43 42 ancoms 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( N || M <-> ( abs ` N ) || ( abs ` M ) ) )
44 43 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M lcm N ) = ( M gcd N ) ) -> ( N || M <-> ( abs ` N ) || ( abs ` M ) ) )
45 37 44 mpbid 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M lcm N ) = ( M gcd N ) ) -> ( abs ` N ) || ( abs ` M ) )
46 nn0abscl 
 |-  ( M e. ZZ -> ( abs ` M ) e. NN0 )
47 nn0abscl 
 |-  ( N e. ZZ -> ( abs ` N ) e. NN0 )
48 46 47 anim12i 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( abs ` M ) e. NN0 /\ ( abs ` N ) e. NN0 ) )
49 dvdseq 
 |-  ( ( ( ( abs ` M ) e. NN0 /\ ( abs ` N ) e. NN0 ) /\ ( ( abs ` M ) || ( abs ` N ) /\ ( abs ` N ) || ( abs ` M ) ) ) -> ( abs ` M ) = ( abs ` N ) )
50 48 49 sylan 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( ( abs ` M ) || ( abs ` N ) /\ ( abs ` N ) || ( abs ` M ) ) ) -> ( abs ` M ) = ( abs ` N ) )
51 50 ex 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( abs ` M ) || ( abs ` N ) /\ ( abs ` N ) || ( abs ` M ) ) -> ( abs ` M ) = ( abs ` N ) ) )
52 51 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M lcm N ) = ( M gcd N ) ) -> ( ( ( abs ` M ) || ( abs ` N ) /\ ( abs ` N ) || ( abs ` M ) ) -> ( abs ` M ) = ( abs ` N ) ) )
53 24 45 52 mp2and 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M lcm N ) = ( M gcd N ) ) -> ( abs ` M ) = ( abs ` N ) )
54 lcmid 
 |-  ( ( abs ` M ) e. ZZ -> ( ( abs ` M ) lcm ( abs ` M ) ) = ( abs ` ( abs ` M ) ) )
55 19 54 syl 
 |-  ( M e. ZZ -> ( ( abs ` M ) lcm ( abs ` M ) ) = ( abs ` ( abs ` M ) ) )
56 gcdid 
 |-  ( ( abs ` M ) e. ZZ -> ( ( abs ` M ) gcd ( abs ` M ) ) = ( abs ` ( abs ` M ) ) )
57 19 56 syl 
 |-  ( M e. ZZ -> ( ( abs ` M ) gcd ( abs ` M ) ) = ( abs ` ( abs ` M ) ) )
58 55 57 eqtr4d 
 |-  ( M e. ZZ -> ( ( abs ` M ) lcm ( abs ` M ) ) = ( ( abs ` M ) gcd ( abs ` M ) ) )
59 oveq2 
 |-  ( ( abs ` M ) = ( abs ` N ) -> ( ( abs ` M ) lcm ( abs ` M ) ) = ( ( abs ` M ) lcm ( abs ` N ) ) )
60 oveq2 
 |-  ( ( abs ` M ) = ( abs ` N ) -> ( ( abs ` M ) gcd ( abs ` M ) ) = ( ( abs ` M ) gcd ( abs ` N ) ) )
61 59 60 eqeq12d 
 |-  ( ( abs ` M ) = ( abs ` N ) -> ( ( ( abs ` M ) lcm ( abs ` M ) ) = ( ( abs ` M ) gcd ( abs ` M ) ) <-> ( ( abs ` M ) lcm ( abs ` N ) ) = ( ( abs ` M ) gcd ( abs ` N ) ) ) )
62 58 61 syl5ibcom 
 |-  ( M e. ZZ -> ( ( abs ` M ) = ( abs ` N ) -> ( ( abs ` M ) lcm ( abs ` N ) ) = ( ( abs ` M ) gcd ( abs ` N ) ) ) )
63 62 imp 
 |-  ( ( M e. ZZ /\ ( abs ` M ) = ( abs ` N ) ) -> ( ( abs ` M ) lcm ( abs ` N ) ) = ( ( abs ` M ) gcd ( abs ` N ) ) )
64 63 adantlr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( abs ` M ) = ( abs ` N ) ) -> ( ( abs ` M ) lcm ( abs ` N ) ) = ( ( abs ` M ) gcd ( abs ` N ) ) )
65 lcmabs 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( abs ` M ) lcm ( abs ` N ) ) = ( M lcm N ) )
66 gcdabs 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( abs ` M ) gcd ( abs ` N ) ) = ( M gcd N ) )
67 65 66 eqeq12d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( abs ` M ) lcm ( abs ` N ) ) = ( ( abs ` M ) gcd ( abs ` N ) ) <-> ( M lcm N ) = ( M gcd N ) ) )
68 67 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( abs ` M ) = ( abs ` N ) ) -> ( ( ( abs ` M ) lcm ( abs ` N ) ) = ( ( abs ` M ) gcd ( abs ` N ) ) <-> ( M lcm N ) = ( M gcd N ) ) )
69 64 68 mpbid 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( abs ` M ) = ( abs ` N ) ) -> ( M lcm N ) = ( M gcd N ) )
70 53 69 impbida 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M lcm N ) = ( M gcd N ) <-> ( abs ` M ) = ( abs ` N ) ) )