Metamath Proof Explorer

Theorem lhop

Description: L'Hôpital's Rule. If I is an open set of the reals, F and G are real functions on A containing all of I except possibly B , which are differentiable everywhere on I \ { B } , F and G both approach 0, and the limit of F ' ( x ) / G ' ( x ) at B is C , then the limit F ( x ) / G ( x ) at B also exists and equals C . This is Metamath 100 proof #64. (Contributed by Mario Carneiro, 30-Dec-2016)

Ref Expression
Hypotheses lhop.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
lhop.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
lhop.g ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ ℝ )
lhop.i ⊢ ( 𝜑 → 𝐼 ∈ ( topGen ‘ ran (,) ) )
lhop.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐼 )
lhop.d ⊢ 𝐷 = ( 𝐼 ∖ { 𝐵 } )
lhop.if ⊢ ( 𝜑 → 𝐷 ⊆ dom ( ℝ D 𝐹 ) )
lhop.ig ⊢ ( 𝜑 → 𝐷 ⊆ dom ( ℝ D 𝐺 ) )
lhop.f0 ⊢ ( 𝜑 → 0 ∈ ( 𝐹 limℂ 𝐵 ) )
lhop.g0 ⊢ ( 𝜑 → 0 ∈ ( 𝐺 limℂ 𝐵 ) )
lhop.gn0 ⊢ ( 𝜑 → ¬ 0 ∈ ( 𝐺 “ 𝐷 ) )
lhop.gd0 ⊢ ( 𝜑 → ¬ 0 ∈ ( ( ℝ D 𝐺 ) “ 𝐷 ) )
lhop.c ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) limℂ 𝐵 ) )
Assertion lhop ( 𝜑 → 𝐶 ∈ ( ( 𝑧 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 lhop.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2 lhop.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
3 lhop.g ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ ℝ )
4 lhop.i ⊢ ( 𝜑 → 𝐼 ∈ ( topGen ‘ ran (,) ) )
5 lhop.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐼 )
6 lhop.d ⊢ 𝐷 = ( 𝐼 ∖ { 𝐵 } )
7 lhop.if ⊢ ( 𝜑 → 𝐷 ⊆ dom ( ℝ D 𝐹 ) )
8 lhop.ig ⊢ ( 𝜑 → 𝐷 ⊆ dom ( ℝ D 𝐺 ) )
9 lhop.f0 ⊢ ( 𝜑 → 0 ∈ ( 𝐹 limℂ 𝐵 ) )
10 lhop.g0 ⊢ ( 𝜑 → 0 ∈ ( 𝐺 limℂ 𝐵 ) )
11 lhop.gn0 ⊢ ( 𝜑 → ¬ 0 ∈ ( 𝐺 “ 𝐷 ) )
12 lhop.gd0 ⊢ ( 𝜑 → ¬ 0 ∈ ( ( ℝ D 𝐺 ) “ 𝐷 ) )
13 lhop.c ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) limℂ 𝐵 ) )
14 eqid ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
15 14 rexmet ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ )
16 15 a1i ⊢ ( 𝜑 → ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) )
17 eqid ⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
18 14 17 tgioo ⊢ ( topGen ‘ ran (,) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
19 18 mopni2 ⊢ ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) ∧ 𝐼 ∈ ( topGen ‘ ran (,) ) ∧ 𝐵 ∈ 𝐼 ) → ∃ 𝑟 ∈ ℝ+ ( 𝐵 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝐼 )
20 16 4 5 19 syl3anc ⊢ ( 𝜑 → ∃ 𝑟 ∈ ℝ+ ( 𝐵 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝐼 )
21 elssuni ⊢ ( 𝐼 ∈ ( topGen ‘ ran (,) ) → 𝐼 ⊆ ∪ ( topGen ‘ ran (,) ) )
22 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
23 21 22 sseqtrrdi ⊢ ( 𝐼 ∈ ( topGen ‘ ran (,) ) → 𝐼 ⊆ ℝ )
24 4 23 syl ⊢ ( 𝜑 → 𝐼 ⊆ ℝ )
25 24 5 sseldd ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
26 rpre ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ )
27 14 bl2ioo ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( 𝐵 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) = ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) )
28 25 26 27 syl2an ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( 𝐵 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) = ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) )
29 28 sseq1d ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝐵 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝐼 ↔ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) )
30 25 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐵 ∈ ℝ )
31 simprl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝑟 ∈ ℝ+ )
32 31 rpred ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝑟 ∈ ℝ )
33 30 32 resubcld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝐵 − 𝑟 ) ∈ ℝ )
34 33 rexrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝐵 − 𝑟 ) ∈ ℝ* )
35 30 31 ltsubrpd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝐵 − 𝑟 ) < 𝐵 )
36 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐹 : 𝐴 ⟶ ℝ )
37 ssun1 ⊢ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ⊆ ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) )
38 unass ⊢ ( ( { 𝐵 } ∪ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) = ( { 𝐵 } ∪ ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) )
39 uncom ⊢ ( { 𝐵 } ∪ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) = ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ { 𝐵 } )
40 39 uneq1i ⊢ ( ( { 𝐵 } ∪ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) = ( ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ { 𝐵 } ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) )
41 38 40 eqtr3i ⊢ ( { 𝐵 } ∪ ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) = ( ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ { 𝐵 } ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) )
42 30 rexrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐵 ∈ ℝ* )
43 30 32 readdcld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝐵 + 𝑟 ) ∈ ℝ )
44 43 rexrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝐵 + 𝑟 ) ∈ ℝ* )
45 30 31 ltaddrpd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐵 < ( 𝐵 + 𝑟 ) )
46 ioojoin ⊢ ( ( ( ( 𝐵 − 𝑟 ) ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐵 + 𝑟 ) ∈ ℝ* ) ∧ ( ( 𝐵 − 𝑟 ) < 𝐵 ∧ 𝐵 < ( 𝐵 + 𝑟 ) ) ) → ( ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ { 𝐵 } ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) = ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) )
47 34 42 44 35 45 46 syl32anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ { 𝐵 } ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) = ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) )
48 41 47 eqtrid ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( { 𝐵 } ∪ ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) = ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) )
49 elioo2 ⊢ ( ( ( 𝐵 − 𝑟 ) ∈ ℝ* ∧ ( 𝐵 + 𝑟 ) ∈ ℝ* ) → ( 𝐵 ∈ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ↔ ( 𝐵 ∈ ℝ ∧ ( 𝐵 − 𝑟 ) < 𝐵 ∧ 𝐵 < ( 𝐵 + 𝑟 ) ) ) )
50 34 44 49 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝐵 ∈ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ↔ ( 𝐵 ∈ ℝ ∧ ( 𝐵 − 𝑟 ) < 𝐵 ∧ 𝐵 < ( 𝐵 + 𝑟 ) ) ) )
51 30 35 45 50 mpbir3and ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐵 ∈ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) )
52 51 snssd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → { 𝐵 } ⊆ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) )
53 incom ⊢ ( { 𝐵 } ∩ ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) = ( ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ∩ { 𝐵 } )
54 ubioo ⊢ ¬ 𝐵 ∈ ( ( 𝐵 − 𝑟 ) (,) 𝐵 )
55 lbioo ⊢ ¬ 𝐵 ∈ ( 𝐵 (,) ( 𝐵 + 𝑟 ) )
56 54 55 pm3.2ni ⊢ ¬ ( 𝐵 ∈ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∨ 𝐵 ∈ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) )
57 elun ⊢ ( 𝐵 ∈ ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ↔ ( 𝐵 ∈ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∨ 𝐵 ∈ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) )
58 56 57 mtbir ⊢ ¬ 𝐵 ∈ ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) )
59 disjsn ⊢ ( ( ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ∩ { 𝐵 } ) = ∅ ↔ ¬ 𝐵 ∈ ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) )
60 58 59 mpbir ⊢ ( ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ∩ { 𝐵 } ) = ∅
61 53 60 eqtri ⊢ ( { 𝐵 } ∩ ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) = ∅
62 uneqdifeq ⊢ ( ( { 𝐵 } ⊆ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∧ ( { 𝐵 } ∩ ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) = ∅ ) → ( ( { 𝐵 } ∪ ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) = ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ↔ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) = ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) )
63 52 61 62 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( { 𝐵 } ∪ ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) = ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ↔ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) = ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) )
64 48 63 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) = ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) )
65 37 64 sseqtrrid ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ⊆ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) )
66 ssdif ⊢ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 → ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ⊆ ( 𝐼 ∖ { 𝐵 } ) )
67 66 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ⊆ ( 𝐼 ∖ { 𝐵 } ) )
68 67 6 sseqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ⊆ 𝐷 )
69 ax-resscn ⊢ ℝ ⊆ ℂ
70 69 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
71 fss ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ )
72 2 69 71 sylancl ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
73 70 72 1 dvbss ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) ⊆ 𝐴 )
74 7 73 sstrd ⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 )
75 74 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐷 ⊆ 𝐴 )
76 68 75 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ⊆ 𝐴 )
77 65 76 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ⊆ 𝐴 )
78 36 77 fssresd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝐹 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) : ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ⟶ ℝ )
79 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐺 : 𝐴 ⟶ ℝ )
80 79 77 fssresd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) : ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ⟶ ℝ )
81 69 a1i ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ℝ ⊆ ℂ )
82 72 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐹 : 𝐴 ⟶ ℂ )
83 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐴 ⊆ ℝ )
84 ioossre ⊢ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ⊆ ℝ
85 84 a1i ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ⊆ ℝ )
86 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
87 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
88 86 87 dvres ⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℝ ∧ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ⊆ ℝ ) ) → ( ℝ D ( 𝐹 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) )
89 81 82 83 85 88 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ℝ D ( 𝐹 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) )
90 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
91 iooretop ⊢ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )
92 isopn3i ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) = ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) )
93 90 91 92 mp2an ⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) = ( ( 𝐵 − 𝑟 ) (,) 𝐵 )
94 93 reseq2i ⊢ ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) )
95 89 94 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ℝ D ( 𝐹 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) )
96 95 dmeqd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → dom ( ℝ D ( 𝐹 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) = dom ( ( ℝ D 𝐹 ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) )
97 65 68 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ⊆ 𝐷 )
98 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐷 ⊆ dom ( ℝ D 𝐹 ) )
99 97 98 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ⊆ dom ( ℝ D 𝐹 ) )
100 ssdmres ⊢ ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ⊆ dom ( ℝ D 𝐹 ) ↔ dom ( ( ℝ D 𝐹 ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) = ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) )
101 99 100 sylib ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → dom ( ( ℝ D 𝐹 ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) = ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) )
102 96 101 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → dom ( ℝ D ( 𝐹 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) = ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) )
103 fss ⊢ ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐺 : 𝐴 ⟶ ℂ )
104 3 69 103 sylancl ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ ℂ )
105 104 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐺 : 𝐴 ⟶ ℂ )
106 86 87 dvres ⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℝ ∧ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ⊆ ℝ ) ) → ( ℝ D ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) = ( ( ℝ D 𝐺 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) )
107 81 105 83 85 106 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ℝ D ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) = ( ( ℝ D 𝐺 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) )
108 93 reseq2i ⊢ ( ( ℝ D 𝐺 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) = ( ( ℝ D 𝐺 ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) )
109 107 108 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ℝ D ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) = ( ( ℝ D 𝐺 ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) )
110 109 dmeqd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → dom ( ℝ D ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) = dom ( ( ℝ D 𝐺 ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) )
111 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐷 ⊆ dom ( ℝ D 𝐺 ) )
112 97 111 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ⊆ dom ( ℝ D 𝐺 ) )
113 ssdmres ⊢ ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ⊆ dom ( ℝ D 𝐺 ) ↔ dom ( ( ℝ D 𝐺 ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) = ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) )
114 112 113 sylib ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → dom ( ( ℝ D 𝐺 ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) = ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) )
115 110 114 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → dom ( ℝ D ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) = ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) )
116 limcresi ⊢ ( 𝐹 limℂ 𝐵 ) ⊆ ( ( 𝐹 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) limℂ 𝐵 )
117 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 0 ∈ ( 𝐹 limℂ 𝐵 ) )
118 116 117 sselid ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 0 ∈ ( ( 𝐹 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) limℂ 𝐵 ) )
119 limcresi ⊢ ( 𝐺 limℂ 𝐵 ) ⊆ ( ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) limℂ 𝐵 )
120 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 0 ∈ ( 𝐺 limℂ 𝐵 ) )
121 119 120 sselid ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 0 ∈ ( ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) limℂ 𝐵 ) )
122 df-ima ⊢ ( 𝐺 “ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) = ran ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) )
123 imass2 ⊢ ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ⊆ 𝐷 → ( 𝐺 “ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ⊆ ( 𝐺 “ 𝐷 ) )
124 97 123 syl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝐺 “ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ⊆ ( 𝐺 “ 𝐷 ) )
125 122 124 eqsstrrid ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ran ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ⊆ ( 𝐺 “ 𝐷 ) )
126 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ¬ 0 ∈ ( 𝐺 “ 𝐷 ) )
127 125 126 ssneldd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ¬ 0 ∈ ran ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) )
128 109 rneqd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ran ( ℝ D ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) = ran ( ( ℝ D 𝐺 ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) )
129 df-ima ⊢ ( ( ℝ D 𝐺 ) “ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) = ran ( ( ℝ D 𝐺 ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) )
130 128 129 eqtr4di ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ran ( ℝ D ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) = ( ( ℝ D 𝐺 ) “ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) )
131 imass2 ⊢ ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ⊆ 𝐷 → ( ( ℝ D 𝐺 ) “ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ⊆ ( ( ℝ D 𝐺 ) “ 𝐷 ) )
132 97 131 syl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( ℝ D 𝐺 ) “ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ⊆ ( ( ℝ D 𝐺 ) “ 𝐷 ) )
133 130 132 eqsstrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ran ( ℝ D ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) ⊆ ( ( ℝ D 𝐺 ) “ 𝐷 ) )
134 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ¬ 0 ∈ ( ( ℝ D 𝐺 ) “ 𝐷 ) )
135 133 134 ssneldd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ¬ 0 ∈ ran ( ℝ D ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) )
136 limcresi ⊢ ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) limℂ 𝐵 ) ⊆ ( ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) limℂ 𝐵 )
137 97 resmptd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) = ( 𝑧 ∈ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) )
138 95 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( ℝ D ( 𝐹 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) ‘ 𝑧 ) = ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ‘ 𝑧 ) )
139 fvres ⊢ ( 𝑧 ∈ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) → ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ‘ 𝑧 ) = ( ( ℝ D 𝐹 ) ‘ 𝑧 ) )
140 138 139 sylan9eq ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) ∧ 𝑧 ∈ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) → ( ( ℝ D ( 𝐹 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) ‘ 𝑧 ) = ( ( ℝ D 𝐹 ) ‘ 𝑧 ) )
141 109 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( ℝ D ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) ‘ 𝑧 ) = ( ( ( ℝ D 𝐺 ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ‘ 𝑧 ) )
142 fvres ⊢ ( 𝑧 ∈ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) → ( ( ( ℝ D 𝐺 ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ‘ 𝑧 ) = ( ( ℝ D 𝐺 ) ‘ 𝑧 ) )
143 141 142 sylan9eq ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) ∧ 𝑧 ∈ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) → ( ( ℝ D ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) ‘ 𝑧 ) = ( ( ℝ D 𝐺 ) ‘ 𝑧 ) )
144 140 143 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) ∧ 𝑧 ∈ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) → ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) ‘ 𝑧 ) / ( ( ℝ D ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) ‘ 𝑧 ) ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) )
145 144 mpteq2dva ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝑧 ∈ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ↦ ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) ‘ 𝑧 ) / ( ( ℝ D ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) )
146 137 145 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) = ( 𝑧 ∈ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ↦ ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) ‘ 𝑧 ) / ( ( ℝ D ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) ‘ 𝑧 ) ) ) )
147 146 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) limℂ 𝐵 ) = ( ( 𝑧 ∈ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ↦ ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) ‘ 𝑧 ) / ( ( ℝ D ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) ‘ 𝑧 ) ) ) limℂ 𝐵 ) )
148 136 147 sseqtrid ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) limℂ 𝐵 ) ⊆ ( ( 𝑧 ∈ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ↦ ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) ‘ 𝑧 ) / ( ( ℝ D ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) ‘ 𝑧 ) ) ) limℂ 𝐵 ) )
149 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐶 ∈ ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) limℂ 𝐵 ) )
150 148 149 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐶 ∈ ( ( 𝑧 ∈ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ↦ ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) ‘ 𝑧 ) / ( ( ℝ D ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ) ‘ 𝑧 ) ) ) limℂ 𝐵 ) )
151 34 30 35 78 80 102 115 118 121 127 135 150 lhop2 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐶 ∈ ( ( 𝑧 ∈ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ↦ ( ( ( 𝐹 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ‘ 𝑧 ) / ( ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ‘ 𝑧 ) ) ) limℂ 𝐵 ) )
152 65 resmptd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( 𝑧 ∈ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) = ( 𝑧 ∈ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) )
153 fvres ⊢ ( 𝑧 ∈ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) → ( ( 𝐹 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
154 fvres ⊢ ( 𝑧 ∈ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) → ( ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
155 153 154 oveq12d ⊢ ( 𝑧 ∈ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) → ( ( ( 𝐹 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ‘ 𝑧 ) / ( ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ‘ 𝑧 ) ) = ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) )
156 155 mpteq2ia ⊢ ( 𝑧 ∈ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ↦ ( ( ( 𝐹 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ‘ 𝑧 ) / ( ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) )
157 152 156 eqtr4di ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( 𝑧 ∈ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) = ( 𝑧 ∈ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ↦ ( ( ( 𝐹 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ‘ 𝑧 ) / ( ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ‘ 𝑧 ) ) ) )
158 157 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( ( 𝑧 ∈ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) limℂ 𝐵 ) = ( ( 𝑧 ∈ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ↦ ( ( ( 𝐹 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ‘ 𝑧 ) / ( ( 𝐺 ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) ‘ 𝑧 ) ) ) limℂ 𝐵 ) )
159 151 158 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐶 ∈ ( ( ( 𝑧 ∈ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) limℂ 𝐵 ) )
160 ssun2 ⊢ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ⊆ ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) )
161 160 64 sseqtrrid ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ⊆ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) )
162 161 76 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐴 )
163 36 162 fssresd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝐹 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) : ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ⟶ ℝ )
164 79 162 fssresd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) : ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ⟶ ℝ )
165 ioossre ⊢ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ⊆ ℝ
166 165 a1i ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ⊆ ℝ )
167 86 87 dvres ⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℝ ∧ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ⊆ ℝ ) ) → ( ℝ D ( 𝐹 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) )
168 81 82 83 166 167 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ℝ D ( 𝐹 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) )
169 iooretop ⊢ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ∈ ( topGen ‘ ran (,) )
170 isopn3i ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ∈ ( topGen ‘ ran (,) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) = ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) )
171 90 169 170 mp2an ⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) = ( 𝐵 (,) ( 𝐵 + 𝑟 ) )
172 171 reseq2i ⊢ ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) )
173 168 172 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ℝ D ( 𝐹 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) )
174 173 dmeqd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → dom ( ℝ D ( 𝐹 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) = dom ( ( ℝ D 𝐹 ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) )
175 161 68 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐷 )
176 175 98 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ⊆ dom ( ℝ D 𝐹 ) )
177 ssdmres ⊢ ( ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ⊆ dom ( ℝ D 𝐹 ) ↔ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) = ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) )
178 176 177 sylib ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → dom ( ( ℝ D 𝐹 ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) = ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) )
179 174 178 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → dom ( ℝ D ( 𝐹 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) = ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) )
180 86 87 dvres ⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ) ∧ ( 𝐴 ⊆ ℝ ∧ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ⊆ ℝ ) ) → ( ℝ D ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) = ( ( ℝ D 𝐺 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) )
181 81 105 83 166 180 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ℝ D ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) = ( ( ℝ D 𝐺 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) )
182 171 reseq2i ⊢ ( ( ℝ D 𝐺 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) = ( ( ℝ D 𝐺 ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) )
183 181 182 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ℝ D ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) = ( ( ℝ D 𝐺 ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) )
184 183 dmeqd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → dom ( ℝ D ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) = dom ( ( ℝ D 𝐺 ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) )
185 175 111 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ⊆ dom ( ℝ D 𝐺 ) )
186 ssdmres ⊢ ( ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ⊆ dom ( ℝ D 𝐺 ) ↔ dom ( ( ℝ D 𝐺 ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) = ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) )
187 185 186 sylib ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → dom ( ( ℝ D 𝐺 ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) = ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) )
188 184 187 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → dom ( ℝ D ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) = ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) )
189 limcresi ⊢ ( 𝐹 limℂ 𝐵 ) ⊆ ( ( 𝐹 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) limℂ 𝐵 )
190 189 117 sselid ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 0 ∈ ( ( 𝐹 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) limℂ 𝐵 ) )
191 limcresi ⊢ ( 𝐺 limℂ 𝐵 ) ⊆ ( ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) limℂ 𝐵 )
192 191 120 sselid ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 0 ∈ ( ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) limℂ 𝐵 ) )
193 df-ima ⊢ ( 𝐺 “ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) = ran ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) )
194 imass2 ⊢ ( ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐷 → ( 𝐺 “ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ⊆ ( 𝐺 “ 𝐷 ) )
195 175 194 syl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝐺 “ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ⊆ ( 𝐺 “ 𝐷 ) )
196 193 195 eqsstrrid ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ran ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ⊆ ( 𝐺 “ 𝐷 ) )
197 196 126 ssneldd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ¬ 0 ∈ ran ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) )
198 183 rneqd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ran ( ℝ D ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) = ran ( ( ℝ D 𝐺 ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) )
199 df-ima ⊢ ( ( ℝ D 𝐺 ) “ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) = ran ( ( ℝ D 𝐺 ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) )
200 198 199 eqtr4di ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ran ( ℝ D ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) = ( ( ℝ D 𝐺 ) “ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) )
201 imass2 ⊢ ( ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐷 → ( ( ℝ D 𝐺 ) “ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ⊆ ( ( ℝ D 𝐺 ) “ 𝐷 ) )
202 175 201 syl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( ℝ D 𝐺 ) “ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ⊆ ( ( ℝ D 𝐺 ) “ 𝐷 ) )
203 200 202 eqsstrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ran ( ℝ D ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) ⊆ ( ( ℝ D 𝐺 ) “ 𝐷 ) )
204 203 134 ssneldd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ¬ 0 ∈ ran ( ℝ D ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) )
205 limcresi ⊢ ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) limℂ 𝐵 ) ⊆ ( ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) limℂ 𝐵 )
206 175 resmptd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) = ( 𝑧 ∈ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) )
207 173 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( ℝ D ( 𝐹 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) ‘ 𝑧 ) = ( ( ( ℝ D 𝐹 ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ‘ 𝑧 ) )
208 fvres ⊢ ( 𝑧 ∈ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) → ( ( ( ℝ D 𝐹 ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ‘ 𝑧 ) = ( ( ℝ D 𝐹 ) ‘ 𝑧 ) )
209 207 208 sylan9eq ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) ∧ 𝑧 ∈ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) → ( ( ℝ D ( 𝐹 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) ‘ 𝑧 ) = ( ( ℝ D 𝐹 ) ‘ 𝑧 ) )
210 183 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( ℝ D ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) ‘ 𝑧 ) = ( ( ( ℝ D 𝐺 ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ‘ 𝑧 ) )
211 fvres ⊢ ( 𝑧 ∈ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) → ( ( ( ℝ D 𝐺 ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ‘ 𝑧 ) = ( ( ℝ D 𝐺 ) ‘ 𝑧 ) )
212 210 211 sylan9eq ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) ∧ 𝑧 ∈ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) → ( ( ℝ D ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) ‘ 𝑧 ) = ( ( ℝ D 𝐺 ) ‘ 𝑧 ) )
213 209 212 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) ∧ 𝑧 ∈ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) → ( ( ( ℝ D ( 𝐹 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) ‘ 𝑧 ) / ( ( ℝ D ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) ‘ 𝑧 ) ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) )
214 213 mpteq2dva ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝑧 ∈ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ↦ ( ( ( ℝ D ( 𝐹 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) ‘ 𝑧 ) / ( ( ℝ D ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) )
215 206 214 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) = ( 𝑧 ∈ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ↦ ( ( ( ℝ D ( 𝐹 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) ‘ 𝑧 ) / ( ( ℝ D ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) ‘ 𝑧 ) ) ) )
216 215 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) limℂ 𝐵 ) = ( ( 𝑧 ∈ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ↦ ( ( ( ℝ D ( 𝐹 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) ‘ 𝑧 ) / ( ( ℝ D ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) ‘ 𝑧 ) ) ) limℂ 𝐵 ) )
217 205 216 sseqtrid ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( 𝑧 ∈ 𝐷 ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑧 ) / ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) limℂ 𝐵 ) ⊆ ( ( 𝑧 ∈ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ↦ ( ( ( ℝ D ( 𝐹 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) ‘ 𝑧 ) / ( ( ℝ D ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) ‘ 𝑧 ) ) ) limℂ 𝐵 ) )
218 217 149 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐶 ∈ ( ( 𝑧 ∈ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ↦ ( ( ( ℝ D ( 𝐹 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) ‘ 𝑧 ) / ( ( ℝ D ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ) ‘ 𝑧 ) ) ) limℂ 𝐵 ) )
219 30 44 45 163 164 179 188 190 192 197 204 218 lhop1 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐶 ∈ ( ( 𝑧 ∈ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ↦ ( ( ( 𝐹 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ‘ 𝑧 ) / ( ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ‘ 𝑧 ) ) ) limℂ 𝐵 ) )
220 161 resmptd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( 𝑧 ∈ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) = ( 𝑧 ∈ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) )
221 fvres ⊢ ( 𝑧 ∈ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) → ( ( 𝐹 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
222 fvres ⊢ ( 𝑧 ∈ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) → ( ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
223 221 222 oveq12d ⊢ ( 𝑧 ∈ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) → ( ( ( 𝐹 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ‘ 𝑧 ) / ( ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ‘ 𝑧 ) ) = ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) )
224 223 mpteq2ia ⊢ ( 𝑧 ∈ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ↦ ( ( ( 𝐹 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ‘ 𝑧 ) / ( ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) )
225 220 224 eqtr4di ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( 𝑧 ∈ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) = ( 𝑧 ∈ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ↦ ( ( ( 𝐹 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ‘ 𝑧 ) / ( ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ‘ 𝑧 ) ) ) )
226 225 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( ( 𝑧 ∈ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) limℂ 𝐵 ) = ( ( 𝑧 ∈ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ↦ ( ( ( 𝐹 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ‘ 𝑧 ) / ( ( 𝐺 ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ‘ 𝑧 ) ) ) limℂ 𝐵 ) )
227 219 226 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐶 ∈ ( ( ( 𝑧 ∈ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) limℂ 𝐵 ) )
228 159 227 elind ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐶 ∈ ( ( ( ( 𝑧 ∈ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) limℂ 𝐵 ) ∩ ( ( ( 𝑧 ∈ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) limℂ 𝐵 ) ) )
229 68 resmptd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( 𝑧 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ↾ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ) = ( 𝑧 ∈ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) )
230 229 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( ( 𝑧 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ↾ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ) limℂ 𝐵 ) = ( ( 𝑧 ∈ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐵 ) )
231 74 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → 𝑧 ∈ 𝐴 )
232 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
233 231 232 syldan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
234 233 recnd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
235 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑧 ) ∈ ℝ )
236 231 235 syldan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → ( 𝐺 ‘ 𝑧 ) ∈ ℝ )
237 236 recnd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
238 11 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → ¬ 0 ∈ ( 𝐺 “ 𝐷 ) )
239 3 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
240 239 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → 𝐺 Fn 𝐴 )
241 74 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → 𝐷 ⊆ 𝐴 )
242 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → 𝑧 ∈ 𝐷 )
243 fnfvima ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝐷 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐷 ) → ( 𝐺 ‘ 𝑧 ) ∈ ( 𝐺 “ 𝐷 ) )
244 240 241 242 243 syl3anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → ( 𝐺 ‘ 𝑧 ) ∈ ( 𝐺 “ 𝐷 ) )
245 eleq1 ⊢ ( ( 𝐺 ‘ 𝑧 ) = 0 → ( ( 𝐺 ‘ 𝑧 ) ∈ ( 𝐺 “ 𝐷 ) ↔ 0 ∈ ( 𝐺 “ 𝐷 ) ) )
246 244 245 syl5ibcom ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → ( ( 𝐺 ‘ 𝑧 ) = 0 → 0 ∈ ( 𝐺 “ 𝐷 ) ) )
247 246 necon3bd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → ( ¬ 0 ∈ ( 𝐺 “ 𝐷 ) → ( 𝐺 ‘ 𝑧 ) ≠ 0 ) )
248 238 247 mpd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → ( 𝐺 ‘ 𝑧 ) ≠ 0 )
249 234 237 248 divcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ∈ ℂ )
250 249 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) ∧ 𝑧 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ∈ ℂ )
251 250 fmpttd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝑧 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) : 𝐷 ⟶ ℂ )
252 difss ⊢ ( 𝐼 ∖ { 𝐵 } ) ⊆ 𝐼
253 6 252 eqsstri ⊢ 𝐷 ⊆ 𝐼
254 24 69 sstrdi ⊢ ( 𝜑 → 𝐼 ⊆ ℂ )
255 253 254 sstrid ⊢ ( 𝜑 → 𝐷 ⊆ ℂ )
256 255 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐷 ⊆ ℂ )
257 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐷 ∪ { 𝐵 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐷 ∪ { 𝐵 } ) )
258 6 uneq1i ⊢ ( 𝐷 ∪ { 𝐵 } ) = ( ( 𝐼 ∖ { 𝐵 } ) ∪ { 𝐵 } )
259 undif1 ⊢ ( ( 𝐼 ∖ { 𝐵 } ) ∪ { 𝐵 } ) = ( 𝐼 ∪ { 𝐵 } )
260 258 259 eqtri ⊢ ( 𝐷 ∪ { 𝐵 } ) = ( 𝐼 ∪ { 𝐵 } )
261 simprr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 )
262 52 261 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → { 𝐵 } ⊆ 𝐼 )
263 ssequn2 ⊢ ( { 𝐵 } ⊆ 𝐼 ↔ ( 𝐼 ∪ { 𝐵 } ) = 𝐼 )
264 262 263 sylib ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝐼 ∪ { 𝐵 } ) = 𝐼 )
265 260 264 eqtrid ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝐷 ∪ { 𝐵 } ) = 𝐼 )
266 265 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐷 ∪ { 𝐵 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝐼 ) )
267 24 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐼 ⊆ ℝ )
268 eqid ⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
269 86 268 rerest ⊢ ( 𝐼 ⊆ ℝ → ( ( TopOpen ‘ ℂfld ) ↾t 𝐼 ) = ( ( topGen ‘ ran (,) ) ↾t 𝐼 ) )
270 267 269 syl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝐼 ) = ( ( topGen ‘ ran (,) ) ↾t 𝐼 ) )
271 266 270 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐷 ∪ { 𝐵 } ) ) = ( ( topGen ‘ ran (,) ) ↾t 𝐼 ) )
272 271 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐷 ∪ { 𝐵 } ) ) ) = ( int ‘ ( ( topGen ‘ ran (,) ) ↾t 𝐼 ) ) )
273 272 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐷 ∪ { 𝐵 } ) ) ) ‘ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ) = ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾t 𝐼 ) ) ‘ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ) )
274 86 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
275 254 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐼 ⊆ ℂ )
276 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝐼 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝐼 ) ∈ ( TopOn ‘ 𝐼 ) )
277 274 275 276 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝐼 ) ∈ ( TopOn ‘ 𝐼 ) )
278 topontop ⊢ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐼 ) ∈ ( TopOn ‘ 𝐼 ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝐼 ) ∈ Top )
279 277 278 syl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝐼 ) ∈ Top )
280 270 279 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( topGen ‘ ran (,) ) ↾t 𝐼 ) ∈ Top )
281 iooretop ⊢ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∈ ( topGen ‘ ran (,) )
282 281 a1i ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∈ ( topGen ‘ ran (,) ) )
283 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐼 ∈ ( topGen ‘ ran (,) ) )
284 restopn2 ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ 𝐼 ∈ ( topGen ‘ ran (,) ) ) → ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∈ ( ( topGen ‘ ran (,) ) ↾t 𝐼 ) ↔ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∈ ( topGen ‘ ran (,) ) ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) )
285 90 283 284 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∈ ( ( topGen ‘ ran (,) ) ↾t 𝐼 ) ↔ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∈ ( topGen ‘ ran (,) ) ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) )
286 282 261 285 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∈ ( ( topGen ‘ ran (,) ) ↾t 𝐼 ) )
287 isopn3i ⊢ ( ( ( ( topGen ‘ ran (,) ) ↾t 𝐼 ) ∈ Top ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∈ ( ( topGen ‘ ran (,) ) ↾t 𝐼 ) ) → ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾t 𝐼 ) ) ‘ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ) = ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) )
288 280 286 287 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾t 𝐼 ) ) ‘ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ) = ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) )
289 273 288 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐷 ∪ { 𝐵 } ) ) ) ‘ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ) = ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) )
290 51 289 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐵 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐷 ∪ { 𝐵 } ) ) ) ‘ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ) )
291 undif1 ⊢ ( ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ∪ { 𝐵 } ) = ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∪ { 𝐵 } )
292 ssequn2 ⊢ ( { 𝐵 } ⊆ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ↔ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∪ { 𝐵 } ) = ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) )
293 52 292 sylib ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∪ { 𝐵 } ) = ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) )
294 291 293 eqtrid ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ∪ { 𝐵 } ) = ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) )
295 294 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐷 ∪ { 𝐵 } ) ) ) ‘ ( ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ∪ { 𝐵 } ) ) = ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐷 ∪ { 𝐵 } ) ) ) ‘ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ) )
296 290 295 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐵 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐷 ∪ { 𝐵 } ) ) ) ‘ ( ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ∪ { 𝐵 } ) ) )
297 251 68 256 86 257 296 limcres ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( ( 𝑧 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ↾ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ) limℂ 𝐵 ) = ( ( 𝑧 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐵 ) )
298 84 69 sstri ⊢ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ⊆ ℂ
299 298 a1i ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ⊆ ℂ )
300 165 69 sstri ⊢ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ⊆ ℂ
301 300 a1i ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ⊆ ℂ )
302 68 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) ∧ 𝑧 ∈ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ) → 𝑧 ∈ 𝐷 )
303 302 250 syldan ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) ∧ 𝑧 ∈ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ) → ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ∈ ℂ )
304 303 fmpttd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝑧 ∈ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) : ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ⟶ ℂ )
305 64 feq2d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( 𝑧 ∈ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) : ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ⟶ ℂ ↔ ( 𝑧 ∈ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) : ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ⟶ ℂ ) )
306 304 305 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( 𝑧 ∈ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) : ( ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ∪ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) ⟶ ℂ )
307 299 301 306 limcun ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( 𝑧 ∈ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐵 ) = ( ( ( ( 𝑧 ∈ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) limℂ 𝐵 ) ∩ ( ( ( 𝑧 ∈ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) limℂ 𝐵 ) ) )
308 230 297 307 3eqtr3rd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → ( ( ( ( 𝑧 ∈ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ↾ ( ( 𝐵 − 𝑟 ) (,) 𝐵 ) ) limℂ 𝐵 ) ∩ ( ( ( 𝑧 ∈ ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) ↾ ( 𝐵 (,) ( 𝐵 + 𝑟 ) ) ) limℂ 𝐵 ) ) = ( ( 𝑧 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐵 ) )
309 228 308 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 ) ) → 𝐶 ∈ ( ( 𝑧 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐵 ) )
310 309 expr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ( ( 𝐵 − 𝑟 ) (,) ( 𝐵 + 𝑟 ) ) ⊆ 𝐼 → 𝐶 ∈ ( ( 𝑧 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐵 ) ) )
311 29 310 sylbid ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝐵 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝐼 → 𝐶 ∈ ( ( 𝑧 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐵 ) ) )
312 311 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ ℝ+ ( 𝐵 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝐼 → 𝐶 ∈ ( ( 𝑧 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐵 ) ) )
313 20 312 mpd ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝑧 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑧 ) / ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐵 ) )