Metamath Proof Explorer

Theorem rlimcnp

Description: Relate a limit of a real-valued sequence at infinity to the continuity of the function S ( y ) = R ( 1 / y ) at zero. (Contributed by Mario Carneiro, 1-Mar-2015)

Ref Expression
Hypotheses rlimcnp.a ⊢ ( 𝜑 → 𝐴 ⊆ ( 0 [,) +∞ ) )
rlimcnp.0 ⊢ ( 𝜑 → 0 ∈ 𝐴 )
rlimcnp.b ⊢ ( 𝜑 → 𝐵 ⊆ ℝ+ )
rlimcnp.r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑅 ∈ ℂ )
rlimcnp.d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ∈ 𝐴 ↔ ( 1 / 𝑥 ) ∈ 𝐵 ) )
rlimcnp.c ⊢ ( 𝑥 = 0 → 𝑅 = 𝐶 )
rlimcnp.s ⊢ ( 𝑥 = ( 1 / 𝑦 ) → 𝑅 = 𝑆 )
rlimcnp.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
rlimcnp.k ⊢ 𝐾 = ( 𝐽 ↾t 𝐴 )
Assertion rlimcnp ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ⇝𝑟 𝐶 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ 0 ) ) )

Proof

Step Hyp Ref Expression
1 rlimcnp.a ⊢ ( 𝜑 → 𝐴 ⊆ ( 0 [,) +∞ ) )
2 rlimcnp.0 ⊢ ( 𝜑 → 0 ∈ 𝐴 )
3 rlimcnp.b ⊢ ( 𝜑 → 𝐵 ⊆ ℝ+ )
4 rlimcnp.r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑅 ∈ ℂ )
5 rlimcnp.d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ∈ 𝐴 ↔ ( 1 / 𝑥 ) ∈ 𝐵 ) )
6 rlimcnp.c ⊢ ( 𝑥 = 0 → 𝑅 = 𝐶 )
7 rlimcnp.s ⊢ ( 𝑥 = ( 1 / 𝑦 ) → 𝑅 = 𝑆 )
8 rlimcnp.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
9 rlimcnp.k ⊢ 𝐾 = ( 𝐽 ↾t 𝐴 )
10 rpreccl ⊢ ( 𝑟 ∈ ℝ+ → ( 1 / 𝑟 ) ∈ ℝ+ )
11 10 adantl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( 1 / 𝑟 ) ∈ ℝ+ )
12 rpreccl ⊢ ( 𝑡 ∈ ℝ+ → ( 1 / 𝑡 ) ∈ ℝ+ )
13 rpcnne0 ⊢ ( 𝑡 ∈ ℝ+ → ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) )
14 13 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) )
15 recrec ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( 1 / ( 1 / 𝑡 ) ) = 𝑡 )
16 14 15 syl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 1 / ( 1 / 𝑡 ) ) = 𝑡 )
17 16 eqcomd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 𝑡 = ( 1 / ( 1 / 𝑡 ) ) )
18 oveq2 ⊢ ( 𝑟 = ( 1 / 𝑡 ) → ( 1 / 𝑟 ) = ( 1 / ( 1 / 𝑡 ) ) )
19 18 rspceeqv ⊢ ( ( ( 1 / 𝑡 ) ∈ ℝ+ ∧ 𝑡 = ( 1 / ( 1 / 𝑡 ) ) ) → ∃ 𝑟 ∈ ℝ+ 𝑡 = ( 1 / 𝑟 ) )
20 12 17 19 syl2an2 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ∃ 𝑟 ∈ ℝ+ 𝑡 = ( 1 / 𝑟 ) )
21 simpr ⊢ ( ( 𝜑 ∧ 𝑡 = ( 1 / 𝑟 ) ) → 𝑡 = ( 1 / 𝑟 ) )
22 21 breq1d ⊢ ( ( 𝜑 ∧ 𝑡 = ( 1 / 𝑟 ) ) → ( 𝑡 < 𝑦 ↔ ( 1 / 𝑟 ) < 𝑦 ) )
23 22 imbi1d ⊢ ( ( 𝜑 ∧ 𝑡 = ( 1 / 𝑟 ) ) → ( ( 𝑡 < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ↔ ( ( 1 / 𝑟 ) < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ) )
24 23 ralbidv ⊢ ( ( 𝜑 ∧ 𝑡 = ( 1 / 𝑟 ) ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝑡 < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 1 / 𝑟 ) < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ) )
25 11 20 24 rexxfrd ⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ℝ+ ∀ 𝑦 ∈ 𝐵 ( 𝑡 < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ↔ ∃ 𝑟 ∈ ℝ+ ∀ 𝑦 ∈ 𝐵 ( ( 1 / 𝑟 ) < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ) )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) → ( ∃ 𝑡 ∈ ℝ+ ∀ 𝑦 ∈ 𝐵 ( 𝑡 < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ↔ ∃ 𝑟 ∈ ℝ+ ∀ 𝑦 ∈ 𝐵 ( ( 1 / 𝑟 ) < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ) )
27 simplr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐵 ) → 𝑟 ∈ ℝ+ )
28 3 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ℝ+ )
29 28 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ℝ+ )
30 elrp ⊢ ( 𝑟 ∈ ℝ+ ↔ ( 𝑟 ∈ ℝ ∧ 0 < 𝑟 ) )
31 elrp ⊢ ( 𝑦 ∈ ℝ+ ↔ ( 𝑦 ∈ ℝ ∧ 0 < 𝑦 ) )
32 ltrec1 ⊢ ( ( ( 𝑟 ∈ ℝ ∧ 0 < 𝑟 ) ∧ ( 𝑦 ∈ ℝ ∧ 0 < 𝑦 ) ) → ( ( 1 / 𝑟 ) < 𝑦 ↔ ( 1 / 𝑦 ) < 𝑟 ) )
33 30 31 32 syl2anb ⊢ ( ( 𝑟 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) → ( ( 1 / 𝑟 ) < 𝑦 ↔ ( 1 / 𝑦 ) < 𝑟 ) )
34 27 29 33 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 1 / 𝑟 ) < 𝑦 ↔ ( 1 / 𝑦 ) < 𝑟 ) )
35 34 imbi1d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ( 1 / 𝑟 ) < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ↔ ( ( 1 / 𝑦 ) < 𝑟 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ) )
36 35 ralbidva ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ∀ 𝑦 ∈ 𝐵 ( ( 1 / 𝑟 ) < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 1 / 𝑦 ) < 𝑟 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ) )
37 36 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑟 ∈ ℝ+ ) → ( ∀ 𝑦 ∈ 𝐵 ( ( 1 / 𝑟 ) < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 1 / 𝑦 ) < 𝑟 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ) )
38 rpcn ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℂ )
39 rpne0 ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ≠ 0 )
40 38 39 recrecd ⊢ ( 𝑦 ∈ ℝ+ → ( 1 / ( 1 / 𝑦 ) ) = 𝑦 )
41 28 40 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 1 / ( 1 / 𝑦 ) ) = 𝑦 )
42 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
43 41 42 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 1 / ( 1 / 𝑦 ) ) ∈ 𝐵 )
44 eleq1 ⊢ ( 𝑥 = ( 1 / 𝑦 ) → ( 𝑥 ∈ 𝐴 ↔ ( 1 / 𝑦 ) ∈ 𝐴 ) )
45 oveq2 ⊢ ( 𝑥 = ( 1 / 𝑦 ) → ( 1 / 𝑥 ) = ( 1 / ( 1 / 𝑦 ) ) )
46 45 eleq1d ⊢ ( 𝑥 = ( 1 / 𝑦 ) → ( ( 1 / 𝑥 ) ∈ 𝐵 ↔ ( 1 / ( 1 / 𝑦 ) ) ∈ 𝐵 ) )
47 44 46 bibi12d ⊢ ( 𝑥 = ( 1 / 𝑦 ) → ( ( 𝑥 ∈ 𝐴 ↔ ( 1 / 𝑥 ) ∈ 𝐵 ) ↔ ( ( 1 / 𝑦 ) ∈ 𝐴 ↔ ( 1 / ( 1 / 𝑦 ) ) ∈ 𝐵 ) ) )
48 5 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ( 𝑥 ∈ 𝐴 ↔ ( 1 / 𝑥 ) ∈ 𝐵 ) )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ∀ 𝑥 ∈ ℝ+ ( 𝑥 ∈ 𝐴 ↔ ( 1 / 𝑥 ) ∈ 𝐵 ) )
50 28 rpreccld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 1 / 𝑦 ) ∈ ℝ+ )
51 47 49 50 rspcdva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( 1 / 𝑦 ) ∈ 𝐴 ↔ ( 1 / ( 1 / 𝑦 ) ) ∈ 𝐵 ) )
52 43 51 mpbird ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 1 / 𝑦 ) ∈ 𝐴 )
53 50 rpne0d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 1 / 𝑦 ) ≠ 0 )
54 eldifsn ⊢ ( ( 1 / 𝑦 ) ∈ ( 𝐴 ∖ { 0 } ) ↔ ( ( 1 / 𝑦 ) ∈ 𝐴 ∧ ( 1 / 𝑦 ) ≠ 0 ) )
55 52 53 54 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 1 / 𝑦 ) ∈ ( 𝐴 ∖ { 0 } ) )
56 eldifi ⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 0 } ) → 𝑥 ∈ 𝐴 )
57 56 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → 𝑥 ∈ 𝐴 )
58 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
59 1 ssdifssd ⊢ ( 𝜑 → ( 𝐴 ∖ { 0 } ) ⊆ ( 0 [,) +∞ ) )
60 59 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → 𝑥 ∈ ( 0 [,) +∞ ) )
61 58 60 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → 𝑥 ∈ ℝ )
62 0re ⊢ 0 ∈ ℝ
63 pnfxr ⊢ +∞ ∈ ℝ*
64 elico2 ⊢ ( ( 0 ∈ ℝ ∧ +∞ ∈ ℝ* ) → ( 𝑥 ∈ ( 0 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 < +∞ ) ) )
65 62 63 64 mp2an ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 < +∞ ) )
66 65 simp2bi ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) → 0 ≤ 𝑥 )
67 60 66 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → 0 ≤ 𝑥 )
68 eldifsni ⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 0 } ) → 𝑥 ≠ 0 )
69 68 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → 𝑥 ≠ 0 )
70 61 67 69 ne0gt0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → 0 < 𝑥 )
71 61 70 elrpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → 𝑥 ∈ ℝ+ )
72 71 5 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → ( 𝑥 ∈ 𝐴 ↔ ( 1 / 𝑥 ) ∈ 𝐵 ) )
73 57 72 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → ( 1 / 𝑥 ) ∈ 𝐵 )
74 rpcn ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ )
75 rpne0 ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ≠ 0 )
76 74 75 recrecd ⊢ ( 𝑥 ∈ ℝ+ → ( 1 / ( 1 / 𝑥 ) ) = 𝑥 )
77 71 76 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → ( 1 / ( 1 / 𝑥 ) ) = 𝑥 )
78 77 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → 𝑥 = ( 1 / ( 1 / 𝑥 ) ) )
79 oveq2 ⊢ ( 𝑦 = ( 1 / 𝑥 ) → ( 1 / 𝑦 ) = ( 1 / ( 1 / 𝑥 ) ) )
80 79 rspceeqv ⊢ ( ( ( 1 / 𝑥 ) ∈ 𝐵 ∧ 𝑥 = ( 1 / ( 1 / 𝑥 ) ) ) → ∃ 𝑦 ∈ 𝐵 𝑥 = ( 1 / 𝑦 ) )
81 73 78 80 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → ∃ 𝑦 ∈ 𝐵 𝑥 = ( 1 / 𝑦 ) )
82 breq1 ⊢ ( 𝑥 = ( 1 / 𝑦 ) → ( 𝑥 < 𝑟 ↔ ( 1 / 𝑦 ) < 𝑟 ) )
83 7 fvoveq1d ⊢ ( 𝑥 = ( 1 / 𝑦 ) → ( abs ‘ ( 𝑅 − 𝐶 ) ) = ( abs ‘ ( 𝑆 − 𝐶 ) ) )
84 83 breq1d ⊢ ( 𝑥 = ( 1 / 𝑦 ) → ( ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ↔ ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) )
85 82 84 imbi12d ⊢ ( 𝑥 = ( 1 / 𝑦 ) → ( ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) ↔ ( ( 1 / 𝑦 ) < 𝑟 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ) )
86 85 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = ( 1 / 𝑦 ) ) → ( ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) ↔ ( ( 1 / 𝑦 ) < 𝑟 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ) )
87 55 81 86 ralxfrd ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 1 / 𝑦 ) < 𝑟 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ) )
88 87 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑟 ∈ ℝ+ ) → ( ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 1 / 𝑦 ) < 𝑟 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ) )
89 37 88 bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑟 ∈ ℝ+ ) → ( ∀ 𝑦 ∈ 𝐵 ( ( 1 / 𝑟 ) < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ↔ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) ) )
90 elsni ⊢ ( 𝑥 ∈ { 0 } → 𝑥 = 0 )
91 90 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑥 ∈ { 0 } ) → 𝑥 = 0 )
92 91 6 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑥 ∈ { 0 } ) → 𝑅 = 𝐶 )
93 92 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑥 ∈ { 0 } ) → ( 𝑅 − 𝐶 ) = ( 𝐶 − 𝐶 ) )
94 6 eleq1d ⊢ ( 𝑥 = 0 → ( 𝑅 ∈ ℂ ↔ 𝐶 ∈ ℂ ) )
95 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑅 ∈ ℂ )
96 94 95 2 rspcdva ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
97 96 subidd ⊢ ( 𝜑 → ( 𝐶 − 𝐶 ) = 0 )
98 97 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑥 ∈ { 0 } ) → ( 𝐶 − 𝐶 ) = 0 )
99 93 98 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑥 ∈ { 0 } ) → ( 𝑅 − 𝐶 ) = 0 )
100 99 abs00bd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑥 ∈ { 0 } ) → ( abs ‘ ( 𝑅 − 𝐶 ) ) = 0 )
101 rpgt0 ⊢ ( 𝑧 ∈ ℝ+ → 0 < 𝑧 )
102 101 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑥 ∈ { 0 } ) → 0 < 𝑧 )
103 100 102 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑥 ∈ { 0 } ) → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 )
104 103 a1d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑥 ∈ { 0 } ) → ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) )
105 104 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) → ∀ 𝑥 ∈ { 0 } ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) )
106 105 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑟 ∈ ℝ+ ) → ∀ 𝑥 ∈ { 0 } ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) )
107 106 biantrud ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑟 ∈ ℝ+ ) → ( ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) ↔ ( ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) ∧ ∀ 𝑥 ∈ { 0 } ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) ) ) )
108 ralunb ⊢ ( ∀ 𝑥 ∈ ( ( 𝐴 ∖ { 0 } ) ∪ { 0 } ) ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) ↔ ( ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) ∧ ∀ 𝑥 ∈ { 0 } ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) ) )
109 107 108 bitr4di ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑟 ∈ ℝ+ ) → ( ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) ↔ ∀ 𝑥 ∈ ( ( 𝐴 ∖ { 0 } ) ∪ { 0 } ) ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) ) )
110 undif1 ⊢ ( ( 𝐴 ∖ { 0 } ) ∪ { 0 } ) = ( 𝐴 ∪ { 0 } )
111 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑟 ∈ ℝ+ ) → 0 ∈ 𝐴 )
112 111 snssd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑟 ∈ ℝ+ ) → { 0 } ⊆ 𝐴 )
113 ssequn2 ⊢ ( { 0 } ⊆ 𝐴 ↔ ( 𝐴 ∪ { 0 } ) = 𝐴 )
114 112 113 sylib ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝐴 ∪ { 0 } ) = 𝐴 )
115 110 114 syl5eq ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝐴 ∖ { 0 } ) ∪ { 0 } ) = 𝐴 )
116 115 raleqdv ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑟 ∈ ℝ+ ) → ( ∀ 𝑥 ∈ ( ( 𝐴 ∖ { 0 } ) ∪ { 0 } ) ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) ) )
117 89 109 116 3bitrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑟 ∈ ℝ+ ) → ( ∀ 𝑦 ∈ 𝐵 ( ( 1 / 𝑟 ) < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) ) )
118 117 rexbidva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) → ( ∃ 𝑟 ∈ ℝ+ ∀ 𝑦 ∈ 𝐵 ( ( 1 / 𝑟 ) < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ↔ ∃ 𝑟 ∈ ℝ+ ∀ 𝑥 ∈ 𝐴 ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) ) )
119 26 118 bitrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) → ( ∃ 𝑡 ∈ ℝ+ ∀ 𝑦 ∈ 𝐵 ( 𝑡 < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ↔ ∃ 𝑟 ∈ ℝ+ ∀ 𝑥 ∈ 𝐴 ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) ) )
120 119 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ℝ+ ∃ 𝑡 ∈ ℝ+ ∀ 𝑦 ∈ 𝐵 ( 𝑡 < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ↔ ∀ 𝑧 ∈ ℝ+ ∃ 𝑟 ∈ ℝ+ ∀ 𝑥 ∈ 𝐴 ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) ) )
121 nfv ⊢ Ⅎ 𝑥 ( 𝑤 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) < 𝑟
122 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑤 )
123 nfcv ⊢ Ⅎ 𝑥 ( abs ∘ − )
124 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 )
125 122 123 124 nfov ⊢ Ⅎ 𝑥 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑤 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) )
126 nfcv ⊢ Ⅎ 𝑥 <
127 nfcv ⊢ Ⅎ 𝑥 𝑧
128 125 126 127 nfbr ⊢ Ⅎ 𝑥 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑤 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) ) < 𝑧
129 121 128 nfim ⊢ Ⅎ 𝑥 ( ( 𝑤 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) < 𝑟 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑤 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) ) < 𝑧 )
130 nfv ⊢ Ⅎ 𝑤 ( ( 𝑥 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) < 𝑟 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) ) < 𝑧 )
131 oveq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) = ( 𝑥 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) )
132 131 breq1d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑤 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) < 𝑟 ↔ ( 𝑥 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) < 𝑟 ) )
133 fveq2 ⊢ ( 𝑤 = 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑤 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) )
134 133 oveq1d ⊢ ( 𝑤 = 𝑥 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑤 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) ) = ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) ) )
135 134 breq1d ⊢ ( 𝑤 = 𝑥 → ( ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑤 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) ) < 𝑧 ↔ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) ) < 𝑧 ) )
136 132 135 imbi12d ⊢ ( 𝑤 = 𝑥 → ( ( ( 𝑤 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) < 𝑟 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑤 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) ) < 𝑧 ) ↔ ( ( 𝑥 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) < 𝑟 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) ) < 𝑧 ) ) )
137 129 130 136 cbvralw ⊢ ( ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) < 𝑟 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑤 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) ) < 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝑥 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) < 𝑟 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) ) < 𝑧 ) )
138 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
139 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ∈ 𝐴 )
140 138 139 ovresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) = ( 𝑥 ( abs ∘ − ) 0 ) )
141 1 58 sstrdi ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
142 ax-resscn ⊢ ℝ ⊆ ℂ
143 141 142 sstrdi ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
144 143 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℂ )
145 0cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ∈ ℂ )
146 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
147 146 cnmetdval ⊢ ( ( 𝑥 ∈ ℂ ∧ 0 ∈ ℂ ) → ( 𝑥 ( abs ∘ − ) 0 ) = ( abs ‘ ( 𝑥 − 0 ) ) )
148 144 145 147 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ( abs ∘ − ) 0 ) = ( abs ‘ ( 𝑥 − 0 ) ) )
149 144 subid1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 − 0 ) = 𝑥 )
150 149 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ 𝑥 ) )
151 140 148 150 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) = ( abs ‘ 𝑥 ) )
152 141 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
153 1 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( 0 [,) +∞ ) )
154 153 66 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ 𝑥 )
155 152 154 absidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ 𝑥 ) = 𝑥 )
156 151 155 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) = 𝑥 )
157 156 breq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) < 𝑟 ↔ 𝑥 < 𝑟 ) )
158 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑅 )
159 158 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑅 ∈ ℂ ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) = 𝑅 )
160 138 4 159 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) = 𝑅 )
161 96 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
162 158 6 139 161 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) = 𝐶 )
163 160 162 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) ) = ( 𝑅 ( abs ∘ − ) 𝐶 ) )
164 146 cnmetdval ⊢ ( ( 𝑅 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝑅 ( abs ∘ − ) 𝐶 ) = ( abs ‘ ( 𝑅 − 𝐶 ) ) )
165 4 161 164 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑅 ( abs ∘ − ) 𝐶 ) = ( abs ‘ ( 𝑅 − 𝐶 ) ) )
166 163 165 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) ) = ( abs ‘ ( 𝑅 − 𝐶 ) ) )
167 166 breq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) ) < 𝑧 ↔ ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) )
168 157 167 imbi12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) < 𝑟 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) ) < 𝑧 ) ↔ ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) ) )
169 168 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ( ( 𝑥 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) < 𝑟 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) ) < 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) ) )
170 137 169 syl5bb ⊢ ( 𝜑 → ( ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) < 𝑟 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑤 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) ) < 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) ) )
171 170 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) < 𝑟 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑤 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) ) < 𝑧 ) ↔ ∃ 𝑟 ∈ ℝ+ ∀ 𝑥 ∈ 𝐴 ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) ) )
172 171 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ℝ+ ∃ 𝑟 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) < 𝑟 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑤 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) ) < 𝑧 ) ↔ ∀ 𝑧 ∈ ℝ+ ∃ 𝑟 ∈ ℝ+ ∀ 𝑥 ∈ 𝐴 ( 𝑥 < 𝑟 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑧 ) ) )
173 4 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : 𝐴 ⟶ ℂ )
174 173 biantrurd ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ℝ+ ∃ 𝑟 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) < 𝑟 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑤 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) ) < 𝑧 ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : 𝐴 ⟶ ℂ ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑟 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) < 𝑟 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑤 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) ) < 𝑧 ) ) ) )
175 120 172 174 3bitr2d ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ℝ+ ∃ 𝑡 ∈ ℝ+ ∀ 𝑦 ∈ 𝐵 ( 𝑡 < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : 𝐴 ⟶ ℂ ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑟 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) < 𝑟 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑤 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) ) < 𝑧 ) ) ) )
176 7 eleq1d ⊢ ( 𝑥 = ( 1 / 𝑦 ) → ( 𝑅 ∈ ℂ ↔ 𝑆 ∈ ℂ ) )
177 95 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 𝑅 ∈ ℂ )
178 176 177 52 rspcdva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑆 ∈ ℂ )
179 178 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 𝑆 ∈ ℂ )
180 rpssre ⊢ ℝ+ ⊆ ℝ
181 3 180 sstrdi ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
182 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
183 179 181 96 182 rlim3 ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ⇝𝑟 𝐶 ↔ ∀ 𝑧 ∈ ℝ+ ∃ 𝑡 ∈ ( 1 [,) +∞ ) ∀ 𝑦 ∈ 𝐵 ( 𝑡 ≤ 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ) )
184 0xr ⊢ 0 ∈ ℝ*
185 0lt1 ⊢ 0 < 1
186 df-ioo ⊢ (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) } )
187 df-ico ⊢ [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
188 xrltletr ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( ( 0 < 1 ∧ 1 ≤ 𝑤 ) → 0 < 𝑤 ) )
189 186 187 188 ixxss1 ⊢ ( ( 0 ∈ ℝ* ∧ 0 < 1 ) → ( 1 [,) +∞ ) ⊆ ( 0 (,) +∞ ) )
190 184 185 189 mp2an ⊢ ( 1 [,) +∞ ) ⊆ ( 0 (,) +∞ )
191 ioorp ⊢ ( 0 (,) +∞ ) = ℝ+
192 190 191 sseqtri ⊢ ( 1 [,) +∞ ) ⊆ ℝ+
193 ssrexv ⊢ ( ( 1 [,) +∞ ) ⊆ ℝ+ → ( ∃ 𝑡 ∈ ( 1 [,) +∞ ) ∀ 𝑦 ∈ 𝐵 ( 𝑡 ≤ 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) → ∃ 𝑡 ∈ ℝ+ ∀ 𝑦 ∈ 𝐵 ( 𝑡 ≤ 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ) )
194 192 193 ax-mp ⊢ ( ∃ 𝑡 ∈ ( 1 [,) +∞ ) ∀ 𝑦 ∈ 𝐵 ( 𝑡 ≤ 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) → ∃ 𝑡 ∈ ℝ+ ∀ 𝑦 ∈ 𝐵 ( 𝑡 ≤ 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) )
195 simplr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐵 ) → 𝑡 ∈ ℝ+ )
196 180 195 sselid ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐵 ) → 𝑡 ∈ ℝ )
197 181 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 𝐵 ⊆ ℝ )
198 197 sselda ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ℝ )
199 ltle ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑡 < 𝑦 → 𝑡 ≤ 𝑦 ) )
200 196 198 199 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑡 < 𝑦 → 𝑡 ≤ 𝑦 ) )
201 200 imim1d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑡 ≤ 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) → ( 𝑡 < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ) )
202 201 ralimdva ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝑡 ≤ 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) → ∀ 𝑦 ∈ 𝐵 ( 𝑡 < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ) )
203 202 reximdva ⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ℝ+ ∀ 𝑦 ∈ 𝐵 ( 𝑡 ≤ 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) → ∃ 𝑡 ∈ ℝ+ ∀ 𝑦 ∈ 𝐵 ( 𝑡 < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ) )
204 194 203 syl5 ⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ( 1 [,) +∞ ) ∀ 𝑦 ∈ 𝐵 ( 𝑡 ≤ 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) → ∃ 𝑡 ∈ ℝ+ ∀ 𝑦 ∈ 𝐵 ( 𝑡 < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ) )
205 204 ralimdv ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ℝ+ ∃ 𝑡 ∈ ( 1 [,) +∞ ) ∀ 𝑦 ∈ 𝐵 ( 𝑡 ≤ 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) → ∀ 𝑧 ∈ ℝ+ ∃ 𝑡 ∈ ℝ+ ∀ 𝑦 ∈ 𝐵 ( 𝑡 < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ) )
206 183 205 sylbid ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ⇝𝑟 𝐶 → ∀ 𝑧 ∈ ℝ+ ∃ 𝑡 ∈ ℝ+ ∀ 𝑦 ∈ 𝐵 ( 𝑡 < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ) )
207 ssrexv ⊢ ( ℝ+ ⊆ ℝ → ( ∃ 𝑡 ∈ ℝ+ ∀ 𝑦 ∈ 𝐵 ( 𝑡 < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) → ∃ 𝑡 ∈ ℝ ∀ 𝑦 ∈ 𝐵 ( 𝑡 < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ) )
208 180 207 ax-mp ⊢ ( ∃ 𝑡 ∈ ℝ+ ∀ 𝑦 ∈ 𝐵 ( 𝑡 < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) → ∃ 𝑡 ∈ ℝ ∀ 𝑦 ∈ 𝐵 ( 𝑡 < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) )
209 208 ralimi ⊢ ( ∀ 𝑧 ∈ ℝ+ ∃ 𝑡 ∈ ℝ+ ∀ 𝑦 ∈ 𝐵 ( 𝑡 < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) → ∀ 𝑧 ∈ ℝ+ ∃ 𝑡 ∈ ℝ ∀ 𝑦 ∈ 𝐵 ( 𝑡 < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) )
210 179 181 96 rlim2lt ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ⇝𝑟 𝐶 ↔ ∀ 𝑧 ∈ ℝ+ ∃ 𝑡 ∈ ℝ ∀ 𝑦 ∈ 𝐵 ( 𝑡 < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ) )
211 209 210 syl5ibr ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ℝ+ ∃ 𝑡 ∈ ℝ+ ∀ 𝑦 ∈ 𝐵 ( 𝑡 < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) → ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ⇝𝑟 𝐶 ) )
212 206 211 impbid ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ⇝𝑟 𝐶 ↔ ∀ 𝑧 ∈ ℝ+ ∃ 𝑡 ∈ ℝ+ ∀ 𝑦 ∈ 𝐵 ( 𝑡 < 𝑦 → ( abs ‘ ( 𝑆 − 𝐶 ) ) < 𝑧 ) ) )
213 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
214 xmetres2 ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐴 ⊆ ℂ ) → ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ∈ ( ∞Met ‘ 𝐴 ) )
215 213 143 214 sylancr ⊢ ( 𝜑 → ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ∈ ( ∞Met ‘ 𝐴 ) )
216 213 a1i ⊢ ( 𝜑 → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
217 eqid ⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) )
218 8 cnfldtopn ⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )
219 217 218 metcnp2 ⊢ ( ( ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ∈ ( ∞Met ‘ 𝐴 ) ∧ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 0 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ) CnP 𝐽 ) ‘ 0 ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : 𝐴 ⟶ ℂ ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑟 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) < 𝑟 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑤 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) ) < 𝑧 ) ) ) )
220 215 216 2 219 syl3anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ) CnP 𝐽 ) ‘ 0 ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : 𝐴 ⟶ ℂ ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑟 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) 0 ) < 𝑟 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑤 ) ( abs ∘ − ) ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 0 ) ) < 𝑧 ) ) ) )
221 175 212 220 3bitr4d ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ⇝𝑟 𝐶 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ) CnP 𝐽 ) ‘ 0 ) ) )
222 eqid ⊢ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) = ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) )
223 222 218 217 metrest ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐴 ⊆ ℂ ) → ( 𝐽 ↾t 𝐴 ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ) )
224 213 143 223 sylancr ⊢ ( 𝜑 → ( 𝐽 ↾t 𝐴 ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ) )
225 9 224 syl5eq ⊢ ( 𝜑 → 𝐾 = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ) )
226 225 oveq1d ⊢ ( 𝜑 → ( 𝐾 CnP 𝐽 ) = ( ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ) CnP 𝐽 ) )
227 226 fveq1d ⊢ ( 𝜑 → ( ( 𝐾 CnP 𝐽 ) ‘ 0 ) = ( ( ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ) CnP 𝐽 ) ‘ 0 ) )
228 227 eleq2d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ 0 ) ↔ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ) CnP 𝐽 ) ‘ 0 ) ) )
229 221 228 bitr4d ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ⇝𝑟 𝐶 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ 0 ) ) )