Step | Hyp | Ref
| Expression |
1 | | totbndbnd 35943 |
. 2
⊢ (𝐷 ∈ (TotBnd‘𝑋) → 𝐷 ∈ (Bnd‘𝑋)) |
2 | | rpcn 12739 |
. . . . . . . . . 10
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℂ) |
3 | 2 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℂ) |
4 | | gzcn 16631 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℤ[i] → 𝑧 ∈
ℂ) |
5 | | mulcl 10956 |
. . . . . . . . 9
⊢ ((𝑟 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑟 · 𝑧) ∈ ℂ) |
6 | 3, 4, 5 | syl2an 596 |
. . . . . . . 8
⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ 𝑧 ∈ ℤ[i]) →
(𝑟 · 𝑧) ∈
ℂ) |
7 | 6 | fmpttd 6986 |
. . . . . . 7
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧)):ℤ[i]⟶ℂ) |
8 | 7 | frnd 6606 |
. . . . . 6
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → ran
(𝑧 ∈ ℤ[i]
↦ (𝑟 · 𝑧)) ⊆
ℂ) |
9 | | cnex 10953 |
. . . . . . 7
⊢ ℂ
∈ V |
10 | 9 | elpw2 5273 |
. . . . . 6
⊢ (ran
(𝑧 ∈ ℤ[i]
↦ (𝑟 · 𝑧)) ∈ 𝒫 ℂ
↔ ran (𝑧 ∈
ℤ[i] ↦ (𝑟
· 𝑧)) ⊆
ℂ) |
11 | 8, 10 | sylibr 233 |
. . . . 5
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → ran
(𝑧 ∈ ℤ[i]
↦ (𝑟 · 𝑧)) ∈ 𝒫
ℂ) |
12 | | cnmet 23933 |
. . . . . . . . . . . . . . . . 17
⊢ (abs
∘ − ) ∈ (Met‘ℂ) |
13 | | cntotbnd.d |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐷 = ((abs ∘ − )
↾ (𝑋 × 𝑋)) |
14 | 13 | bnd2lem 35945 |
. . . . . . . . . . . . . . . . 17
⊢ (((abs
∘ − ) ∈ (Met‘ℂ) ∧ 𝐷 ∈ (Bnd‘𝑋)) → 𝑋 ⊆ ℂ) |
15 | 12, 14 | mpan 687 |
. . . . . . . . . . . . . . . 16
⊢ (𝐷 ∈ (Bnd‘𝑋) → 𝑋 ⊆ ℂ) |
16 | 15 | sselda 3926 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ ℂ) |
17 | 16 | adantrl 713 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ ℂ) |
18 | 17 | recld 14903 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (ℜ‘𝑦) ∈ ℝ) |
19 | | simprl 768 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℝ+) |
20 | 18, 19 | rerpdivcld 12802 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℜ‘𝑦) / 𝑟) ∈ ℝ) |
21 | | halfre 12187 |
. . . . . . . . . . . 12
⊢ (1 / 2)
∈ ℝ |
22 | | readdcl 10955 |
. . . . . . . . . . . 12
⊢
((((ℜ‘𝑦)
/ 𝑟) ∈ ℝ ∧
(1 / 2) ∈ ℝ) → (((ℜ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ) |
23 | 20, 21, 22 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((ℜ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ) |
24 | 23 | flcld 13516 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈
ℤ) |
25 | 17 | imcld 14904 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (ℑ‘𝑦) ∈ ℝ) |
26 | 25, 19 | rerpdivcld 12802 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℑ‘𝑦) / 𝑟) ∈ ℝ) |
27 | | readdcl 10955 |
. . . . . . . . . . . 12
⊢
((((ℑ‘𝑦)
/ 𝑟) ∈ ℝ ∧
(1 / 2) ∈ ℝ) → (((ℑ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ) |
28 | 26, 21, 27 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((ℑ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ) |
29 | 28 | flcld 13516 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈
ℤ) |
30 | | gzreim 16638 |
. . . . . . . . . 10
⊢
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℤ ∧
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℤ) →
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈
ℤ[i]) |
31 | 24, 29, 30 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈
ℤ[i]) |
32 | | gzcn 16631 |
. . . . . . . . . . . . . . 15
⊢
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℤ[i] →
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈
ℂ) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈
ℂ) |
34 | 19 | rpcnd 12773 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℂ) |
35 | 19 | rpne0d 12776 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ≠ 0) |
36 | 17, 34, 35 | divcld 11751 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑦 / 𝑟) ∈ ℂ) |
37 | 33, 36 | subcld 11332 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)) ∈ ℂ) |
38 | 37 | abscld 15146 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) ∈ ℝ) |
39 | | 1re 10976 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
40 | 39 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 1 ∈ ℝ) |
41 | 24 | zcnd 12426 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈
ℂ) |
42 | | ax-icn 10931 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ i ∈
ℂ |
43 | 29 | zcnd 12426 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈
ℂ) |
44 | | mulcl 10956 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((i
∈ ℂ ∧ (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℂ) → (i
· (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) ∈
ℂ) |
45 | 42, 43, 44 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) ∈
ℂ) |
46 | 20 | recnd 11004 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℜ‘𝑦) / 𝑟) ∈ ℂ) |
47 | 26 | recnd 11004 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℑ‘𝑦) / 𝑟) ∈ ℂ) |
48 | | mulcl 10956 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((i
∈ ℂ ∧ ((ℑ‘𝑦) / 𝑟) ∈ ℂ) → (i ·
((ℑ‘𝑦) / 𝑟)) ∈
ℂ) |
49 | 42, 47, 48 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (i · ((ℑ‘𝑦) / 𝑟)) ∈ ℂ) |
50 | 41, 45, 46, 49 | addsub4d 11379 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟)))) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + ((i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) − (i ·
((ℑ‘𝑦) / 𝑟))))) |
51 | 36 | replimd 14906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑦 / 𝑟) = ((ℜ‘(𝑦 / 𝑟)) + (i · (ℑ‘(𝑦 / 𝑟))))) |
52 | 19 | rpred 12771 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℝ) |
53 | 52, 17, 35 | redivd 14938 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (ℜ‘(𝑦 / 𝑟)) = ((ℜ‘𝑦) / 𝑟)) |
54 | 52, 17, 35 | imdivd 14939 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (ℑ‘(𝑦 / 𝑟)) = ((ℑ‘𝑦) / 𝑟)) |
55 | 54 | oveq2d 7287 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (i · (ℑ‘(𝑦 / 𝑟))) = (i · ((ℑ‘𝑦) / 𝑟))) |
56 | 53, 55 | oveq12d 7289 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℜ‘(𝑦 / 𝑟)) + (i · (ℑ‘(𝑦 / 𝑟)))) = (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟)))) |
57 | 51, 56 | eqtrd 2780 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑦 / 𝑟) = (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟)))) |
58 | 57 | oveq2d 7287 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟))))) |
59 | 42 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → i ∈ ℂ) |
60 | 59, 43, 47 | subdid 11431 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (i ·
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) = ((i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) − (i ·
((ℑ‘𝑦) / 𝑟)))) |
61 | 60 | oveq2d 7287 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i ·
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + ((i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) − (i ·
((ℑ‘𝑦) / 𝑟))))) |
62 | 50, 58, 61 | 3eqtr4d 2790 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i ·
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))))) |
63 | 62 | fveq2d 6775 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) =
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i ·
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))) |
64 | 63 | oveq1d 7286 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) =
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i ·
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))↑2)) |
65 | 24 | zred 12425 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈
ℝ) |
66 | 65, 20 | resubcld 11403 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℝ) |
67 | 29 | zred 12425 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈
ℝ) |
68 | 67, 26 | resubcld 11403 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℝ) |
69 | | absreimsq 15002 |
. . . . . . . . . . . . . . . . 17
⊢
((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℝ ∧
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℝ) →
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i ·
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))↑2) =
((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) +
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2))) |
70 | 66, 68, 69 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i ·
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))↑2) =
((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) +
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2))) |
71 | 64, 70 | eqtrd 2780 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) =
((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) +
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2))) |
72 | 66 | resqcld 13963 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) ∈ ℝ) |
73 | 68 | resqcld 13963 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2) ∈ ℝ) |
74 | 21 | resqcli 13901 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1 /
2)↑2) ∈ ℝ |
75 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((1 / 2)↑2) ∈
ℝ) |
76 | 21 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (1 / 2) ∈
ℝ) |
77 | | absresq 15012 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℝ →
((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))↑2) =
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2)) |
78 | 66, 77 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))↑2) =
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2)) |
79 | | rddif 15050 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((ℜ‘𝑦) /
𝑟) ∈ ℝ →
(abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ≤ (1 / 2)) |
80 | 20, 79 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ≤ (1 / 2)) |
81 | 66 | recnd 11004 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℂ) |
82 | 81 | abscld 15146 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ∈ ℝ) |
83 | 81 | absge0d 15154 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤
(abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))) |
84 | | halfgt0 12189 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 < (1
/ 2) |
85 | 21, 84 | elrpii 12732 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 / 2)
∈ ℝ+ |
86 | | rpge0 12742 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1 / 2)
∈ ℝ+ → 0 ≤ (1 / 2)) |
87 | 85, 86 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (1 / 2)) |
88 | 82, 76, 83, 87 | le2sqd 13972 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ≤ (1 / 2) ↔
((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))↑2) ≤ ((1 /
2)↑2))) |
89 | 80, 88 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))↑2) ≤ ((1 /
2)↑2)) |
90 | 78, 89 | eqbrtrrd 5103 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) ≤ ((1 /
2)↑2)) |
91 | | halfcn 12188 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 / 2)
∈ ℂ |
92 | 91 | sqvali 13895 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1 /
2)↑2) = ((1 / 2) · (1 / 2)) |
93 | | halflt1 12191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 / 2)
< 1 |
94 | 21, 39, 21, 84 | ltmul1ii 11903 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1 / 2)
< 1 ↔ ((1 / 2) · (1 / 2)) < (1 · (1 /
2))) |
95 | 93, 94 | mpbi 229 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1 / 2)
· (1 / 2)) < (1 · (1 / 2)) |
96 | 91 | mulid2i 10981 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1
· (1 / 2)) = (1 / 2) |
97 | 95, 96 | breqtri 5104 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1 / 2)
· (1 / 2)) < (1 / 2) |
98 | 92, 97 | eqbrtri 5100 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1 /
2)↑2) < (1 / 2) |
99 | 98 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((1 / 2)↑2) < (1 /
2)) |
100 | 72, 75, 76, 90, 99 | lelttrd 11133 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) < (1 / 2)) |
101 | | absresq 15012 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℝ →
((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))↑2) =
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)) |
102 | 68, 101 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))↑2) =
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)) |
103 | | rddif 15050 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((ℑ‘𝑦)
/ 𝑟) ∈ ℝ →
(abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ≤ (1 / 2)) |
104 | 26, 103 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ≤ (1 / 2)) |
105 | 68 | recnd 11004 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℂ) |
106 | 105 | abscld 15146 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ∈ ℝ) |
107 | 105 | absge0d 15154 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤
(abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))) |
108 | 106, 76, 107, 87 | le2sqd 13972 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ≤ (1 / 2) ↔
((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))↑2) ≤ ((1 /
2)↑2))) |
109 | 104, 108 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))↑2) ≤ ((1 /
2)↑2)) |
110 | 102, 109 | eqbrtrrd 5103 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2) ≤ ((1 /
2)↑2)) |
111 | 73, 75, 76, 110, 99 | lelttrd 11133 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2) < (1 / 2)) |
112 | 72, 73, 40, 100, 111 | lt2halvesd 12221 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) +
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)) < 1) |
113 | 71, 112 | eqbrtrd 5101 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) < 1) |
114 | | sq1 13910 |
. . . . . . . . . . . . . 14
⊢
(1↑2) = 1 |
115 | 113, 114 | breqtrrdi 5121 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) < (1↑2)) |
116 | 37 | absge0d 15154 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) |
117 | | 0le1 11498 |
. . . . . . . . . . . . . . 15
⊢ 0 ≤
1 |
118 | 117 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ 1) |
119 | 38, 40, 116, 118 | lt2sqd 13971 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) < 1 ↔
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) <
(1↑2))) |
120 | 115, 119 | mpbird 256 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) < 1) |
121 | 38, 40, 19, 120 | ltmul2dd 12827 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 ·
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) < (𝑟 · 1)) |
122 | 34, 33 | mulcld 10996 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) ∈
ℂ) |
123 | | eqid 2740 |
. . . . . . . . . . . . . 14
⊢ (abs
∘ − ) = (abs ∘ − ) |
124 | 123 | cnmetdval 23932 |
. . . . . . . . . . . . 13
⊢ (((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) = (abs‘((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦))) |
125 | 122, 17, 124 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) = (abs‘((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦))) |
126 | 34, 33, 36 | subdid 11431 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 ·
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) = ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − (𝑟 · (𝑦 / 𝑟)))) |
127 | 17, 34, 35 | divcan2d 11753 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · (𝑦 / 𝑟)) = 𝑦) |
128 | 127 | oveq2d 7287 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − (𝑟 · (𝑦 / 𝑟))) = ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)) |
129 | 126, 128 | eqtrd 2780 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 ·
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) = ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)) |
130 | 129 | fveq2d 6775 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘(𝑟 ·
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = (abs‘((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦))) |
131 | 34, 37 | absmuld 15164 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘(𝑟 ·
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = ((abs‘𝑟) ·
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))))) |
132 | 130, 131 | eqtr3d 2782 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)) = ((abs‘𝑟) ·
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))))) |
133 | 19 | rpge0d 12775 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ 𝑟) |
134 | 52, 133 | absidd 15132 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘𝑟) = 𝑟) |
135 | 134 | oveq1d 7286 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘𝑟) ·
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = (𝑟 ·
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))))) |
136 | 125, 132,
135 | 3eqtrrd 2785 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 ·
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦)) |
137 | 34 | mulid1d 10993 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · 1) = 𝑟) |
138 | 121, 136,
137 | 3brtr3d 5110 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) < 𝑟) |
139 | | cnxmet 23934 |
. . . . . . . . . . . 12
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
140 | 139 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
141 | | rpxr 12738 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
142 | 141 | ad2antrl 725 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℝ*) |
143 | | elbl2 23541 |
. . . . . . . . . . 11
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑦 ∈ ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘
− ))𝑟) ↔ ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) < 𝑟)) |
144 | 140, 142,
122, 17, 143 | syl22anc 836 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑦 ∈ ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘
− ))𝑟) ↔ ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) < 𝑟)) |
145 | 138, 144 | mpbird 256 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘
− ))𝑟)) |
146 | | oveq2 7279 |
. . . . . . . . . . . 12
⊢ (𝑧 =
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) → (𝑟 · 𝑧) = (𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))) |
147 | 146 | oveq1d 7286 |
. . . . . . . . . . 11
⊢ (𝑧 =
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) → ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) = ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘
− ))𝑟)) |
148 | 147 | eleq2d 2826 |
. . . . . . . . . 10
⊢ (𝑧 =
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) → (𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ↔ 𝑦 ∈ ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘
− ))𝑟))) |
149 | 148 | rspcev 3561 |
. . . . . . . . 9
⊢
((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) ∈ ℤ[i] ∧ 𝑦 ∈ ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘
− ))𝑟)) →
∃𝑧 ∈ ℤ[i]
𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟)) |
150 | 31, 145, 149 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟)) |
151 | 150 | expr 457 |
. . . . . . 7
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑦 ∈ 𝑋 → ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))) |
152 | | eliun 4934 |
. . . . . . . 8
⊢ (𝑦 ∈ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ↔ ∃𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) |
153 | | ovex 7304 |
. . . . . . . . . 10
⊢ (𝑟 · 𝑧) ∈ V |
154 | 153 | rgenw 3078 |
. . . . . . . . 9
⊢
∀𝑧 ∈
ℤ[i] (𝑟 ·
𝑧) ∈
V |
155 | | eqid 2740 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧)) = (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) |
156 | | oveq1 7278 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑟 · 𝑧) → (𝑥(ball‘(abs ∘ − ))𝑟) = ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟)) |
157 | 156 | eleq2d 2826 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑟 · 𝑧) → (𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))) |
158 | 155, 157 | rexrnmptw 6968 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
ℤ[i] (𝑟 ·
𝑧) ∈ V →
(∃𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧))𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))) |
159 | 154, 158 | ax-mp 5 |
. . . . . . . 8
⊢
(∃𝑥 ∈ ran
(𝑧 ∈ ℤ[i]
↦ (𝑟 · 𝑧))𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟)) |
160 | 152, 159 | bitri 274 |
. . . . . . 7
⊢ (𝑦 ∈ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ↔ ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟)) |
161 | 151, 160 | syl6ibr 251 |
. . . . . 6
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑦 ∈ 𝑋 → 𝑦 ∈ ∪
𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟))) |
162 | 161 | ssrdv 3932 |
. . . . 5
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → 𝑋 ⊆ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟)) |
163 | | simpl 483 |
. . . . . . 7
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → 𝐷 ∈ (Bnd‘𝑋)) |
164 | | 0cn 10968 |
. . . . . . . 8
⊢ 0 ∈
ℂ |
165 | 13 | ssbnd 35942 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∈ (Met‘ℂ) ∧ 0 ∈ ℂ) →
(𝐷 ∈ (Bnd‘𝑋) ↔ ∃𝑑 ∈ ℝ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑))) |
166 | 12, 164, 165 | mp2an 689 |
. . . . . . 7
⊢ (𝐷 ∈ (Bnd‘𝑋) ↔ ∃𝑑 ∈ ℝ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)) |
167 | 163, 166 | sylib 217 |
. . . . . 6
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) →
∃𝑑 ∈ ℝ
𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑)) |
168 | | fzfi 13690 |
. . . . . . . . 9
⊢
(-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∈ Fin |
169 | | xpfi 9063 |
. . . . . . . . 9
⊢
(((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∈ Fin ∧
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∈ Fin) →
((-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) ∈ Fin) |
170 | 168, 168,
169 | mp2an 689 |
. . . . . . . 8
⊢
((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) ∈ Fin |
171 | | eqid 2740 |
. . . . . . . . . 10
⊢ (𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) = (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) |
172 | | ovex 7304 |
. . . . . . . . . 10
⊢ (𝑟 · (𝑎 + (i · 𝑏))) ∈ V |
173 | 171, 172 | fnmpoi 7903 |
. . . . . . . . 9
⊢ (𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) Fn ((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) |
174 | | dffn4 6692 |
. . . . . . . . 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 · 𝑏))))) |
175 | 173, 174 | mpbi 229 |
. . . . . . . 8
⊢ (𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))):((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))–onto→ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) |
176 | | fofi 9083 |
. . . . . . . 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) |
177 | 170, 175,
176 | mp2an 689 |
. . . . . . 7
⊢ ran
(𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ∈ Fin |
178 | 155, 153 | elrnmpti 5868 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ↔ ∃𝑧 ∈ ℤ[i] 𝑥 = (𝑟 · 𝑧)) |
179 | | elgz 16630 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ ℤ[i] ↔ (𝑧 ∈ ℂ ∧
(ℜ‘𝑧) ∈
ℤ ∧ (ℑ‘𝑧) ∈ ℤ)) |
180 | 179 | simp2bi 1145 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ ℤ[i] →
(ℜ‘𝑧) ∈
ℤ) |
181 | 180 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈
ℤ) |
182 | 181 | zcnd 12426 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈
ℂ) |
183 | 182 | abscld 15146 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(abs‘(ℜ‘𝑧)) ∈ ℝ) |
184 | 4 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑧 ∈ ℂ) |
185 | 184 | abscld 15146 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) ∈
ℝ) |
186 | | simpllr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ 𝑟 ∈
ℝ+) |
187 | 186 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑟 ∈ ℝ+) |
188 | 187 | rpred 12771 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑟 ∈ ℝ) |
189 | | simplrl 774 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ 𝑑 ∈
ℝ) |
190 | 189 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑑 ∈ ℝ) |
191 | 188, 190 | readdcld 11005 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 + 𝑑) ∈ ℝ) |
192 | 191, 187 | rerpdivcld 12802 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 + 𝑑) / 𝑟) ∈ ℝ) |
193 | 192 | flcld 13516 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(⌊‘((𝑟 + 𝑑) / 𝑟)) ∈ ℤ) |
194 | 193 | peano2zd 12428 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ) |
195 | 194 | zred 12425 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℝ) |
196 | | absrele 15018 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ ℂ →
(abs‘(ℜ‘𝑧)) ≤ (abs‘𝑧)) |
197 | 184, 196 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(abs‘(ℜ‘𝑧)) ≤ (abs‘𝑧)) |
198 | 187 | rpcnd 12773 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑟 ∈ ℂ) |
199 | 198, 184 | absmuld 15164 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) = ((abs‘𝑟) · (abs‘𝑧))) |
200 | 187 | rpge0d 12775 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 0 ≤ 𝑟) |
201 | 188, 200 | absidd 15132 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑟) = 𝑟) |
202 | 201 | oveq1d 7286 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((abs‘𝑟) · (abs‘𝑧)) = (𝑟 · (abs‘𝑧))) |
203 | 199, 202 | eqtrd 2780 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) = (𝑟 · (abs‘𝑧))) |
204 | | simplrr 775 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑)) |
205 | | sslin 4174 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑) →
(((𝑟 · 𝑧)(ball‘(abs ∘
− ))𝑟) ∩ 𝑋) ⊆ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs
∘ − ))𝑑))) |
206 | 204, 205 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ (((𝑟 · 𝑧)(ball‘(abs ∘
− ))𝑟) ∩ 𝑋) ⊆ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs
∘ − ))𝑑))) |
207 | 139 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ (abs ∘ − ) ∈
(∞Met‘ℂ)) |
208 | 6 | adantlr 712 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ (𝑟 · 𝑧) ∈
ℂ) |
209 | 164 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ 0 ∈ ℂ) |
210 | 186 | rpxrd 12772 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ 𝑟 ∈
ℝ*) |
211 | 189 | rexrd 11026 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ 𝑑 ∈
ℝ*) |
212 | | bldisj 23549 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ)
∧ (𝑟 ∈
ℝ* ∧ 𝑑
∈ ℝ* ∧ (𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0))) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs
∘ − ))𝑑)) =
∅) |
213 | 212 | 3exp2 1353 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ)
→ (𝑟 ∈
ℝ* → (𝑑 ∈ ℝ* → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs
∘ − ))𝑑)) =
∅)))) |
214 | 213 | imp32 419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ)
∧ (𝑟 ∈
ℝ* ∧ 𝑑
∈ ℝ*)) → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs
∘ − ))𝑑)) =
∅)) |
215 | 207, 208,
209, 210, 211, 214 | syl32anc 1377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ ((𝑟
+𝑒 𝑑)
≤ ((𝑟 · 𝑧)(abs ∘ − )0) →
(((𝑟 · 𝑧)(ball‘(abs ∘
− ))𝑟) ∩
(0(ball‘(abs ∘ − ))𝑑)) = ∅)) |
216 | | sseq0 4339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝑟 ·
𝑧)(ball‘(abs ∘
− ))𝑟) ∩ 𝑋) ⊆ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs
∘ − ))𝑑)) ∧
(((𝑟 · 𝑧)(ball‘(abs ∘
− ))𝑟) ∩
(0(ball‘(abs ∘ − ))𝑑)) = ∅) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ∅) |
217 | 206, 215,
216 | syl6an 681 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ ((𝑟
+𝑒 𝑑)
≤ ((𝑟 · 𝑧)(abs ∘ − )0) →
(((𝑟 · 𝑧)(ball‘(abs ∘
− ))𝑟) ∩ 𝑋) = ∅)) |
218 | 217 | necon3ad 2958 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ ((((𝑟 · 𝑧)(ball‘(abs ∘
− ))𝑟) ∩ 𝑋) ≠ ∅ → ¬
(𝑟 +𝑒
𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0))) |
219 | 218 | imp 407 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ¬ (𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0)) |
220 | | rexadd 12965 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑟 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑟 +𝑒 𝑑) = (𝑟 + 𝑑)) |
221 | 188, 190,
220 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 +𝑒 𝑑) = (𝑟 + 𝑑)) |
222 | 208 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 · 𝑧) ∈ ℂ) |
223 | 123 | cnmetdval 23932 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ)
→ ((𝑟 · 𝑧)(abs ∘ − )0) =
(abs‘((𝑟 ·
𝑧) −
0))) |
224 | 222, 164,
223 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · 𝑧)(abs ∘ − )0) =
(abs‘((𝑟 ·
𝑧) −
0))) |
225 | 222 | subid1d 11321 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · 𝑧) − 0) = (𝑟 · 𝑧)) |
226 | 225 | fveq2d 6775 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘((𝑟 · 𝑧) − 0)) = (abs‘(𝑟 · 𝑧))) |
227 | 224, 226 | eqtrd 2780 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · 𝑧)(abs ∘ − )0) = (abs‘(𝑟 · 𝑧))) |
228 | 221, 227 | breq12d 5092 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) ↔ (𝑟 + 𝑑) ≤ (abs‘(𝑟 · 𝑧)))) |
229 | 219, 228 | mtbid 324 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ¬ (𝑟 + 𝑑) ≤ (abs‘(𝑟 · 𝑧))) |
230 | 222 | abscld 15146 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) ∈ ℝ) |
231 | 230, 191 | ltnled 11122 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((abs‘(𝑟 · 𝑧)) < (𝑟 + 𝑑) ↔ ¬ (𝑟 + 𝑑) ≤ (abs‘(𝑟 · 𝑧)))) |
232 | 229, 231 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) < (𝑟 + 𝑑)) |
233 | 203, 232 | eqbrtrrd 5103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 · (abs‘𝑧)) < (𝑟 + 𝑑)) |
234 | 185, 191,
187 | ltmuldiv2d 12819 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · (abs‘𝑧)) < (𝑟 + 𝑑) ↔ (abs‘𝑧) < ((𝑟 + 𝑑) / 𝑟))) |
235 | 233, 234 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) < ((𝑟 + 𝑑) / 𝑟)) |
236 | | flltp1 13518 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑟 + 𝑑) / 𝑟) ∈ ℝ → ((𝑟 + 𝑑) / 𝑟) < ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) |
237 | 192, 236 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 + 𝑑) / 𝑟) < ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) |
238 | 185, 192,
195, 235, 237 | lttrd 11136 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) < ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) |
239 | 185, 195,
238 | ltled 11123 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) |
240 | 183, 185,
195, 197, 239 | letrd 11132 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(abs‘(ℜ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) |
241 | 181 | zred 12425 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈
ℝ) |
242 | 241, 195 | absled 15140 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
((abs‘(ℜ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))) |
243 | 240, 242 | mpbid 231 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) |
244 | 194 | znegcld 12427 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1) ∈ ℤ) |
245 | | elfz 13244 |
. . . . . . . . . . . . . . . . 17
⊢
(((ℜ‘𝑧)
∈ ℤ ∧ -((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ ∧
((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ) →
((ℜ‘𝑧) ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))) |
246 | 181, 244,
194, 245 | syl3anc 1370 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((ℜ‘𝑧) ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))) |
247 | 243, 246 | mpbird 256 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) |
248 | 179 | simp3bi 1146 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ ℤ[i] →
(ℑ‘𝑧) ∈
ℤ) |
249 | 248 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈
ℤ) |
250 | 249 | zcnd 12426 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈
ℂ) |
251 | 250 | abscld 15146 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(abs‘(ℑ‘𝑧)) ∈ ℝ) |
252 | | absimle 15019 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ ℂ →
(abs‘(ℑ‘𝑧)) ≤ (abs‘𝑧)) |
253 | 184, 252 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(abs‘(ℑ‘𝑧)) ≤ (abs‘𝑧)) |
254 | 251, 185,
195, 253, 239 | letrd 11132 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(abs‘(ℑ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) |
255 | 249 | zred 12425 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈
ℝ) |
256 | 255, 195 | absled 15140 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
((abs‘(ℑ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))) |
257 | 254, 256 | mpbid 231 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) |
258 | | elfz 13244 |
. . . . . . . . . . . . . . . . 17
⊢
(((ℑ‘𝑧)
∈ ℤ ∧ -((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ ∧
((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ) →
((ℑ‘𝑧) ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))) |
259 | 249, 244,
194, 258 | syl3anc 1370 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((ℑ‘𝑧) ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))) |
260 | 257, 259 | mpbird 256 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) |
261 | 184 | replimd 14906 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑧 = ((ℜ‘𝑧) + (i · (ℑ‘𝑧)))) |
262 | 261 | oveq2d 7287 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))) |
263 | | oveq1 7278 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = (ℜ‘𝑧) → (𝑎 + (i · 𝑏)) = ((ℜ‘𝑧) + (i · 𝑏))) |
264 | 263 | oveq2d 7287 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (ℜ‘𝑧) → (𝑟 · (𝑎 + (i · 𝑏))) = (𝑟 · ((ℜ‘𝑧) + (i · 𝑏)))) |
265 | 264 | eqeq2d 2751 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (ℜ‘𝑧) → ((𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏))) ↔ (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · 𝑏))))) |
266 | | oveq2 7279 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = (ℑ‘𝑧) → (i · 𝑏) = (i ·
(ℑ‘𝑧))) |
267 | 266 | oveq2d 7287 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (ℑ‘𝑧) → ((ℜ‘𝑧) + (i · 𝑏)) = ((ℜ‘𝑧) + (i ·
(ℑ‘𝑧)))) |
268 | 267 | oveq2d 7287 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (ℑ‘𝑧) → (𝑟 · ((ℜ‘𝑧) + (i · 𝑏))) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))) |
269 | 268 | eqeq2d 2751 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (ℑ‘𝑧) → ((𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · 𝑏))) ↔ (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧)))))) |
270 | 265, 269 | rspc2ev 3573 |
. . . . . . . . . . . . . . 15
⊢
(((ℜ‘𝑧)
∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∧ (ℑ‘𝑧) ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∧ (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))) → ∃𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏)))) |
271 | 247, 260,
262, 270 | syl3anc 1370 |
. . . . . . . . . . . . . 14
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ∃𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏)))) |
272 | 271 | ex 413 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ ((((𝑟 · 𝑧)(ball‘(abs ∘
− ))𝑟) ∩ 𝑋) ≠ ∅ →
∃𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏))))) |
273 | 171, 172 | elrnmpo 7404 |
. . . . . . . . . . . . 13
⊢ ((𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ↔ ∃𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏)))) |
274 | 272, 273 | syl6ibr 251 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ ((((𝑟 · 𝑧)(ball‘(abs ∘
− ))𝑟) ∩ 𝑋) ≠ ∅ → (𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))) |
275 | 156 | ineq1d 4151 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑟 · 𝑧) → ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)) |
276 | 275 | neeq1d 3005 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑟 · 𝑧) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ ↔ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅)) |
277 | | eleq1 2828 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑟 · 𝑧) → (𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ↔ (𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))) |
278 | 276, 277 | imbi12d 345 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑟 · 𝑧) → ((((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))) ↔ ((((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → (𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))))) |
279 | 274, 278 | syl5ibrcom 246 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ (𝑥 = (𝑟 · 𝑧) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))))) |
280 | 279 | rexlimdva 3215 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
→ (∃𝑧 ∈
ℤ[i] 𝑥 = (𝑟 · 𝑧) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))))) |
281 | 178, 280 | syl5bi 241 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
→ (𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧)) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))))) |
282 | 281 | 3imp 1110 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧)) ∧ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))) |
283 | 282 | rabssdv 4013 |
. . . . . . 7
⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
→ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ⊆ ran (𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))) |
284 | | ssfi 8938 |
. . . . . . 7
⊢ ((ran
(𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ∈ Fin ∧ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ⊆ ran (𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))) → {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin) |
285 | 177, 283,
284 | sylancr 587 |
. . . . . 6
⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
→ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin) |
286 | 167, 285 | rexlimddv 3222 |
. . . . 5
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin) |
287 | | iuneq1 4946 |
. . . . . . . 8
⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → ∪
𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) = ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟)) |
288 | 287 | sseq2d 3958 |
. . . . . . 7
⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → (𝑋 ⊆ ∪
𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ↔ 𝑋 ⊆ ∪
𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟))) |
289 | | rabeq 3417 |
. . . . . . . 8
⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} = {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅}) |
290 | 289 | eleq1d 2825 |
. . . . . . 7
⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → ({𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin ↔ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈
Fin)) |
291 | 288, 290 | anbi12d 631 |
. . . . . 6
⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → ((𝑋 ⊆ ∪
𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin) ↔ (𝑋 ⊆ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈
Fin))) |
292 | 291 | rspcev 3561 |
. . . . 5
⊢ ((ran
(𝑧 ∈ ℤ[i]
↦ (𝑟 · 𝑧)) ∈ 𝒫 ℂ
∧ (𝑋 ⊆ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)) →
∃𝑦 ∈ 𝒫
ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈
Fin)) |
293 | 11, 162, 286, 292 | syl12anc 834 |
. . . 4
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) →
∃𝑦 ∈ 𝒫
ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈
Fin)) |
294 | 293 | ralrimiva 3110 |
. . 3
⊢ (𝐷 ∈ (Bnd‘𝑋) → ∀𝑟 ∈ ℝ+
∃𝑦 ∈ 𝒫
ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈
Fin)) |
295 | 13 | sstotbnd3 35930 |
. . . 4
⊢ (((abs
∘ − ) ∈ (Met‘ℂ) ∧ 𝑋 ⊆ ℂ) → (𝐷 ∈ (TotBnd‘𝑋) ↔ ∀𝑟 ∈ ℝ+ ∃𝑦 ∈ 𝒫 ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈
Fin))) |
296 | 12, 15, 295 | sylancr 587 |
. . 3
⊢ (𝐷 ∈ (Bnd‘𝑋) → (𝐷 ∈ (TotBnd‘𝑋) ↔ ∀𝑟 ∈ ℝ+ ∃𝑦 ∈ 𝒫 ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈
Fin))) |
297 | 294, 296 | mpbird 256 |
. 2
⊢ (𝐷 ∈ (Bnd‘𝑋) → 𝐷 ∈ (TotBnd‘𝑋)) |
298 | 1, 297 | impbii 208 |
1
⊢ (𝐷 ∈ (TotBnd‘𝑋) ↔ 𝐷 ∈ (Bnd‘𝑋)) |