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 15499 |
. . . . . 6
⊢ inf(𝑆, ℝ, < ) ∈ 𝑆 |
7 | 1, 6 | eqeltri 2902 |
. . . . 5
⊢ 𝑅 ∈ 𝑆 |
8 | | oveq2 6918 |
. . . . . . 7
⊢ (𝑥 = 𝑅 → (𝑁 − 𝑥) = (𝑁 − 𝑅)) |
9 | 8 | breq2d 4887 |
. . . . . 6
⊢ (𝑥 = 𝑅 → (𝐷 ∥ (𝑁 − 𝑥) ↔ 𝐷 ∥ (𝑁 − 𝑅))) |
10 | | oveq2 6918 |
. . . . . . . . 9
⊢ (𝑟 = 𝑥 → (𝑁 − 𝑟) = (𝑁 − 𝑥)) |
11 | 10 | breq2d 4887 |
. . . . . . . 8
⊢ (𝑟 = 𝑥 → (𝐷 ∥ (𝑁 − 𝑟) ↔ 𝐷 ∥ (𝑁 − 𝑥))) |
12 | 11 | cbvrabv 3412 |
. . . . . . 7
⊢ {𝑟 ∈ ℕ0
∣ 𝐷 ∥ (𝑁 − 𝑟)} = {𝑥 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑥)} |
13 | 5, 12 | eqtri 2849 |
. . . . . 6
⊢ 𝑆 = {𝑥 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑥)} |
14 | 9, 13 | elrab2 3589 |
. . . . 5
⊢ (𝑅 ∈ 𝑆 ↔ (𝑅 ∈ ℕ0 ∧ 𝐷 ∥ (𝑁 − 𝑅))) |
15 | 7, 14 | mpbi 222 |
. . . 4
⊢ (𝑅 ∈ ℕ0
∧ 𝐷 ∥ (𝑁 − 𝑅)) |
16 | 15 | simpli 478 |
. . 3
⊢ 𝑅 ∈
ℕ0 |
17 | 16 | nn0ge0i 11654 |
. 2
⊢ 0 ≤
𝑅 |
18 | | nnabscl 14449 |
. . . . . . 7
⊢ ((𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → (abs‘𝐷) ∈
ℕ) |
19 | 3, 4, 18 | mp2an 683 |
. . . . . 6
⊢
(abs‘𝐷) ∈
ℕ |
20 | 19 | nngt0i 11397 |
. . . . 5
⊢ 0 <
(abs‘𝐷) |
21 | | 0re 10365 |
. . . . . 6
⊢ 0 ∈
ℝ |
22 | | zcn 11716 |
. . . . . . . 8
⊢ (𝐷 ∈ ℤ → 𝐷 ∈
ℂ) |
23 | 3, 22 | ax-mp 5 |
. . . . . . 7
⊢ 𝐷 ∈ ℂ |
24 | 23 | abscli 14518 |
. . . . . 6
⊢
(abs‘𝐷) ∈
ℝ |
25 | 21, 24 | ltnlei 10484 |
. . . . 5
⊢ (0 <
(abs‘𝐷) ↔ ¬
(abs‘𝐷) ≤
0) |
26 | 20, 25 | mpbi 222 |
. . . 4
⊢ ¬
(abs‘𝐷) ≤
0 |
27 | | ssrab2 3914 |
. . . . . . . . 9
⊢ {𝑟 ∈ ℕ0
∣ 𝐷 ∥ (𝑁 − 𝑟)} ⊆
ℕ0 |
28 | 5, 27 | eqsstri 3860 |
. . . . . . . 8
⊢ 𝑆 ⊆
ℕ0 |
29 | | nn0uz 12011 |
. . . . . . . 8
⊢
ℕ0 = (ℤ≥‘0) |
30 | 28, 29 | sseqtri 3862 |
. . . . . . 7
⊢ 𝑆 ⊆
(ℤ≥‘0) |
31 | | nn0abscl 14436 |
. . . . . . . . . 10
⊢ (𝐷 ∈ ℤ →
(abs‘𝐷) ∈
ℕ0) |
32 | 3, 31 | ax-mp 5 |
. . . . . . . . 9
⊢
(abs‘𝐷) ∈
ℕ0 |
33 | | nn0sub2 11773 |
. . . . . . . . 9
⊢
(((abs‘𝐷)
∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧
(abs‘𝐷) ≤ 𝑅) → (𝑅 − (abs‘𝐷)) ∈
ℕ0) |
34 | 32, 16, 33 | mp3an12 1579 |
. . . . . . . 8
⊢
((abs‘𝐷) ≤
𝑅 → (𝑅 − (abs‘𝐷)) ∈
ℕ0) |
35 | 15 | a1i 11 |
. . . . . . . . 9
⊢
((abs‘𝐷) ≤
𝑅 → (𝑅 ∈ ℕ0 ∧ 𝐷 ∥ (𝑁 − 𝑅))) |
36 | | nn0z 11735 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℕ0
→ 𝑅 ∈
ℤ) |
37 | | 1z 11742 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℤ |
38 | 2, 3 | divalglem0 15497 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℤ ∧ 1 ∈
ℤ) → (𝐷 ∥
(𝑁 − 𝑅) → 𝐷 ∥ (𝑁 − (𝑅 − (1 · (abs‘𝐷)))))) |
39 | 37, 38 | mpan2 682 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℤ → (𝐷 ∥ (𝑁 − 𝑅) → 𝐷 ∥ (𝑁 − (𝑅 − (1 · (abs‘𝐷)))))) |
40 | 24 | recni 10378 |
. . . . . . . . . . . . . . . 16
⊢
(abs‘𝐷) ∈
ℂ |
41 | 40 | mulid2i 10369 |
. . . . . . . . . . . . . . 15
⊢ (1
· (abs‘𝐷)) =
(abs‘𝐷) |
42 | 41 | oveq2i 6921 |
. . . . . . . . . . . . . 14
⊢ (𝑅 − (1 ·
(abs‘𝐷))) = (𝑅 − (abs‘𝐷)) |
43 | 42 | oveq2i 6921 |
. . . . . . . . . . . . 13
⊢ (𝑁 − (𝑅 − (1 · (abs‘𝐷)))) = (𝑁 − (𝑅 − (abs‘𝐷))) |
44 | 43 | breq2i 4883 |
. . . . . . . . . . . 12
⊢ (𝐷 ∥ (𝑁 − (𝑅 − (1 · (abs‘𝐷)))) ↔ 𝐷 ∥ (𝑁 − (𝑅 − (abs‘𝐷)))) |
45 | 39, 44 | syl6ib 243 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℤ → (𝐷 ∥ (𝑁 − 𝑅) → 𝐷 ∥ (𝑁 − (𝑅 − (abs‘𝐷))))) |
46 | 36, 45 | syl 17 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℕ0
→ (𝐷 ∥ (𝑁 − 𝑅) → 𝐷 ∥ (𝑁 − (𝑅 − (abs‘𝐷))))) |
47 | 46 | imp 397 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℕ0
∧ 𝐷 ∥ (𝑁 − 𝑅)) → 𝐷 ∥ (𝑁 − (𝑅 − (abs‘𝐷)))) |
48 | 35, 47 | syl 17 |
. . . . . . . 8
⊢
((abs‘𝐷) ≤
𝑅 → 𝐷 ∥ (𝑁 − (𝑅 − (abs‘𝐷)))) |
49 | | oveq2 6918 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑅 − (abs‘𝐷)) → (𝑁 − 𝑥) = (𝑁 − (𝑅 − (abs‘𝐷)))) |
50 | 49 | breq2d 4887 |
. . . . . . . . 9
⊢ (𝑥 = (𝑅 − (abs‘𝐷)) → (𝐷 ∥ (𝑁 − 𝑥) ↔ 𝐷 ∥ (𝑁 − (𝑅 − (abs‘𝐷))))) |
51 | 50, 13 | elrab2 3589 |
. . . . . . . 8
⊢ ((𝑅 − (abs‘𝐷)) ∈ 𝑆 ↔ ((𝑅 − (abs‘𝐷)) ∈ ℕ0 ∧ 𝐷 ∥ (𝑁 − (𝑅 − (abs‘𝐷))))) |
52 | 34, 48, 51 | sylanbrc 578 |
. . . . . . 7
⊢
((abs‘𝐷) ≤
𝑅 → (𝑅 − (abs‘𝐷)) ∈ 𝑆) |
53 | | infssuzle 12061 |
. . . . . . 7
⊢ ((𝑆 ⊆
(ℤ≥‘0) ∧ (𝑅 − (abs‘𝐷)) ∈ 𝑆) → inf(𝑆, ℝ, < ) ≤ (𝑅 − (abs‘𝐷))) |
54 | 30, 52, 53 | sylancr 581 |
. . . . . 6
⊢
((abs‘𝐷) ≤
𝑅 → inf(𝑆, ℝ, < ) ≤ (𝑅 − (abs‘𝐷))) |
55 | 1, 54 | syl5eqbr 4910 |
. . . . 5
⊢
((abs‘𝐷) ≤
𝑅 → 𝑅 ≤ (𝑅 − (abs‘𝐷))) |
56 | 35 | simpld 490 |
. . . . . . . 8
⊢
((abs‘𝐷) ≤
𝑅 → 𝑅 ∈
ℕ0) |
57 | | nn0re 11635 |
. . . . . . . 8
⊢ (𝑅 ∈ ℕ0
→ 𝑅 ∈
ℝ) |
58 | 56, 57 | syl 17 |
. . . . . . 7
⊢
((abs‘𝐷) ≤
𝑅 → 𝑅 ∈ ℝ) |
59 | | lesub 10838 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ ∧
(abs‘𝐷) ∈
ℝ) → (𝑅 ≤
(𝑅 − (abs‘𝐷)) ↔ (abs‘𝐷) ≤ (𝑅 − 𝑅))) |
60 | 24, 59 | mp3an3 1578 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑅 ≤ (𝑅 − (abs‘𝐷)) ↔ (abs‘𝐷) ≤ (𝑅 − 𝑅))) |
61 | 58, 58, 60 | syl2anc 579 |
. . . . . 6
⊢
((abs‘𝐷) ≤
𝑅 → (𝑅 ≤ (𝑅 − (abs‘𝐷)) ↔ (abs‘𝐷) ≤ (𝑅 − 𝑅))) |
62 | 58 | recnd 10392 |
. . . . . . . 8
⊢
((abs‘𝐷) ≤
𝑅 → 𝑅 ∈ ℂ) |
63 | 62 | subidd 10708 |
. . . . . . 7
⊢
((abs‘𝐷) ≤
𝑅 → (𝑅 − 𝑅) = 0) |
64 | 63 | breq2d 4887 |
. . . . . 6
⊢
((abs‘𝐷) ≤
𝑅 → ((abs‘𝐷) ≤ (𝑅 − 𝑅) ↔ (abs‘𝐷) ≤ 0)) |
65 | 61, 64 | bitrd 271 |
. . . . 5
⊢
((abs‘𝐷) ≤
𝑅 → (𝑅 ≤ (𝑅 − (abs‘𝐷)) ↔ (abs‘𝐷) ≤ 0)) |
66 | 55, 65 | mpbid 224 |
. . . 4
⊢
((abs‘𝐷) ≤
𝑅 → (abs‘𝐷) ≤ 0) |
67 | 26, 66 | mto 189 |
. . 3
⊢ ¬
(abs‘𝐷) ≤ 𝑅 |
68 | 16, 57 | ax-mp 5 |
. . . 4
⊢ 𝑅 ∈ ℝ |
69 | 68, 24 | ltnlei 10484 |
. . 3
⊢ (𝑅 < (abs‘𝐷) ↔ ¬ (abs‘𝐷) ≤ 𝑅) |
70 | 67, 69 | mpbir 223 |
. 2
⊢ 𝑅 < (abs‘𝐷) |
71 | 17, 70 | pm3.2i 464 |
1
⊢ (0 ≤
𝑅 ∧ 𝑅 < (abs‘𝐷)) |