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
|- ( ph -> A C_ RR )
lhop.f
|- ( ph -> F : A --> RR )
lhop.g
|- ( ph -> G : A --> RR )
lhop.i
|- ( ph -> I e. ( topGen ` ran (,) ) )
lhop.b
|- ( ph -> B e. I )
lhop.d
|- D = ( I \ { B } )
lhop.if
|- ( ph -> D C_ dom ( RR _D F ) )
lhop.ig
|- ( ph -> D C_ dom ( RR _D G ) )
lhop.f0
|- ( ph -> 0 e. ( F limCC B ) )
lhop.g0
|- ( ph -> 0 e. ( G limCC B ) )
lhop.gn0
|- ( ph -> -. 0 e. ( G " D ) )
lhop.gd0
|- ( ph -> -. 0 e. ( ( RR _D G ) " D ) )
lhop.c
|- ( ph -> C e. ( ( z e. D |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) limCC B ) )
Assertion lhop
|- ( ph -> C e. ( ( z e. D |-> ( ( F ` z ) / ( G ` z ) ) ) limCC B ) )

Proof

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