Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cntotbnd Structured version   Visualization version   GIF version

Theorem cntotbnd 36301
Description: A subset of the complex numbers is totally bounded iff it is bounded. (Contributed by Mario Carneiro, 14-Sep-2015.)
Hypothesis
Ref Expression
cntotbnd.d 𝐷 = ((abs ∘ βˆ’ ) β†Ύ (𝑋 Γ— 𝑋))
Assertion
Ref Expression
cntotbnd (𝐷 ∈ (TotBndβ€˜π‘‹) ↔ 𝐷 ∈ (Bndβ€˜π‘‹))

Proof of Theorem cntotbnd
Dummy variables π‘Ž 𝑏 𝑑 π‘Ÿ π‘₯ 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 totbndbnd 36294 . 2 (𝐷 ∈ (TotBndβ€˜π‘‹) β†’ 𝐷 ∈ (Bndβ€˜π‘‹))
2 rpcn 12930 . . . . . . . . . 10 (π‘Ÿ ∈ ℝ+ β†’ π‘Ÿ ∈ β„‚)
32adantl 483 . . . . . . . . 9 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) β†’ π‘Ÿ ∈ β„‚)
4 gzcn 16809 . . . . . . . . 9 (𝑧 ∈ β„€[i] β†’ 𝑧 ∈ β„‚)
5 mulcl 11140 . . . . . . . . 9 ((π‘Ÿ ∈ β„‚ ∧ 𝑧 ∈ β„‚) β†’ (π‘Ÿ Β· 𝑧) ∈ β„‚)
63, 4, 5syl2an 597 . . . . . . . 8 (((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ 𝑧 ∈ β„€[i]) β†’ (π‘Ÿ Β· 𝑧) ∈ β„‚)
76fmpttd 7064 . . . . . . 7 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) β†’ (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧)):β„€[i]βŸΆβ„‚)
87frnd 6677 . . . . . 6 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) β†’ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧)) βŠ† β„‚)
9 cnex 11137 . . . . . . 7 β„‚ ∈ V
109elpw2 5303 . . . . . 6 (ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧)) ∈ 𝒫 β„‚ ↔ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧)) βŠ† β„‚)
118, 10sylibr 233 . . . . 5 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) β†’ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧)) ∈ 𝒫 β„‚)
12 cnmet 24151 . . . . . . . . . . . . . . . . 17 (abs ∘ βˆ’ ) ∈ (Metβ€˜β„‚)
13 cntotbnd.d . . . . . . . . . . . . . . . . . 18 𝐷 = ((abs ∘ βˆ’ ) β†Ύ (𝑋 Γ— 𝑋))
1413bnd2lem 36296 . . . . . . . . . . . . . . . . 17 (((abs ∘ βˆ’ ) ∈ (Metβ€˜β„‚) ∧ 𝐷 ∈ (Bndβ€˜π‘‹)) β†’ 𝑋 βŠ† β„‚)
1512, 14mpan 689 . . . . . . . . . . . . . . . 16 (𝐷 ∈ (Bndβ€˜π‘‹) β†’ 𝑋 βŠ† β„‚)
1615sselda 3945 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ 𝑦 ∈ 𝑋) β†’ 𝑦 ∈ β„‚)
1716adantrl 715 . . . . . . . . . . . . . 14 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ 𝑦 ∈ β„‚)
1817recld 15085 . . . . . . . . . . . . 13 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (β„œβ€˜π‘¦) ∈ ℝ)
19 simprl 770 . . . . . . . . . . . . 13 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ π‘Ÿ ∈ ℝ+)
2018, 19rerpdivcld 12993 . . . . . . . . . . . 12 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((β„œβ€˜π‘¦) / π‘Ÿ) ∈ ℝ)
21 halfre 12372 . . . . . . . . . . . 12 (1 / 2) ∈ ℝ
22 readdcl 11139 . . . . . . . . . . . 12 ((((β„œβ€˜π‘¦) / π‘Ÿ) ∈ ℝ ∧ (1 / 2) ∈ ℝ) β†’ (((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2)) ∈ ℝ)
2320, 21, 22sylancl 587 . . . . . . . . . . 11 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2)) ∈ ℝ)
2423flcld 13709 . . . . . . . . . 10 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) ∈ β„€)
2517imcld 15086 . . . . . . . . . . . . 13 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (β„‘β€˜π‘¦) ∈ ℝ)
2625, 19rerpdivcld 12993 . . . . . . . . . . . 12 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((β„‘β€˜π‘¦) / π‘Ÿ) ∈ ℝ)
27 readdcl 11139 . . . . . . . . . . . 12 ((((β„‘β€˜π‘¦) / π‘Ÿ) ∈ ℝ ∧ (1 / 2) ∈ ℝ) β†’ (((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2)) ∈ ℝ)
2826, 21, 27sylancl 587 . . . . . . . . . . 11 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2)) ∈ ℝ)
2928flcld 13709 . . . . . . . . . 10 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) ∈ β„€)
30 gzreim 16816 . . . . . . . . . 10 (((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) ∈ β„€ ∧ (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) ∈ β„€) β†’ ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) ∈ β„€[i])
3124, 29, 30syl2anc 585 . . . . . . . . 9 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) ∈ β„€[i])
32 gzcn 16809 . . . . . . . . . . . . . . 15 (((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) ∈ β„€[i] β†’ ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) ∈ β„‚)
3331, 32syl 17 . . . . . . . . . . . . . 14 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) ∈ β„‚)
3419rpcnd 12964 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ π‘Ÿ ∈ β„‚)
3519rpne0d 12967 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ π‘Ÿ β‰  0)
3617, 34, 35divcld 11936 . . . . . . . . . . . . . 14 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (𝑦 / π‘Ÿ) ∈ β„‚)
3733, 36subcld 11517 . . . . . . . . . . . . 13 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (𝑦 / π‘Ÿ)) ∈ β„‚)
3837abscld 15327 . . . . . . . . . . . 12 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (absβ€˜(((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (𝑦 / π‘Ÿ))) ∈ ℝ)
39 1re 11160 . . . . . . . . . . . . 13 1 ∈ ℝ
4039a1i 11 . . . . . . . . . . . 12 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ 1 ∈ ℝ)
4124zcnd 12613 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) ∈ β„‚)
42 ax-icn 11115 . . . . . . . . . . . . . . . . . . . . 21 i ∈ β„‚
4329zcnd 12613 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) ∈ β„‚)
44 mulcl 11140 . . . . . . . . . . . . . . . . . . . . 21 ((i ∈ β„‚ ∧ (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) ∈ β„‚) β†’ (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2)))) ∈ β„‚)
4542, 43, 44sylancr 588 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2)))) ∈ β„‚)
4620recnd 11188 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((β„œβ€˜π‘¦) / π‘Ÿ) ∈ β„‚)
4726recnd 11188 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((β„‘β€˜π‘¦) / π‘Ÿ) ∈ β„‚)
48 mulcl 11140 . . . . . . . . . . . . . . . . . . . . 21 ((i ∈ β„‚ ∧ ((β„‘β€˜π‘¦) / π‘Ÿ) ∈ β„‚) β†’ (i Β· ((β„‘β€˜π‘¦) / π‘Ÿ)) ∈ β„‚)
4942, 47, 48sylancr 588 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (i Β· ((β„‘β€˜π‘¦) / π‘Ÿ)) ∈ β„‚)
5041, 45, 46, 49addsub4d 11564 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (((β„œβ€˜π‘¦) / π‘Ÿ) + (i Β· ((β„‘β€˜π‘¦) / π‘Ÿ)))) = (((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ)) + ((i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2)))) βˆ’ (i Β· ((β„‘β€˜π‘¦) / π‘Ÿ)))))
5136replimd 15088 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (𝑦 / π‘Ÿ) = ((β„œβ€˜(𝑦 / π‘Ÿ)) + (i Β· (β„‘β€˜(𝑦 / π‘Ÿ)))))
5219rpred 12962 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ π‘Ÿ ∈ ℝ)
5352, 17, 35redivd 15120 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (β„œβ€˜(𝑦 / π‘Ÿ)) = ((β„œβ€˜π‘¦) / π‘Ÿ))
5452, 17, 35imdivd 15121 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (β„‘β€˜(𝑦 / π‘Ÿ)) = ((β„‘β€˜π‘¦) / π‘Ÿ))
5554oveq2d 7374 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (i Β· (β„‘β€˜(𝑦 / π‘Ÿ))) = (i Β· ((β„‘β€˜π‘¦) / π‘Ÿ)))
5653, 55oveq12d 7376 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((β„œβ€˜(𝑦 / π‘Ÿ)) + (i Β· (β„‘β€˜(𝑦 / π‘Ÿ)))) = (((β„œβ€˜π‘¦) / π‘Ÿ) + (i Β· ((β„‘β€˜π‘¦) / π‘Ÿ))))
5751, 56eqtrd 2773 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (𝑦 / π‘Ÿ) = (((β„œβ€˜π‘¦) / π‘Ÿ) + (i Β· ((β„‘β€˜π‘¦) / π‘Ÿ))))
5857oveq2d 7374 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (𝑦 / π‘Ÿ)) = (((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (((β„œβ€˜π‘¦) / π‘Ÿ) + (i Β· ((β„‘β€˜π‘¦) / π‘Ÿ)))))
5942a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ i ∈ β„‚)
6059, 43, 47subdid 11616 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (i Β· ((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ))) = ((i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2)))) βˆ’ (i Β· ((β„‘β€˜π‘¦) / π‘Ÿ))))
6160oveq2d 7374 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ)) + (i Β· ((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ)))) = (((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ)) + ((i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2)))) βˆ’ (i Β· ((β„‘β€˜π‘¦) / π‘Ÿ)))))
6250, 58, 613eqtr4d 2783 . . . . . . . . . . . . . . . . . 18 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (𝑦 / π‘Ÿ)) = (((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ)) + (i Β· ((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ)))))
6362fveq2d 6847 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (absβ€˜(((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (𝑦 / π‘Ÿ))) = (absβ€˜(((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ)) + (i Β· ((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ))))))
6463oveq1d 7373 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((absβ€˜(((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (𝑦 / π‘Ÿ)))↑2) = ((absβ€˜(((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ)) + (i Β· ((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ)))))↑2))
6524zred 12612 . . . . . . . . . . . . . . . . . 18 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) ∈ ℝ)
6665, 20resubcld 11588 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ)) ∈ ℝ)
6729zred 12612 . . . . . . . . . . . . . . . . . 18 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) ∈ ℝ)
6867, 26resubcld 11588 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ)) ∈ ℝ)
69 absreimsq 15183 . . . . . . . . . . . . . . . . 17 ((((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ)) ∈ ℝ ∧ ((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ)) ∈ ℝ) β†’ ((absβ€˜(((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ)) + (i Β· ((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ)))))↑2) = ((((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ))↑2) + (((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ))↑2)))
7066, 68, 69syl2anc 585 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((absβ€˜(((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ)) + (i Β· ((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ)))))↑2) = ((((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ))↑2) + (((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ))↑2)))
7164, 70eqtrd 2773 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((absβ€˜(((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (𝑦 / π‘Ÿ)))↑2) = ((((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ))↑2) + (((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ))↑2)))
7266resqcld 14036 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ))↑2) ∈ ℝ)
7368resqcld 14036 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ))↑2) ∈ ℝ)
7421resqcli 14096 . . . . . . . . . . . . . . . . . 18 ((1 / 2)↑2) ∈ ℝ
7574a1i 11 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((1 / 2)↑2) ∈ ℝ)
7621a1i 11 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (1 / 2) ∈ ℝ)
77 absresq 15193 . . . . . . . . . . . . . . . . . . 19 (((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ)) ∈ ℝ β†’ ((absβ€˜((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ)))↑2) = (((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ))↑2))
7866, 77syl 17 . . . . . . . . . . . . . . . . . 18 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((absβ€˜((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ)))↑2) = (((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ))↑2))
79 rddif 15231 . . . . . . . . . . . . . . . . . . . 20 (((β„œβ€˜π‘¦) / π‘Ÿ) ∈ ℝ β†’ (absβ€˜((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ))) ≀ (1 / 2))
8020, 79syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (absβ€˜((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ))) ≀ (1 / 2))
8166recnd 11188 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ)) ∈ β„‚)
8281abscld 15327 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (absβ€˜((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ))) ∈ ℝ)
8381absge0d 15335 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ 0 ≀ (absβ€˜((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ))))
84 halfgt0 12374 . . . . . . . . . . . . . . . . . . . . . 22 0 < (1 / 2)
8521, 84elrpii 12923 . . . . . . . . . . . . . . . . . . . . 21 (1 / 2) ∈ ℝ+
86 rpge0 12933 . . . . . . . . . . . . . . . . . . . . 21 ((1 / 2) ∈ ℝ+ β†’ 0 ≀ (1 / 2))
8785, 86mp1i 13 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ 0 ≀ (1 / 2))
8882, 76, 83, 87le2sqd 14166 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((absβ€˜((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ))) ≀ (1 / 2) ↔ ((absβ€˜((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ)))↑2) ≀ ((1 / 2)↑2)))
8980, 88mpbid 231 . . . . . . . . . . . . . . . . . 18 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((absβ€˜((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ)))↑2) ≀ ((1 / 2)↑2))
9078, 89eqbrtrrd 5130 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ))↑2) ≀ ((1 / 2)↑2))
91 halfcn 12373 . . . . . . . . . . . . . . . . . . . 20 (1 / 2) ∈ β„‚
9291sqvali 14090 . . . . . . . . . . . . . . . . . . 19 ((1 / 2)↑2) = ((1 / 2) Β· (1 / 2))
93 halflt1 12376 . . . . . . . . . . . . . . . . . . . . 21 (1 / 2) < 1
9421, 39, 21, 84ltmul1ii 12088 . . . . . . . . . . . . . . . . . . . . 21 ((1 / 2) < 1 ↔ ((1 / 2) Β· (1 / 2)) < (1 Β· (1 / 2)))
9593, 94mpbi 229 . . . . . . . . . . . . . . . . . . . 20 ((1 / 2) Β· (1 / 2)) < (1 Β· (1 / 2))
9691mulid2i 11165 . . . . . . . . . . . . . . . . . . . 20 (1 Β· (1 / 2)) = (1 / 2)
9795, 96breqtri 5131 . . . . . . . . . . . . . . . . . . 19 ((1 / 2) Β· (1 / 2)) < (1 / 2)
9892, 97eqbrtri 5127 . . . . . . . . . . . . . . . . . 18 ((1 / 2)↑2) < (1 / 2)
9998a1i 11 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((1 / 2)↑2) < (1 / 2))
10072, 75, 76, 90, 99lelttrd 11318 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ))↑2) < (1 / 2))
101 absresq 15193 . . . . . . . . . . . . . . . . . . 19 (((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ)) ∈ ℝ β†’ ((absβ€˜((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ)))↑2) = (((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ))↑2))
10268, 101syl 17 . . . . . . . . . . . . . . . . . 18 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((absβ€˜((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ)))↑2) = (((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ))↑2))
103 rddif 15231 . . . . . . . . . . . . . . . . . . . 20 (((β„‘β€˜π‘¦) / π‘Ÿ) ∈ ℝ β†’ (absβ€˜((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ))) ≀ (1 / 2))
10426, 103syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (absβ€˜((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ))) ≀ (1 / 2))
10568recnd 11188 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ)) ∈ β„‚)
106105abscld 15327 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (absβ€˜((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ))) ∈ ℝ)
107105absge0d 15335 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ 0 ≀ (absβ€˜((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ))))
108106, 76, 107, 87le2sqd 14166 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((absβ€˜((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ))) ≀ (1 / 2) ↔ ((absβ€˜((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ)))↑2) ≀ ((1 / 2)↑2)))
109104, 108mpbid 231 . . . . . . . . . . . . . . . . . 18 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((absβ€˜((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ)))↑2) ≀ ((1 / 2)↑2))
110102, 109eqbrtrrd 5130 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ))↑2) ≀ ((1 / 2)↑2))
11173, 75, 76, 110, 99lelttrd 11318 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ))↑2) < (1 / 2))
11272, 73, 40, 100, 111lt2halvesd 12406 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„œβ€˜π‘¦) / π‘Ÿ))↑2) + (((βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))) βˆ’ ((β„‘β€˜π‘¦) / π‘Ÿ))↑2)) < 1)
11371, 112eqbrtrd 5128 . . . . . . . . . . . . . 14 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((absβ€˜(((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (𝑦 / π‘Ÿ)))↑2) < 1)
114 sq1 14105 . . . . . . . . . . . . . 14 (1↑2) = 1
115113, 114breqtrrdi 5148 . . . . . . . . . . . . 13 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((absβ€˜(((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (𝑦 / π‘Ÿ)))↑2) < (1↑2))
11637absge0d 15335 . . . . . . . . . . . . . 14 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ 0 ≀ (absβ€˜(((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (𝑦 / π‘Ÿ))))
117 0le1 11683 . . . . . . . . . . . . . . 15 0 ≀ 1
118117a1i 11 . . . . . . . . . . . . . 14 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ 0 ≀ 1)
11938, 40, 116, 118lt2sqd 14165 . . . . . . . . . . . . 13 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((absβ€˜(((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (𝑦 / π‘Ÿ))) < 1 ↔ ((absβ€˜(((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (𝑦 / π‘Ÿ)))↑2) < (1↑2)))
120115, 119mpbird 257 . . . . . . . . . . . 12 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (absβ€˜(((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (𝑦 / π‘Ÿ))) < 1)
12138, 40, 19, 120ltmul2dd 13018 . . . . . . . . . . 11 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (π‘Ÿ Β· (absβ€˜(((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (𝑦 / π‘Ÿ)))) < (π‘Ÿ Β· 1))
12234, 33mulcld 11180 . . . . . . . . . . . . 13 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (π‘Ÿ Β· ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2)))))) ∈ β„‚)
123 eqid 2733 . . . . . . . . . . . . . 14 (abs ∘ βˆ’ ) = (abs ∘ βˆ’ )
124123cnmetdval 24150 . . . . . . . . . . . . 13 (((π‘Ÿ Β· ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2)))))) ∈ β„‚ ∧ 𝑦 ∈ β„‚) β†’ ((π‘Ÿ Β· ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))))(abs ∘ βˆ’ )𝑦) = (absβ€˜((π‘Ÿ Β· ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2)))))) βˆ’ 𝑦)))
125122, 17, 124syl2anc 585 . . . . . . . . . . . 12 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((π‘Ÿ Β· ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))))(abs ∘ βˆ’ )𝑦) = (absβ€˜((π‘Ÿ Β· ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2)))))) βˆ’ 𝑦)))
12634, 33, 36subdid 11616 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (π‘Ÿ Β· (((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (𝑦 / π‘Ÿ))) = ((π‘Ÿ Β· ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2)))))) βˆ’ (π‘Ÿ Β· (𝑦 / π‘Ÿ))))
12717, 34, 35divcan2d 11938 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (π‘Ÿ Β· (𝑦 / π‘Ÿ)) = 𝑦)
128127oveq2d 7374 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((π‘Ÿ Β· ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2)))))) βˆ’ (π‘Ÿ Β· (𝑦 / π‘Ÿ))) = ((π‘Ÿ Β· ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2)))))) βˆ’ 𝑦))
129126, 128eqtrd 2773 . . . . . . . . . . . . . 14 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (π‘Ÿ Β· (((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (𝑦 / π‘Ÿ))) = ((π‘Ÿ Β· ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2)))))) βˆ’ 𝑦))
130129fveq2d 6847 . . . . . . . . . . . . 13 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (absβ€˜(π‘Ÿ Β· (((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (𝑦 / π‘Ÿ)))) = (absβ€˜((π‘Ÿ Β· ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2)))))) βˆ’ 𝑦)))
13134, 37absmuld 15345 . . . . . . . . . . . . 13 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (absβ€˜(π‘Ÿ Β· (((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (𝑦 / π‘Ÿ)))) = ((absβ€˜π‘Ÿ) Β· (absβ€˜(((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (𝑦 / π‘Ÿ)))))
132130, 131eqtr3d 2775 . . . . . . . . . . . 12 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (absβ€˜((π‘Ÿ Β· ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2)))))) βˆ’ 𝑦)) = ((absβ€˜π‘Ÿ) Β· (absβ€˜(((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (𝑦 / π‘Ÿ)))))
13319rpge0d 12966 . . . . . . . . . . . . . 14 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ 0 ≀ π‘Ÿ)
13452, 133absidd 15313 . . . . . . . . . . . . 13 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (absβ€˜π‘Ÿ) = π‘Ÿ)
135134oveq1d 7373 . . . . . . . . . . . 12 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((absβ€˜π‘Ÿ) Β· (absβ€˜(((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (𝑦 / π‘Ÿ)))) = (π‘Ÿ Β· (absβ€˜(((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (𝑦 / π‘Ÿ)))))
136125, 132, 1353eqtrrd 2778 . . . . . . . . . . 11 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (π‘Ÿ Β· (absβ€˜(((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) βˆ’ (𝑦 / π‘Ÿ)))) = ((π‘Ÿ Β· ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))))(abs ∘ βˆ’ )𝑦))
13734mulid1d 11177 . . . . . . . . . . 11 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (π‘Ÿ Β· 1) = π‘Ÿ)
138121, 136, 1373brtr3d 5137 . . . . . . . . . 10 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ ((π‘Ÿ Β· ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))))(abs ∘ βˆ’ )𝑦) < π‘Ÿ)
139 cnxmet 24152 . . . . . . . . . . . 12 (abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚)
140139a1i 11 . . . . . . . . . . 11 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚))
141 rpxr 12929 . . . . . . . . . . . 12 (π‘Ÿ ∈ ℝ+ β†’ π‘Ÿ ∈ ℝ*)
142141ad2antrl 727 . . . . . . . . . . 11 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ π‘Ÿ ∈ ℝ*)
143 elbl2 23759 . . . . . . . . . . 11 ((((abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚) ∧ π‘Ÿ ∈ ℝ*) ∧ ((π‘Ÿ Β· ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2)))))) ∈ β„‚ ∧ 𝑦 ∈ β„‚)) β†’ (𝑦 ∈ ((π‘Ÿ Β· ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))))(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ↔ ((π‘Ÿ Β· ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))))(abs ∘ βˆ’ )𝑦) < π‘Ÿ))
144140, 142, 122, 17, 143syl22anc 838 . . . . . . . . . 10 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ (𝑦 ∈ ((π‘Ÿ Β· ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))))(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ↔ ((π‘Ÿ Β· ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))))(abs ∘ βˆ’ )𝑦) < π‘Ÿ))
145138, 144mpbird 257 . . . . . . . . 9 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ 𝑦 ∈ ((π‘Ÿ Β· ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))))(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))
146 oveq2 7366 . . . . . . . . . . . 12 (𝑧 = ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) β†’ (π‘Ÿ Β· 𝑧) = (π‘Ÿ Β· ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2)))))))
147146oveq1d 7373 . . . . . . . . . . 11 (𝑧 = ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) β†’ ((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) = ((π‘Ÿ Β· ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))))(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))
148147eleq2d 2820 . . . . . . . . . 10 (𝑧 = ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) β†’ (𝑦 ∈ ((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ↔ 𝑦 ∈ ((π‘Ÿ Β· ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))))(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
149148rspcev 3580 . . . . . . . . 9 ((((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))) ∈ β„€[i] ∧ 𝑦 ∈ ((π‘Ÿ Β· ((βŒŠβ€˜(((β„œβ€˜π‘¦) / π‘Ÿ) + (1 / 2))) + (i Β· (βŒŠβ€˜(((β„‘β€˜π‘¦) / π‘Ÿ) + (1 / 2))))))(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)) β†’ βˆƒπ‘§ ∈ β„€[i] 𝑦 ∈ ((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))
15031, 145, 149syl2anc 585 . . . . . . . 8 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ (π‘Ÿ ∈ ℝ+ ∧ 𝑦 ∈ 𝑋)) β†’ βˆƒπ‘§ ∈ β„€[i] 𝑦 ∈ ((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))
151150expr 458 . . . . . . 7 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) β†’ (𝑦 ∈ 𝑋 β†’ βˆƒπ‘§ ∈ β„€[i] 𝑦 ∈ ((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
152 eliun 4959 . . . . . . . 8 (𝑦 ∈ βˆͺ π‘₯ ∈ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧))(π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ↔ βˆƒπ‘₯ ∈ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧))𝑦 ∈ (π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))
153 ovex 7391 . . . . . . . . . 10 (π‘Ÿ Β· 𝑧) ∈ V
154153rgenw 3065 . . . . . . . . 9 βˆ€π‘§ ∈ β„€[i] (π‘Ÿ Β· 𝑧) ∈ V
155 eqid 2733 . . . . . . . . . 10 (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧)) = (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧))
156 oveq1 7365 . . . . . . . . . . 11 (π‘₯ = (π‘Ÿ Β· 𝑧) β†’ (π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) = ((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))
157156eleq2d 2820 . . . . . . . . . 10 (π‘₯ = (π‘Ÿ Β· 𝑧) β†’ (𝑦 ∈ (π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ↔ 𝑦 ∈ ((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
158155, 157rexrnmptw 7046 . . . . . . . . 9 (βˆ€π‘§ ∈ β„€[i] (π‘Ÿ Β· 𝑧) ∈ V β†’ (βˆƒπ‘₯ ∈ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧))𝑦 ∈ (π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ↔ βˆƒπ‘§ ∈ β„€[i] 𝑦 ∈ ((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
159154, 158ax-mp 5 . . . . . . . 8 (βˆƒπ‘₯ ∈ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧))𝑦 ∈ (π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ↔ βˆƒπ‘§ ∈ β„€[i] 𝑦 ∈ ((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))
160152, 159bitri 275 . . . . . . 7 (𝑦 ∈ βˆͺ π‘₯ ∈ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧))(π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ↔ βˆƒπ‘§ ∈ β„€[i] 𝑦 ∈ ((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))
161151, 160syl6ibr 252 . . . . . 6 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) β†’ (𝑦 ∈ 𝑋 β†’ 𝑦 ∈ βˆͺ π‘₯ ∈ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧))(π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
162161ssrdv 3951 . . . . 5 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) β†’ 𝑋 βŠ† βˆͺ π‘₯ ∈ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧))(π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))
163 simpl 484 . . . . . . 7 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) β†’ 𝐷 ∈ (Bndβ€˜π‘‹))
164 0cn 11152 . . . . . . . 8 0 ∈ β„‚
16513ssbnd 36293 . . . . . . . 8 (((abs ∘ βˆ’ ) ∈ (Metβ€˜β„‚) ∧ 0 ∈ β„‚) β†’ (𝐷 ∈ (Bndβ€˜π‘‹) ↔ βˆƒπ‘‘ ∈ ℝ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑)))
16612, 164, 165mp2an 691 . . . . . . 7 (𝐷 ∈ (Bndβ€˜π‘‹) ↔ βˆƒπ‘‘ ∈ ℝ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))
167163, 166sylib 217 . . . . . 6 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) β†’ βˆƒπ‘‘ ∈ ℝ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))
168 fzfi 13883 . . . . . . . . 9 (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ∈ Fin
169 xpfi 9264 . . . . . . . . 9 (((-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ∈ Fin ∧ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ∈ Fin) β†’ ((-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) Γ— (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1))) ∈ Fin)
170168, 168, 169mp2an 691 . . . . . . . 8 ((-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) Γ— (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1))) ∈ Fin
171 eqid 2733 . . . . . . . . . 10 (π‘Ž ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)), 𝑏 ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ↦ (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏)))) = (π‘Ž ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)), 𝑏 ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ↦ (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏))))
172 ovex 7391 . . . . . . . . . 10 (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏))) ∈ V
173171, 172fnmpoi 8003 . . . . . . . . 9 (π‘Ž ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)), 𝑏 ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ↦ (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏)))) Fn ((-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) Γ— (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)))
174 dffn4 6763 . . . . . . . . 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 Β· 𝑏)))))
175173, 174mpbi 229 . . . . . . . 8 (π‘Ž ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)), 𝑏 ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ↦ (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏)))):((-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) Γ— (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)))–ontoβ†’ran (π‘Ž ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)), 𝑏 ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ↦ (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏))))
176 fofi 9285 . . . . . . . 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)
177170, 175, 176mp2an 691 . . . . . . 7 ran (π‘Ž ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)), 𝑏 ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ↦ (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏)))) ∈ Fin
178155, 153elrnmpti 5916 . . . . . . . . . 10 (π‘₯ ∈ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧)) ↔ βˆƒπ‘§ ∈ β„€[i] π‘₯ = (π‘Ÿ Β· 𝑧))
179 elgz 16808 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ β„€[i] ↔ (𝑧 ∈ β„‚ ∧ (β„œβ€˜π‘§) ∈ β„€ ∧ (β„‘β€˜π‘§) ∈ β„€))
180179simp2bi 1147 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ β„€[i] β†’ (β„œβ€˜π‘§) ∈ β„€)
181180ad2antlr 726 . . . . . . . . . . . . . . . . . . . 20 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (β„œβ€˜π‘§) ∈ β„€)
182181zcnd 12613 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (β„œβ€˜π‘§) ∈ β„‚)
183182abscld 15327 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (absβ€˜(β„œβ€˜π‘§)) ∈ ℝ)
1844ad2antlr 726 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ 𝑧 ∈ β„‚)
185184abscld 15327 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (absβ€˜π‘§) ∈ ℝ)
186 simpllr 775 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) β†’ π‘Ÿ ∈ ℝ+)
187186adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ π‘Ÿ ∈ ℝ+)
188187rpred 12962 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ π‘Ÿ ∈ ℝ)
189 simplrl 776 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) β†’ 𝑑 ∈ ℝ)
190189adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ 𝑑 ∈ ℝ)
191188, 190readdcld 11189 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (π‘Ÿ + 𝑑) ∈ ℝ)
192191, 187rerpdivcld 12993 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ ((π‘Ÿ + 𝑑) / π‘Ÿ) ∈ ℝ)
193192flcld 13709 . . . . . . . . . . . . . . . . . . . 20 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) ∈ β„€)
194193peano2zd 12615 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ ((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1) ∈ β„€)
195194zred 12612 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ ((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1) ∈ ℝ)
196 absrele 15199 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ β„‚ β†’ (absβ€˜(β„œβ€˜π‘§)) ≀ (absβ€˜π‘§))
197184, 196syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (absβ€˜(β„œβ€˜π‘§)) ≀ (absβ€˜π‘§))
198187rpcnd 12964 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ π‘Ÿ ∈ β„‚)
199198, 184absmuld 15345 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (absβ€˜(π‘Ÿ Β· 𝑧)) = ((absβ€˜π‘Ÿ) Β· (absβ€˜π‘§)))
200187rpge0d 12966 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ 0 ≀ π‘Ÿ)
201188, 200absidd 15313 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (absβ€˜π‘Ÿ) = π‘Ÿ)
202201oveq1d 7373 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ ((absβ€˜π‘Ÿ) Β· (absβ€˜π‘§)) = (π‘Ÿ Β· (absβ€˜π‘§)))
203199, 202eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (absβ€˜(π‘Ÿ Β· 𝑧)) = (π‘Ÿ Β· (absβ€˜π‘§)))
204 simplrr 777 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) β†’ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))
205 sslin 4195 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑) β†’ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) βŠ† (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ (0(ballβ€˜(abs ∘ βˆ’ ))𝑑)))
206204, 205syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) β†’ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) βŠ† (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ (0(ballβ€˜(abs ∘ βˆ’ ))𝑑)))
207139a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) β†’ (abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚))
2086adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) β†’ (π‘Ÿ Β· 𝑧) ∈ β„‚)
209164a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) β†’ 0 ∈ β„‚)
210186rpxrd 12963 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) β†’ π‘Ÿ ∈ ℝ*)
211189rexrd 11210 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) β†’ 𝑑 ∈ ℝ*)
212 bldisj 23767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚) ∧ (π‘Ÿ Β· 𝑧) ∈ β„‚ ∧ 0 ∈ β„‚) ∧ (π‘Ÿ ∈ ℝ* ∧ 𝑑 ∈ ℝ* ∧ (π‘Ÿ +𝑒 𝑑) ≀ ((π‘Ÿ Β· 𝑧)(abs ∘ βˆ’ )0))) β†’ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ (0(ballβ€˜(abs ∘ βˆ’ ))𝑑)) = βˆ…)
2132123exp2 1355 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚) ∧ (π‘Ÿ Β· 𝑧) ∈ β„‚ ∧ 0 ∈ β„‚) β†’ (π‘Ÿ ∈ ℝ* β†’ (𝑑 ∈ ℝ* β†’ ((π‘Ÿ +𝑒 𝑑) ≀ ((π‘Ÿ Β· 𝑧)(abs ∘ βˆ’ )0) β†’ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ (0(ballβ€˜(abs ∘ βˆ’ ))𝑑)) = βˆ…))))
214213imp32 420 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚) ∧ (π‘Ÿ Β· 𝑧) ∈ β„‚ ∧ 0 ∈ β„‚) ∧ (π‘Ÿ ∈ ℝ* ∧ 𝑑 ∈ ℝ*)) β†’ ((π‘Ÿ +𝑒 𝑑) ≀ ((π‘Ÿ Β· 𝑧)(abs ∘ βˆ’ )0) β†’ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ (0(ballβ€˜(abs ∘ βˆ’ ))𝑑)) = βˆ…))
215207, 208, 209, 210, 211, 214syl32anc 1379 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) β†’ ((π‘Ÿ +𝑒 𝑑) ≀ ((π‘Ÿ Β· 𝑧)(abs ∘ βˆ’ )0) β†’ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ (0(ballβ€˜(abs ∘ βˆ’ ))𝑑)) = βˆ…))
216 sseq0 4360 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) βŠ† (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ (0(ballβ€˜(abs ∘ βˆ’ ))𝑑)) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ (0(ballβ€˜(abs ∘ βˆ’ ))𝑑)) = βˆ…) β†’ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) = βˆ…)
217206, 215, 216syl6an 683 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) β†’ ((π‘Ÿ +𝑒 𝑑) ≀ ((π‘Ÿ Β· 𝑧)(abs ∘ βˆ’ )0) β†’ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) = βˆ…))
218217necon3ad 2953 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) β†’ ((((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ… β†’ Β¬ (π‘Ÿ +𝑒 𝑑) ≀ ((π‘Ÿ Β· 𝑧)(abs ∘ βˆ’ )0)))
219218imp 408 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ Β¬ (π‘Ÿ +𝑒 𝑑) ≀ ((π‘Ÿ Β· 𝑧)(abs ∘ βˆ’ )0))
220 rexadd 13157 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘Ÿ ∈ ℝ ∧ 𝑑 ∈ ℝ) β†’ (π‘Ÿ +𝑒 𝑑) = (π‘Ÿ + 𝑑))
221188, 190, 220syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (π‘Ÿ +𝑒 𝑑) = (π‘Ÿ + 𝑑))
222208adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (π‘Ÿ Β· 𝑧) ∈ β„‚)
223123cnmetdval 24150 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((π‘Ÿ Β· 𝑧) ∈ β„‚ ∧ 0 ∈ β„‚) β†’ ((π‘Ÿ Β· 𝑧)(abs ∘ βˆ’ )0) = (absβ€˜((π‘Ÿ Β· 𝑧) βˆ’ 0)))
224222, 164, 223sylancl 587 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ ((π‘Ÿ Β· 𝑧)(abs ∘ βˆ’ )0) = (absβ€˜((π‘Ÿ Β· 𝑧) βˆ’ 0)))
225222subid1d 11506 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ ((π‘Ÿ Β· 𝑧) βˆ’ 0) = (π‘Ÿ Β· 𝑧))
226225fveq2d 6847 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (absβ€˜((π‘Ÿ Β· 𝑧) βˆ’ 0)) = (absβ€˜(π‘Ÿ Β· 𝑧)))
227224, 226eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ ((π‘Ÿ Β· 𝑧)(abs ∘ βˆ’ )0) = (absβ€˜(π‘Ÿ Β· 𝑧)))
228221, 227breq12d 5119 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ ((π‘Ÿ +𝑒 𝑑) ≀ ((π‘Ÿ Β· 𝑧)(abs ∘ βˆ’ )0) ↔ (π‘Ÿ + 𝑑) ≀ (absβ€˜(π‘Ÿ Β· 𝑧))))
229219, 228mtbid 324 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ Β¬ (π‘Ÿ + 𝑑) ≀ (absβ€˜(π‘Ÿ Β· 𝑧)))
230222abscld 15327 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (absβ€˜(π‘Ÿ Β· 𝑧)) ∈ ℝ)
231230, 191ltnled 11307 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ ((absβ€˜(π‘Ÿ Β· 𝑧)) < (π‘Ÿ + 𝑑) ↔ Β¬ (π‘Ÿ + 𝑑) ≀ (absβ€˜(π‘Ÿ Β· 𝑧))))
232229, 231mpbird 257 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (absβ€˜(π‘Ÿ Β· 𝑧)) < (π‘Ÿ + 𝑑))
233203, 232eqbrtrrd 5130 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (π‘Ÿ Β· (absβ€˜π‘§)) < (π‘Ÿ + 𝑑))
234185, 191, 187ltmuldiv2d 13010 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ ((π‘Ÿ Β· (absβ€˜π‘§)) < (π‘Ÿ + 𝑑) ↔ (absβ€˜π‘§) < ((π‘Ÿ + 𝑑) / π‘Ÿ)))
235233, 234mpbid 231 . . . . . . . . . . . . . . . . . . . 20 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (absβ€˜π‘§) < ((π‘Ÿ + 𝑑) / π‘Ÿ))
236 flltp1 13711 . . . . . . . . . . . . . . . . . . . . 21 (((π‘Ÿ + 𝑑) / π‘Ÿ) ∈ ℝ β†’ ((π‘Ÿ + 𝑑) / π‘Ÿ) < ((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1))
237192, 236syl 17 . . . . . . . . . . . . . . . . . . . 20 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ ((π‘Ÿ + 𝑑) / π‘Ÿ) < ((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1))
238185, 192, 195, 235, 237lttrd 11321 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (absβ€˜π‘§) < ((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1))
239185, 195, 238ltled 11308 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (absβ€˜π‘§) ≀ ((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1))
240183, 185, 195, 197, 239letrd 11317 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (absβ€˜(β„œβ€˜π‘§)) ≀ ((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1))
241181zred 12612 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (β„œβ€˜π‘§) ∈ ℝ)
242241, 195absled 15321 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ ((absβ€˜(β„œβ€˜π‘§)) ≀ ((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1) ↔ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1) ≀ (β„œβ€˜π‘§) ∧ (β„œβ€˜π‘§) ≀ ((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1))))
243240, 242mpbid 231 . . . . . . . . . . . . . . . 16 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1) ≀ (β„œβ€˜π‘§) ∧ (β„œβ€˜π‘§) ≀ ((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)))
244194znegcld 12614 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ -((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1) ∈ β„€)
245 elfz 13436 . . . . . . . . . . . . . . . . 17 (((β„œβ€˜π‘§) ∈ β„€ ∧ -((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1) ∈ β„€ ∧ ((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1) ∈ β„€) β†’ ((β„œβ€˜π‘§) ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ↔ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1) ≀ (β„œβ€˜π‘§) ∧ (β„œβ€˜π‘§) ≀ ((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1))))
246181, 244, 194, 245syl3anc 1372 . . . . . . . . . . . . . . . 16 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ ((β„œβ€˜π‘§) ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ↔ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1) ≀ (β„œβ€˜π‘§) ∧ (β„œβ€˜π‘§) ≀ ((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1))))
247243, 246mpbird 257 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (β„œβ€˜π‘§) ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)))
248179simp3bi 1148 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ β„€[i] β†’ (β„‘β€˜π‘§) ∈ β„€)
249248ad2antlr 726 . . . . . . . . . . . . . . . . . . . 20 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (β„‘β€˜π‘§) ∈ β„€)
250249zcnd 12613 . . . . . . . . . . . . . . . . . . 19 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (β„‘β€˜π‘§) ∈ β„‚)
251250abscld 15327 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (absβ€˜(β„‘β€˜π‘§)) ∈ ℝ)
252 absimle 15200 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ β„‚ β†’ (absβ€˜(β„‘β€˜π‘§)) ≀ (absβ€˜π‘§))
253184, 252syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (absβ€˜(β„‘β€˜π‘§)) ≀ (absβ€˜π‘§))
254251, 185, 195, 253, 239letrd 11317 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (absβ€˜(β„‘β€˜π‘§)) ≀ ((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1))
255249zred 12612 . . . . . . . . . . . . . . . . . 18 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (β„‘β€˜π‘§) ∈ ℝ)
256255, 195absled 15321 . . . . . . . . . . . . . . . . 17 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ ((absβ€˜(β„‘β€˜π‘§)) ≀ ((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1) ↔ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1) ≀ (β„‘β€˜π‘§) ∧ (β„‘β€˜π‘§) ≀ ((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1))))
257254, 256mpbid 231 . . . . . . . . . . . . . . . 16 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1) ≀ (β„‘β€˜π‘§) ∧ (β„‘β€˜π‘§) ≀ ((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)))
258 elfz 13436 . . . . . . . . . . . . . . . . 17 (((β„‘β€˜π‘§) ∈ β„€ ∧ -((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1) ∈ β„€ ∧ ((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1) ∈ β„€) β†’ ((β„‘β€˜π‘§) ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ↔ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1) ≀ (β„‘β€˜π‘§) ∧ (β„‘β€˜π‘§) ≀ ((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1))))
259249, 244, 194, 258syl3anc 1372 . . . . . . . . . . . . . . . 16 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ ((β„‘β€˜π‘§) ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ↔ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1) ≀ (β„‘β€˜π‘§) ∧ (β„‘β€˜π‘§) ≀ ((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1))))
260257, 259mpbird 257 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (β„‘β€˜π‘§) ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)))
261184replimd 15088 . . . . . . . . . . . . . . . 16 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ 𝑧 = ((β„œβ€˜π‘§) + (i Β· (β„‘β€˜π‘§))))
262261oveq2d 7374 . . . . . . . . . . . . . . 15 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ (π‘Ÿ Β· 𝑧) = (π‘Ÿ Β· ((β„œβ€˜π‘§) + (i Β· (β„‘β€˜π‘§)))))
263 oveq1 7365 . . . . . . . . . . . . . . . . . 18 (π‘Ž = (β„œβ€˜π‘§) β†’ (π‘Ž + (i Β· 𝑏)) = ((β„œβ€˜π‘§) + (i Β· 𝑏)))
264263oveq2d 7374 . . . . . . . . . . . . . . . . 17 (π‘Ž = (β„œβ€˜π‘§) β†’ (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏))) = (π‘Ÿ Β· ((β„œβ€˜π‘§) + (i Β· 𝑏))))
265264eqeq2d 2744 . . . . . . . . . . . . . . . 16 (π‘Ž = (β„œβ€˜π‘§) β†’ ((π‘Ÿ Β· 𝑧) = (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏))) ↔ (π‘Ÿ Β· 𝑧) = (π‘Ÿ Β· ((β„œβ€˜π‘§) + (i Β· 𝑏)))))
266 oveq2 7366 . . . . . . . . . . . . . . . . . . 19 (𝑏 = (β„‘β€˜π‘§) β†’ (i Β· 𝑏) = (i Β· (β„‘β€˜π‘§)))
267266oveq2d 7374 . . . . . . . . . . . . . . . . . 18 (𝑏 = (β„‘β€˜π‘§) β†’ ((β„œβ€˜π‘§) + (i Β· 𝑏)) = ((β„œβ€˜π‘§) + (i Β· (β„‘β€˜π‘§))))
268267oveq2d 7374 . . . . . . . . . . . . . . . . 17 (𝑏 = (β„‘β€˜π‘§) β†’ (π‘Ÿ Β· ((β„œβ€˜π‘§) + (i Β· 𝑏))) = (π‘Ÿ Β· ((β„œβ€˜π‘§) + (i Β· (β„‘β€˜π‘§)))))
269268eqeq2d 2744 . . . . . . . . . . . . . . . 16 (𝑏 = (β„‘β€˜π‘§) β†’ ((π‘Ÿ Β· 𝑧) = (π‘Ÿ Β· ((β„œβ€˜π‘§) + (i Β· 𝑏))) ↔ (π‘Ÿ Β· 𝑧) = (π‘Ÿ Β· ((β„œβ€˜π‘§) + (i Β· (β„‘β€˜π‘§))))))
270265, 269rspc2ev 3591 . . . . . . . . . . . . . . 15 (((β„œβ€˜π‘§) ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ∧ (β„‘β€˜π‘§) ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ∧ (π‘Ÿ Β· 𝑧) = (π‘Ÿ Β· ((β„œβ€˜π‘§) + (i Β· (β„‘β€˜π‘§))))) β†’ βˆƒπ‘Ž ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1))βˆƒπ‘ ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1))(π‘Ÿ Β· 𝑧) = (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏))))
271247, 260, 262, 270syl3anc 1372 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) ∧ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ βˆƒπ‘Ž ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1))βˆƒπ‘ ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1))(π‘Ÿ Β· 𝑧) = (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏))))
272271ex 414 . . . . . . . . . . . . 13 ((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) β†’ ((((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ… β†’ βˆƒπ‘Ž ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1))βˆƒπ‘ ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1))(π‘Ÿ Β· 𝑧) = (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏)))))
273171, 172elrnmpo 7493 . . . . . . . . . . . . 13 ((π‘Ÿ Β· 𝑧) ∈ ran (π‘Ž ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)), 𝑏 ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ↦ (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏)))) ↔ βˆƒπ‘Ž ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1))βˆƒπ‘ ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1))(π‘Ÿ Β· 𝑧) = (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏))))
274272, 273syl6ibr 252 . . . . . . . . . . . 12 ((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) β†’ ((((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ… β†’ (π‘Ÿ Β· 𝑧) ∈ ran (π‘Ž ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)), 𝑏 ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ↦ (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏))))))
275156ineq1d 4172 . . . . . . . . . . . . . 14 (π‘₯ = (π‘Ÿ Β· 𝑧) β†’ ((π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) = (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋))
276275neeq1d 3000 . . . . . . . . . . . . 13 (π‘₯ = (π‘Ÿ Β· 𝑧) β†’ (((π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ… ↔ (((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…))
277 eleq1 2822 . . . . . . . . . . . . 13 (π‘₯ = (π‘Ÿ Β· 𝑧) β†’ (π‘₯ ∈ ran (π‘Ž ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)), 𝑏 ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ↦ (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏)))) ↔ (π‘Ÿ Β· 𝑧) ∈ ran (π‘Ž ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)), 𝑏 ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ↦ (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏))))))
278276, 277imbi12d 345 . . . . . . . . . . . 12 (π‘₯ = (π‘Ÿ Β· 𝑧) β†’ ((((π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ… β†’ π‘₯ ∈ ran (π‘Ž ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)), 𝑏 ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ↦ (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏))))) ↔ ((((π‘Ÿ Β· 𝑧)(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ… β†’ (π‘Ÿ Β· 𝑧) ∈ ran (π‘Ž ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)), 𝑏 ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ↦ (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏)))))))
279274, 278syl5ibrcom 247 . . . . . . . . . . 11 ((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ 𝑧 ∈ β„€[i]) β†’ (π‘₯ = (π‘Ÿ Β· 𝑧) β†’ (((π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ… β†’ π‘₯ ∈ ran (π‘Ž ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)), 𝑏 ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ↦ (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏)))))))
280279rexlimdva 3149 . . . . . . . . . 10 (((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) β†’ (βˆƒπ‘§ ∈ β„€[i] π‘₯ = (π‘Ÿ Β· 𝑧) β†’ (((π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ… β†’ π‘₯ ∈ ran (π‘Ž ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)), 𝑏 ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ↦ (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏)))))))
281178, 280biimtrid 241 . . . . . . . . 9 (((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) β†’ (π‘₯ ∈ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧)) β†’ (((π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ… β†’ π‘₯ ∈ ran (π‘Ž ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)), 𝑏 ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ↦ (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏)))))))
2822813imp 1112 . . . . . . . 8 ((((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) ∧ π‘₯ ∈ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧)) ∧ ((π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…) β†’ π‘₯ ∈ ran (π‘Ž ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)), 𝑏 ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ↦ (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏)))))
283282rabssdv 4033 . . . . . . 7 (((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) β†’ {π‘₯ ∈ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧)) ∣ ((π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…} βŠ† ran (π‘Ž ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)), 𝑏 ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ↦ (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏)))))
284 ssfi 9120 . . . . . . 7 ((ran (π‘Ž ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)), 𝑏 ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ↦ (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏)))) ∈ Fin ∧ {π‘₯ ∈ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧)) ∣ ((π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…} βŠ† ran (π‘Ž ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)), 𝑏 ∈ (-((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)...((βŒŠβ€˜((π‘Ÿ + 𝑑) / π‘Ÿ)) + 1)) ↦ (π‘Ÿ Β· (π‘Ž + (i Β· 𝑏))))) β†’ {π‘₯ ∈ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧)) ∣ ((π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…} ∈ Fin)
285177, 283, 284sylancr 588 . . . . . 6 (((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑑 ∈ ℝ ∧ 𝑋 βŠ† (0(ballβ€˜(abs ∘ βˆ’ ))𝑑))) β†’ {π‘₯ ∈ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧)) ∣ ((π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…} ∈ Fin)
286167, 285rexlimddv 3155 . . . . 5 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) β†’ {π‘₯ ∈ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧)) ∣ ((π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…} ∈ Fin)
287 iuneq1 4971 . . . . . . . 8 (𝑦 = ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧)) β†’ βˆͺ π‘₯ ∈ 𝑦 (π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) = βˆͺ π‘₯ ∈ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧))(π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))
288287sseq2d 3977 . . . . . . 7 (𝑦 = ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧)) β†’ (𝑋 βŠ† βˆͺ π‘₯ ∈ 𝑦 (π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ↔ 𝑋 βŠ† βˆͺ π‘₯ ∈ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧))(π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
289 rabeq 3420 . . . . . . . 8 (𝑦 = ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧)) β†’ {π‘₯ ∈ 𝑦 ∣ ((π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…} = {π‘₯ ∈ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧)) ∣ ((π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…})
290289eleq1d 2819 . . . . . . 7 (𝑦 = ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧)) β†’ ({π‘₯ ∈ 𝑦 ∣ ((π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…} ∈ Fin ↔ {π‘₯ ∈ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧)) ∣ ((π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…} ∈ Fin))
291288, 290anbi12d 632 . . . . . 6 (𝑦 = ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧)) β†’ ((𝑋 βŠ† βˆͺ π‘₯ ∈ 𝑦 (π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∧ {π‘₯ ∈ 𝑦 ∣ ((π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…} ∈ Fin) ↔ (𝑋 βŠ† βˆͺ π‘₯ ∈ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧))(π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∧ {π‘₯ ∈ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧)) ∣ ((π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…} ∈ Fin)))
292291rspcev 3580 . . . . 5 ((ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧)) ∈ 𝒫 β„‚ ∧ (𝑋 βŠ† βˆͺ π‘₯ ∈ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧))(π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∧ {π‘₯ ∈ ran (𝑧 ∈ β„€[i] ↦ (π‘Ÿ Β· 𝑧)) ∣ ((π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…} ∈ Fin)) β†’ βˆƒπ‘¦ ∈ 𝒫 β„‚(𝑋 βŠ† βˆͺ π‘₯ ∈ 𝑦 (π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∧ {π‘₯ ∈ 𝑦 ∣ ((π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…} ∈ Fin))
29311, 162, 286, 292syl12anc 836 . . . 4 ((𝐷 ∈ (Bndβ€˜π‘‹) ∧ π‘Ÿ ∈ ℝ+) β†’ βˆƒπ‘¦ ∈ 𝒫 β„‚(𝑋 βŠ† βˆͺ π‘₯ ∈ 𝑦 (π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∧ {π‘₯ ∈ 𝑦 ∣ ((π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…} ∈ Fin))
294293ralrimiva 3140 . . 3 (𝐷 ∈ (Bndβ€˜π‘‹) β†’ βˆ€π‘Ÿ ∈ ℝ+ βˆƒπ‘¦ ∈ 𝒫 β„‚(𝑋 βŠ† βˆͺ π‘₯ ∈ 𝑦 (π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∧ {π‘₯ ∈ 𝑦 ∣ ((π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…} ∈ Fin))
29513sstotbnd3 36281 . . . 4 (((abs ∘ βˆ’ ) ∈ (Metβ€˜β„‚) ∧ 𝑋 βŠ† β„‚) β†’ (𝐷 ∈ (TotBndβ€˜π‘‹) ↔ βˆ€π‘Ÿ ∈ ℝ+ βˆƒπ‘¦ ∈ 𝒫 β„‚(𝑋 βŠ† βˆͺ π‘₯ ∈ 𝑦 (π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∧ {π‘₯ ∈ 𝑦 ∣ ((π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…} ∈ Fin)))
29612, 15, 295sylancr 588 . . 3 (𝐷 ∈ (Bndβ€˜π‘‹) β†’ (𝐷 ∈ (TotBndβ€˜π‘‹) ↔ βˆ€π‘Ÿ ∈ ℝ+ βˆƒπ‘¦ ∈ 𝒫 β„‚(𝑋 βŠ† βˆͺ π‘₯ ∈ 𝑦 (π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∧ {π‘₯ ∈ 𝑦 ∣ ((π‘₯(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∩ 𝑋) β‰  βˆ…} ∈ Fin)))
297294, 296mpbird 257 . 2 (𝐷 ∈ (Bndβ€˜π‘‹) β†’ 𝐷 ∈ (TotBndβ€˜π‘‹))
2981, 297impbii 208 1 (𝐷 ∈ (TotBndβ€˜π‘‹) ↔ 𝐷 ∈ (Bndβ€˜π‘‹))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  {crab 3406  Vcvv 3444   ∩ cin 3910   βŠ† wss 3911  βˆ…c0 4283  π’« cpw 4561  βˆͺ ciun 4955   class class class wbr 5106   ↦ cmpt 5189   Γ— cxp 5632  ran crn 5635   β†Ύ cres 5636   ∘ ccom 5638   Fn wfn 6492  β€“ontoβ†’wfo 6495  β€˜cfv 6497  (class class class)co 7358   ∈ cmpo 7360  Fincfn 8886  β„‚cc 11054  β„cr 11055  0cc0 11056  1c1 11057  ici 11058   + caddc 11059   Β· cmul 11061  β„*cxr 11193   < clt 11194   ≀ cle 11195   βˆ’ cmin 11390  -cneg 11391   / cdiv 11817  2c2 12213  β„€cz 12504  β„+crp 12920   +𝑒 cxad 13036  ...cfz 13430  βŒŠcfl 13701  β†‘cexp 13973  β„œcre 14988  β„‘cim 14989  abscabs 15125  β„€[i]cgz 16806  βˆžMetcxmet 20797  Metcmet 20798  ballcbl 20799  TotBndctotbnd 36271  Bndcbnd 36272
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133  ax-pre-sup 11134
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-1st 7922  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-er 8651  df-ec 8653  df-map 8770  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-sup 9383  df-inf 9384  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-div 11818  df-nn 12159  df-2 12221  df-3 12222  df-n0 12419  df-z 12505  df-uz 12769  df-rp 12921  df-xneg 13038  df-xadd 13039  df-xmul 13040  df-fz 13431  df-fl 13703  df-seq 13913  df-exp 13974  df-cj 14990  df-re 14991  df-im 14992  df-sqrt 15126  df-abs 15127  df-gz 16807  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-totbnd 36273  df-bnd 36284
This theorem is referenced by:  cnpwstotbnd  36302
  Copyright terms: Public domain W3C validator