Proof of Theorem dvdslelem
| Step | Hyp | Ref
| Expression |
| 1 | | dvdslelem.3 |
. . . . . 6
⊢ 𝐾 ∈ ℤ |
| 2 | 1 | zrei 12619 |
. . . . 5
⊢ 𝐾 ∈ ℝ |
| 3 | | 0re 11263 |
. . . . 5
⊢ 0 ∈
ℝ |
| 4 | | lelttric 11368 |
. . . . 5
⊢ ((𝐾 ∈ ℝ ∧ 0 ∈
ℝ) → (𝐾 ≤ 0
∨ 0 < 𝐾)) |
| 5 | 2, 3, 4 | mp2an 692 |
. . . 4
⊢ (𝐾 ≤ 0 ∨ 0 < 𝐾) |
| 6 | | zgt0ge1 12672 |
. . . . . 6
⊢ (𝐾 ∈ ℤ → (0 <
𝐾 ↔ 1 ≤ 𝐾)) |
| 7 | 1, 6 | ax-mp 5 |
. . . . 5
⊢ (0 <
𝐾 ↔ 1 ≤ 𝐾) |
| 8 | 7 | orbi2i 913 |
. . . 4
⊢ ((𝐾 ≤ 0 ∨ 0 < 𝐾) ↔ (𝐾 ≤ 0 ∨ 1 ≤ 𝐾)) |
| 9 | 5, 8 | mpbi 230 |
. . 3
⊢ (𝐾 ≤ 0 ∨ 1 ≤ 𝐾) |
| 10 | | le0neg1 11771 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℝ → (𝐾 ≤ 0 ↔ 0 ≤ -𝐾)) |
| 11 | 2, 10 | ax-mp 5 |
. . . . . . . 8
⊢ (𝐾 ≤ 0 ↔ 0 ≤ -𝐾) |
| 12 | | dvdslelem.2 |
. . . . . . . . . . . 12
⊢ 𝑁 ∈ ℕ |
| 13 | 12 | nngt0i 12305 |
. . . . . . . . . . 11
⊢ 0 <
𝑁 |
| 14 | 12 | nnrei 12275 |
. . . . . . . . . . . 12
⊢ 𝑁 ∈ ℝ |
| 15 | | dvdslelem.1 |
. . . . . . . . . . . . 13
⊢ 𝑀 ∈ ℤ |
| 16 | 15 | zrei 12619 |
. . . . . . . . . . . 12
⊢ 𝑀 ∈ ℝ |
| 17 | 3, 14, 16 | lttri 11387 |
. . . . . . . . . . 11
⊢ ((0 <
𝑁 ∧ 𝑁 < 𝑀) → 0 < 𝑀) |
| 18 | 13, 17 | mpan 690 |
. . . . . . . . . 10
⊢ (𝑁 < 𝑀 → 0 < 𝑀) |
| 19 | 3, 16 | ltlei 11383 |
. . . . . . . . . 10
⊢ (0 <
𝑀 → 0 ≤ 𝑀) |
| 20 | 18, 19 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 < 𝑀 → 0 ≤ 𝑀) |
| 21 | 2 | renegcli 11570 |
. . . . . . . . . 10
⊢ -𝐾 ∈ ℝ |
| 22 | 21, 16 | mulge0i 11810 |
. . . . . . . . 9
⊢ ((0 ≤
-𝐾 ∧ 0 ≤ 𝑀) → 0 ≤ (-𝐾 · 𝑀)) |
| 23 | 20, 22 | sylan2 593 |
. . . . . . . 8
⊢ ((0 ≤
-𝐾 ∧ 𝑁 < 𝑀) → 0 ≤ (-𝐾 · 𝑀)) |
| 24 | 11, 23 | sylanb 581 |
. . . . . . 7
⊢ ((𝐾 ≤ 0 ∧ 𝑁 < 𝑀) → 0 ≤ (-𝐾 · 𝑀)) |
| 25 | 24 | expcom 413 |
. . . . . 6
⊢ (𝑁 < 𝑀 → (𝐾 ≤ 0 → 0 ≤ (-𝐾 · 𝑀))) |
| 26 | 2, 16 | remulcli 11277 |
. . . . . . . 8
⊢ (𝐾 · 𝑀) ∈ ℝ |
| 27 | | le0neg1 11771 |
. . . . . . . 8
⊢ ((𝐾 · 𝑀) ∈ ℝ → ((𝐾 · 𝑀) ≤ 0 ↔ 0 ≤ -(𝐾 · 𝑀))) |
| 28 | 26, 27 | ax-mp 5 |
. . . . . . 7
⊢ ((𝐾 · 𝑀) ≤ 0 ↔ 0 ≤ -(𝐾 · 𝑀)) |
| 29 | 2 | recni 11275 |
. . . . . . . . 9
⊢ 𝐾 ∈ ℂ |
| 30 | 16 | recni 11275 |
. . . . . . . . 9
⊢ 𝑀 ∈ ℂ |
| 31 | 29, 30 | mulneg1i 11709 |
. . . . . . . 8
⊢ (-𝐾 · 𝑀) = -(𝐾 · 𝑀) |
| 32 | 31 | breq2i 5151 |
. . . . . . 7
⊢ (0 ≤
(-𝐾 · 𝑀) ↔ 0 ≤ -(𝐾 · 𝑀)) |
| 33 | 28, 32 | bitr4i 278 |
. . . . . 6
⊢ ((𝐾 · 𝑀) ≤ 0 ↔ 0 ≤ (-𝐾 · 𝑀)) |
| 34 | 25, 33 | imbitrrdi 252 |
. . . . 5
⊢ (𝑁 < 𝑀 → (𝐾 ≤ 0 → (𝐾 · 𝑀) ≤ 0)) |
| 35 | 26, 3, 14 | lelttri 11388 |
. . . . . 6
⊢ (((𝐾 · 𝑀) ≤ 0 ∧ 0 < 𝑁) → (𝐾 · 𝑀) < 𝑁) |
| 36 | 13, 35 | mpan2 691 |
. . . . 5
⊢ ((𝐾 · 𝑀) ≤ 0 → (𝐾 · 𝑀) < 𝑁) |
| 37 | 34, 36 | syl6 35 |
. . . 4
⊢ (𝑁 < 𝑀 → (𝐾 ≤ 0 → (𝐾 · 𝑀) < 𝑁)) |
| 38 | | lemulge12 12131 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ) ∧ (0 ≤
𝑀 ∧ 1 ≤ 𝐾)) → 𝑀 ≤ (𝐾 · 𝑀)) |
| 39 | 16, 2, 38 | mpanl12 702 |
. . . . . . 7
⊢ ((0 ≤
𝑀 ∧ 1 ≤ 𝐾) → 𝑀 ≤ (𝐾 · 𝑀)) |
| 40 | 20, 39 | sylan 580 |
. . . . . 6
⊢ ((𝑁 < 𝑀 ∧ 1 ≤ 𝐾) → 𝑀 ≤ (𝐾 · 𝑀)) |
| 41 | 40 | ex 412 |
. . . . 5
⊢ (𝑁 < 𝑀 → (1 ≤ 𝐾 → 𝑀 ≤ (𝐾 · 𝑀))) |
| 42 | 14, 16, 26 | ltletri 11389 |
. . . . . 6
⊢ ((𝑁 < 𝑀 ∧ 𝑀 ≤ (𝐾 · 𝑀)) → 𝑁 < (𝐾 · 𝑀)) |
| 43 | 42 | ex 412 |
. . . . 5
⊢ (𝑁 < 𝑀 → (𝑀 ≤ (𝐾 · 𝑀) → 𝑁 < (𝐾 · 𝑀))) |
| 44 | 41, 43 | syld 47 |
. . . 4
⊢ (𝑁 < 𝑀 → (1 ≤ 𝐾 → 𝑁 < (𝐾 · 𝑀))) |
| 45 | 37, 44 | orim12d 967 |
. . 3
⊢ (𝑁 < 𝑀 → ((𝐾 ≤ 0 ∨ 1 ≤ 𝐾) → ((𝐾 · 𝑀) < 𝑁 ∨ 𝑁 < (𝐾 · 𝑀)))) |
| 46 | 9, 45 | mpi 20 |
. 2
⊢ (𝑁 < 𝑀 → ((𝐾 · 𝑀) < 𝑁 ∨ 𝑁 < (𝐾 · 𝑀))) |
| 47 | 26, 14 | lttri2i 11375 |
. 2
⊢ ((𝐾 · 𝑀) ≠ 𝑁 ↔ ((𝐾 · 𝑀) < 𝑁 ∨ 𝑁 < (𝐾 · 𝑀))) |
| 48 | 46, 47 | sylibr 234 |
1
⊢ (𝑁 < 𝑀 → (𝐾 · 𝑀) ≠ 𝑁) |