Proof of Theorem coprmdvdsOLD
Step | Hyp | Ref
| Expression |
1 | | zcn 11259 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
2 | | zcn 11259 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
3 | | mulcom 9901 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑀 · 𝑁) = (𝑁 · 𝑀)) |
4 | 1, 2, 3 | syl2an 493 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 · 𝑁) = (𝑁 · 𝑀)) |
5 | 4 | 3adant1 1072 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 · 𝑁) = (𝑁 · 𝑀)) |
6 | 5 | breq2d 4595 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∥ (𝑀 · 𝑁) ↔ 𝐾 ∥ (𝑁 · 𝑀))) |
7 | | dvdsmul2 14842 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → 𝐾 ∥ (𝑁 · 𝐾)) |
8 | 7 | ancoms 468 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝐾 ∥ (𝑁 · 𝐾)) |
9 | 8 | 3adant2 1073 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝐾 ∥ (𝑁 · 𝐾)) |
10 | | simp1 1054 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝐾 ∈
ℤ) |
11 | | zmulcl 11303 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 · 𝐾) ∈ ℤ) |
12 | 11 | ancoms 468 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 · 𝐾) ∈ ℤ) |
13 | 12 | 3adant2 1073 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 · 𝐾) ∈ ℤ) |
14 | | zmulcl 11303 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 · 𝑀) ∈ ℤ) |
15 | 14 | ancoms 468 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 · 𝑀) ∈ ℤ) |
16 | 15 | 3adant1 1072 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 · 𝑀) ∈ ℤ) |
17 | | dvdsgcd 15099 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℤ ∧ (𝑁 · 𝐾) ∈ ℤ ∧ (𝑁 · 𝑀) ∈ ℤ) → ((𝐾 ∥ (𝑁 · 𝐾) ∧ 𝐾 ∥ (𝑁 · 𝑀)) → 𝐾 ∥ ((𝑁 · 𝐾) gcd (𝑁 · 𝑀)))) |
18 | 10, 13, 16, 17 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ (𝑁 · 𝐾) ∧ 𝐾 ∥ (𝑁 · 𝑀)) → 𝐾 ∥ ((𝑁 · 𝐾) gcd (𝑁 · 𝑀)))) |
19 | 9, 18 | mpand 707 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∥ (𝑁 · 𝑀) → 𝐾 ∥ ((𝑁 · 𝐾) gcd (𝑁 · 𝑀)))) |
20 | 6, 19 | sylbid 229 |
. . . . . 6
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∥ (𝑀 · 𝑁) → 𝐾 ∥ ((𝑁 · 𝐾) gcd (𝑁 · 𝑀)))) |
21 | 20 | adantr 480 |
. . . . 5
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑀) = 1) → (𝐾 ∥ (𝑀 · 𝑁) → 𝐾 ∥ ((𝑁 · 𝐾) gcd (𝑁 · 𝑀)))) |
22 | | absmulgcd 15104 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑁 · 𝐾) gcd (𝑁 · 𝑀)) = (abs‘(𝑁 · (𝐾 gcd 𝑀)))) |
23 | 22 | 3coml 1264 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑁 · 𝐾) gcd (𝑁 · 𝑀)) = (abs‘(𝑁 · (𝐾 gcd 𝑀)))) |
24 | 23 | adantr 480 |
. . . . . . . 8
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑀) = 1) → ((𝑁 · 𝐾) gcd (𝑁 · 𝑀)) = (abs‘(𝑁 · (𝐾 gcd 𝑀)))) |
25 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ ((𝐾 gcd 𝑀) = 1 → (𝑁 · (𝐾 gcd 𝑀)) = (𝑁 · 1)) |
26 | 2 | mulid1d 9936 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → (𝑁 · 1) = 𝑁) |
27 | 25, 26 | sylan9eqr 2666 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ (𝐾 gcd 𝑀) = 1) → (𝑁 · (𝐾 gcd 𝑀)) = 𝑁) |
28 | 27 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ (𝐾 gcd 𝑀) = 1) → (abs‘(𝑁 · (𝐾 gcd 𝑀))) = (abs‘𝑁)) |
29 | 28 | 3ad2antl3 1218 |
. . . . . . . 8
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑀) = 1) → (abs‘(𝑁 · (𝐾 gcd 𝑀))) = (abs‘𝑁)) |
30 | 24, 29 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑀) = 1) → ((𝑁 · 𝐾) gcd (𝑁 · 𝑀)) = (abs‘𝑁)) |
31 | 30 | breq2d 4595 |
. . . . . 6
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑀) = 1) → (𝐾 ∥ ((𝑁 · 𝐾) gcd (𝑁 · 𝑀)) ↔ 𝐾 ∥ (abs‘𝑁))) |
32 | | dvdsabsb 14839 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∥ 𝑁 ↔ 𝐾 ∥ (abs‘𝑁))) |
33 | 32 | 3adant2 1073 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∥ 𝑁 ↔ 𝐾 ∥ (abs‘𝑁))) |
34 | 33 | adantr 480 |
. . . . . 6
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑀) = 1) → (𝐾 ∥ 𝑁 ↔ 𝐾 ∥ (abs‘𝑁))) |
35 | 31, 34 | bitr4d 270 |
. . . . 5
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑀) = 1) → (𝐾 ∥ ((𝑁 · 𝐾) gcd (𝑁 · 𝑀)) ↔ 𝐾 ∥ 𝑁)) |
36 | 21, 35 | sylibd 228 |
. . . 4
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 gcd 𝑀) = 1) → (𝐾 ∥ (𝑀 · 𝑁) → 𝐾 ∥ 𝑁)) |
37 | 36 | ex 449 |
. . 3
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 gcd 𝑀) = 1 → (𝐾 ∥ (𝑀 · 𝑁) → 𝐾 ∥ 𝑁))) |
38 | 37 | com23 84 |
. 2
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∥ (𝑀 · 𝑁) → ((𝐾 gcd 𝑀) = 1 → 𝐾 ∥ 𝑁))) |
39 | 38 | impd 446 |
1
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ (𝑀 · 𝑁) ∧ (𝐾 gcd 𝑀) = 1) → 𝐾 ∥ 𝑁)) |