| Step | Hyp | Ref
| Expression |
| 1 | | zmulcl 12666 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐾 · 𝑀) ∈ ℤ) |
| 2 | 1 | 3adant3 1133 |
. . . . . 6
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 · 𝑀) ∈ ℤ) |
| 3 | | zmulcl 12666 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 · 𝑁) ∈ ℤ) |
| 4 | 3 | 3adant2 1132 |
. . . . . 6
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 · 𝑁) ∈ ℤ) |
| 5 | 2, 4 | jca 511 |
. . . . 5
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) ∈ ℤ ∧ (𝐾 · 𝑁) ∈ ℤ)) |
| 6 | 5 | 3coml 1128 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝐾 · 𝑀) ∈ ℤ ∧ (𝐾 · 𝑁) ∈ ℤ)) |
| 7 | 6 | 3adant3r 1182 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) → ((𝐾 · 𝑀) ∈ ℤ ∧ (𝐾 · 𝑁) ∈ ℤ)) |
| 8 | | 3simpa 1149 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈
ℤ)) |
| 9 | | simpr 484 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) ∧ 𝑥 ∈ ℤ) → 𝑥 ∈
ℤ) |
| 10 | | zcn 12618 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
| 11 | | zcn 12618 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
| 12 | 10, 11 | anim12i 613 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑥 ∈ ℂ ∧ 𝑀 ∈
ℂ)) |
| 13 | | zcn 12618 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
| 14 | | zcn 12618 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℂ) |
| 15 | 14 | anim1i 615 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℤ ∧ 𝐾 ≠ 0) → (𝐾 ∈ ℂ ∧ 𝐾 ≠ 0)) |
| 16 | | mul12 11426 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (𝐾 · (𝑥 · 𝑀)) = (𝑥 · (𝐾 · 𝑀))) |
| 17 | 16 | 3adant1r 1178 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ ℂ ∧ 𝐾 ≠ 0) ∧ 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (𝐾 · (𝑥 · 𝑀)) = (𝑥 · (𝐾 · 𝑀))) |
| 18 | 17 | 3expb 1121 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ ℂ ∧ 𝐾 ≠ 0) ∧ (𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ)) → (𝐾 · (𝑥 · 𝑀)) = (𝑥 · (𝐾 · 𝑀))) |
| 19 | 18 | ancoms 458 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ) ∧ (𝐾 ∈ ℂ ∧ 𝐾 ≠ 0)) → (𝐾 · (𝑥 · 𝑀)) = (𝑥 · (𝐾 · 𝑀))) |
| 20 | 19 | 3adant2 1132 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ) ∧ 𝑁 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝐾 ≠ 0)) → (𝐾 · (𝑥 · 𝑀)) = (𝑥 · (𝐾 · 𝑀))) |
| 21 | 20 | eqeq1d 2739 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ) ∧ 𝑁 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝐾 ≠ 0)) → ((𝐾 · (𝑥 · 𝑀)) = (𝐾 · 𝑁) ↔ (𝑥 · (𝐾 · 𝑀)) = (𝐾 · 𝑁))) |
| 22 | | mulcl 11239 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (𝑥 · 𝑀) ∈ ℂ) |
| 23 | | mulcan 11900 |
. . . . . . . . . . . . 13
⊢ (((𝑥 · 𝑀) ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝐾 ≠ 0)) → ((𝐾 · (𝑥 · 𝑀)) = (𝐾 · 𝑁) ↔ (𝑥 · 𝑀) = 𝑁)) |
| 24 | 22, 23 | syl3an1 1164 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ) ∧ 𝑁 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝐾 ≠ 0)) → ((𝐾 · (𝑥 · 𝑀)) = (𝐾 · 𝑁) ↔ (𝑥 · 𝑀) = 𝑁)) |
| 25 | 21, 24 | bitr3d 281 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ) ∧ 𝑁 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝐾 ≠ 0)) → ((𝑥 · (𝐾 · 𝑀)) = (𝐾 · 𝑁) ↔ (𝑥 · 𝑀) = 𝑁)) |
| 26 | 12, 13, 15, 25 | syl3an 1161 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ 𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) → ((𝑥 · (𝐾 · 𝑀)) = (𝐾 · 𝑁) ↔ (𝑥 · 𝑀) = 𝑁)) |
| 27 | 26 | 3expb 1121 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0))) → ((𝑥 · (𝐾 · 𝑀)) = (𝐾 · 𝑁) ↔ (𝑥 · 𝑀) = 𝑁)) |
| 28 | 27 | 3impa 1110 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0))) → ((𝑥 · (𝐾 · 𝑀)) = (𝐾 · 𝑁) ↔ (𝑥 · 𝑀) = 𝑁)) |
| 29 | 28 | 3coml 1128 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) ∧ 𝑥 ∈ ℤ) → ((𝑥 · (𝐾 · 𝑀)) = (𝐾 · 𝑁) ↔ (𝑥 · 𝑀) = 𝑁)) |
| 30 | 29 | 3expia 1122 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0))) → (𝑥 ∈ ℤ → ((𝑥 · (𝐾 · 𝑀)) = (𝐾 · 𝑁) ↔ (𝑥 · 𝑀) = 𝑁))) |
| 31 | 30 | 3impb 1115 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) → (𝑥 ∈ ℤ → ((𝑥 · (𝐾 · 𝑀)) = (𝐾 · 𝑁) ↔ (𝑥 · 𝑀) = 𝑁))) |
| 32 | 31 | imp 406 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) ∧ 𝑥 ∈ ℤ) → ((𝑥 · (𝐾 · 𝑀)) = (𝐾 · 𝑁) ↔ (𝑥 · 𝑀) = 𝑁)) |
| 33 | 32 | biimpd 229 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) ∧ 𝑥 ∈ ℤ) → ((𝑥 · (𝐾 · 𝑀)) = (𝐾 · 𝑁) → (𝑥 · 𝑀) = 𝑁)) |
| 34 | 7, 8, 9, 33 | dvds1lem 16305 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) → ((𝐾 · 𝑀) ∥ (𝐾 · 𝑁) → 𝑀 ∥ 𝑁)) |
| 35 | | dvdscmul 16320 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ∥ 𝑁 → (𝐾 · 𝑀) ∥ (𝐾 · 𝑁))) |
| 36 | 35 | 3adant3r 1182 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) → (𝑀 ∥ 𝑁 → (𝐾 · 𝑀) ∥ (𝐾 · 𝑁))) |
| 37 | 34, 36 | impbid 212 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) → ((𝐾 · 𝑀) ∥ (𝐾 · 𝑁) ↔ 𝑀 ∥ 𝑁)) |