Step | Hyp | Ref
| Expression |
1 | | totbndbnd 33588 |
. 2
⊢ (𝐷 ∈ (TotBnd‘𝑋) → 𝐷 ∈ (Bnd‘𝑋)) |
2 | | rpcn 11841 |
. . . . . . . . . 10
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℂ) |
3 | 2 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℂ) |
4 | | gzcn 15636 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℤ[i] → 𝑧 ∈
ℂ) |
5 | | mulcl 10020 |
. . . . . . . . 9
⊢ ((𝑟 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑟 · 𝑧) ∈ ℂ) |
6 | 3, 4, 5 | syl2an 494 |
. . . . . . . 8
⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ 𝑧 ∈ ℤ[i]) →
(𝑟 · 𝑧) ∈
ℂ) |
7 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧)) = (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) |
8 | 6, 7 | fmptd 6385 |
. . . . . . 7
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧)):ℤ[i]⟶ℂ) |
9 | | frn 6053 |
. . . . . . 7
⊢ ((𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧)):ℤ[i]⟶ℂ
→ ran (𝑧 ∈
ℤ[i] ↦ (𝑟
· 𝑧)) ⊆
ℂ) |
10 | 8, 9 | syl 17 |
. . . . . 6
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → ran
(𝑧 ∈ ℤ[i]
↦ (𝑟 · 𝑧)) ⊆
ℂ) |
11 | | cnex 10017 |
. . . . . . 7
⊢ ℂ
∈ V |
12 | 11 | elpw2 4828 |
. . . . . 6
⊢ (ran
(𝑧 ∈ ℤ[i]
↦ (𝑟 · 𝑧)) ∈ 𝒫 ℂ
↔ ran (𝑧 ∈
ℤ[i] ↦ (𝑟
· 𝑧)) ⊆
ℂ) |
13 | 10, 12 | sylibr 224 |
. . . . 5
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → ran
(𝑧 ∈ ℤ[i]
↦ (𝑟 · 𝑧)) ∈ 𝒫
ℂ) |
14 | | cnmet 22575 |
. . . . . . . . . . . . . . . . 17
⊢ (abs
∘ − ) ∈ (Met‘ℂ) |
15 | | cntotbnd.d |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐷 = ((abs ∘ − )
↾ (𝑋 × 𝑋)) |
16 | 15 | bnd2lem 33590 |
. . . . . . . . . . . . . . . . 17
⊢ (((abs
∘ − ) ∈ (Met‘ℂ) ∧ 𝐷 ∈ (Bnd‘𝑋)) → 𝑋 ⊆ ℂ) |
17 | 14, 16 | mpan 706 |
. . . . . . . . . . . . . . . 16
⊢ (𝐷 ∈ (Bnd‘𝑋) → 𝑋 ⊆ ℂ) |
18 | 17 | sselda 3603 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ ℂ) |
19 | 18 | adantrl 752 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ ℂ) |
20 | 19 | recld 13934 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (ℜ‘𝑦) ∈ ℝ) |
21 | | simprl 794 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℝ+) |
22 | 20, 21 | rerpdivcld 11903 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℜ‘𝑦) / 𝑟) ∈ ℝ) |
23 | | halfre 11246 |
. . . . . . . . . . . 12
⊢ (1 / 2)
∈ ℝ |
24 | | readdcl 10019 |
. . . . . . . . . . . 12
⊢
((((ℜ‘𝑦)
/ 𝑟) ∈ ℝ ∧
(1 / 2) ∈ ℝ) → (((ℜ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ) |
25 | 22, 23, 24 | sylancl 694 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((ℜ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ) |
26 | 25 | flcld 12599 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈
ℤ) |
27 | 19 | imcld 13935 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (ℑ‘𝑦) ∈ ℝ) |
28 | 27, 21 | rerpdivcld 11903 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℑ‘𝑦) / 𝑟) ∈ ℝ) |
29 | | readdcl 10019 |
. . . . . . . . . . . 12
⊢
((((ℑ‘𝑦)
/ 𝑟) ∈ ℝ ∧
(1 / 2) ∈ ℝ) → (((ℑ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ) |
30 | 28, 23, 29 | sylancl 694 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((ℑ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ) |
31 | 30 | flcld 12599 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈
ℤ) |
32 | | gzreim 15643 |
. . . . . . . . . 10
⊢
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℤ ∧
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℤ) →
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈
ℤ[i]) |
33 | 26, 31, 32 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈
ℤ[i]) |
34 | | gzcn 15636 |
. . . . . . . . . . . . . . 15
⊢
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℤ[i] →
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈
ℂ) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈
ℂ) |
36 | 21 | rpcnd 11874 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℂ) |
37 | 21 | rpne0d 11877 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ≠ 0) |
38 | 19, 36, 37 | divcld 10801 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑦 / 𝑟) ∈ ℂ) |
39 | 35, 38 | subcld 10392 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)) ∈ ℂ) |
40 | 39 | abscld 14175 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) ∈ ℝ) |
41 | | 1re 10039 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
42 | 41 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 1 ∈ ℝ) |
43 | 26 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈
ℂ) |
44 | | ax-icn 9995 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ i ∈
ℂ |
45 | 31 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈
ℂ) |
46 | | mulcl 10020 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((i
∈ ℂ ∧ (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℂ) → (i
· (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) ∈
ℂ) |
47 | 44, 45, 46 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) ∈
ℂ) |
48 | 22 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℜ‘𝑦) / 𝑟) ∈ ℂ) |
49 | 28 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℑ‘𝑦) / 𝑟) ∈ ℂ) |
50 | | mulcl 10020 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((i
∈ ℂ ∧ ((ℑ‘𝑦) / 𝑟) ∈ ℂ) → (i ·
((ℑ‘𝑦) / 𝑟)) ∈
ℂ) |
51 | 44, 49, 50 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (i · ((ℑ‘𝑦) / 𝑟)) ∈ ℂ) |
52 | 43, 47, 48, 51 | addsub4d 10439 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟)))) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + ((i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) − (i ·
((ℑ‘𝑦) / 𝑟))))) |
53 | 38 | replimd 13937 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑦 / 𝑟) = ((ℜ‘(𝑦 / 𝑟)) + (i · (ℑ‘(𝑦 / 𝑟))))) |
54 | 21 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℝ) |
55 | 54, 19, 37 | redivd 13969 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (ℜ‘(𝑦 / 𝑟)) = ((ℜ‘𝑦) / 𝑟)) |
56 | 54, 19, 37 | imdivd 13970 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (ℑ‘(𝑦 / 𝑟)) = ((ℑ‘𝑦) / 𝑟)) |
57 | 56 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (i · (ℑ‘(𝑦 / 𝑟))) = (i · ((ℑ‘𝑦) / 𝑟))) |
58 | 55, 57 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℜ‘(𝑦 / 𝑟)) + (i · (ℑ‘(𝑦 / 𝑟)))) = (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟)))) |
59 | 53, 58 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑦 / 𝑟) = (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟)))) |
60 | 59 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟))))) |
61 | 44 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → i ∈ ℂ) |
62 | 61, 45, 49 | subdid 10486 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (i ·
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) = ((i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) − (i ·
((ℑ‘𝑦) / 𝑟)))) |
63 | 62 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i ·
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + ((i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) − (i ·
((ℑ‘𝑦) / 𝑟))))) |
64 | 52, 60, 63 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i ·
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))))) |
65 | 64 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) =
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i ·
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))) |
66 | 65 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) =
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i ·
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))↑2)) |
67 | 26 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈
ℝ) |
68 | 67, 22 | resubcld 10458 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℝ) |
69 | 31 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈
ℝ) |
70 | 69, 28 | resubcld 10458 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℝ) |
71 | | absreimsq 14032 |
. . . . . . . . . . . . . . . . 17
⊢
((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℝ ∧
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℝ) →
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i ·
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))↑2) =
((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) +
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2))) |
72 | 68, 70, 71 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i ·
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))↑2) =
((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) +
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2))) |
73 | 66, 72 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) =
((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) +
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2))) |
74 | 68 | resqcld 13035 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) ∈ ℝ) |
75 | 70 | resqcld 13035 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2) ∈ ℝ) |
76 | 23 | resqcli 12949 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1 /
2)↑2) ∈ ℝ |
77 | 76 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((1 / 2)↑2) ∈
ℝ) |
78 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (1 / 2) ∈
ℝ) |
79 | | absresq 14042 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℝ →
((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))↑2) =
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2)) |
80 | 68, 79 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))↑2) =
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2)) |
81 | | rddif 14080 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((ℜ‘𝑦) /
𝑟) ∈ ℝ →
(abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ≤ (1 / 2)) |
82 | 22, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ≤ (1 / 2)) |
83 | 68 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℂ) |
84 | 83 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ∈ ℝ) |
85 | 83 | absge0d 14183 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤
(abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))) |
86 | | halfgt0 11248 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 < (1
/ 2) |
87 | 23, 86 | elrpii 11835 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 / 2)
∈ ℝ+ |
88 | | rpge0 11845 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1 / 2)
∈ ℝ+ → 0 ≤ (1 / 2)) |
89 | 87, 88 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (1 / 2)) |
90 | 84, 78, 85, 89 | le2sqd 13044 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ≤ (1 / 2) ↔
((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))↑2) ≤ ((1 /
2)↑2))) |
91 | 82, 90 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))↑2) ≤ ((1 /
2)↑2)) |
92 | 80, 91 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) ≤ ((1 /
2)↑2)) |
93 | | halfcn 11247 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 / 2)
∈ ℂ |
94 | 93 | sqvali 12943 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1 /
2)↑2) = ((1 / 2) · (1 / 2)) |
95 | | halflt1 11250 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 / 2)
< 1 |
96 | 23, 41, 23, 86 | ltmul1ii 10952 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1 / 2)
< 1 ↔ ((1 / 2) · (1 / 2)) < (1 · (1 /
2))) |
97 | 95, 96 | mpbi 220 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1 / 2)
· (1 / 2)) < (1 · (1 / 2)) |
98 | 93 | mulid2i 10043 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1
· (1 / 2)) = (1 / 2) |
99 | 97, 98 | breqtri 4678 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1 / 2)
· (1 / 2)) < (1 / 2) |
100 | 94, 99 | eqbrtri 4674 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1 /
2)↑2) < (1 / 2) |
101 | 100 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((1 / 2)↑2) < (1 /
2)) |
102 | 74, 77, 78, 92, 101 | lelttrd 10195 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) < (1 / 2)) |
103 | | absresq 14042 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℝ →
((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))↑2) =
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)) |
104 | 70, 103 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))↑2) =
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)) |
105 | | rddif 14080 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((ℑ‘𝑦)
/ 𝑟) ∈ ℝ →
(abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ≤ (1 / 2)) |
106 | 28, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ≤ (1 / 2)) |
107 | 70 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℂ) |
108 | 107 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ∈ ℝ) |
109 | 107 | absge0d 14183 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤
(abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))) |
110 | 108, 78, 109, 89 | le2sqd 13044 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ≤ (1 / 2) ↔
((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))↑2) ≤ ((1 /
2)↑2))) |
111 | 106, 110 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))↑2) ≤ ((1 /
2)↑2)) |
112 | 104, 111 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2) ≤ ((1 /
2)↑2)) |
113 | 75, 77, 78, 112, 101 | lelttrd 10195 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2) < (1 / 2)) |
114 | 74, 75, 42, 102, 113 | lt2halvesd 11280 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) +
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)) < 1) |
115 | 73, 114 | eqbrtrd 4675 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) < 1) |
116 | | sq1 12958 |
. . . . . . . . . . . . . 14
⊢
(1↑2) = 1 |
117 | 115, 116 | syl6breqr 4695 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) < (1↑2)) |
118 | 39 | absge0d 14183 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) |
119 | | 0le1 10551 |
. . . . . . . . . . . . . . 15
⊢ 0 ≤
1 |
120 | 119 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ 1) |
121 | 40, 42, 118, 120 | lt2sqd 13043 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) < 1 ↔
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) <
(1↑2))) |
122 | 117, 121 | mpbird 247 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) < 1) |
123 | 40, 42, 21, 122 | ltmul2dd 11928 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 ·
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) < (𝑟 · 1)) |
124 | 36, 35 | mulcld 10060 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) ∈
ℂ) |
125 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (abs
∘ − ) = (abs ∘ − ) |
126 | 125 | cnmetdval 22574 |
. . . . . . . . . . . . 13
⊢ (((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) = (abs‘((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦))) |
127 | 124, 19, 126 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) = (abs‘((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦))) |
128 | 36, 35, 38 | subdid 10486 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 ·
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) = ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − (𝑟 · (𝑦 / 𝑟)))) |
129 | 19, 36, 37 | divcan2d 10803 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · (𝑦 / 𝑟)) = 𝑦) |
130 | 129 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − (𝑟 · (𝑦 / 𝑟))) = ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)) |
131 | 128, 130 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 ·
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) = ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)) |
132 | 131 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘(𝑟 ·
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = (abs‘((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦))) |
133 | 36, 39 | absmuld 14193 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘(𝑟 ·
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = ((abs‘𝑟) ·
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))))) |
134 | 132, 133 | eqtr3d 2658 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)) = ((abs‘𝑟) ·
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))))) |
135 | 21 | rpge0d 11876 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ 𝑟) |
136 | 54, 135 | absidd 14161 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘𝑟) = 𝑟) |
137 | 136 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘𝑟) ·
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = (𝑟 ·
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))))) |
138 | 127, 134,
137 | 3eqtrrd 2661 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 ·
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦)) |
139 | 36 | mulid1d 10057 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · 1) = 𝑟) |
140 | 123, 138,
139 | 3brtr3d 4684 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) < 𝑟) |
141 | | cnxmet 22576 |
. . . . . . . . . . . 12
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
142 | 141 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
143 | | rpxr 11840 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
144 | 143 | ad2antrl 764 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℝ*) |
145 | | elbl2 22195 |
. . . . . . . . . . 11
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑦 ∈ ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘
− ))𝑟) ↔ ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) < 𝑟)) |
146 | 142, 144,
124, 19, 145 | syl22anc 1327 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑦 ∈ ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘
− ))𝑟) ↔ ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) < 𝑟)) |
147 | 140, 146 | mpbird 247 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘
− ))𝑟)) |
148 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑧 =
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) → (𝑟 · 𝑧) = (𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))) |
149 | 148 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝑧 =
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) → ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) = ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘
− ))𝑟)) |
150 | 149 | eleq2d 2687 |
. . . . . . . . . 10
⊢ (𝑧 =
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) → (𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ↔ 𝑦 ∈ ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘
− ))𝑟))) |
151 | 150 | rspcev 3309 |
. . . . . . . . 9
⊢
((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℤ[i] ∧ 𝑦 ∈ ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘
− ))𝑟)) →
∃𝑧 ∈ ℤ[i]
𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟)) |
152 | 33, 147, 151 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟)) |
153 | 152 | expr 643 |
. . . . . . 7
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑦 ∈ 𝑋 → ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))) |
154 | | eliun 4524 |
. . . . . . . 8
⊢ (𝑦 ∈ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ↔ ∃𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) |
155 | | ovex 6678 |
. . . . . . . . . 10
⊢ (𝑟 · 𝑧) ∈ V |
156 | 155 | rgenw 2924 |
. . . . . . . . 9
⊢
∀𝑧 ∈
ℤ[i] (𝑟 ·
𝑧) ∈
V |
157 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑟 · 𝑧) → (𝑥(ball‘(abs ∘ − ))𝑟) = ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟)) |
158 | 157 | eleq2d 2687 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑟 · 𝑧) → (𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))) |
159 | 7, 158 | rexrnmpt 6369 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
ℤ[i] (𝑟 ·
𝑧) ∈ V →
(∃𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧))𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))) |
160 | 156, 159 | ax-mp 5 |
. . . . . . . 8
⊢
(∃𝑥 ∈ ran
(𝑧 ∈ ℤ[i]
↦ (𝑟 · 𝑧))𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟)) |
161 | 154, 160 | bitri 264 |
. . . . . . 7
⊢ (𝑦 ∈ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ↔ ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟)) |
162 | 153, 161 | syl6ibr 242 |
. . . . . 6
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑦 ∈ 𝑋 → 𝑦 ∈ ∪
𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟))) |
163 | 162 | ssrdv 3609 |
. . . . 5
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → 𝑋 ⊆ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟)) |
164 | | simpl 473 |
. . . . . . 7
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → 𝐷 ∈ (Bnd‘𝑋)) |
165 | | 0cn 10032 |
. . . . . . . 8
⊢ 0 ∈
ℂ |
166 | 15 | ssbnd 33587 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∈ (Met‘ℂ) ∧ 0 ∈ ℂ) →
(𝐷 ∈ (Bnd‘𝑋) ↔ ∃𝑑 ∈ ℝ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑))) |
167 | 14, 165, 166 | mp2an 708 |
. . . . . . 7
⊢ (𝐷 ∈ (Bnd‘𝑋) ↔ ∃𝑑 ∈ ℝ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)) |
168 | 164, 167 | sylib 208 |
. . . . . 6
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) →
∃𝑑 ∈ ℝ
𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑)) |
169 | | fzfi 12771 |
. . . . . . . . 9
⊢
(-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∈ Fin |
170 | | xpfi 8231 |
. . . . . . . . 9
⊢
(((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∈ Fin ∧
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∈ Fin) →
((-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) ∈ Fin) |
171 | 169, 169,
170 | mp2an 708 |
. . . . . . . 8
⊢
((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) ∈ Fin |
172 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) = (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) |
173 | | ovex 6678 |
. . . . . . . . . 10
⊢ (𝑟 · (𝑎 + (i · 𝑏))) ∈ V |
174 | 172, 173 | fnmpt2i 7239 |
. . . . . . . . 9
⊢ (𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) Fn ((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) |
175 | | dffn4 6121 |
. . . . . . . . 9
⊢ ((𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) Fn ((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) ↔ (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))):((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))–onto→ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))) |
176 | 174, 175 | mpbi 220 |
. . . . . . . 8
⊢ (𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))):((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))–onto→ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) |
177 | | fofi 8252 |
. . . . . . . 8
⊢
((((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) ∈ Fin ∧ (𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))):((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))–onto→ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))) → ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ∈ Fin) |
178 | 171, 176,
177 | mp2an 708 |
. . . . . . 7
⊢ ran
(𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ∈ Fin |
179 | 7, 155 | elrnmpti 5376 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ↔ ∃𝑧 ∈ ℤ[i] 𝑥 = (𝑟 · 𝑧)) |
180 | | elgz 15635 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ ℤ[i] ↔ (𝑧 ∈ ℂ ∧
(ℜ‘𝑧) ∈
ℤ ∧ (ℑ‘𝑧) ∈ ℤ)) |
181 | 180 | simp2bi 1077 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ ℤ[i] →
(ℜ‘𝑧) ∈
ℤ) |
182 | 181 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈
ℤ) |
183 | 182 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈
ℂ) |
184 | 183 | abscld 14175 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(abs‘(ℜ‘𝑧)) ∈ ℝ) |
185 | 4 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑧 ∈ ℂ) |
186 | 185 | abscld 14175 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) ∈
ℝ) |
187 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ 𝑟 ∈
ℝ+) |
188 | 187 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑟 ∈ ℝ+) |
189 | 188 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑟 ∈ ℝ) |
190 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ 𝑑 ∈
ℝ) |
191 | 190 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑑 ∈ ℝ) |
192 | 189, 191 | readdcld 10069 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 + 𝑑) ∈ ℝ) |
193 | 192, 188 | rerpdivcld 11903 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 + 𝑑) / 𝑟) ∈ ℝ) |
194 | 193 | flcld 12599 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(⌊‘((𝑟 + 𝑑) / 𝑟)) ∈ ℤ) |
195 | 194 | peano2zd 11485 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ) |
196 | 195 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℝ) |
197 | | absrele 14048 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ ℂ →
(abs‘(ℜ‘𝑧)) ≤ (abs‘𝑧)) |
198 | 185, 197 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(abs‘(ℜ‘𝑧)) ≤ (abs‘𝑧)) |
199 | 188 | rpcnd 11874 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑟 ∈ ℂ) |
200 | 199, 185 | absmuld 14193 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) = ((abs‘𝑟) · (abs‘𝑧))) |
201 | 188 | rpge0d 11876 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 0 ≤ 𝑟) |
202 | 189, 201 | absidd 14161 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑟) = 𝑟) |
203 | 202 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((abs‘𝑟) · (abs‘𝑧)) = (𝑟 · (abs‘𝑧))) |
204 | 200, 203 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) = (𝑟 · (abs‘𝑧))) |
205 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑)) |
206 | | sslin 3839 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑) →
(((𝑟 · 𝑧)(ball‘(abs ∘
− ))𝑟) ∩ 𝑋) ⊆ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs
∘ − ))𝑑))) |
207 | 205, 206 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ (((𝑟 · 𝑧)(ball‘(abs ∘
− ))𝑟) ∩ 𝑋) ⊆ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs
∘ − ))𝑑))) |
208 | 141 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ (abs ∘ − ) ∈
(∞Met‘ℂ)) |
209 | 6 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ (𝑟 · 𝑧) ∈
ℂ) |
210 | 165 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ 0 ∈ ℂ) |
211 | 187 | rpxrd 11873 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ 𝑟 ∈
ℝ*) |
212 | 190 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ 𝑑 ∈
ℝ*) |
213 | | bldisj 22203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ)
∧ (𝑟 ∈
ℝ* ∧ 𝑑
∈ ℝ* ∧ (𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0))) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs
∘ − ))𝑑)) =
∅) |
214 | 213 | 3exp2 1285 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ)
→ (𝑟 ∈
ℝ* → (𝑑 ∈ ℝ* → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs
∘ − ))𝑑)) =
∅)))) |
215 | 214 | imp32 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ)
∧ (𝑟 ∈
ℝ* ∧ 𝑑
∈ ℝ*)) → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs
∘ − ))𝑑)) =
∅)) |
216 | 208, 209,
210, 211, 212, 215 | syl32anc 1334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ ((𝑟
+𝑒 𝑑)
≤ ((𝑟 · 𝑧)(abs ∘ − )0) →
(((𝑟 · 𝑧)(ball‘(abs ∘
− ))𝑟) ∩
(0(ball‘(abs ∘ − ))𝑑)) = ∅)) |
217 | | sseq0 3975 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝑟 ·
𝑧)(ball‘(abs ∘
− ))𝑟) ∩ 𝑋) ⊆ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs
∘ − ))𝑑)) ∧
(((𝑟 · 𝑧)(ball‘(abs ∘
− ))𝑟) ∩
(0(ball‘(abs ∘ − ))𝑑)) = ∅) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ∅) |
218 | 207, 216,
217 | syl6an 568 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ ((𝑟
+𝑒 𝑑)
≤ ((𝑟 · 𝑧)(abs ∘ − )0) →
(((𝑟 · 𝑧)(ball‘(abs ∘
− ))𝑟) ∩ 𝑋) = ∅)) |
219 | 218 | necon3ad 2807 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ ((((𝑟 · 𝑧)(ball‘(abs ∘
− ))𝑟) ∩ 𝑋) ≠ ∅ → ¬
(𝑟 +𝑒
𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0))) |
220 | 219 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ¬ (𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0)) |
221 | | rexadd 12063 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑟 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑟 +𝑒 𝑑) = (𝑟 + 𝑑)) |
222 | 189, 191,
221 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 +𝑒 𝑑) = (𝑟 + 𝑑)) |
223 | 209 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 · 𝑧) ∈ ℂ) |
224 | 125 | cnmetdval 22574 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ)
→ ((𝑟 · 𝑧)(abs ∘ − )0) =
(abs‘((𝑟 ·
𝑧) −
0))) |
225 | 223, 165,
224 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · 𝑧)(abs ∘ − )0) =
(abs‘((𝑟 ·
𝑧) −
0))) |
226 | 223 | subid1d 10381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · 𝑧) − 0) = (𝑟 · 𝑧)) |
227 | 226 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘((𝑟 · 𝑧) − 0)) = (abs‘(𝑟 · 𝑧))) |
228 | 225, 227 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · 𝑧)(abs ∘ − )0) = (abs‘(𝑟 · 𝑧))) |
229 | 222, 228 | breq12d 4666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) ↔ (𝑟 + 𝑑) ≤ (abs‘(𝑟 · 𝑧)))) |
230 | 220, 229 | mtbid 314 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ¬ (𝑟 + 𝑑) ≤ (abs‘(𝑟 · 𝑧))) |
231 | 223 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) ∈ ℝ) |
232 | 231, 192 | ltnled 10184 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((abs‘(𝑟 · 𝑧)) < (𝑟 + 𝑑) ↔ ¬ (𝑟 + 𝑑) ≤ (abs‘(𝑟 · 𝑧)))) |
233 | 230, 232 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) < (𝑟 + 𝑑)) |
234 | 204, 233 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 · (abs‘𝑧)) < (𝑟 + 𝑑)) |
235 | 186, 192,
188 | ltmuldiv2d 11920 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · (abs‘𝑧)) < (𝑟 + 𝑑) ↔ (abs‘𝑧) < ((𝑟 + 𝑑) / 𝑟))) |
236 | 234, 235 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) < ((𝑟 + 𝑑) / 𝑟)) |
237 | | flltp1 12601 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑟 + 𝑑) / 𝑟) ∈ ℝ → ((𝑟 + 𝑑) / 𝑟) < ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) |
238 | 193, 237 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 + 𝑑) / 𝑟) < ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) |
239 | 186, 193,
196, 236, 238 | lttrd 10198 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) < ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) |
240 | 186, 196,
239 | ltled 10185 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) |
241 | 184, 186,
196, 198, 240 | letrd 10194 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(abs‘(ℜ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) |
242 | 182 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈
ℝ) |
243 | 242, 196 | absled 14169 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
((abs‘(ℜ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))) |
244 | 241, 243 | mpbid 222 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) |
245 | 195 | znegcld 11484 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1) ∈ ℤ) |
246 | | elfz 12332 |
. . . . . . . . . . . . . . . . 17
⊢
(((ℜ‘𝑧)
∈ ℤ ∧ -((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ ∧
((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ) →
((ℜ‘𝑧) ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))) |
247 | 182, 245,
195, 246 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((ℜ‘𝑧) ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))) |
248 | 244, 247 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) |
249 | 180 | simp3bi 1078 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ ℤ[i] →
(ℑ‘𝑧) ∈
ℤ) |
250 | 249 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈
ℤ) |
251 | 250 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈
ℂ) |
252 | 251 | abscld 14175 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(abs‘(ℑ‘𝑧)) ∈ ℝ) |
253 | | absimle 14049 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ ℂ →
(abs‘(ℑ‘𝑧)) ≤ (abs‘𝑧)) |
254 | 185, 253 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(abs‘(ℑ‘𝑧)) ≤ (abs‘𝑧)) |
255 | 252, 186,
196, 254, 240 | letrd 10194 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(abs‘(ℑ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) |
256 | 250 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈
ℝ) |
257 | 256, 196 | absled 14169 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
((abs‘(ℑ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))) |
258 | 255, 257 | mpbid 222 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) |
259 | | elfz 12332 |
. . . . . . . . . . . . . . . . 17
⊢
(((ℑ‘𝑧)
∈ ℤ ∧ -((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ ∧
((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ) →
((ℑ‘𝑧) ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))) |
260 | 250, 245,
195, 259 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((ℑ‘𝑧) ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))) |
261 | 258, 260 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) |
262 | 185 | replimd 13937 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑧 = ((ℜ‘𝑧) + (i · (ℑ‘𝑧)))) |
263 | 262 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))) |
264 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = (ℜ‘𝑧) → (𝑎 + (i · 𝑏)) = ((ℜ‘𝑧) + (i · 𝑏))) |
265 | 264 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (ℜ‘𝑧) → (𝑟 · (𝑎 + (i · 𝑏))) = (𝑟 · ((ℜ‘𝑧) + (i · 𝑏)))) |
266 | 265 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (ℜ‘𝑧) → ((𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏))) ↔ (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · 𝑏))))) |
267 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = (ℑ‘𝑧) → (i · 𝑏) = (i ·
(ℑ‘𝑧))) |
268 | 267 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (ℑ‘𝑧) → ((ℜ‘𝑧) + (i · 𝑏)) = ((ℜ‘𝑧) + (i ·
(ℑ‘𝑧)))) |
269 | 268 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (ℑ‘𝑧) → (𝑟 · ((ℜ‘𝑧) + (i · 𝑏))) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))) |
270 | 269 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (ℑ‘𝑧) → ((𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · 𝑏))) ↔ (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧)))))) |
271 | 266, 270 | rspc2ev 3324 |
. . . . . . . . . . . . . . 15
⊢
(((ℜ‘𝑧)
∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∧ (ℑ‘𝑧) ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∧ (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))) → ∃𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏)))) |
272 | 248, 261,
263, 271 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ∃𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏)))) |
273 | 272 | ex 450 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ ((((𝑟 · 𝑧)(ball‘(abs ∘
− ))𝑟) ∩ 𝑋) ≠ ∅ →
∃𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏))))) |
274 | 172, 173 | elrnmpt2 6773 |
. . . . . . . . . . . . 13
⊢ ((𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ↔ ∃𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏)))) |
275 | 273, 274 | syl6ibr 242 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ ((((𝑟 · 𝑧)(ball‘(abs ∘
− ))𝑟) ∩ 𝑋) ≠ ∅ → (𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))) |
276 | 157 | ineq1d 3813 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑟 · 𝑧) → ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)) |
277 | 276 | neeq1d 2853 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑟 · 𝑧) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ ↔ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅)) |
278 | | eleq1 2689 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑟 · 𝑧) → (𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ↔ (𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))) |
279 | 277, 278 | imbi12d 334 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑟 · 𝑧) → ((((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))) ↔ ((((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → (𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))))) |
280 | 275, 279 | syl5ibrcom 237 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ (𝑥 = (𝑟 · 𝑧) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))))) |
281 | 280 | rexlimdva 3031 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
→ (∃𝑧 ∈
ℤ[i] 𝑥 = (𝑟 · 𝑧) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))))) |
282 | 179, 281 | syl5bi 232 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
→ (𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧)) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))))) |
283 | 282 | 3imp 1256 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧)) ∧ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))) |
284 | 283 | rabssdv 3682 |
. . . . . . 7
⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
→ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ⊆ ran (𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))) |
285 | | ssfi 8180 |
. . . . . . 7
⊢ ((ran
(𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ∈ Fin ∧ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ⊆ ran (𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))) → {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin) |
286 | 178, 284,
285 | sylancr 695 |
. . . . . 6
⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
→ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin) |
287 | 168, 286 | rexlimddv 3035 |
. . . . 5
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin) |
288 | | iuneq1 4534 |
. . . . . . . 8
⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → ∪
𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) = ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟)) |
289 | 288 | sseq2d 3633 |
. . . . . . 7
⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → (𝑋 ⊆ ∪
𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ↔ 𝑋 ⊆ ∪
𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟))) |
290 | | rabeq 3192 |
. . . . . . . 8
⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} = {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅}) |
291 | 290 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → ({𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin ↔ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈
Fin)) |
292 | 289, 291 | anbi12d 747 |
. . . . . 6
⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → ((𝑋 ⊆ ∪
𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin) ↔ (𝑋 ⊆ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈
Fin))) |
293 | 292 | rspcev 3309 |
. . . . 5
⊢ ((ran
(𝑧 ∈ ℤ[i]
↦ (𝑟 · 𝑧)) ∈ 𝒫 ℂ
∧ (𝑋 ⊆ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)) →
∃𝑦 ∈ 𝒫
ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈
Fin)) |
294 | 13, 163, 287, 293 | syl12anc 1324 |
. . . 4
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) →
∃𝑦 ∈ 𝒫
ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈
Fin)) |
295 | 294 | ralrimiva 2966 |
. . 3
⊢ (𝐷 ∈ (Bnd‘𝑋) → ∀𝑟 ∈ ℝ+
∃𝑦 ∈ 𝒫
ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈
Fin)) |
296 | 15 | sstotbnd3 33575 |
. . . 4
⊢ (((abs
∘ − ) ∈ (Met‘ℂ) ∧ 𝑋 ⊆ ℂ) → (𝐷 ∈ (TotBnd‘𝑋) ↔ ∀𝑟 ∈ ℝ+ ∃𝑦 ∈ 𝒫 ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈
Fin))) |
297 | 14, 17, 296 | sylancr 695 |
. . 3
⊢ (𝐷 ∈ (Bnd‘𝑋) → (𝐷 ∈ (TotBnd‘𝑋) ↔ ∀𝑟 ∈ ℝ+ ∃𝑦 ∈ 𝒫 ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈
Fin))) |
298 | 295, 297 | mpbird 247 |
. 2
⊢ (𝐷 ∈ (Bnd‘𝑋) → 𝐷 ∈ (TotBnd‘𝑋)) |
299 | 1, 298 | impbii 199 |
1
⊢ (𝐷 ∈ (TotBnd‘𝑋) ↔ 𝐷 ∈ (Bnd‘𝑋)) |