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 15840 |
. . . . . 6
⊢ inf(𝑆, ℝ, < ) ∈ 𝑆 |
7 | 1, 6 | eqeltri 2829 |
. . . . 5
⊢ 𝑅 ∈ 𝑆 |
8 | | oveq2 7178 |
. . . . . . 7
⊢ (𝑥 = 𝑅 → (𝑁 − 𝑥) = (𝑁 − 𝑅)) |
9 | 8 | breq2d 5042 |
. . . . . 6
⊢ (𝑥 = 𝑅 → (𝐷 ∥ (𝑁 − 𝑥) ↔ 𝐷 ∥ (𝑁 − 𝑅))) |
10 | | oveq2 7178 |
. . . . . . . . 9
⊢ (𝑟 = 𝑥 → (𝑁 − 𝑟) = (𝑁 − 𝑥)) |
11 | 10 | breq2d 5042 |
. . . . . . . 8
⊢ (𝑟 = 𝑥 → (𝐷 ∥ (𝑁 − 𝑟) ↔ 𝐷 ∥ (𝑁 − 𝑥))) |
12 | 11 | cbvrabv 3393 |
. . . . . . 7
⊢ {𝑟 ∈ ℕ0
∣ 𝐷 ∥ (𝑁 − 𝑟)} = {𝑥 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑥)} |
13 | 5, 12 | eqtri 2761 |
. . . . . 6
⊢ 𝑆 = {𝑥 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑥)} |
14 | 9, 13 | elrab2 3591 |
. . . . 5
⊢ (𝑅 ∈ 𝑆 ↔ (𝑅 ∈ ℕ0 ∧ 𝐷 ∥ (𝑁 − 𝑅))) |
15 | 7, 14 | mpbi 233 |
. . . 4
⊢ (𝑅 ∈ ℕ0
∧ 𝐷 ∥ (𝑁 − 𝑅)) |
16 | 15 | simpli 487 |
. . 3
⊢ 𝑅 ∈
ℕ0 |
17 | 16 | nn0ge0i 12003 |
. 2
⊢ 0 ≤
𝑅 |
18 | | nnabscl 14775 |
. . . . . . 7
⊢ ((𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → (abs‘𝐷) ∈
ℕ) |
19 | 3, 4, 18 | mp2an 692 |
. . . . . 6
⊢
(abs‘𝐷) ∈
ℕ |
20 | 19 | nngt0i 11755 |
. . . . 5
⊢ 0 <
(abs‘𝐷) |
21 | | 0re 10721 |
. . . . . 6
⊢ 0 ∈
ℝ |
22 | | zcn 12067 |
. . . . . . . 8
⊢ (𝐷 ∈ ℤ → 𝐷 ∈
ℂ) |
23 | 3, 22 | ax-mp 5 |
. . . . . . 7
⊢ 𝐷 ∈ ℂ |
24 | 23 | abscli 14845 |
. . . . . 6
⊢
(abs‘𝐷) ∈
ℝ |
25 | 21, 24 | ltnlei 10839 |
. . . . 5
⊢ (0 <
(abs‘𝐷) ↔ ¬
(abs‘𝐷) ≤
0) |
26 | 20, 25 | mpbi 233 |
. . . 4
⊢ ¬
(abs‘𝐷) ≤
0 |
27 | 5 | ssrab3 3971 |
. . . . . . . 8
⊢ 𝑆 ⊆
ℕ0 |
28 | | nn0uz 12362 |
. . . . . . . 8
⊢
ℕ0 = (ℤ≥‘0) |
29 | 27, 28 | sseqtri 3913 |
. . . . . . 7
⊢ 𝑆 ⊆
(ℤ≥‘0) |
30 | | nn0abscl 14762 |
. . . . . . . . . 10
⊢ (𝐷 ∈ ℤ →
(abs‘𝐷) ∈
ℕ0) |
31 | 3, 30 | ax-mp 5 |
. . . . . . . . 9
⊢
(abs‘𝐷) ∈
ℕ0 |
32 | | nn0sub2 12124 |
. . . . . . . . 9
⊢
(((abs‘𝐷)
∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧
(abs‘𝐷) ≤ 𝑅) → (𝑅 − (abs‘𝐷)) ∈
ℕ0) |
33 | 31, 16, 32 | mp3an12 1452 |
. . . . . . . 8
⊢
((abs‘𝐷) ≤
𝑅 → (𝑅 − (abs‘𝐷)) ∈
ℕ0) |
34 | 15 | a1i 11 |
. . . . . . . . 9
⊢
((abs‘𝐷) ≤
𝑅 → (𝑅 ∈ ℕ0 ∧ 𝐷 ∥ (𝑁 − 𝑅))) |
35 | | nn0z 12086 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℕ0
→ 𝑅 ∈
ℤ) |
36 | | 1z 12093 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℤ |
37 | 2, 3 | divalglem0 15838 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℤ ∧ 1 ∈
ℤ) → (𝐷 ∥
(𝑁 − 𝑅) → 𝐷 ∥ (𝑁 − (𝑅 − (1 · (abs‘𝐷)))))) |
38 | 36, 37 | mpan2 691 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℤ → (𝐷 ∥ (𝑁 − 𝑅) → 𝐷 ∥ (𝑁 − (𝑅 − (1 · (abs‘𝐷)))))) |
39 | 24 | recni 10733 |
. . . . . . . . . . . . . . . 16
⊢
(abs‘𝐷) ∈
ℂ |
40 | 39 | mulid2i 10724 |
. . . . . . . . . . . . . . 15
⊢ (1
· (abs‘𝐷)) =
(abs‘𝐷) |
41 | 40 | oveq2i 7181 |
. . . . . . . . . . . . . 14
⊢ (𝑅 − (1 ·
(abs‘𝐷))) = (𝑅 − (abs‘𝐷)) |
42 | 41 | oveq2i 7181 |
. . . . . . . . . . . . 13
⊢ (𝑁 − (𝑅 − (1 · (abs‘𝐷)))) = (𝑁 − (𝑅 − (abs‘𝐷))) |
43 | 42 | breq2i 5038 |
. . . . . . . . . . . 12
⊢ (𝐷 ∥ (𝑁 − (𝑅 − (1 · (abs‘𝐷)))) ↔ 𝐷 ∥ (𝑁 − (𝑅 − (abs‘𝐷)))) |
44 | 38, 43 | syl6ib 254 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℤ → (𝐷 ∥ (𝑁 − 𝑅) → 𝐷 ∥ (𝑁 − (𝑅 − (abs‘𝐷))))) |
45 | 35, 44 | syl 17 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℕ0
→ (𝐷 ∥ (𝑁 − 𝑅) → 𝐷 ∥ (𝑁 − (𝑅 − (abs‘𝐷))))) |
46 | 45 | imp 410 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℕ0
∧ 𝐷 ∥ (𝑁 − 𝑅)) → 𝐷 ∥ (𝑁 − (𝑅 − (abs‘𝐷)))) |
47 | 34, 46 | syl 17 |
. . . . . . . 8
⊢
((abs‘𝐷) ≤
𝑅 → 𝐷 ∥ (𝑁 − (𝑅 − (abs‘𝐷)))) |
48 | | oveq2 7178 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑅 − (abs‘𝐷)) → (𝑁 − 𝑥) = (𝑁 − (𝑅 − (abs‘𝐷)))) |
49 | 48 | breq2d 5042 |
. . . . . . . . 9
⊢ (𝑥 = (𝑅 − (abs‘𝐷)) → (𝐷 ∥ (𝑁 − 𝑥) ↔ 𝐷 ∥ (𝑁 − (𝑅 − (abs‘𝐷))))) |
50 | 49, 13 | elrab2 3591 |
. . . . . . . 8
⊢ ((𝑅 − (abs‘𝐷)) ∈ 𝑆 ↔ ((𝑅 − (abs‘𝐷)) ∈ ℕ0 ∧ 𝐷 ∥ (𝑁 − (𝑅 − (abs‘𝐷))))) |
51 | 33, 47, 50 | sylanbrc 586 |
. . . . . . 7
⊢
((abs‘𝐷) ≤
𝑅 → (𝑅 − (abs‘𝐷)) ∈ 𝑆) |
52 | | infssuzle 12413 |
. . . . . . 7
⊢ ((𝑆 ⊆
(ℤ≥‘0) ∧ (𝑅 − (abs‘𝐷)) ∈ 𝑆) → inf(𝑆, ℝ, < ) ≤ (𝑅 − (abs‘𝐷))) |
53 | 29, 51, 52 | sylancr 590 |
. . . . . 6
⊢
((abs‘𝐷) ≤
𝑅 → inf(𝑆, ℝ, < ) ≤ (𝑅 − (abs‘𝐷))) |
54 | 1, 53 | eqbrtrid 5065 |
. . . . 5
⊢
((abs‘𝐷) ≤
𝑅 → 𝑅 ≤ (𝑅 − (abs‘𝐷))) |
55 | 34 | simpld 498 |
. . . . . . . 8
⊢
((abs‘𝐷) ≤
𝑅 → 𝑅 ∈
ℕ0) |
56 | 55 | nn0red 12037 |
. . . . . . 7
⊢
((abs‘𝐷) ≤
𝑅 → 𝑅 ∈ ℝ) |
57 | | lesub 11197 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ ∧
(abs‘𝐷) ∈
ℝ) → (𝑅 ≤
(𝑅 − (abs‘𝐷)) ↔ (abs‘𝐷) ≤ (𝑅 − 𝑅))) |
58 | 24, 57 | mp3an3 1451 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑅 ≤ (𝑅 − (abs‘𝐷)) ↔ (abs‘𝐷) ≤ (𝑅 − 𝑅))) |
59 | 56, 56, 58 | syl2anc 587 |
. . . . . 6
⊢
((abs‘𝐷) ≤
𝑅 → (𝑅 ≤ (𝑅 − (abs‘𝐷)) ↔ (abs‘𝐷) ≤ (𝑅 − 𝑅))) |
60 | 56 | recnd 10747 |
. . . . . . . 8
⊢
((abs‘𝐷) ≤
𝑅 → 𝑅 ∈ ℂ) |
61 | 60 | subidd 11063 |
. . . . . . 7
⊢
((abs‘𝐷) ≤
𝑅 → (𝑅 − 𝑅) = 0) |
62 | 61 | breq2d 5042 |
. . . . . 6
⊢
((abs‘𝐷) ≤
𝑅 → ((abs‘𝐷) ≤ (𝑅 − 𝑅) ↔ (abs‘𝐷) ≤ 0)) |
63 | 59, 62 | bitrd 282 |
. . . . 5
⊢
((abs‘𝐷) ≤
𝑅 → (𝑅 ≤ (𝑅 − (abs‘𝐷)) ↔ (abs‘𝐷) ≤ 0)) |
64 | 54, 63 | mpbid 235 |
. . . 4
⊢
((abs‘𝐷) ≤
𝑅 → (abs‘𝐷) ≤ 0) |
65 | 26, 64 | mto 200 |
. . 3
⊢ ¬
(abs‘𝐷) ≤ 𝑅 |
66 | 16 | nn0rei 11987 |
. . . 4
⊢ 𝑅 ∈ ℝ |
67 | 66, 24 | ltnlei 10839 |
. . 3
⊢ (𝑅 < (abs‘𝐷) ↔ ¬ (abs‘𝐷) ≤ 𝑅) |
68 | 65, 67 | mpbir 234 |
. 2
⊢ 𝑅 < (abs‘𝐷) |
69 | 17, 68 | pm3.2i 474 |
1
⊢ (0 ≤
𝑅 ∧ 𝑅 < (abs‘𝐷)) |