| Step | Hyp | Ref
| Expression |
| 1 | | totbndbnd 37796 |
. 2
⊢ (𝐷 ∈ (TotBnd‘𝑋) → 𝐷 ∈ (Bnd‘𝑋)) |
| 2 | | rpcn 13045 |
. . . . . . . . . 10
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℂ) |
| 3 | 2 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℂ) |
| 4 | | gzcn 16970 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℤ[i] → 𝑧 ∈
ℂ) |
| 5 | | mulcl 11239 |
. . . . . . . . 9
⊢ ((𝑟 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑟 · 𝑧) ∈ ℂ) |
| 6 | 3, 4, 5 | syl2an 596 |
. . . . . . . 8
⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ 𝑧 ∈ ℤ[i]) →
(𝑟 · 𝑧) ∈
ℂ) |
| 7 | 6 | fmpttd 7135 |
. . . . . . 7
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧)):ℤ[i]⟶ℂ) |
| 8 | 7 | frnd 6744 |
. . . . . 6
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → ran
(𝑧 ∈ ℤ[i]
↦ (𝑟 · 𝑧)) ⊆
ℂ) |
| 9 | | cnex 11236 |
. . . . . . 7
⊢ ℂ
∈ V |
| 10 | 9 | elpw2 5334 |
. . . . . 6
⊢ (ran
(𝑧 ∈ ℤ[i]
↦ (𝑟 · 𝑧)) ∈ 𝒫 ℂ
↔ ran (𝑧 ∈
ℤ[i] ↦ (𝑟
· 𝑧)) ⊆
ℂ) |
| 11 | 8, 10 | sylibr 234 |
. . . . 5
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → ran
(𝑧 ∈ ℤ[i]
↦ (𝑟 · 𝑧)) ∈ 𝒫
ℂ) |
| 12 | | cnmet 24792 |
. . . . . . . . . . . . . . . . 17
⊢ (abs
∘ − ) ∈ (Met‘ℂ) |
| 13 | | cntotbnd.d |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐷 = ((abs ∘ − )
↾ (𝑋 × 𝑋)) |
| 14 | 13 | bnd2lem 37798 |
. . . . . . . . . . . . . . . . 17
⊢ (((abs
∘ − ) ∈ (Met‘ℂ) ∧ 𝐷 ∈ (Bnd‘𝑋)) → 𝑋 ⊆ ℂ) |
| 15 | 12, 14 | mpan 690 |
. . . . . . . . . . . . . . . 16
⊢ (𝐷 ∈ (Bnd‘𝑋) → 𝑋 ⊆ ℂ) |
| 16 | 15 | sselda 3983 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ ℂ) |
| 17 | 16 | adantrl 716 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ ℂ) |
| 18 | 17 | recld 15233 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (ℜ‘𝑦) ∈ ℝ) |
| 19 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℝ+) |
| 20 | 18, 19 | rerpdivcld 13108 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℜ‘𝑦) / 𝑟) ∈ ℝ) |
| 21 | | halfre 12480 |
. . . . . . . . . . . 12
⊢ (1 / 2)
∈ ℝ |
| 22 | | readdcl 11238 |
. . . . . . . . . . . 12
⊢
((((ℜ‘𝑦)
/ 𝑟) ∈ ℝ ∧
(1 / 2) ∈ ℝ) → (((ℜ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ) |
| 23 | 20, 21, 22 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((ℜ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ) |
| 24 | 23 | flcld 13838 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈
ℤ) |
| 25 | 17 | imcld 15234 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (ℑ‘𝑦) ∈ ℝ) |
| 26 | 25, 19 | rerpdivcld 13108 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℑ‘𝑦) / 𝑟) ∈ ℝ) |
| 27 | | readdcl 11238 |
. . . . . . . . . . . 12
⊢
((((ℑ‘𝑦)
/ 𝑟) ∈ ℝ ∧
(1 / 2) ∈ ℝ) → (((ℑ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ) |
| 28 | 26, 21, 27 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (((ℑ‘𝑦) / 𝑟) + (1 / 2)) ∈ ℝ) |
| 29 | 28 | flcld 13838 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈
ℤ) |
| 30 | | gzreim 16977 |
. . . . . . . . . 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 16970 |
. . . . . . . . . . . . . . 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 13079 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℂ) |
| 35 | 19 | rpne0d 13082 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ≠ 0) |
| 36 | 17, 34, 35 | divcld 12043 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑦 / 𝑟) ∈ ℂ) |
| 37 | 33, 36 | subcld 11620 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)) ∈ ℂ) |
| 38 | 37 | abscld 15475 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) ∈ ℝ) |
| 39 | | 1re 11261 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
| 40 | 39 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 1 ∈ ℝ) |
| 41 | 24 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈
ℂ) |
| 42 | | ax-icn 11214 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ i ∈
ℂ |
| 43 | 29 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈
ℂ) |
| 44 | | mulcl 11239 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((i
∈ ℂ ∧ (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈ ℂ) → (i
· (⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) ∈
ℂ) |
| 45 | 42, 43, 44 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) ∈
ℂ) |
| 46 | 20 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℜ‘𝑦) / 𝑟) ∈ ℂ) |
| 47 | 26 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℑ‘𝑦) / 𝑟) ∈ ℂ) |
| 48 | | mulcl 11239 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((i
∈ ℂ ∧ ((ℑ‘𝑦) / 𝑟) ∈ ℂ) → (i ·
((ℑ‘𝑦) / 𝑟)) ∈
ℂ) |
| 49 | 42, 47, 48 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (i · ((ℑ‘𝑦) / 𝑟)) ∈ ℂ) |
| 50 | 41, 45, 46, 49 | addsub4d 11667 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟)))) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + ((i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) − (i ·
((ℑ‘𝑦) / 𝑟))))) |
| 51 | 36 | replimd 15236 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑦 / 𝑟) = ((ℜ‘(𝑦 / 𝑟)) + (i · (ℑ‘(𝑦 / 𝑟))))) |
| 52 | 19 | rpred 13077 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℝ) |
| 53 | 52, 17, 35 | redivd 15268 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (ℜ‘(𝑦 / 𝑟)) = ((ℜ‘𝑦) / 𝑟)) |
| 54 | 52, 17, 35 | imdivd 15269 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (ℑ‘(𝑦 / 𝑟)) = ((ℑ‘𝑦) / 𝑟)) |
| 55 | 54 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (i · (ℑ‘(𝑦 / 𝑟))) = (i · ((ℑ‘𝑦) / 𝑟))) |
| 56 | 53, 55 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((ℜ‘(𝑦 / 𝑟)) + (i · (ℑ‘(𝑦 / 𝑟)))) = (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟)))) |
| 57 | 51, 56 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑦 / 𝑟) = (((ℜ‘𝑦) / 𝑟) + (i · ((ℑ‘𝑦) / 𝑟)))) |
| 58 | 57 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . 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 11719 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (i ·
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) = ((i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) − (i ·
((ℑ‘𝑦) / 𝑟)))) |
| 61 | 60 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i ·
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + ((i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))) − (i ·
((ℑ‘𝑦) / 𝑟))))) |
| 62 | 50, 58, 61 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)) = (((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i ·
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))))) |
| 63 | 62 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) =
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i ·
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))) |
| 64 | 63 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) =
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) + (i ·
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))))↑2)) |
| 65 | 24 | zred 12722 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) ∈
ℝ) |
| 66 | 65, 20 | resubcld 11691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℝ) |
| 67 | 29 | zred 12722 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) ∈
ℝ) |
| 68 | 67, 26 | resubcld 11691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℝ) |
| 69 | | absreimsq 15331 |
. . . . . . . . . . . . . . . . 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 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) =
((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) +
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2))) |
| 72 | 66 | resqcld 14165 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) ∈ ℝ) |
| 73 | 68 | resqcld 14165 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2) ∈ ℝ) |
| 74 | 21 | resqcli 14225 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1 /
2)↑2) ∈ ℝ |
| 75 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((1 / 2)↑2) ∈
ℝ) |
| 76 | 21 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (1 / 2) ∈
ℝ) |
| 77 | | absresq 15341 |
. . . . . . . . . . . . . . . . . . 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 15379 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((ℜ‘𝑦) /
𝑟) ∈ ℝ →
(abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ≤ (1 / 2)) |
| 80 | 20, 79 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ≤ (1 / 2)) |
| 81 | 66 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)) ∈ ℂ) |
| 82 | 81 | abscld 15475 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ∈ ℝ) |
| 83 | 81 | absge0d 15483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤
(abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))) |
| 84 | | halfgt0 12482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 < (1
/ 2) |
| 85 | 21, 84 | elrpii 13037 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 / 2)
∈ ℝ+ |
| 86 | | rpge0 13048 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1 / 2)
∈ ℝ+ → 0 ≤ (1 / 2)) |
| 87 | 85, 86 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (1 / 2)) |
| 88 | 82, 76, 83, 87 | le2sqd 14296 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))) ≤ (1 / 2) ↔
((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))↑2) ≤ ((1 /
2)↑2))) |
| 89 | 80, 88 | mpbid 232 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟)))↑2) ≤ ((1 /
2)↑2)) |
| 90 | 78, 89 | eqbrtrrd 5167 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) ≤ ((1 /
2)↑2)) |
| 91 | | halfcn 12481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 / 2)
∈ ℂ |
| 92 | 91 | sqvali 14219 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1 /
2)↑2) = ((1 / 2) · (1 / 2)) |
| 93 | | halflt1 12484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 / 2)
< 1 |
| 94 | 21, 39, 21, 84 | ltmul1ii 12196 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1 / 2)
< 1 ↔ ((1 / 2) · (1 / 2)) < (1 · (1 /
2))) |
| 95 | 93, 94 | mpbi 230 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1 / 2)
· (1 / 2)) < (1 · (1 / 2)) |
| 96 | 91 | mullidi 11266 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1
· (1 / 2)) = (1 / 2) |
| 97 | 95, 96 | breqtri 5168 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1 / 2)
· (1 / 2)) < (1 / 2) |
| 98 | 92, 97 | eqbrtri 5164 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1 /
2)↑2) < (1 / 2) |
| 99 | 98 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((1 / 2)↑2) < (1 /
2)) |
| 100 | 72, 75, 76, 90, 99 | lelttrd 11419 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) < (1 / 2)) |
| 101 | | absresq 15341 |
. . . . . . . . . . . . . . . . . . 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 15379 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((ℑ‘𝑦)
/ 𝑟) ∈ ℝ →
(abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ≤ (1 / 2)) |
| 104 | 26, 103 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ≤ (1 / 2)) |
| 105 | 68 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)) ∈ ℂ) |
| 106 | 105 | abscld 15475 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ∈ ℝ) |
| 107 | 105 | absge0d 15483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤
(abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))) |
| 108 | 106, 76, 107, 87 | le2sqd 14296 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))) ≤ (1 / 2) ↔
((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))↑2) ≤ ((1 /
2)↑2))) |
| 109 | 104, 108 | mpbid 232 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟)))↑2) ≤ ((1 /
2)↑2)) |
| 110 | 102, 109 | eqbrtrrd 5167 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2) ≤ ((1 /
2)↑2)) |
| 111 | 73, 75, 76, 110, 99 | lelttrd 11419 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2) < (1 / 2)) |
| 112 | 72, 73, 40, 100, 111 | lt2halvesd 12514 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) − ((ℜ‘𝑦) / 𝑟))↑2) +
(((⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))) − ((ℑ‘𝑦) / 𝑟))↑2)) < 1) |
| 113 | 71, 112 | eqbrtrd 5165 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) < 1) |
| 114 | | sq1 14234 |
. . . . . . . . . . . . . 14
⊢
(1↑2) = 1 |
| 115 | 113, 114 | breqtrrdi 5185 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) < (1↑2)) |
| 116 | 37 | absge0d 15483 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) |
| 117 | | 0le1 11786 |
. . . . . . . . . . . . . . 15
⊢ 0 ≤
1 |
| 118 | 117 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ 1) |
| 119 | 38, 40, 116, 118 | lt2sqd 14295 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) < 1 ↔
((abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))↑2) <
(1↑2))) |
| 120 | 115, 119 | mpbird 257 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) →
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) < 1) |
| 121 | 38, 40, 19, 120 | ltmul2dd 13133 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 ·
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) < (𝑟 · 1)) |
| 122 | 34, 33 | mulcld 11281 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) ∈
ℂ) |
| 123 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (abs
∘ − ) = (abs ∘ − ) |
| 124 | 123 | cnmetdval 24791 |
. . . . . . . . . . . . 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 11719 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 ·
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) = ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − (𝑟 · (𝑦 / 𝑟)))) |
| 127 | 17, 34, 35 | divcan2d 12045 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · (𝑦 / 𝑟)) = 𝑦) |
| 128 | 127 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − (𝑟 · (𝑦 / 𝑟))) = ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)) |
| 129 | 126, 128 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 ·
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))) = ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)) |
| 130 | 129 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘(𝑟 ·
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = (abs‘((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦))) |
| 131 | 34, 37 | absmuld 15493 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘(𝑟 ·
(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = ((abs‘𝑟) ·
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))))) |
| 132 | 130, 131 | eqtr3d 2779 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2)))))) − 𝑦)) = ((abs‘𝑟) ·
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))))) |
| 133 | 19 | rpge0d 13081 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 0 ≤ 𝑟) |
| 134 | 52, 133 | absidd 15461 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs‘𝑟) = 𝑟) |
| 135 | 134 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((abs‘𝑟) ·
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = (𝑟 ·
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟))))) |
| 136 | 125, 132,
135 | 3eqtrrd 2782 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 ·
(abs‘(((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) − (𝑦 / 𝑟)))) = ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦)) |
| 137 | 34 | mulridd 11278 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑟 · 1) = 𝑟) |
| 138 | 121, 136,
137 | 3brtr3d 5174 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) < 𝑟) |
| 139 | | cnxmet 24793 |
. . . . . . . . . . . 12
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
| 140 | 139 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
| 141 | | rpxr 13044 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
| 142 | 141 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑟 ∈ ℝ*) |
| 143 | | elbl2 24400 |
. . . . . . . . . . 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 839 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → (𝑦 ∈ ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘
− ))𝑟) ↔ ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(abs ∘ − )𝑦) < 𝑟)) |
| 145 | 138, 144 | mpbird 257 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘
− ))𝑟)) |
| 146 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑧 =
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) → (𝑟 · 𝑧) = (𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))) |
| 147 | 146 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑧 =
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) → ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) = ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘
− ))𝑟)) |
| 148 | 147 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝑧 =
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))) → (𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ↔ 𝑦 ∈ ((𝑟 ·
((⌊‘(((ℜ‘𝑦) / 𝑟) + (1 / 2))) + (i ·
(⌊‘(((ℑ‘𝑦) / 𝑟) + (1 / 2))))))(ball‘(abs ∘
− ))𝑟))) |
| 149 | 148 | rspcev 3622 |
. . . . . . . . 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 456 |
. . . . . . 7
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑦 ∈ 𝑋 → ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))) |
| 152 | | eliun 4995 |
. . . . . . . 8
⊢ (𝑦 ∈ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ↔ ∃𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟)) |
| 153 | | ovex 7464 |
. . . . . . . . . 10
⊢ (𝑟 · 𝑧) ∈ V |
| 154 | 153 | rgenw 3065 |
. . . . . . . . 9
⊢
∀𝑧 ∈
ℤ[i] (𝑟 ·
𝑧) ∈
V |
| 155 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧)) = (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) |
| 156 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑟 · 𝑧) → (𝑥(ball‘(abs ∘ − ))𝑟) = ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟)) |
| 157 | 156 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑟 · 𝑧) → (𝑦 ∈ (𝑥(ball‘(abs ∘ − ))𝑟) ↔ 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟))) |
| 158 | 155, 157 | rexrnmptw 7115 |
. . . . . . . . 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 275 |
. . . . . . 7
⊢ (𝑦 ∈ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ↔ ∃𝑧 ∈ ℤ[i] 𝑦 ∈ ((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟)) |
| 161 | 151, 160 | imbitrrdi 252 |
. . . . . 6
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑦 ∈ 𝑋 → 𝑦 ∈ ∪
𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟))) |
| 162 | 161 | ssrdv 3989 |
. . . . 5
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → 𝑋 ⊆ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟)) |
| 163 | | simpl 482 |
. . . . . . 7
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → 𝐷 ∈ (Bnd‘𝑋)) |
| 164 | | 0cn 11253 |
. . . . . . . 8
⊢ 0 ∈
ℂ |
| 165 | 13 | ssbnd 37795 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∈ (Met‘ℂ) ∧ 0 ∈ ℂ) →
(𝐷 ∈ (Bnd‘𝑋) ↔ ∃𝑑 ∈ ℝ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑))) |
| 166 | 12, 164, 165 | mp2an 692 |
. . . . . . 7
⊢ (𝐷 ∈ (Bnd‘𝑋) ↔ ∃𝑑 ∈ ℝ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)) |
| 167 | 163, 166 | sylib 218 |
. . . . . 6
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) →
∃𝑑 ∈ ℝ
𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑)) |
| 168 | | fzfi 14013 |
. . . . . . . . 9
⊢
(-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∈ Fin |
| 169 | | xpfi 9358 |
. . . . . . . . 9
⊢
(((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∈ Fin ∧
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∈ Fin) →
((-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) ∈ Fin) |
| 170 | 168, 168,
169 | mp2an 692 |
. . . . . . . 8
⊢
((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) ∈ Fin |
| 171 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) = (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) |
| 172 | | ovex 7464 |
. . . . . . . . . 10
⊢ (𝑟 · (𝑎 + (i · 𝑏))) ∈ V |
| 173 | 171, 172 | fnmpoi 8095 |
. . . . . . . . 9
⊢ (𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) Fn ((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) |
| 174 | | dffn4 6826 |
. . . . . . . . 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 230 |
. . . . . . . 8
⊢ (𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))):((-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) × (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))–onto→ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) |
| 176 | | fofi 9351 |
. . . . . . . 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 692 |
. . . . . . 7
⊢ ran
(𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ∈ Fin |
| 178 | 155, 153 | elrnmpti 5973 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ↔ ∃𝑧 ∈ ℤ[i] 𝑥 = (𝑟 · 𝑧)) |
| 179 | | elgz 16969 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ ℤ[i] ↔ (𝑧 ∈ ℂ ∧
(ℜ‘𝑧) ∈
ℤ ∧ (ℑ‘𝑧) ∈ ℤ)) |
| 180 | 179 | simp2bi 1147 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ ℤ[i] →
(ℜ‘𝑧) ∈
ℤ) |
| 181 | 180 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈
ℤ) |
| 182 | 181 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈
ℂ) |
| 183 | 182 | abscld 15475 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(abs‘(ℜ‘𝑧)) ∈ ℝ) |
| 184 | 4 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑧 ∈ ℂ) |
| 185 | 184 | abscld 15475 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) ∈
ℝ) |
| 186 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ 𝑟 ∈
ℝ+) |
| 187 | 186 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑟 ∈ ℝ+) |
| 188 | 187 | rpred 13077 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑟 ∈ ℝ) |
| 189 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ 𝑑 ∈
ℝ) |
| 190 | 189 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑑 ∈ ℝ) |
| 191 | 188, 190 | readdcld 11290 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 + 𝑑) ∈ ℝ) |
| 192 | 191, 187 | rerpdivcld 13108 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 + 𝑑) / 𝑟) ∈ ℝ) |
| 193 | 192 | flcld 13838 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(⌊‘((𝑟 + 𝑑) / 𝑟)) ∈ ℤ) |
| 194 | 193 | peano2zd 12725 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ) |
| 195 | 194 | zred 12722 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℝ) |
| 196 | | absrele 15347 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ ℂ →
(abs‘(ℜ‘𝑧)) ≤ (abs‘𝑧)) |
| 197 | 184, 196 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(abs‘(ℜ‘𝑧)) ≤ (abs‘𝑧)) |
| 198 | 187 | rpcnd 13079 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑟 ∈ ℂ) |
| 199 | 198, 184 | absmuld 15493 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) = ((abs‘𝑟) · (abs‘𝑧))) |
| 200 | 187 | rpge0d 13081 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 0 ≤ 𝑟) |
| 201 | 188, 200 | absidd 15461 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑟) = 𝑟) |
| 202 | 201 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((abs‘𝑟) · (abs‘𝑧)) = (𝑟 · (abs‘𝑧))) |
| 203 | 199, 202 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) = (𝑟 · (abs‘𝑧))) |
| 204 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑)) |
| 205 | | sslin 4243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ (𝑟 · 𝑧) ∈
ℂ) |
| 209 | 164 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ 0 ∈ ℂ) |
| 210 | 186 | rpxrd 13078 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ 𝑟 ∈
ℝ*) |
| 211 | 189 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ 𝑑 ∈
ℝ*) |
| 212 | | bldisj 24408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ)
∧ (𝑟 ∈
ℝ* ∧ 𝑑
∈ ℝ* ∧ (𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0))) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs
∘ − ))𝑑)) =
∅) |
| 213 | 212 | 3exp2 1355 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ)
→ (𝑟 ∈
ℝ* → (𝑑 ∈ ℝ* → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs
∘ − ))𝑑)) =
∅)))) |
| 214 | 213 | imp32 418 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (𝑟 · 𝑧) ∈ ℂ ∧ 0 ∈ ℂ)
∧ (𝑟 ∈
ℝ* ∧ 𝑑
∈ ℝ*)) → ((𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs
∘ − ))𝑑)) =
∅)) |
| 215 | 207, 208,
209, 210, 211, 214 | syl32anc 1380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ ((𝑟
+𝑒 𝑑)
≤ ((𝑟 · 𝑧)(abs ∘ − )0) →
(((𝑟 · 𝑧)(ball‘(abs ∘
− ))𝑟) ∩
(0(ball‘(abs ∘ − ))𝑑)) = ∅)) |
| 216 | | sseq0 4403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝑟 ·
𝑧)(ball‘(abs ∘
− ))𝑟) ∩ 𝑋) ⊆ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ (0(ball‘(abs
∘ − ))𝑑)) ∧
(((𝑟 · 𝑧)(ball‘(abs ∘
− ))𝑟) ∩
(0(ball‘(abs ∘ − ))𝑑)) = ∅) → (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = ∅) |
| 217 | 206, 215,
216 | syl6an 684 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ ((𝑟
+𝑒 𝑑)
≤ ((𝑟 · 𝑧)(abs ∘ − )0) →
(((𝑟 · 𝑧)(ball‘(abs ∘
− ))𝑟) ∩ 𝑋) = ∅)) |
| 218 | 217 | necon3ad 2953 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ ((((𝑟 · 𝑧)(ball‘(abs ∘
− ))𝑟) ∩ 𝑋) ≠ ∅ → ¬
(𝑟 +𝑒
𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0))) |
| 219 | 218 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ¬ (𝑟 +𝑒 𝑑) ≤ ((𝑟 · 𝑧)(abs ∘ − )0)) |
| 220 | | rexadd 13274 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑟 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑟 +𝑒 𝑑) = (𝑟 + 𝑑)) |
| 221 | 188, 190,
220 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 +𝑒 𝑑) = (𝑟 + 𝑑)) |
| 222 | 208 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 · 𝑧) ∈ ℂ) |
| 223 | 123 | cnmetdval 24791 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 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 11609 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · 𝑧) − 0) = (𝑟 · 𝑧)) |
| 226 | 225 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘((𝑟 · 𝑧) − 0)) = (abs‘(𝑟 · 𝑧))) |
| 227 | 224, 226 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · 𝑧)(abs ∘ − )0) = (abs‘(𝑟 · 𝑧))) |
| 228 | 221, 227 | breq12d 5156 |
. . . . . . . . . . . . . . . . . . . . . . . 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 15475 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) ∈ ℝ) |
| 231 | 230, 191 | ltnled 11408 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((abs‘(𝑟 · 𝑧)) < (𝑟 + 𝑑) ↔ ¬ (𝑟 + 𝑑) ≤ (abs‘(𝑟 · 𝑧)))) |
| 232 | 229, 231 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘(𝑟 · 𝑧)) < (𝑟 + 𝑑)) |
| 233 | 203, 232 | eqbrtrrd 5167 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 · (abs‘𝑧)) < (𝑟 + 𝑑)) |
| 234 | 185, 191,
187 | ltmuldiv2d 13125 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 · (abs‘𝑧)) < (𝑟 + 𝑑) ↔ (abs‘𝑧) < ((𝑟 + 𝑑) / 𝑟))) |
| 235 | 233, 234 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) < ((𝑟 + 𝑑) / 𝑟)) |
| 236 | | flltp1 13840 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑟 + 𝑑) / 𝑟) ∈ ℝ → ((𝑟 + 𝑑) / 𝑟) < ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) |
| 237 | 192, 236 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((𝑟 + 𝑑) / 𝑟) < ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) |
| 238 | 185, 192,
195, 235, 237 | lttrd 11422 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) < ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) |
| 239 | 185, 195,
238 | ltled 11409 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (abs‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) |
| 240 | 183, 185,
195, 197, 239 | letrd 11418 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(abs‘(ℜ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) |
| 241 | 181 | zred 12722 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈
ℝ) |
| 242 | 241, 195 | absled 15469 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
((abs‘(ℜ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))) |
| 243 | 240, 242 | mpbid 232 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) |
| 244 | 194 | znegcld 12724 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1) ∈ ℤ) |
| 245 | | elfz 13553 |
. . . . . . . . . . . . . . . . 17
⊢
(((ℜ‘𝑧)
∈ ℤ ∧ -((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ ∧
((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ) →
((ℜ‘𝑧) ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))) |
| 246 | 181, 244,
194, 245 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((ℜ‘𝑧) ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℜ‘𝑧) ∧ (ℜ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))) |
| 247 | 243, 246 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℜ‘𝑧) ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) |
| 248 | 179 | simp3bi 1148 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ ℤ[i] →
(ℑ‘𝑧) ∈
ℤ) |
| 249 | 248 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈
ℤ) |
| 250 | 249 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈
ℂ) |
| 251 | 250 | abscld 15475 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(abs‘(ℑ‘𝑧)) ∈ ℝ) |
| 252 | | absimle 15348 |
. . . . . . . . . . . . . . . . . . 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 11418 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(abs‘(ℑ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) |
| 255 | 249 | zred 12722 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈
ℝ) |
| 256 | 255, 195 | absled 15469 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
((abs‘(ℑ‘𝑧)) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))) |
| 257 | 254, 256 | mpbid 232 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) →
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) |
| 258 | | elfz 13553 |
. . . . . . . . . . . . . . . . 17
⊢
(((ℑ‘𝑧)
∈ ℤ ∧ -((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ ∧
((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ∈ ℤ) →
((ℑ‘𝑧) ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))) |
| 259 | 249, 244,
194, 258 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ((ℑ‘𝑧) ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↔ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1) ≤ (ℑ‘𝑧) ∧ (ℑ‘𝑧) ≤ ((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)))) |
| 260 | 257, 259 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (ℑ‘𝑧) ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))) |
| 261 | 184 | replimd 15236 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑧 = ((ℜ‘𝑧) + (i · (ℑ‘𝑧)))) |
| 262 | 261 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))) |
| 263 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = (ℜ‘𝑧) → (𝑎 + (i · 𝑏)) = ((ℜ‘𝑧) + (i · 𝑏))) |
| 264 | 263 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (ℜ‘𝑧) → (𝑟 · (𝑎 + (i · 𝑏))) = (𝑟 · ((ℜ‘𝑧) + (i · 𝑏)))) |
| 265 | 264 | eqeq2d 2748 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (ℜ‘𝑧) → ((𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏))) ↔ (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · 𝑏))))) |
| 266 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = (ℑ‘𝑧) → (i · 𝑏) = (i ·
(ℑ‘𝑧))) |
| 267 | 266 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (ℑ‘𝑧) → ((ℜ‘𝑧) + (i · 𝑏)) = ((ℜ‘𝑧) + (i ·
(ℑ‘𝑧)))) |
| 268 | 267 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (ℑ‘𝑧) → (𝑟 · ((ℜ‘𝑧) + (i · 𝑏))) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))) |
| 269 | 268 | eqeq2d 2748 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (ℑ‘𝑧) → ((𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · 𝑏))) ↔ (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧)))))) |
| 270 | 265, 269 | rspc2ev 3635 |
. . . . . . . . . . . . . . 15
⊢
(((ℜ‘𝑧)
∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∧ (ℑ‘𝑧) ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ∧ (𝑟 · 𝑧) = (𝑟 · ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))) → ∃𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏)))) |
| 271 | 247, 260,
262, 270 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢
(((((𝐷 ∈
(Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+)
∧ (𝑑 ∈ ℝ
∧ 𝑋 ⊆
(0(ball‘(abs ∘ − ))𝑑))) ∧ 𝑧 ∈ ℤ[i]) ∧ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → ∃𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏)))) |
| 272 | 271 | ex 412 |
. . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ ((((𝑟 · 𝑧)(ball‘(abs ∘
− ))𝑟) ∩ 𝑋) ≠ ∅ →
∃𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏))))) |
| 273 | 171, 172 | elrnmpo 7569 |
. . . . . . . . . . . . 13
⊢ ((𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ↔ ∃𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))∃𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1))(𝑟 · 𝑧) = (𝑟 · (𝑎 + (i · 𝑏)))) |
| 274 | 272, 273 | imbitrrdi 252 |
. . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ ((((𝑟 · 𝑧)(ball‘(abs ∘
− ))𝑟) ∩ 𝑋) ≠ ∅ → (𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))) |
| 275 | 156 | ineq1d 4219 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑟 · 𝑧) → ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) = (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋)) |
| 276 | 275 | neeq1d 3000 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑟 · 𝑧) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ ↔ (((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅)) |
| 277 | | eleq1 2829 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑟 · 𝑧) → (𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))) ↔ (𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏)))))) |
| 278 | 276, 277 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑟 · 𝑧) → ((((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))) ↔ ((((𝑟 · 𝑧)(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → (𝑟 · 𝑧) ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))))) |
| 279 | 274, 278 | syl5ibrcom 247 |
. . . . . . . . . . 11
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑧 ∈ ℤ[i])
→ (𝑥 = (𝑟 · 𝑧) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))))) |
| 280 | 279 | rexlimdva 3155 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
→ (∃𝑧 ∈
ℤ[i] 𝑥 = (𝑟 · 𝑧) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))))) |
| 281 | 178, 280 | biimtrid 242 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
→ (𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧)) → (((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅ → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))))) |
| 282 | 281 | 3imp 1111 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
∧ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧)) ∧ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅) → 𝑥 ∈ ran (𝑎 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))) |
| 283 | 282 | rabssdv 4075 |
. . . . . . 7
⊢ (((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 ⊆ (0(ball‘(abs
∘ − ))𝑑)))
→ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ⊆ ran (𝑎 ∈
(-((⌊‘((𝑟 +
𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)), 𝑏 ∈ (-((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)...((⌊‘((𝑟 + 𝑑) / 𝑟)) + 1)) ↦ (𝑟 · (𝑎 + (i · 𝑏))))) |
| 284 | | ssfi 9213 |
. . . . . . 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 3161 |
. . . . 5
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) → {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin) |
| 287 | | iuneq1 5008 |
. . . . . . . 8
⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → ∪
𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) = ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟)) |
| 288 | 287 | sseq2d 4016 |
. . . . . . 7
⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → (𝑋 ⊆ ∪
𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ↔ 𝑋 ⊆ ∪
𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦
(𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟))) |
| 289 | | rabeq 3451 |
. . . . . . . 8
⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} = {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅}) |
| 290 | 289 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → ({𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin ↔ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈
Fin)) |
| 291 | 288, 290 | anbi12d 632 |
. . . . . 6
⊢ (𝑦 = ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) → ((𝑋 ⊆ ∪
𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin) ↔ (𝑋 ⊆ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈
Fin))) |
| 292 | 291 | rspcev 3622 |
. . . . 5
⊢ ((ran
(𝑧 ∈ ℤ[i]
↦ (𝑟 · 𝑧)) ∈ 𝒫 ℂ
∧ (𝑋 ⊆ ∪ 𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧))(𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ ran (𝑧 ∈ ℤ[i] ↦ (𝑟 · 𝑧)) ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈ Fin)) →
∃𝑦 ∈ 𝒫
ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈
Fin)) |
| 293 | 11, 162, 286, 292 | syl12anc 837 |
. . . 4
⊢ ((𝐷 ∈ (Bnd‘𝑋) ∧ 𝑟 ∈ ℝ+) →
∃𝑦 ∈ 𝒫
ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈
Fin)) |
| 294 | 293 | ralrimiva 3146 |
. . 3
⊢ (𝐷 ∈ (Bnd‘𝑋) → ∀𝑟 ∈ ℝ+
∃𝑦 ∈ 𝒫
ℂ(𝑋 ⊆ ∪ 𝑥 ∈ 𝑦 (𝑥(ball‘(abs ∘ − ))𝑟) ∧ {𝑥 ∈ 𝑦 ∣ ((𝑥(ball‘(abs ∘ − ))𝑟) ∩ 𝑋) ≠ ∅} ∈
Fin)) |
| 295 | 13 | sstotbnd3 37783 |
. . . 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 257 |
. 2
⊢ (𝐷 ∈ (Bnd‘𝑋) → 𝐷 ∈ (TotBnd‘𝑋)) |
| 298 | 1, 297 | impbii 209 |
1
⊢ (𝐷 ∈ (TotBnd‘𝑋) ↔ 𝐷 ∈ (Bnd‘𝑋)) |