Proof of Theorem lcmgcdeq
Step | Hyp | Ref
| Expression |
1 | | dvdslcm 12023 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ (𝑀 lcm 𝑁) ∧ 𝑁 ∥ (𝑀 lcm 𝑁))) |
2 | 1 | simpld 111 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∥ (𝑀 lcm 𝑁)) |
3 | 2 | adantr 274 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 lcm 𝑁) = (𝑀 gcd 𝑁)) → 𝑀 ∥ (𝑀 lcm 𝑁)) |
4 | | gcddvds 11918 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)) |
5 | 4 | simprd 113 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∥ 𝑁) |
6 | | breq1 3992 |
. . . . . . 7
⊢ ((𝑀 lcm 𝑁) = (𝑀 gcd 𝑁) → ((𝑀 lcm 𝑁) ∥ 𝑁 ↔ (𝑀 gcd 𝑁) ∥ 𝑁)) |
7 | 5, 6 | syl5ibrcom 156 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 lcm 𝑁) = (𝑀 gcd 𝑁) → (𝑀 lcm 𝑁) ∥ 𝑁)) |
8 | 7 | imp 123 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 lcm 𝑁) = (𝑀 gcd 𝑁)) → (𝑀 lcm 𝑁) ∥ 𝑁) |
9 | | lcmcl 12026 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm 𝑁) ∈
ℕ0) |
10 | 9 | nn0zd 9332 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm 𝑁) ∈ ℤ) |
11 | | dvdstr 11790 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ (𝑀 lcm 𝑁) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ (𝑀 lcm 𝑁) ∥ 𝑁) → 𝑀 ∥ 𝑁)) |
12 | 10, 11 | syl3an2 1267 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ (𝑀 lcm 𝑁) ∥ 𝑁) → 𝑀 ∥ 𝑁)) |
13 | 12 | 3com12 1202 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ (𝑀 lcm 𝑁) ∥ 𝑁) → 𝑀 ∥ 𝑁)) |
14 | 13 | 3expb 1199 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ (𝑀 lcm 𝑁) ∥ 𝑁) → 𝑀 ∥ 𝑁)) |
15 | 14 | anidms 395 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ (𝑀 lcm 𝑁) ∥ 𝑁) → 𝑀 ∥ 𝑁)) |
16 | 15 | adantr 274 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 lcm 𝑁) = (𝑀 gcd 𝑁)) → ((𝑀 ∥ (𝑀 lcm 𝑁) ∧ (𝑀 lcm 𝑁) ∥ 𝑁) → 𝑀 ∥ 𝑁)) |
17 | 3, 8, 16 | mp2and 431 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 lcm 𝑁) = (𝑀 gcd 𝑁)) → 𝑀 ∥ 𝑁) |
18 | | absdvdsb 11771 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (abs‘𝑀) ∥ 𝑁)) |
19 | | zabscl 11050 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ →
(abs‘𝑀) ∈
ℤ) |
20 | | dvdsabsb 11772 |
. . . . . . 7
⊢
(((abs‘𝑀)
∈ ℤ ∧ 𝑁
∈ ℤ) → ((abs‘𝑀) ∥ 𝑁 ↔ (abs‘𝑀) ∥ (abs‘𝑁))) |
21 | 19, 20 | sylan 281 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
((abs‘𝑀) ∥
𝑁 ↔ (abs‘𝑀) ∥ (abs‘𝑁))) |
22 | 18, 21 | bitrd 187 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (abs‘𝑀) ∥ (abs‘𝑁))) |
23 | 22 | adantr 274 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 lcm 𝑁) = (𝑀 gcd 𝑁)) → (𝑀 ∥ 𝑁 ↔ (abs‘𝑀) ∥ (abs‘𝑁))) |
24 | 17, 23 | mpbid 146 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 lcm 𝑁) = (𝑀 gcd 𝑁)) → (abs‘𝑀) ∥ (abs‘𝑁)) |
25 | 1 | simprd 113 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∥ (𝑀 lcm 𝑁)) |
26 | 25 | adantr 274 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 lcm 𝑁) = (𝑀 gcd 𝑁)) → 𝑁 ∥ (𝑀 lcm 𝑁)) |
27 | 4 | simpld 111 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∥ 𝑀) |
28 | | breq1 3992 |
. . . . . . 7
⊢ ((𝑀 lcm 𝑁) = (𝑀 gcd 𝑁) → ((𝑀 lcm 𝑁) ∥ 𝑀 ↔ (𝑀 gcd 𝑁) ∥ 𝑀)) |
29 | 27, 28 | syl5ibrcom 156 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 lcm 𝑁) = (𝑀 gcd 𝑁) → (𝑀 lcm 𝑁) ∥ 𝑀)) |
30 | 29 | imp 123 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 lcm 𝑁) = (𝑀 gcd 𝑁)) → (𝑀 lcm 𝑁) ∥ 𝑀) |
31 | | dvdstr 11790 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ (𝑀 lcm 𝑁) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑁 ∥ (𝑀 lcm 𝑁) ∧ (𝑀 lcm 𝑁) ∥ 𝑀) → 𝑁 ∥ 𝑀)) |
32 | 10, 31 | syl3an2 1267 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ∈ ℤ) → ((𝑁 ∥ (𝑀 lcm 𝑁) ∧ (𝑀 lcm 𝑁) ∥ 𝑀) → 𝑁 ∥ 𝑀)) |
33 | 32 | 3coml 1205 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑁 ∥ (𝑀 lcm 𝑁) ∧ (𝑀 lcm 𝑁) ∥ 𝑀) → 𝑁 ∥ 𝑀)) |
34 | 33 | 3expb 1199 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑁 ∥ (𝑀 lcm 𝑁) ∧ (𝑀 lcm 𝑁) ∥ 𝑀) → 𝑁 ∥ 𝑀)) |
35 | 34 | anidms 395 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑁 ∥ (𝑀 lcm 𝑁) ∧ (𝑀 lcm 𝑁) ∥ 𝑀) → 𝑁 ∥ 𝑀)) |
36 | 35 | adantr 274 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 lcm 𝑁) = (𝑀 gcd 𝑁)) → ((𝑁 ∥ (𝑀 lcm 𝑁) ∧ (𝑀 lcm 𝑁) ∥ 𝑀) → 𝑁 ∥ 𝑀)) |
37 | 26, 30, 36 | mp2and 431 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 lcm 𝑁) = (𝑀 gcd 𝑁)) → 𝑁 ∥ 𝑀) |
38 | | absdvdsb 11771 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 ∥ 𝑀 ↔ (abs‘𝑁) ∥ 𝑀)) |
39 | | zabscl 11050 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ →
(abs‘𝑁) ∈
ℤ) |
40 | | dvdsabsb 11772 |
. . . . . . . 8
⊢
(((abs‘𝑁)
∈ ℤ ∧ 𝑀
∈ ℤ) → ((abs‘𝑁) ∥ 𝑀 ↔ (abs‘𝑁) ∥ (abs‘𝑀))) |
41 | 39, 40 | sylan 281 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) →
((abs‘𝑁) ∥
𝑀 ↔ (abs‘𝑁) ∥ (abs‘𝑀))) |
42 | 38, 41 | bitrd 187 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 ∥ 𝑀 ↔ (abs‘𝑁) ∥ (abs‘𝑀))) |
43 | 42 | ancoms 266 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∥ 𝑀 ↔ (abs‘𝑁) ∥ (abs‘𝑀))) |
44 | 43 | adantr 274 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 lcm 𝑁) = (𝑀 gcd 𝑁)) → (𝑁 ∥ 𝑀 ↔ (abs‘𝑁) ∥ (abs‘𝑀))) |
45 | 37, 44 | mpbid 146 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 lcm 𝑁) = (𝑀 gcd 𝑁)) → (abs‘𝑁) ∥ (abs‘𝑀)) |
46 | | nn0abscl 11049 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ →
(abs‘𝑀) ∈
ℕ0) |
47 | | nn0abscl 11049 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ →
(abs‘𝑁) ∈
ℕ0) |
48 | 46, 47 | anim12i 336 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
((abs‘𝑀) ∈
ℕ0 ∧ (abs‘𝑁) ∈
ℕ0)) |
49 | | dvdseq 11808 |
. . . . . 6
⊢
((((abs‘𝑀)
∈ ℕ0 ∧ (abs‘𝑁) ∈ ℕ0) ∧
((abs‘𝑀) ∥
(abs‘𝑁) ∧
(abs‘𝑁) ∥
(abs‘𝑀))) →
(abs‘𝑀) =
(abs‘𝑁)) |
50 | 48, 49 | sylan 281 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧
((abs‘𝑀) ∥
(abs‘𝑁) ∧
(abs‘𝑁) ∥
(abs‘𝑀))) →
(abs‘𝑀) =
(abs‘𝑁)) |
51 | 50 | ex 114 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(((abs‘𝑀) ∥
(abs‘𝑁) ∧
(abs‘𝑁) ∥
(abs‘𝑀)) →
(abs‘𝑀) =
(abs‘𝑁))) |
52 | 51 | adantr 274 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 lcm 𝑁) = (𝑀 gcd 𝑁)) → (((abs‘𝑀) ∥ (abs‘𝑁) ∧ (abs‘𝑁) ∥ (abs‘𝑀)) → (abs‘𝑀) = (abs‘𝑁))) |
53 | 24, 45, 52 | mp2and 431 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 lcm 𝑁) = (𝑀 gcd 𝑁)) → (abs‘𝑀) = (abs‘𝑁)) |
54 | | lcmid 12034 |
. . . . . . . 8
⊢
((abs‘𝑀)
∈ ℤ → ((abs‘𝑀) lcm (abs‘𝑀)) = (abs‘(abs‘𝑀))) |
55 | 19, 54 | syl 14 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ →
((abs‘𝑀) lcm
(abs‘𝑀)) =
(abs‘(abs‘𝑀))) |
56 | | gcdid 11941 |
. . . . . . . 8
⊢
((abs‘𝑀)
∈ ℤ → ((abs‘𝑀) gcd (abs‘𝑀)) = (abs‘(abs‘𝑀))) |
57 | 19, 56 | syl 14 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ →
((abs‘𝑀) gcd
(abs‘𝑀)) =
(abs‘(abs‘𝑀))) |
58 | 55, 57 | eqtr4d 2206 |
. . . . . 6
⊢ (𝑀 ∈ ℤ →
((abs‘𝑀) lcm
(abs‘𝑀)) =
((abs‘𝑀) gcd
(abs‘𝑀))) |
59 | | oveq2 5861 |
. . . . . . 7
⊢
((abs‘𝑀) =
(abs‘𝑁) →
((abs‘𝑀) lcm
(abs‘𝑀)) =
((abs‘𝑀) lcm
(abs‘𝑁))) |
60 | | oveq2 5861 |
. . . . . . 7
⊢
((abs‘𝑀) =
(abs‘𝑁) →
((abs‘𝑀) gcd
(abs‘𝑀)) =
((abs‘𝑀) gcd
(abs‘𝑁))) |
61 | 59, 60 | eqeq12d 2185 |
. . . . . 6
⊢
((abs‘𝑀) =
(abs‘𝑁) →
(((abs‘𝑀) lcm
(abs‘𝑀)) =
((abs‘𝑀) gcd
(abs‘𝑀)) ↔
((abs‘𝑀) lcm
(abs‘𝑁)) =
((abs‘𝑀) gcd
(abs‘𝑁)))) |
62 | 58, 61 | syl5ibcom 154 |
. . . . 5
⊢ (𝑀 ∈ ℤ →
((abs‘𝑀) =
(abs‘𝑁) →
((abs‘𝑀) lcm
(abs‘𝑁)) =
((abs‘𝑀) gcd
(abs‘𝑁)))) |
63 | 62 | imp 123 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧
(abs‘𝑀) =
(abs‘𝑁)) →
((abs‘𝑀) lcm
(abs‘𝑁)) =
((abs‘𝑀) gcd
(abs‘𝑁))) |
64 | 63 | adantlr 474 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧
(abs‘𝑀) =
(abs‘𝑁)) →
((abs‘𝑀) lcm
(abs‘𝑁)) =
((abs‘𝑀) gcd
(abs‘𝑁))) |
65 | | lcmabs 12030 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
((abs‘𝑀) lcm
(abs‘𝑁)) = (𝑀 lcm 𝑁)) |
66 | | gcdabs 11943 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
((abs‘𝑀) gcd
(abs‘𝑁)) = (𝑀 gcd 𝑁)) |
67 | 65, 66 | eqeq12d 2185 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(((abs‘𝑀) lcm
(abs‘𝑁)) =
((abs‘𝑀) gcd
(abs‘𝑁)) ↔
(𝑀 lcm 𝑁) = (𝑀 gcd 𝑁))) |
68 | 67 | adantr 274 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧
(abs‘𝑀) =
(abs‘𝑁)) →
(((abs‘𝑀) lcm
(abs‘𝑁)) =
((abs‘𝑀) gcd
(abs‘𝑁)) ↔
(𝑀 lcm 𝑁) = (𝑀 gcd 𝑁))) |
69 | 64, 68 | mpbid 146 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧
(abs‘𝑀) =
(abs‘𝑁)) →
(𝑀 lcm 𝑁) = (𝑀 gcd 𝑁)) |
70 | 53, 69 | impbida 591 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 lcm 𝑁) = (𝑀 gcd 𝑁) ↔ (abs‘𝑀) = (abs‘𝑁))) |