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∈ℤ→MlcmN=MgcdN↔M=N

Proof

Step Hyp Ref Expression
1 dvdslcm ⊢M∈ℤ∧N∈ℤ→M∥MlcmN∧N∥MlcmN
2 1 simpld ⊢M∈ℤ∧N∈ℤ→M∥MlcmN
3 2 adantr ⊢M∈ℤ∧N∈ℤ∧MlcmN=MgcdN→M∥MlcmN
4 gcddvds ⊢M∈ℤ∧N∈ℤ→MgcdN∥M∧MgcdN∥N
5 4 simprd ⊢M∈ℤ∧N∈ℤ→MgcdN∥N
6 breq1 ⊢MlcmN=MgcdN→MlcmN∥N↔MgcdN∥N
7 5 6 syl5ibrcom ⊢M∈ℤ∧N∈ℤ→MlcmN=MgcdN→MlcmN∥N
8 7 imp ⊢M∈ℤ∧N∈ℤ∧MlcmN=MgcdN→MlcmN∥N
9 lcmcl ⊢M∈ℤ∧N∈ℤ→MlcmN∈ℕ0
10 9 nn0zd ⊢M∈ℤ∧N∈ℤ→MlcmN∈ℤ
11 dvdstr ⊢M∈ℤ∧MlcmN∈ℤ∧N∈ℤ→M∥MlcmN∧MlcmN∥N→M∥N
12 10 11 syl3an2 ⊢M∈ℤ∧M∈ℤ∧N∈ℤ∧N∈ℤ→M∥MlcmN∧MlcmN∥N→M∥N
13 12 3com12 ⊢M∈ℤ∧N∈ℤ∧M∈ℤ∧N∈ℤ→M∥MlcmN∧MlcmN∥N→M∥N
14 13 3expb ⊢M∈ℤ∧N∈ℤ∧M∈ℤ∧N∈ℤ→M∥MlcmN∧MlcmN∥N→M∥N
15 14 anidms ⊢M∈ℤ∧N∈ℤ→M∥MlcmN∧MlcmN∥N→M∥N
16 15 adantr ⊢M∈ℤ∧N∈ℤ∧MlcmN=MgcdN→M∥MlcmN∧MlcmN∥N→M∥N
17 3 8 16 mp2and ⊢M∈ℤ∧N∈ℤ∧MlcmN=MgcdN→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∈ℤ∧MlcmN=MgcdN→M∥N↔M∥N
24 17 23 mpbid ⊢M∈ℤ∧N∈ℤ∧MlcmN=MgcdN→M∥N
25 1 simprd ⊢M∈ℤ∧N∈ℤ→N∥MlcmN
26 25 adantr ⊢M∈ℤ∧N∈ℤ∧MlcmN=MgcdN→N∥MlcmN
27 4 simpld ⊢M∈ℤ∧N∈ℤ→MgcdN∥M
28 breq1 ⊢MlcmN=MgcdN→MlcmN∥M↔MgcdN∥M
29 27 28 syl5ibrcom ⊢M∈ℤ∧N∈ℤ→MlcmN=MgcdN→MlcmN∥M
30 29 imp ⊢M∈ℤ∧N∈ℤ∧MlcmN=MgcdN→MlcmN∥M
31 dvdstr ⊢N∈ℤ∧MlcmN∈ℤ∧M∈ℤ→N∥MlcmN∧MlcmN∥M→N∥M
32 10 31 syl3an2 ⊢N∈ℤ∧M∈ℤ∧N∈ℤ∧M∈ℤ→N∥MlcmN∧MlcmN∥M→N∥M
33 32 3coml ⊢M∈ℤ∧N∈ℤ∧M∈ℤ∧N∈ℤ→N∥MlcmN∧MlcmN∥M→N∥M
34 33 3expb ⊢M∈ℤ∧N∈ℤ∧M∈ℤ∧N∈ℤ→N∥MlcmN∧MlcmN∥M→N∥M
35 34 anidms ⊢M∈ℤ∧N∈ℤ→N∥MlcmN∧MlcmN∥M→N∥M
36 35 adantr ⊢M∈ℤ∧N∈ℤ∧MlcmN=MgcdN→N∥MlcmN∧MlcmN∥M→N∥M
37 26 30 36 mp2and ⊢M∈ℤ∧N∈ℤ∧MlcmN=MgcdN→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∈ℤ∧MlcmN=MgcdN→N∥M↔N∥M
45 37 44 mpbid ⊢M∈ℤ∧N∈ℤ∧MlcmN=MgcdN→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∈ℤ∧MlcmN=MgcdN→M∥N∧N∥M→M=N
53 24 45 52 mp2and ⊢M∈ℤ∧N∈ℤ∧MlcmN=MgcdN→M=N
54 lcmid ⊢M∈ℤ→MlcmM=M
55 19 54 syl ⊢M∈ℤ→MlcmM=M
56 gcdid ⊢M∈ℤ→MgcdM=M
57 19 56 syl ⊢M∈ℤ→MgcdM=M
58 55 57 eqtr4d ⊢M∈ℤ→MlcmM=MgcdM
59 oveq2 ⊢M=N→MlcmM=MlcmN
60 oveq2 ⊢M=N→MgcdM=MgcdN
61 59 60 eqeq12d ⊢M=N→MlcmM=MgcdM↔MlcmN=MgcdN
62 58 61 syl5ibcom ⊢M∈ℤ→M=N→MlcmN=MgcdN
63 62 imp ⊢M∈ℤ∧M=N→MlcmN=MgcdN
64 63 adantlr ⊢M∈ℤ∧N∈ℤ∧M=N→MlcmN=MgcdN
65 lcmabs ⊢M∈ℤ∧N∈ℤ→MlcmN=MlcmN
66 gcdabs ⊢M∈ℤ∧N∈ℤ→MgcdN=MgcdN
67 65 66 eqeq12d ⊢M∈ℤ∧N∈ℤ→MlcmN=MgcdN↔MlcmN=MgcdN
68 67 adantr ⊢M∈ℤ∧N∈ℤ∧M=N→MlcmN=MgcdN↔MlcmN=MgcdN
69 64 68 mpbid ⊢M∈ℤ∧N∈ℤ∧M=N→MlcmN=MgcdN
70 53 69 impbida ⊢M∈ℤ∧N∈ℤ→MlcmN=MgcdN↔M=N