Step | Hyp | Ref
| Expression |
1 | | divalglem5.5 |
. . . . . 6
⊢ 𝑅 = inf(𝑆, ℝ, < ) |
2 | | divalglem0.1 |
. . . . . . 7
⊢ 𝑁 ∈ ℤ |
3 | | divalglem0.2 |
. . . . . . 7
⊢ 𝐷 ∈ ℤ |
4 | | divalglem1.3 |
. . . . . . 7
⊢ 𝐷 ≠ 0 |
5 | | divalglem2.4 |
. . . . . . 7
⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} |
6 | 2, 3, 4, 5 | divalglem2 14956 |
. . . . . 6
⊢ inf(𝑆, ℝ, < ) ∈ 𝑆 |
7 | 1, 6 | eqeltri 2684 |
. . . . 5
⊢ 𝑅 ∈ 𝑆 |
8 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑥 = 𝑅 → (𝑁 − 𝑥) = (𝑁 − 𝑅)) |
9 | 8 | breq2d 4595 |
. . . . . 6
⊢ (𝑥 = 𝑅 → (𝐷 ∥ (𝑁 − 𝑥) ↔ 𝐷 ∥ (𝑁 − 𝑅))) |
10 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑟 = 𝑥 → (𝑁 − 𝑟) = (𝑁 − 𝑥)) |
11 | 10 | breq2d 4595 |
. . . . . . . 8
⊢ (𝑟 = 𝑥 → (𝐷 ∥ (𝑁 − 𝑟) ↔ 𝐷 ∥ (𝑁 − 𝑥))) |
12 | 11 | cbvrabv 3172 |
. . . . . . 7
⊢ {𝑟 ∈ ℕ0
∣ 𝐷 ∥ (𝑁 − 𝑟)} = {𝑥 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑥)} |
13 | 5, 12 | eqtri 2632 |
. . . . . 6
⊢ 𝑆 = {𝑥 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑥)} |
14 | 9, 13 | elrab2 3333 |
. . . . 5
⊢ (𝑅 ∈ 𝑆 ↔ (𝑅 ∈ ℕ0 ∧ 𝐷 ∥ (𝑁 − 𝑅))) |
15 | 7, 14 | mpbi 219 |
. . . 4
⊢ (𝑅 ∈ ℕ0
∧ 𝐷 ∥ (𝑁 − 𝑅)) |
16 | 15 | simpli 473 |
. . 3
⊢ 𝑅 ∈
ℕ0 |
17 | 16 | nn0ge0i 11197 |
. 2
⊢ 0 ≤
𝑅 |
18 | | nnabscl 13913 |
. . . . . . 7
⊢ ((𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → (abs‘𝐷) ∈
ℕ) |
19 | 3, 4, 18 | mp2an 704 |
. . . . . 6
⊢
(abs‘𝐷) ∈
ℕ |
20 | 19 | nngt0i 10931 |
. . . . 5
⊢ 0 <
(abs‘𝐷) |
21 | | 0re 9919 |
. . . . . 6
⊢ 0 ∈
ℝ |
22 | | zcn 11259 |
. . . . . . . 8
⊢ (𝐷 ∈ ℤ → 𝐷 ∈
ℂ) |
23 | 3, 22 | ax-mp 5 |
. . . . . . 7
⊢ 𝐷 ∈ ℂ |
24 | 23 | abscli 13982 |
. . . . . 6
⊢
(abs‘𝐷) ∈
ℝ |
25 | 21, 24 | ltnlei 10037 |
. . . . 5
⊢ (0 <
(abs‘𝐷) ↔ ¬
(abs‘𝐷) ≤
0) |
26 | 20, 25 | mpbi 219 |
. . . 4
⊢ ¬
(abs‘𝐷) ≤
0 |
27 | | ssrab2 3650 |
. . . . . . . . 9
⊢ {𝑟 ∈ ℕ0
∣ 𝐷 ∥ (𝑁 − 𝑟)} ⊆
ℕ0 |
28 | 5, 27 | eqsstri 3598 |
. . . . . . . 8
⊢ 𝑆 ⊆
ℕ0 |
29 | | nn0uz 11598 |
. . . . . . . 8
⊢
ℕ0 = (ℤ≥‘0) |
30 | 28, 29 | sseqtri 3600 |
. . . . . . 7
⊢ 𝑆 ⊆
(ℤ≥‘0) |
31 | | nn0abscl 13900 |
. . . . . . . . . 10
⊢ (𝐷 ∈ ℤ →
(abs‘𝐷) ∈
ℕ0) |
32 | 3, 31 | ax-mp 5 |
. . . . . . . . 9
⊢
(abs‘𝐷) ∈
ℕ0 |
33 | | nn0sub2 11315 |
. . . . . . . . 9
⊢
(((abs‘𝐷)
∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧
(abs‘𝐷) ≤ 𝑅) → (𝑅 − (abs‘𝐷)) ∈
ℕ0) |
34 | 32, 16, 33 | mp3an12 1406 |
. . . . . . . 8
⊢
((abs‘𝐷) ≤
𝑅 → (𝑅 − (abs‘𝐷)) ∈
ℕ0) |
35 | 15 | a1i 11 |
. . . . . . . . 9
⊢
((abs‘𝐷) ≤
𝑅 → (𝑅 ∈ ℕ0 ∧ 𝐷 ∥ (𝑁 − 𝑅))) |
36 | | nn0z 11277 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℕ0
→ 𝑅 ∈
ℤ) |
37 | | 1z 11284 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℤ |
38 | 2, 3 | divalglem0 14954 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℤ ∧ 1 ∈
ℤ) → (𝐷 ∥
(𝑁 − 𝑅) → 𝐷 ∥ (𝑁 − (𝑅 − (1 · (abs‘𝐷)))))) |
39 | 37, 38 | mpan2 703 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℤ → (𝐷 ∥ (𝑁 − 𝑅) → 𝐷 ∥ (𝑁 − (𝑅 − (1 · (abs‘𝐷)))))) |
40 | 24 | recni 9931 |
. . . . . . . . . . . . . . . 16
⊢
(abs‘𝐷) ∈
ℂ |
41 | 40 | mulid2i 9922 |
. . . . . . . . . . . . . . 15
⊢ (1
· (abs‘𝐷)) =
(abs‘𝐷) |
42 | 41 | oveq2i 6560 |
. . . . . . . . . . . . . 14
⊢ (𝑅 − (1 ·
(abs‘𝐷))) = (𝑅 − (abs‘𝐷)) |
43 | 42 | oveq2i 6560 |
. . . . . . . . . . . . 13
⊢ (𝑁 − (𝑅 − (1 · (abs‘𝐷)))) = (𝑁 − (𝑅 − (abs‘𝐷))) |
44 | 43 | breq2i 4591 |
. . . . . . . . . . . 12
⊢ (𝐷 ∥ (𝑁 − (𝑅 − (1 · (abs‘𝐷)))) ↔ 𝐷 ∥ (𝑁 − (𝑅 − (abs‘𝐷)))) |
45 | 39, 44 | syl6ib 240 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℤ → (𝐷 ∥ (𝑁 − 𝑅) → 𝐷 ∥ (𝑁 − (𝑅 − (abs‘𝐷))))) |
46 | 36, 45 | syl 17 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℕ0
→ (𝐷 ∥ (𝑁 − 𝑅) → 𝐷 ∥ (𝑁 − (𝑅 − (abs‘𝐷))))) |
47 | 46 | imp 444 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℕ0
∧ 𝐷 ∥ (𝑁 − 𝑅)) → 𝐷 ∥ (𝑁 − (𝑅 − (abs‘𝐷)))) |
48 | 35, 47 | syl 17 |
. . . . . . . 8
⊢
((abs‘𝐷) ≤
𝑅 → 𝐷 ∥ (𝑁 − (𝑅 − (abs‘𝐷)))) |
49 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑅 − (abs‘𝐷)) → (𝑁 − 𝑥) = (𝑁 − (𝑅 − (abs‘𝐷)))) |
50 | 49 | breq2d 4595 |
. . . . . . . . 9
⊢ (𝑥 = (𝑅 − (abs‘𝐷)) → (𝐷 ∥ (𝑁 − 𝑥) ↔ 𝐷 ∥ (𝑁 − (𝑅 − (abs‘𝐷))))) |
51 | 50, 13 | elrab2 3333 |
. . . . . . . 8
⊢ ((𝑅 − (abs‘𝐷)) ∈ 𝑆 ↔ ((𝑅 − (abs‘𝐷)) ∈ ℕ0 ∧ 𝐷 ∥ (𝑁 − (𝑅 − (abs‘𝐷))))) |
52 | 34, 48, 51 | sylanbrc 695 |
. . . . . . 7
⊢
((abs‘𝐷) ≤
𝑅 → (𝑅 − (abs‘𝐷)) ∈ 𝑆) |
53 | | infssuzle 11647 |
. . . . . . 7
⊢ ((𝑆 ⊆
(ℤ≥‘0) ∧ (𝑅 − (abs‘𝐷)) ∈ 𝑆) → inf(𝑆, ℝ, < ) ≤ (𝑅 − (abs‘𝐷))) |
54 | 30, 52, 53 | sylancr 694 |
. . . . . 6
⊢
((abs‘𝐷) ≤
𝑅 → inf(𝑆, ℝ, < ) ≤ (𝑅 − (abs‘𝐷))) |
55 | 1, 54 | syl5eqbr 4618 |
. . . . 5
⊢
((abs‘𝐷) ≤
𝑅 → 𝑅 ≤ (𝑅 − (abs‘𝐷))) |
56 | 35 | simpld 474 |
. . . . . . . 8
⊢
((abs‘𝐷) ≤
𝑅 → 𝑅 ∈
ℕ0) |
57 | | nn0re 11178 |
. . . . . . . 8
⊢ (𝑅 ∈ ℕ0
→ 𝑅 ∈
ℝ) |
58 | 56, 57 | syl 17 |
. . . . . . 7
⊢
((abs‘𝐷) ≤
𝑅 → 𝑅 ∈ ℝ) |
59 | | lesub 10386 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ ∧
(abs‘𝐷) ∈
ℝ) → (𝑅 ≤
(𝑅 − (abs‘𝐷)) ↔ (abs‘𝐷) ≤ (𝑅 − 𝑅))) |
60 | 24, 59 | mp3an3 1405 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑅 ≤ (𝑅 − (abs‘𝐷)) ↔ (abs‘𝐷) ≤ (𝑅 − 𝑅))) |
61 | 58, 58, 60 | syl2anc 691 |
. . . . . 6
⊢
((abs‘𝐷) ≤
𝑅 → (𝑅 ≤ (𝑅 − (abs‘𝐷)) ↔ (abs‘𝐷) ≤ (𝑅 − 𝑅))) |
62 | 58 | recnd 9947 |
. . . . . . . 8
⊢
((abs‘𝐷) ≤
𝑅 → 𝑅 ∈ ℂ) |
63 | 62 | subidd 10259 |
. . . . . . 7
⊢
((abs‘𝐷) ≤
𝑅 → (𝑅 − 𝑅) = 0) |
64 | 63 | breq2d 4595 |
. . . . . 6
⊢
((abs‘𝐷) ≤
𝑅 → ((abs‘𝐷) ≤ (𝑅 − 𝑅) ↔ (abs‘𝐷) ≤ 0)) |
65 | 61, 64 | bitrd 267 |
. . . . 5
⊢
((abs‘𝐷) ≤
𝑅 → (𝑅 ≤ (𝑅 − (abs‘𝐷)) ↔ (abs‘𝐷) ≤ 0)) |
66 | 55, 65 | mpbid 221 |
. . . 4
⊢
((abs‘𝐷) ≤
𝑅 → (abs‘𝐷) ≤ 0) |
67 | 26, 66 | mto 187 |
. . 3
⊢ ¬
(abs‘𝐷) ≤ 𝑅 |
68 | 16, 57 | ax-mp 5 |
. . . 4
⊢ 𝑅 ∈ ℝ |
69 | 68, 24 | ltnlei 10037 |
. . 3
⊢ (𝑅 < (abs‘𝐷) ↔ ¬ (abs‘𝐷) ≤ 𝑅) |
70 | 67, 69 | mpbir 220 |
. 2
⊢ 𝑅 < (abs‘𝐷) |
71 | 17, 70 | pm3.2i 470 |
1
⊢ (0 ≤
𝑅 ∧ 𝑅 < (abs‘𝐷)) |