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 eqtrid 
 |-  ( ( 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 eqtrid 
 |-  ( ( 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 eqtrid 
 |-  ( ( 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 ) )