Proof of Theorem dvdslelemd
Step | Hyp | Ref
| Expression |
1 | | dvdslelemd.3 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ ℤ) |
2 | | 0z 9223 |
. . . . 5
⊢ 0 ∈
ℤ |
3 | | zlelttric 9257 |
. . . . 5
⊢ ((𝐾 ∈ ℤ ∧ 0 ∈
ℤ) → (𝐾 ≤ 0
∨ 0 < 𝐾)) |
4 | 1, 2, 3 | sylancl 411 |
. . . 4
⊢ (𝜑 → (𝐾 ≤ 0 ∨ 0 < 𝐾)) |
5 | | zgt0ge1 9270 |
. . . . . 6
⊢ (𝐾 ∈ ℤ → (0 <
𝐾 ↔ 1 ≤ 𝐾)) |
6 | 1, 5 | syl 14 |
. . . . 5
⊢ (𝜑 → (0 < 𝐾 ↔ 1 ≤ 𝐾)) |
7 | 6 | orbi2d 785 |
. . . 4
⊢ (𝜑 → ((𝐾 ≤ 0 ∨ 0 < 𝐾) ↔ (𝐾 ≤ 0 ∨ 1 ≤ 𝐾))) |
8 | 4, 7 | mpbid 146 |
. . 3
⊢ (𝜑 → (𝐾 ≤ 0 ∨ 1 ≤ 𝐾)) |
9 | 1 | zred 9334 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ ℝ) |
10 | 9 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 ≤ 0) → 𝐾 ∈ ℝ) |
11 | | dvdslelemd.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
12 | 11 | zred 9334 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℝ) |
13 | 12 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 ≤ 0) → 𝑀 ∈ ℝ) |
14 | 10, 13 | remulcld 7950 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 ≤ 0) → (𝐾 · 𝑀) ∈ ℝ) |
15 | | 0red 7921 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 ≤ 0) → 0 ∈
ℝ) |
16 | | dvdslelemd.2 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
17 | 16 | nnred 8891 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℝ) |
18 | 17 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 ≤ 0) → 𝑁 ∈ ℝ) |
19 | 10 | renegcld 8299 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 ≤ 0) → -𝐾 ∈ ℝ) |
20 | 9 | le0neg1d 8436 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 ≤ 0 ↔ 0 ≤ -𝐾)) |
21 | 20 | biimpa 294 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 ≤ 0) → 0 ≤ -𝐾) |
22 | | 0red 7921 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℝ) |
23 | 16 | nngt0d 8922 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < 𝑁) |
24 | | dvdslelemd.lt |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 < 𝑀) |
25 | 22, 17, 12, 23, 24 | lttrd 8045 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < 𝑀) |
26 | 22, 12, 25 | ltled 8038 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ 𝑀) |
27 | 26 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 ≤ 0) → 0 ≤ 𝑀) |
28 | 19, 13, 21, 27 | mulge0d 8540 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 ≤ 0) → 0 ≤ (-𝐾 · 𝑀)) |
29 | 14 | le0neg1d 8436 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 ≤ 0) → ((𝐾 · 𝑀) ≤ 0 ↔ 0 ≤ -(𝐾 · 𝑀))) |
30 | 10 | recnd 7948 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ≤ 0) → 𝐾 ∈ ℂ) |
31 | 13 | recnd 7948 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐾 ≤ 0) → 𝑀 ∈ ℂ) |
32 | 30, 31 | mulneg1d 8330 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐾 ≤ 0) → (-𝐾 · 𝑀) = -(𝐾 · 𝑀)) |
33 | 32 | breq2d 4001 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐾 ≤ 0) → (0 ≤ (-𝐾 · 𝑀) ↔ 0 ≤ -(𝐾 · 𝑀))) |
34 | 29, 33 | bitr4d 190 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐾 ≤ 0) → ((𝐾 · 𝑀) ≤ 0 ↔ 0 ≤ (-𝐾 · 𝑀))) |
35 | 28, 34 | mpbird 166 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 ≤ 0) → (𝐾 · 𝑀) ≤ 0) |
36 | 23 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐾 ≤ 0) → 0 < 𝑁) |
37 | 14, 15, 18, 35, 36 | lelttrd 8044 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 ≤ 0) → (𝐾 · 𝑀) < 𝑁) |
38 | 37 | ex 114 |
. . . 4
⊢ (𝜑 → (𝐾 ≤ 0 → (𝐾 · 𝑀) < 𝑁)) |
39 | 17 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ 1 ≤ 𝐾) → 𝑁 ∈ ℝ) |
40 | 12 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ 1 ≤ 𝐾) → 𝑀 ∈ ℝ) |
41 | 9 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 1 ≤ 𝐾) → 𝐾 ∈ ℝ) |
42 | 41, 40 | remulcld 7950 |
. . . . . 6
⊢ ((𝜑 ∧ 1 ≤ 𝐾) → (𝐾 · 𝑀) ∈ ℝ) |
43 | 24 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ 1 ≤ 𝐾) → 𝑁 < 𝑀) |
44 | 26 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 1 ≤ 𝐾) → 0 ≤ 𝑀) |
45 | | simpr 109 |
. . . . . . 7
⊢ ((𝜑 ∧ 1 ≤ 𝐾) → 1 ≤ 𝐾) |
46 | 40, 41, 44, 45 | lemulge12d 8854 |
. . . . . 6
⊢ ((𝜑 ∧ 1 ≤ 𝐾) → 𝑀 ≤ (𝐾 · 𝑀)) |
47 | 39, 40, 42, 43, 46 | ltletrd 8342 |
. . . . 5
⊢ ((𝜑 ∧ 1 ≤ 𝐾) → 𝑁 < (𝐾 · 𝑀)) |
48 | 47 | ex 114 |
. . . 4
⊢ (𝜑 → (1 ≤ 𝐾 → 𝑁 < (𝐾 · 𝑀))) |
49 | 38, 48 | orim12d 781 |
. . 3
⊢ (𝜑 → ((𝐾 ≤ 0 ∨ 1 ≤ 𝐾) → ((𝐾 · 𝑀) < 𝑁 ∨ 𝑁 < (𝐾 · 𝑀)))) |
50 | 8, 49 | mpd 13 |
. 2
⊢ (𝜑 → ((𝐾 · 𝑀) < 𝑁 ∨ 𝑁 < (𝐾 · 𝑀))) |
51 | | zq 9585 |
. . . . 5
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℚ) |
52 | 1, 51 | syl 14 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ ℚ) |
53 | | zq 9585 |
. . . . 5
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℚ) |
54 | 11, 53 | syl 14 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℚ) |
55 | | qmulcl 9596 |
. . . 4
⊢ ((𝐾 ∈ ℚ ∧ 𝑀 ∈ ℚ) → (𝐾 · 𝑀) ∈ ℚ) |
56 | 52, 54, 55 | syl2anc 409 |
. . 3
⊢ (𝜑 → (𝐾 · 𝑀) ∈ ℚ) |
57 | | nnq 9592 |
. . . 4
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℚ) |
58 | 16, 57 | syl 14 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℚ) |
59 | | qlttri2 9600 |
. . 3
⊢ (((𝐾 · 𝑀) ∈ ℚ ∧ 𝑁 ∈ ℚ) → ((𝐾 · 𝑀) ≠ 𝑁 ↔ ((𝐾 · 𝑀) < 𝑁 ∨ 𝑁 < (𝐾 · 𝑀)))) |
60 | 56, 58, 59 | syl2anc 409 |
. 2
⊢ (𝜑 → ((𝐾 · 𝑀) ≠ 𝑁 ↔ ((𝐾 · 𝑀) < 𝑁 ∨ 𝑁 < (𝐾 · 𝑀)))) |
61 | 50, 60 | mpbird 166 |
1
⊢ (𝜑 → (𝐾 · 𝑀) ≠ 𝑁) |