This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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