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

Proof

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