Metamath Proof Explorer

Theorem lhop1lem

Description: Lemma for lhop1 . (Contributed by Mario Carneiro, 29-Dec-2016)

Ref Expression
Hypotheses lhop1.a 
|- ( ph -> A e. RR )
lhop1.b 
|- ( ph -> B e. RR* )
lhop1.l 
|- ( ph -> A < B )
lhop1.f 
|- ( ph -> F : ( A (,) B ) --> RR )
lhop1.g 
|- ( ph -> G : ( A (,) B ) --> RR )
lhop1.if 
|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
lhop1.ig 
|- ( ph -> dom ( RR _D G ) = ( A (,) B ) )
lhop1.f0 
|- ( ph -> 0 e. ( F limCC A ) )
lhop1.g0 
|- ( ph -> 0 e. ( G limCC A ) )
lhop1.gn0 
|- ( ph -> -. 0 e. ran G )
lhop1.gd0 
|- ( ph -> -. 0 e. ran ( RR _D G ) )
lhop1.c 
|- ( ph -> C e. ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) limCC A ) )
lhop1lem.e 
|- ( ph -> E e. RR+ )
lhop1lem.d 
|- ( ph -> D e. RR )
lhop1lem.db 
|- ( ph -> D <_ B )
lhop1lem.x 
|- ( ph -> X e. ( A (,) D ) )
lhop1lem.t 
|- ( ph -> A. t e. ( A (,) D ) ( abs ` ( ( ( ( RR _D F ) ` t ) / ( ( RR _D G ) ` t ) ) - C ) ) < E )
lhop1lem.r 
|- R = ( A + ( r / 2 ) )
Assertion lhop1lem 
|- ( ph -> ( abs ` ( ( ( F ` X ) / ( G ` X ) ) - C ) ) < ( 2 x. E ) )

Proof

Step Hyp Ref Expression
1 lhop1.a 
 |-  ( ph -> A e. RR )
2 lhop1.b 
 |-  ( ph -> B e. RR* )
3 lhop1.l 
 |-  ( ph -> A < B )
4 lhop1.f 
 |-  ( ph -> F : ( A (,) B ) --> RR )
5 lhop1.g 
 |-  ( ph -> G : ( A (,) B ) --> RR )
6 lhop1.if 
 |-  ( ph -> dom ( RR _D F ) = ( A (,) B ) )
7 lhop1.ig 
 |-  ( ph -> dom ( RR _D G ) = ( A (,) B ) )
8 lhop1.f0 
 |-  ( ph -> 0 e. ( F limCC A ) )
9 lhop1.g0 
 |-  ( ph -> 0 e. ( G limCC A ) )
10 lhop1.gn0 
 |-  ( ph -> -. 0 e. ran G )
11 lhop1.gd0 
 |-  ( ph -> -. 0 e. ran ( RR _D G ) )
12 lhop1.c 
 |-  ( ph -> C e. ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) limCC A ) )
13 lhop1lem.e 
 |-  ( ph -> E e. RR+ )
14 lhop1lem.d 
 |-  ( ph -> D e. RR )
15 lhop1lem.db 
 |-  ( ph -> D <_ B )
16 lhop1lem.x 
 |-  ( ph -> X e. ( A (,) D ) )
17 lhop1lem.t 
 |-  ( ph -> A. t e. ( A (,) D ) ( abs ` ( ( ( ( RR _D F ) ` t ) / ( ( RR _D G ) ` t ) ) - C ) ) < E )
18 lhop1lem.r 
 |-  R = ( A + ( r / 2 ) )
19 iooss2 
 |-  ( ( B e. RR* /\ D <_ B ) -> ( A (,) D ) C_ ( A (,) B ) )
20 2 15 19 syl2anc 
 |-  ( ph -> ( A (,) D ) C_ ( A (,) B ) )
21 20 16 sseldd 
 |-  ( ph -> X e. ( A (,) B ) )
22 4 21 ffvelrnd 
 |-  ( ph -> ( F ` X ) e. RR )
23 22 recnd 
 |-  ( ph -> ( F ` X ) e. CC )
24 5 21 ffvelrnd 
 |-  ( ph -> ( G ` X ) e. RR )
25 24 recnd 
 |-  ( ph -> ( G ` X ) e. CC )
26 5 ffnd 
 |-  ( ph -> G Fn ( A (,) B ) )
27 fnfvelrn 
 |-  ( ( G Fn ( A (,) B ) /\ X e. ( A (,) B ) ) -> ( G ` X ) e. ran G )
28 26 21 27 syl2anc 
 |-  ( ph -> ( G ` X ) e. ran G )
29 eleq1 
 |-  ( ( G ` X ) = 0 -> ( ( G ` X ) e. ran G <-> 0 e. ran G ) )
30 28 29 syl5ibcom 
 |-  ( ph -> ( ( G ` X ) = 0 -> 0 e. ran G ) )
31 30 necon3bd 
 |-  ( ph -> ( -. 0 e. ran G -> ( G ` X ) =/= 0 ) )
32 10 31 mpd 
 |-  ( ph -> ( G ` X ) =/= 0 )
33 23 25 32 divcld 
 |-  ( ph -> ( ( F ` X ) / ( G ` X ) ) e. CC )
34 limccl 
 |-  ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) limCC A ) C_ CC
35 34 12 sseldi 
 |-  ( ph -> C e. CC )
36 33 35 subcld 
 |-  ( ph -> ( ( ( F ` X ) / ( G ` X ) ) - C ) e. CC )
37 36 abscld 
 |-  ( ph -> ( abs ` ( ( ( F ` X ) / ( G ` X ) ) - C ) ) e. RR )
38 13 rpred 
 |-  ( ph -> E e. RR )
39 2re 
 |-  2 e. RR
40 39 a1i 
 |-  ( ph -> 2 e. RR )
41 40 38 remulcld 
 |-  ( ph -> ( 2 x. E ) e. RR )
42 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
43 42 a1i 
 |-  ( ( ph /\ ( v e. ( TopOpen ` CCfld ) /\ A e. v ) ) -> ( abs o. - ) e. ( *Met ` CC ) )
44 simprl 
 |-  ( ( ph /\ ( v e. ( TopOpen ` CCfld ) /\ A e. v ) ) -> v e. ( TopOpen ` CCfld ) )
45 simprr 
 |-  ( ( ph /\ ( v e. ( TopOpen ` CCfld ) /\ A e. v ) ) -> A e. v )
46 eliooord 
 |-  ( X e. ( A (,) D ) -> ( A < X /\ X < D ) )
47 16 46 syl 
 |-  ( ph -> ( A < X /\ X < D ) )
48 47 simpld 
 |-  ( ph -> A < X )
49 ioossre 
 |-  ( A (,) D ) C_ RR
50 49 16 sseldi 
 |-  ( ph -> X e. RR )
51 difrp 
 |-  ( ( A e. RR /\ X e. RR ) -> ( A < X <-> ( X - A ) e. RR+ ) )
52 1 50 51 syl2anc 
 |-  ( ph -> ( A < X <-> ( X - A ) e. RR+ ) )
53 48 52 mpbid 
 |-  ( ph -> ( X - A ) e. RR+ )
54 53 adantr 
 |-  ( ( ph /\ ( v e. ( TopOpen ` CCfld ) /\ A e. v ) ) -> ( X - A ) e. RR+ )
55 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
56 55 cnfldtopn 
 |-  ( TopOpen ` CCfld ) = ( MetOpen ` ( abs o. - ) )
57 56 mopni3 
 |-  ( ( ( ( abs o. - ) e. ( *Met ` CC ) /\ v e. ( TopOpen ` CCfld ) /\ A e. v ) /\ ( X - A ) e. RR+ ) -> E. r e. RR+ ( r < ( X - A ) /\ ( A ( ball ` ( abs o. - ) ) r ) C_ v ) )
58 43 44 45 54 57 syl31anc 
 |-  ( ( ph /\ ( v e. ( TopOpen ` CCfld ) /\ A e. v ) ) -> E. r e. RR+ ( r < ( X - A ) /\ ( A ( ball ` ( abs o. - ) ) r ) C_ v ) )
59 ssrin 
 |-  ( ( A ( ball ` ( abs o. - ) ) r ) C_ v -> ( ( A ( ball ` ( abs o. - ) ) r ) i^i ( A (,) X ) ) C_ ( v i^i ( A (,) X ) ) )
60 lbioo 
 |-  -. A e. ( A (,) X )
61 disjsn 
 |-  ( ( ( A (,) X ) i^i { A } ) = (/) <-> -. A e. ( A (,) X ) )
62 60 61 mpbir 
 |-  ( ( A (,) X ) i^i { A } ) = (/)
63 disj3 
 |-  ( ( ( A (,) X ) i^i { A } ) = (/) <-> ( A (,) X ) = ( ( A (,) X ) \ { A } ) )
64 62 63 mpbi 
 |-  ( A (,) X ) = ( ( A (,) X ) \ { A } )
65 64 ineq2i 
 |-  ( v i^i ( A (,) X ) ) = ( v i^i ( ( A (,) X ) \ { A } ) )
66 59 65 sseqtrdi 
 |-  ( ( A ( ball ` ( abs o. - ) ) r ) C_ v -> ( ( A ( ball ` ( abs o. - ) ) r ) i^i ( A (,) X ) ) C_ ( v i^i ( ( A (,) X ) \ { A } ) ) )
67 1 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> A e. RR )
68 simprl 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> r e. RR+ )
69 68 rpred 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> r e. RR )
70 69 rehalfcld 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( r / 2 ) e. RR )
71 67 70 readdcld 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( A + ( r / 2 ) ) e. RR )
72 18 71 eqeltrid 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> R e. RR )
73 72 recnd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> R e. CC )
74 1 recnd 
 |-  ( ph -> A e. CC )
75 74 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> A e. CC )
76 eqid 
 |-  ( abs o. - ) = ( abs o. - )
77 76 cnmetdval 
 |-  ( ( R e. CC /\ A e. CC ) -> ( R ( abs o. - ) A ) = ( abs ` ( R - A ) ) )
78 73 75 77 syl2anc 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( R ( abs o. - ) A ) = ( abs ` ( R - A ) ) )
79 18 oveq1i 
 |-  ( R - A ) = ( ( A + ( r / 2 ) ) - A )
80 69 recnd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> r e. CC )
81 80 halfcld 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( r / 2 ) e. CC )
82 75 81 pncan2d 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( ( A + ( r / 2 ) ) - A ) = ( r / 2 ) )
83 79 82 syl5eq 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( R - A ) = ( r / 2 ) )
84 83 fveq2d 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( abs ` ( R - A ) ) = ( abs ` ( r / 2 ) ) )
85 68 rphalfcld 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( r / 2 ) e. RR+ )
86 85 rpred 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( r / 2 ) e. RR )
87 85 rpge0d 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> 0 <_ ( r / 2 ) )
88 86 87 absidd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( abs ` ( r / 2 ) ) = ( r / 2 ) )
89 78 84 88 3eqtrd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( R ( abs o. - ) A ) = ( r / 2 ) )
90 rphalflt 
 |-  ( r e. RR+ -> ( r / 2 ) < r )
91 68 90 syl 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( r / 2 ) < r )
92 89 91 eqbrtrd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( R ( abs o. - ) A ) < r )
93 42 a1i 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( abs o. - ) e. ( *Met ` CC ) )
94 69 rexrd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> r e. RR* )
95 elbl3 
 |-  ( ( ( ( abs o. - ) e. ( *Met ` CC ) /\ r e. RR* ) /\ ( A e. CC /\ R e. CC ) ) -> ( R e. ( A ( ball ` ( abs o. - ) ) r ) <-> ( R ( abs o. - ) A ) < r ) )
96 93 94 75 73 95 syl22anc 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( R e. ( A ( ball ` ( abs o. - ) ) r ) <-> ( R ( abs o. - ) A ) < r ) )
97 92 96 mpbird 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> R e. ( A ( ball ` ( abs o. - ) ) r ) )
98 67 85 ltaddrpd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> A < ( A + ( r / 2 ) ) )
99 98 18 breqtrrdi 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> A < R )
100 50 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> X e. RR )
101 100 67 resubcld 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( X - A ) e. RR )
102 simprr 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> r < ( X - A ) )
103 86 69 101 91 102 lttrd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( r / 2 ) < ( X - A ) )
104 67 86 100 ltaddsub2d 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( ( A + ( r / 2 ) ) < X <-> ( r / 2 ) < ( X - A ) ) )
105 103 104 mpbird 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( A + ( r / 2 ) ) < X )
106 18 105 eqbrtrid 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> R < X )
107 67 rexrd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> A e. RR* )
108 50 rexrd 
 |-  ( ph -> X e. RR* )
109 108 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> X e. RR* )
110 elioo2 
 |-  ( ( A e. RR* /\ X e. RR* ) -> ( R e. ( A (,) X ) <-> ( R e. RR /\ A < R /\ R < X ) ) )
111 107 109 110 syl2anc 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( R e. ( A (,) X ) <-> ( R e. RR /\ A < R /\ R < X ) ) )
112 72 99 106 111 mpbir3and 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> R e. ( A (,) X ) )
113 97 112 elind 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> R e. ( ( A ( ball ` ( abs o. - ) ) r ) i^i ( A (,) X ) ) )
114 23 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( F ` X ) e. CC )
115 4 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> F : ( A (,) B ) --> RR )
116 14 rexrd 
 |-  ( ph -> D e. RR* )
117 47 simprd 
 |-  ( ph -> X < D )
118 50 14 117 ltled 
 |-  ( ph -> X <_ D )
119 108 116 2 118 15 xrletrd 
 |-  ( ph -> X <_ B )
120 iooss2 
 |-  ( ( B e. RR* /\ X <_ B ) -> ( A (,) X ) C_ ( A (,) B ) )
121 2 119 120 syl2anc 
 |-  ( ph -> ( A (,) X ) C_ ( A (,) B ) )
122 121 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( A (,) X ) C_ ( A (,) B ) )
123 122 112 sseldd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> R e. ( A (,) B ) )
124 115 123 ffvelrnd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( F ` R ) e. RR )
125 124 recnd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( F ` R ) e. CC )
126 114 125 subcld 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( ( F ` X ) - ( F ` R ) ) e. CC )
127 25 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( G ` X ) e. CC )
128 5 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> G : ( A (,) B ) --> RR )
129 128 123 ffvelrnd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( G ` R ) e. RR )
130 129 recnd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( G ` R ) e. CC )
131 127 130 subcld 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( ( G ` X ) - ( G ` R ) ) e. CC )
132 fveq2 
 |-  ( z = R -> ( G ` z ) = ( G ` R ) )
133 132 oveq2d 
 |-  ( z = R -> ( ( G ` X ) - ( G ` z ) ) = ( ( G ` X ) - ( G ` R ) ) )
134 133 neeq1d 
 |-  ( z = R -> ( ( ( G ` X ) - ( G ` z ) ) =/= 0 <-> ( ( G ` X ) - ( G ` R ) ) =/= 0 ) )
135 11 adantr 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> -. 0 e. ran ( RR _D G ) )
136 25 adantr 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> ( G ` X ) e. CC )
137 121 sselda 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> z e. ( A (,) B ) )
138 5 ffvelrnda 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( G ` z ) e. RR )
139 137 138 syldan 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> ( G ` z ) e. RR )
140 139 recnd 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> ( G ` z ) e. CC )
141 136 140 subeq0ad 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> ( ( ( G ` X ) - ( G ` z ) ) = 0 <-> ( G ` X ) = ( G ` z ) ) )
142 ioossre 
 |-  ( A (,) B ) C_ RR
143 142 137 sseldi 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> z e. RR )
144 143 adantr 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> z e. RR )
145 50 ad2antrr 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> X e. RR )
146 eliooord 
 |-  ( z e. ( A (,) X ) -> ( A < z /\ z < X ) )
147 146 adantl 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> ( A < z /\ z < X ) )
148 147 simprd 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> z < X )
149 148 adantr 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> z < X )
150 1 rexrd 
 |-  ( ph -> A e. RR* )
151 150 adantr 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> A e. RR* )
152 2 adantr 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> B e. RR* )
153 147 simpld 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> A < z )
154 108 116 2 117 15 xrltletrd 
 |-  ( ph -> X < B )
155 154 adantr 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> X < B )
156 iccssioo 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( A < z /\ X < B ) ) -> ( z [,] X ) C_ ( A (,) B ) )
157 151 152 153 155 156 syl22anc 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> ( z [,] X ) C_ ( A (,) B ) )
158 157 adantr 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> ( z [,] X ) C_ ( A (,) B ) )
159 ax-resscn 
 |-  RR C_ CC
160 159 a1i 
 |-  ( ph -> RR C_ CC )
161 fss 
 |-  ( ( G : ( A (,) B ) --> RR /\ RR C_ CC ) -> G : ( A (,) B ) --> CC )
162 5 159 161 sylancl 
 |-  ( ph -> G : ( A (,) B ) --> CC )
163 142 a1i 
 |-  ( ph -> ( A (,) B ) C_ RR )
164 dvcn 
 |-  ( ( ( RR C_ CC /\ G : ( A (,) B ) --> CC /\ ( A (,) B ) C_ RR ) /\ dom ( RR _D G ) = ( A (,) B ) ) -> G e. ( ( A (,) B ) -cn-> CC ) )
165 160 162 163 7 164 syl31anc 
 |-  ( ph -> G e. ( ( A (,) B ) -cn-> CC ) )
166 cncffvrn 
 |-  ( ( RR C_ CC /\ G e. ( ( A (,) B ) -cn-> CC ) ) -> ( G e. ( ( A (,) B ) -cn-> RR ) <-> G : ( A (,) B ) --> RR ) )
167 159 165 166 sylancr 
 |-  ( ph -> ( G e. ( ( A (,) B ) -cn-> RR ) <-> G : ( A (,) B ) --> RR ) )
168 5 167 mpbird 
 |-  ( ph -> G e. ( ( A (,) B ) -cn-> RR ) )
169 168 ad2antrr 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> G e. ( ( A (,) B ) -cn-> RR ) )
170 rescncf 
 |-  ( ( z [,] X ) C_ ( A (,) B ) -> ( G e. ( ( A (,) B ) -cn-> RR ) -> ( G |` ( z [,] X ) ) e. ( ( z [,] X ) -cn-> RR ) ) )
171 158 169 170 sylc 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> ( G |` ( z [,] X ) ) e. ( ( z [,] X ) -cn-> RR ) )
172 159 a1i 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> RR C_ CC )
173 162 ad2antrr 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> G : ( A (,) B ) --> CC )
174 142 a1i 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> ( A (,) B ) C_ RR )
175 158 142 sstrdi 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> ( z [,] X ) C_ RR )
176 55 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
177 55 176 dvres 
 |-  ( ( ( RR C_ CC /\ G : ( A (,) B ) --> CC ) /\ ( ( A (,) B ) C_ RR /\ ( z [,] X ) C_ RR ) ) -> ( RR _D ( G |` ( z [,] X ) ) ) = ( ( RR _D G ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( z [,] X ) ) ) )
178 172 173 174 175 177 syl22anc 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> ( RR _D ( G |` ( z [,] X ) ) ) = ( ( RR _D G ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( z [,] X ) ) ) )
179 iccntr 
 |-  ( ( z e. RR /\ X e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( z [,] X ) ) = ( z (,) X ) )
180 144 145 179 syl2anc 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( z [,] X ) ) = ( z (,) X ) )
181 180 reseq2d 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> ( ( RR _D G ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( z [,] X ) ) ) = ( ( RR _D G ) |` ( z (,) X ) ) )
182 178 181 eqtrd 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> ( RR _D ( G |` ( z [,] X ) ) ) = ( ( RR _D G ) |` ( z (,) X ) ) )
183 182 dmeqd 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> dom ( RR _D ( G |` ( z [,] X ) ) ) = dom ( ( RR _D G ) |` ( z (,) X ) ) )
184 ioossicc 
 |-  ( z (,) X ) C_ ( z [,] X )
185 184 158 sstrid 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> ( z (,) X ) C_ ( A (,) B ) )
186 7 ad2antrr 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> dom ( RR _D G ) = ( A (,) B ) )
187 185 186 sseqtrrd 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> ( z (,) X ) C_ dom ( RR _D G ) )
188 ssdmres 
 |-  ( ( z (,) X ) C_ dom ( RR _D G ) <-> dom ( ( RR _D G ) |` ( z (,) X ) ) = ( z (,) X ) )
189 187 188 sylib 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> dom ( ( RR _D G ) |` ( z (,) X ) ) = ( z (,) X ) )
190 183 189 eqtrd 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> dom ( RR _D ( G |` ( z [,] X ) ) ) = ( z (,) X ) )
191 143 rexrd 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> z e. RR* )
192 108 adantr 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> X e. RR* )
193 50 adantr 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> X e. RR )
194 143 193 148 ltled 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> z <_ X )
195 ubicc2 
 |-  ( ( z e. RR* /\ X e. RR* /\ z <_ X ) -> X e. ( z [,] X ) )
196 191 192 194 195 syl3anc 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> X e. ( z [,] X ) )
197 196 fvresd 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> ( ( G |` ( z [,] X ) ) ` X ) = ( G ` X ) )
198 lbicc2 
 |-  ( ( z e. RR* /\ X e. RR* /\ z <_ X ) -> z e. ( z [,] X ) )
199 191 192 194 198 syl3anc 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> z e. ( z [,] X ) )
200 199 fvresd 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> ( ( G |` ( z [,] X ) ) ` z ) = ( G ` z ) )
201 197 200 eqeq12d 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> ( ( ( G |` ( z [,] X ) ) ` X ) = ( ( G |` ( z [,] X ) ) ` z ) <-> ( G ` X ) = ( G ` z ) ) )
202 201 biimpar 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> ( ( G |` ( z [,] X ) ) ` X ) = ( ( G |` ( z [,] X ) ) ` z ) )
203 202 eqcomd 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> ( ( G |` ( z [,] X ) ) ` z ) = ( ( G |` ( z [,] X ) ) ` X ) )
204 144 145 149 171 190 203 rolle 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> E. w e. ( z (,) X ) ( ( RR _D ( G |` ( z [,] X ) ) ) ` w ) = 0 )
205 182 fveq1d 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> ( ( RR _D ( G |` ( z [,] X ) ) ) ` w ) = ( ( ( RR _D G ) |` ( z (,) X ) ) ` w ) )
206 fvres 
 |-  ( w e. ( z (,) X ) -> ( ( ( RR _D G ) |` ( z (,) X ) ) ` w ) = ( ( RR _D G ) ` w ) )
207 205 206 sylan9eq 
 |-  ( ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) /\ w e. ( z (,) X ) ) -> ( ( RR _D ( G |` ( z [,] X ) ) ) ` w ) = ( ( RR _D G ) ` w ) )
208 dvf 
 |-  ( RR _D G ) : dom ( RR _D G ) --> CC
209 7 feq2d 
 |-  ( ph -> ( ( RR _D G ) : dom ( RR _D G ) --> CC <-> ( RR _D G ) : ( A (,) B ) --> CC ) )
210 208 209 mpbii 
 |-  ( ph -> ( RR _D G ) : ( A (,) B ) --> CC )
211 210 ad2antrr 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> ( RR _D G ) : ( A (,) B ) --> CC )
212 211 ffnd 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> ( RR _D G ) Fn ( A (,) B ) )
213 212 adantr 
 |-  ( ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) /\ w e. ( z (,) X ) ) -> ( RR _D G ) Fn ( A (,) B ) )
214 185 sselda 
 |-  ( ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) /\ w e. ( z (,) X ) ) -> w e. ( A (,) B ) )
215 fnfvelrn 
 |-  ( ( ( RR _D G ) Fn ( A (,) B ) /\ w e. ( A (,) B ) ) -> ( ( RR _D G ) ` w ) e. ran ( RR _D G ) )
216 213 214 215 syl2anc 
 |-  ( ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) /\ w e. ( z (,) X ) ) -> ( ( RR _D G ) ` w ) e. ran ( RR _D G ) )
217 207 216 eqeltrd 
 |-  ( ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) /\ w e. ( z (,) X ) ) -> ( ( RR _D ( G |` ( z [,] X ) ) ) ` w ) e. ran ( RR _D G ) )
218 eleq1 
 |-  ( ( ( RR _D ( G |` ( z [,] X ) ) ) ` w ) = 0 -> ( ( ( RR _D ( G |` ( z [,] X ) ) ) ` w ) e. ran ( RR _D G ) <-> 0 e. ran ( RR _D G ) ) )
219 217 218 syl5ibcom 
 |-  ( ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) /\ w e. ( z (,) X ) ) -> ( ( ( RR _D ( G |` ( z [,] X ) ) ) ` w ) = 0 -> 0 e. ran ( RR _D G ) ) )
220 219 rexlimdva 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> ( E. w e. ( z (,) X ) ( ( RR _D ( G |` ( z [,] X ) ) ) ` w ) = 0 -> 0 e. ran ( RR _D G ) ) )
221 204 220 mpd 
 |-  ( ( ( ph /\ z e. ( A (,) X ) ) /\ ( G ` X ) = ( G ` z ) ) -> 0 e. ran ( RR _D G ) )
222 221 ex 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> ( ( G ` X ) = ( G ` z ) -> 0 e. ran ( RR _D G ) ) )
223 141 222 sylbid 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> ( ( ( G ` X ) - ( G ` z ) ) = 0 -> 0 e. ran ( RR _D G ) ) )
224 223 necon3bd 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> ( -. 0 e. ran ( RR _D G ) -> ( ( G ` X ) - ( G ` z ) ) =/= 0 ) )
225 135 224 mpd 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> ( ( G ` X ) - ( G ` z ) ) =/= 0 )
226 225 ralrimiva 
 |-  ( ph -> A. z e. ( A (,) X ) ( ( G ` X ) - ( G ` z ) ) =/= 0 )
227 226 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> A. z e. ( A (,) X ) ( ( G ` X ) - ( G ` z ) ) =/= 0 )
228 134 227 112 rspcdva 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( ( G ` X ) - ( G ` R ) ) =/= 0 )
229 126 131 228 divcld 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( ( ( F ` X ) - ( F ` R ) ) / ( ( G ` X ) - ( G ` R ) ) ) e. CC )
230 35 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> C e. CC )
231 229 230 subcld 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( ( ( ( F ` X ) - ( F ` R ) ) / ( ( G ` X ) - ( G ` R ) ) ) - C ) e. CC )
232 231 abscld 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( abs ` ( ( ( ( F ` X ) - ( F ` R ) ) / ( ( G ` X ) - ( G ` R ) ) ) - C ) ) e. RR )
233 38 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> E e. RR )
234 116 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> D e. RR* )
235 117 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> X < D )
236 iccssioo 
 |-  ( ( ( A e. RR* /\ D e. RR* ) /\ ( A < R /\ X < D ) ) -> ( R [,] X ) C_ ( A (,) D ) )
237 107 234 99 235 236 syl22anc 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( R [,] X ) C_ ( A (,) D ) )
238 20 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( A (,) D ) C_ ( A (,) B ) )
239 237 238 sstrd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( R [,] X ) C_ ( A (,) B ) )
240 fss 
 |-  ( ( F : ( A (,) B ) --> RR /\ RR C_ CC ) -> F : ( A (,) B ) --> CC )
241 4 159 240 sylancl 
 |-  ( ph -> F : ( A (,) B ) --> CC )
242 dvcn 
 |-  ( ( ( RR C_ CC /\ F : ( A (,) B ) --> CC /\ ( A (,) B ) C_ RR ) /\ dom ( RR _D F ) = ( A (,) B ) ) -> F e. ( ( A (,) B ) -cn-> CC ) )
243 160 241 163 6 242 syl31anc 
 |-  ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
244 cncffvrn 
 |-  ( ( RR C_ CC /\ F e. ( ( A (,) B ) -cn-> CC ) ) -> ( F e. ( ( A (,) B ) -cn-> RR ) <-> F : ( A (,) B ) --> RR ) )
245 159 243 244 sylancr 
 |-  ( ph -> ( F e. ( ( A (,) B ) -cn-> RR ) <-> F : ( A (,) B ) --> RR ) )
246 4 245 mpbird 
 |-  ( ph -> F e. ( ( A (,) B ) -cn-> RR ) )
247 246 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> F e. ( ( A (,) B ) -cn-> RR ) )
248 rescncf 
 |-  ( ( R [,] X ) C_ ( A (,) B ) -> ( F e. ( ( A (,) B ) -cn-> RR ) -> ( F |` ( R [,] X ) ) e. ( ( R [,] X ) -cn-> RR ) ) )
249 239 247 248 sylc 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( F |` ( R [,] X ) ) e. ( ( R [,] X ) -cn-> RR ) )
250 168 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> G e. ( ( A (,) B ) -cn-> RR ) )
251 rescncf 
 |-  ( ( R [,] X ) C_ ( A (,) B ) -> ( G e. ( ( A (,) B ) -cn-> RR ) -> ( G |` ( R [,] X ) ) e. ( ( R [,] X ) -cn-> RR ) ) )
252 239 250 251 sylc 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( G |` ( R [,] X ) ) e. ( ( R [,] X ) -cn-> RR ) )
253 159 a1i 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> RR C_ CC )
254 241 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> F : ( A (,) B ) --> CC )
255 142 a1i 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( A (,) B ) C_ RR )
256 iccssre 
 |-  ( ( R e. RR /\ X e. RR ) -> ( R [,] X ) C_ RR )
257 72 100 256 syl2anc 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( R [,] X ) C_ RR )
258 55 176 dvres 
 |-  ( ( ( RR C_ CC /\ F : ( A (,) B ) --> CC ) /\ ( ( A (,) B ) C_ RR /\ ( R [,] X ) C_ RR ) ) -> ( RR _D ( F |` ( R [,] X ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( R [,] X ) ) ) )
259 253 254 255 257 258 syl22anc 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( RR _D ( F |` ( R [,] X ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( R [,] X ) ) ) )
260 iccntr 
 |-  ( ( R e. RR /\ X e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( R [,] X ) ) = ( R (,) X ) )
261 72 100 260 syl2anc 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( R [,] X ) ) = ( R (,) X ) )
262 261 reseq2d 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( R [,] X ) ) ) = ( ( RR _D F ) |` ( R (,) X ) ) )
263 259 262 eqtrd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( RR _D ( F |` ( R [,] X ) ) ) = ( ( RR _D F ) |` ( R (,) X ) ) )
264 263 dmeqd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> dom ( RR _D ( F |` ( R [,] X ) ) ) = dom ( ( RR _D F ) |` ( R (,) X ) ) )
265 67 72 99 ltled 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> A <_ R )
266 iooss1 
 |-  ( ( A e. RR* /\ A <_ R ) -> ( R (,) X ) C_ ( A (,) X ) )
267 107 265 266 syl2anc 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( R (,) X ) C_ ( A (,) X ) )
268 118 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> X <_ D )
269 iooss2 
 |-  ( ( D e. RR* /\ X <_ D ) -> ( A (,) X ) C_ ( A (,) D ) )
270 234 268 269 syl2anc 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( A (,) X ) C_ ( A (,) D ) )
271 267 270 sstrd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( R (,) X ) C_ ( A (,) D ) )
272 271 238 sstrd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( R (,) X ) C_ ( A (,) B ) )
273 6 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> dom ( RR _D F ) = ( A (,) B ) )
274 272 273 sseqtrrd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( R (,) X ) C_ dom ( RR _D F ) )
275 ssdmres 
 |-  ( ( R (,) X ) C_ dom ( RR _D F ) <-> dom ( ( RR _D F ) |` ( R (,) X ) ) = ( R (,) X ) )
276 274 275 sylib 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> dom ( ( RR _D F ) |` ( R (,) X ) ) = ( R (,) X ) )
277 264 276 eqtrd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> dom ( RR _D ( F |` ( R [,] X ) ) ) = ( R (,) X ) )
278 162 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> G : ( A (,) B ) --> CC )
279 55 176 dvres 
 |-  ( ( ( RR C_ CC /\ G : ( A (,) B ) --> CC ) /\ ( ( A (,) B ) C_ RR /\ ( R [,] X ) C_ RR ) ) -> ( RR _D ( G |` ( R [,] X ) ) ) = ( ( RR _D G ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( R [,] X ) ) ) )
280 253 278 255 257 279 syl22anc 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( RR _D ( G |` ( R [,] X ) ) ) = ( ( RR _D G ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( R [,] X ) ) ) )
281 261 reseq2d 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( ( RR _D G ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( R [,] X ) ) ) = ( ( RR _D G ) |` ( R (,) X ) ) )
282 280 281 eqtrd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( RR _D ( G |` ( R [,] X ) ) ) = ( ( RR _D G ) |` ( R (,) X ) ) )
283 282 dmeqd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> dom ( RR _D ( G |` ( R [,] X ) ) ) = dom ( ( RR _D G ) |` ( R (,) X ) ) )
284 7 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> dom ( RR _D G ) = ( A (,) B ) )
285 272 284 sseqtrrd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( R (,) X ) C_ dom ( RR _D G ) )
286 ssdmres 
 |-  ( ( R (,) X ) C_ dom ( RR _D G ) <-> dom ( ( RR _D G ) |` ( R (,) X ) ) = ( R (,) X ) )
287 285 286 sylib 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> dom ( ( RR _D G ) |` ( R (,) X ) ) = ( R (,) X ) )
288 283 287 eqtrd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> dom ( RR _D ( G |` ( R [,] X ) ) ) = ( R (,) X ) )
289 72 100 106 249 252 277 288 cmvth 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> E. w e. ( R (,) X ) ( ( ( ( F |` ( R [,] X ) ) ` X ) - ( ( F |` ( R [,] X ) ) ` R ) ) x. ( ( RR _D ( G |` ( R [,] X ) ) ) ` w ) ) = ( ( ( ( G |` ( R [,] X ) ) ` X ) - ( ( G |` ( R [,] X ) ) ` R ) ) x. ( ( RR _D ( F |` ( R [,] X ) ) ) ` w ) ) )
290 72 rexrd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> R e. RR* )
291 290 adantr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> R e. RR* )
292 108 ad2antrr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> X e. RR* )
293 72 100 106 ltled 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> R <_ X )
294 293 adantr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> R <_ X )
295 ubicc2 
 |-  ( ( R e. RR* /\ X e. RR* /\ R <_ X ) -> X e. ( R [,] X ) )
296 291 292 294 295 syl3anc 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> X e. ( R [,] X ) )
297 296 fvresd 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( ( F |` ( R [,] X ) ) ` X ) = ( F ` X ) )
298 lbicc2 
 |-  ( ( R e. RR* /\ X e. RR* /\ R <_ X ) -> R e. ( R [,] X ) )
299 291 292 294 298 syl3anc 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> R e. ( R [,] X ) )
300 299 fvresd 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( ( F |` ( R [,] X ) ) ` R ) = ( F ` R ) )
301 297 300 oveq12d 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( ( ( F |` ( R [,] X ) ) ` X ) - ( ( F |` ( R [,] X ) ) ` R ) ) = ( ( F ` X ) - ( F ` R ) ) )
302 282 fveq1d 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( ( RR _D ( G |` ( R [,] X ) ) ) ` w ) = ( ( ( RR _D G ) |` ( R (,) X ) ) ` w ) )
303 fvres 
 |-  ( w e. ( R (,) X ) -> ( ( ( RR _D G ) |` ( R (,) X ) ) ` w ) = ( ( RR _D G ) ` w ) )
304 302 303 sylan9eq 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( ( RR _D ( G |` ( R [,] X ) ) ) ` w ) = ( ( RR _D G ) ` w ) )
305 301 304 oveq12d 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( ( ( ( F |` ( R [,] X ) ) ` X ) - ( ( F |` ( R [,] X ) ) ` R ) ) x. ( ( RR _D ( G |` ( R [,] X ) ) ) ` w ) ) = ( ( ( F ` X ) - ( F ` R ) ) x. ( ( RR _D G ) ` w ) ) )
306 296 fvresd 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( ( G |` ( R [,] X ) ) ` X ) = ( G ` X ) )
307 299 fvresd 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( ( G |` ( R [,] X ) ) ` R ) = ( G ` R ) )
308 306 307 oveq12d 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( ( ( G |` ( R [,] X ) ) ` X ) - ( ( G |` ( R [,] X ) ) ` R ) ) = ( ( G ` X ) - ( G ` R ) ) )
309 263 fveq1d 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( ( RR _D ( F |` ( R [,] X ) ) ) ` w ) = ( ( ( RR _D F ) |` ( R (,) X ) ) ` w ) )
310 fvres 
 |-  ( w e. ( R (,) X ) -> ( ( ( RR _D F ) |` ( R (,) X ) ) ` w ) = ( ( RR _D F ) ` w ) )
311 309 310 sylan9eq 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( ( RR _D ( F |` ( R [,] X ) ) ) ` w ) = ( ( RR _D F ) ` w ) )
312 308 311 oveq12d 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( ( ( ( G |` ( R [,] X ) ) ` X ) - ( ( G |` ( R [,] X ) ) ` R ) ) x. ( ( RR _D ( F |` ( R [,] X ) ) ) ` w ) ) = ( ( ( G ` X ) - ( G ` R ) ) x. ( ( RR _D F ) ` w ) ) )
313 131 adantr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( ( G ` X ) - ( G ` R ) ) e. CC )
314 dvf 
 |-  ( RR _D F ) : dom ( RR _D F ) --> CC
315 6 feq2d 
 |-  ( ph -> ( ( RR _D F ) : dom ( RR _D F ) --> CC <-> ( RR _D F ) : ( A (,) B ) --> CC ) )
316 314 315 mpbii 
 |-  ( ph -> ( RR _D F ) : ( A (,) B ) --> CC )
317 316 ad2antrr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( RR _D F ) : ( A (,) B ) --> CC )
318 272 sselda 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> w e. ( A (,) B ) )
319 317 318 ffvelrnd 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( ( RR _D F ) ` w ) e. CC )
320 313 319 mulcomd 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( ( ( G ` X ) - ( G ` R ) ) x. ( ( RR _D F ) ` w ) ) = ( ( ( RR _D F ) ` w ) x. ( ( G ` X ) - ( G ` R ) ) ) )
321 312 320 eqtrd 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( ( ( ( G |` ( R [,] X ) ) ` X ) - ( ( G |` ( R [,] X ) ) ` R ) ) x. ( ( RR _D ( F |` ( R [,] X ) ) ) ` w ) ) = ( ( ( RR _D F ) ` w ) x. ( ( G ` X ) - ( G ` R ) ) ) )
322 305 321 eqeq12d 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( ( ( ( ( F |` ( R [,] X ) ) ` X ) - ( ( F |` ( R [,] X ) ) ` R ) ) x. ( ( RR _D ( G |` ( R [,] X ) ) ) ` w ) ) = ( ( ( ( G |` ( R [,] X ) ) ` X ) - ( ( G |` ( R [,] X ) ) ` R ) ) x. ( ( RR _D ( F |` ( R [,] X ) ) ) ` w ) ) <-> ( ( ( F ` X ) - ( F ` R ) ) x. ( ( RR _D G ) ` w ) ) = ( ( ( RR _D F ) ` w ) x. ( ( G ` X ) - ( G ` R ) ) ) ) )
323 126 adantr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( ( F ` X ) - ( F ` R ) ) e. CC )
324 210 ad2antrr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( RR _D G ) : ( A (,) B ) --> CC )
325 324 318 ffvelrnd 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( ( RR _D G ) ` w ) e. CC )
326 228 adantr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( ( G ` X ) - ( G ` R ) ) =/= 0 )
327 11 ad2antrr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> -. 0 e. ran ( RR _D G ) )
328 324 ffnd 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( RR _D G ) Fn ( A (,) B ) )
329 328 318 215 syl2anc 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( ( RR _D G ) ` w ) e. ran ( RR _D G ) )
330 eleq1 
 |-  ( ( ( RR _D G ) ` w ) = 0 -> ( ( ( RR _D G ) ` w ) e. ran ( RR _D G ) <-> 0 e. ran ( RR _D G ) ) )
331 329 330 syl5ibcom 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( ( ( RR _D G ) ` w ) = 0 -> 0 e. ran ( RR _D G ) ) )
332 331 necon3bd 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( -. 0 e. ran ( RR _D G ) -> ( ( RR _D G ) ` w ) =/= 0 ) )
333 327 332 mpd 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( ( RR _D G ) ` w ) =/= 0 )
334 323 313 319 325 326 333 divmuleqd 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( ( ( ( F ` X ) - ( F ` R ) ) / ( ( G ` X ) - ( G ` R ) ) ) = ( ( ( RR _D F ) ` w ) / ( ( RR _D G ) ` w ) ) <-> ( ( ( F ` X ) - ( F ` R ) ) x. ( ( RR _D G ) ` w ) ) = ( ( ( RR _D F ) ` w ) x. ( ( G ` X ) - ( G ` R ) ) ) ) )
335 322 334 bitr4d 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( ( ( ( ( F |` ( R [,] X ) ) ` X ) - ( ( F |` ( R [,] X ) ) ` R ) ) x. ( ( RR _D ( G |` ( R [,] X ) ) ) ` w ) ) = ( ( ( ( G |` ( R [,] X ) ) ` X ) - ( ( G |` ( R [,] X ) ) ` R ) ) x. ( ( RR _D ( F |` ( R [,] X ) ) ) ` w ) ) <-> ( ( ( F ` X ) - ( F ` R ) ) / ( ( G ` X ) - ( G ` R ) ) ) = ( ( ( RR _D F ) ` w ) / ( ( RR _D G ) ` w ) ) ) )
336 335 rexbidva 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( E. w e. ( R (,) X ) ( ( ( ( F |` ( R [,] X ) ) ` X ) - ( ( F |` ( R [,] X ) ) ` R ) ) x. ( ( RR _D ( G |` ( R [,] X ) ) ) ` w ) ) = ( ( ( ( G |` ( R [,] X ) ) ` X ) - ( ( G |` ( R [,] X ) ) ` R ) ) x. ( ( RR _D ( F |` ( R [,] X ) ) ) ` w ) ) <-> E. w e. ( R (,) X ) ( ( ( F ` X ) - ( F ` R ) ) / ( ( G ` X ) - ( G ` R ) ) ) = ( ( ( RR _D F ) ` w ) / ( ( RR _D G ) ` w ) ) ) )
337 289 336 mpbid 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> E. w e. ( R (,) X ) ( ( ( F ` X ) - ( F ` R ) ) / ( ( G ` X ) - ( G ` R ) ) ) = ( ( ( RR _D F ) ` w ) / ( ( RR _D G ) ` w ) ) )
338 fveq2 
 |-  ( t = w -> ( ( RR _D F ) ` t ) = ( ( RR _D F ) ` w ) )
339 fveq2 
 |-  ( t = w -> ( ( RR _D G ) ` t ) = ( ( RR _D G ) ` w ) )
340 338 339 oveq12d 
 |-  ( t = w -> ( ( ( RR _D F ) ` t ) / ( ( RR _D G ) ` t ) ) = ( ( ( RR _D F ) ` w ) / ( ( RR _D G ) ` w ) ) )
341 340 fvoveq1d 
 |-  ( t = w -> ( abs ` ( ( ( ( RR _D F ) ` t ) / ( ( RR _D G ) ` t ) ) - C ) ) = ( abs ` ( ( ( ( RR _D F ) ` w ) / ( ( RR _D G ) ` w ) ) - C ) ) )
342 341 breq1d 
 |-  ( t = w -> ( ( abs ` ( ( ( ( RR _D F ) ` t ) / ( ( RR _D G ) ` t ) ) - C ) ) < E <-> ( abs ` ( ( ( ( RR _D F ) ` w ) / ( ( RR _D G ) ` w ) ) - C ) ) < E ) )
343 17 ad2antrr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> A. t e. ( A (,) D ) ( abs ` ( ( ( ( RR _D F ) ` t ) / ( ( RR _D G ) ` t ) ) - C ) ) < E )
344 271 sselda 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> w e. ( A (,) D ) )
345 342 343 344 rspcdva 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( abs ` ( ( ( ( RR _D F ) ` w ) / ( ( RR _D G ) ` w ) ) - C ) ) < E )
346 fvoveq1 
 |-  ( ( ( ( F ` X ) - ( F ` R ) ) / ( ( G ` X ) - ( G ` R ) ) ) = ( ( ( RR _D F ) ` w ) / ( ( RR _D G ) ` w ) ) -> ( abs ` ( ( ( ( F ` X ) - ( F ` R ) ) / ( ( G ` X ) - ( G ` R ) ) ) - C ) ) = ( abs ` ( ( ( ( RR _D F ) ` w ) / ( ( RR _D G ) ` w ) ) - C ) ) )
347 346 breq1d 
 |-  ( ( ( ( F ` X ) - ( F ` R ) ) / ( ( G ` X ) - ( G ` R ) ) ) = ( ( ( RR _D F ) ` w ) / ( ( RR _D G ) ` w ) ) -> ( ( abs ` ( ( ( ( F ` X ) - ( F ` R ) ) / ( ( G ` X ) - ( G ` R ) ) ) - C ) ) < E <-> ( abs ` ( ( ( ( RR _D F ) ` w ) / ( ( RR _D G ) ` w ) ) - C ) ) < E ) )
348 345 347 syl5ibrcom 
 |-  ( ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) /\ w e. ( R (,) X ) ) -> ( ( ( ( F ` X ) - ( F ` R ) ) / ( ( G ` X ) - ( G ` R ) ) ) = ( ( ( RR _D F ) ` w ) / ( ( RR _D G ) ` w ) ) -> ( abs ` ( ( ( ( F ` X ) - ( F ` R ) ) / ( ( G ` X ) - ( G ` R ) ) ) - C ) ) < E ) )
349 348 rexlimdva 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( E. w e. ( R (,) X ) ( ( ( F ` X ) - ( F ` R ) ) / ( ( G ` X ) - ( G ` R ) ) ) = ( ( ( RR _D F ) ` w ) / ( ( RR _D G ) ` w ) ) -> ( abs ` ( ( ( ( F ` X ) - ( F ` R ) ) / ( ( G ` X ) - ( G ` R ) ) ) - C ) ) < E ) )
350 337 349 mpd 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( abs ` ( ( ( ( F ` X ) - ( F ` R ) ) / ( ( G ` X ) - ( G ` R ) ) ) - C ) ) < E )
351 232 233 350 ltled 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( abs ` ( ( ( ( F ` X ) - ( F ` R ) ) / ( ( G ` X ) - ( G ` R ) ) ) - C ) ) <_ E )
352 fveq2 
 |-  ( u = R -> ( F ` u ) = ( F ` R ) )
353 352 oveq2d 
 |-  ( u = R -> ( ( F ` X ) - ( F ` u ) ) = ( ( F ` X ) - ( F ` R ) ) )
354 fveq2 
 |-  ( u = R -> ( G ` u ) = ( G ` R ) )
355 354 oveq2d 
 |-  ( u = R -> ( ( G ` X ) - ( G ` u ) ) = ( ( G ` X ) - ( G ` R ) ) )
356 353 355 oveq12d 
 |-  ( u = R -> ( ( ( F ` X ) - ( F ` u ) ) / ( ( G ` X ) - ( G ` u ) ) ) = ( ( ( F ` X ) - ( F ` R ) ) / ( ( G ` X ) - ( G ` R ) ) ) )
357 356 fvoveq1d 
 |-  ( u = R -> ( abs ` ( ( ( ( F ` X ) - ( F ` u ) ) / ( ( G ` X ) - ( G ` u ) ) ) - C ) ) = ( abs ` ( ( ( ( F ` X ) - ( F ` R ) ) / ( ( G ` X ) - ( G ` R ) ) ) - C ) ) )
358 357 breq1d 
 |-  ( u = R -> ( ( abs ` ( ( ( ( F ` X ) - ( F ` u ) ) / ( ( G ` X ) - ( G ` u ) ) ) - C ) ) <_ E <-> ( abs ` ( ( ( ( F ` X ) - ( F ` R ) ) / ( ( G ` X ) - ( G ` R ) ) ) - C ) ) <_ E ) )
359 358 rspcev 
 |-  ( ( R e. ( ( A ( ball ` ( abs o. - ) ) r ) i^i ( A (,) X ) ) /\ ( abs ` ( ( ( ( F ` X ) - ( F ` R ) ) / ( ( G ` X ) - ( G ` R ) ) ) - C ) ) <_ E ) -> E. u e. ( ( A ( ball ` ( abs o. - ) ) r ) i^i ( A (,) X ) ) ( abs ` ( ( ( ( F ` X ) - ( F ` u ) ) / ( ( G ` X ) - ( G ` u ) ) ) - C ) ) <_ E )
360 113 351 359 syl2anc 
 |-  ( ( ph /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> E. u e. ( ( A ( ball ` ( abs o. - ) ) r ) i^i ( A (,) X ) ) ( abs ` ( ( ( ( F ` X ) - ( F ` u ) ) / ( ( G ` X ) - ( G ` u ) ) ) - C ) ) <_ E )
361 360 adantlr 
 |-  ( ( ( ph /\ ( v e. ( TopOpen ` CCfld ) /\ A e. v ) ) /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> E. u e. ( ( A ( ball ` ( abs o. - ) ) r ) i^i ( A (,) X ) ) ( abs ` ( ( ( ( F ` X ) - ( F ` u ) ) / ( ( G ` X ) - ( G ` u ) ) ) - C ) ) <_ E )
362 ssrexv 
 |-  ( ( ( A ( ball ` ( abs o. - ) ) r ) i^i ( A (,) X ) ) C_ ( v i^i ( ( A (,) X ) \ { A } ) ) -> ( E. u e. ( ( A ( ball ` ( abs o. - ) ) r ) i^i ( A (,) X ) ) ( abs ` ( ( ( ( F ` X ) - ( F ` u ) ) / ( ( G ` X ) - ( G ` u ) ) ) - C ) ) <_ E -> E. u e. ( v i^i ( ( A (,) X ) \ { A } ) ) ( abs ` ( ( ( ( F ` X ) - ( F ` u ) ) / ( ( G ` X ) - ( G ` u ) ) ) - C ) ) <_ E ) )
363 66 361 362 syl2imc 
 |-  ( ( ( ph /\ ( v e. ( TopOpen ` CCfld ) /\ A e. v ) ) /\ ( r e. RR+ /\ r < ( X - A ) ) ) -> ( ( A ( ball ` ( abs o. - ) ) r ) C_ v -> E. u e. ( v i^i ( ( A (,) X ) \ { A } ) ) ( abs ` ( ( ( ( F ` X ) - ( F ` u ) ) / ( ( G ` X ) - ( G ` u ) ) ) - C ) ) <_ E ) )
364 363 anassrs 
 |-  ( ( ( ( ph /\ ( v e. ( TopOpen ` CCfld ) /\ A e. v ) ) /\ r e. RR+ ) /\ r < ( X - A ) ) -> ( ( A ( ball ` ( abs o. - ) ) r ) C_ v -> E. u e. ( v i^i ( ( A (,) X ) \ { A } ) ) ( abs ` ( ( ( ( F ` X ) - ( F ` u ) ) / ( ( G ` X ) - ( G ` u ) ) ) - C ) ) <_ E ) )
365 364 expimpd 
 |-  ( ( ( ph /\ ( v e. ( TopOpen ` CCfld ) /\ A e. v ) ) /\ r e. RR+ ) -> ( ( r < ( X - A ) /\ ( A ( ball ` ( abs o. - ) ) r ) C_ v ) -> E. u e. ( v i^i ( ( A (,) X ) \ { A } ) ) ( abs ` ( ( ( ( F ` X ) - ( F ` u ) ) / ( ( G ` X ) - ( G ` u ) ) ) - C ) ) <_ E ) )
366 365 rexlimdva 
 |-  ( ( ph /\ ( v e. ( TopOpen ` CCfld ) /\ A e. v ) ) -> ( E. r e. RR+ ( r < ( X - A ) /\ ( A ( ball ` ( abs o. - ) ) r ) C_ v ) -> E. u e. ( v i^i ( ( A (,) X ) \ { A } ) ) ( abs ` ( ( ( ( F ` X ) - ( F ` u ) ) / ( ( G ` X ) - ( G ` u ) ) ) - C ) ) <_ E ) )
367 58 366 mpd 
 |-  ( ( ph /\ ( v e. ( TopOpen ` CCfld ) /\ A e. v ) ) -> E. u e. ( v i^i ( ( A (,) X ) \ { A } ) ) ( abs ` ( ( ( ( F ` X ) - ( F ` u ) ) / ( ( G ` X ) - ( G ` u ) ) ) - C ) ) <_ E )
368 inss2 
 |-  ( v i^i ( ( A (,) X ) \ { A } ) ) C_ ( ( A (,) X ) \ { A } )
369 difss 
 |-  ( ( A (,) X ) \ { A } ) C_ ( A (,) X )
370 368 369 sstri 
 |-  ( v i^i ( ( A (,) X ) \ { A } ) ) C_ ( A (,) X )
371 370 sseli 
 |-  ( u e. ( v i^i ( ( A (,) X ) \ { A } ) ) -> u e. ( A (,) X ) )
372 fveq2 
 |-  ( z = u -> ( F ` z ) = ( F ` u ) )
373 372 oveq2d 
 |-  ( z = u -> ( ( F ` X ) - ( F ` z ) ) = ( ( F ` X ) - ( F ` u ) ) )
374 fveq2 
 |-  ( z = u -> ( G ` z ) = ( G ` u ) )
375 374 oveq2d 
 |-  ( z = u -> ( ( G ` X ) - ( G ` z ) ) = ( ( G ` X ) - ( G ` u ) ) )
376 373 375 oveq12d 
 |-  ( z = u -> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) = ( ( ( F ` X ) - ( F ` u ) ) / ( ( G ` X ) - ( G ` u ) ) ) )
377 eqid 
 |-  ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) = ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) )
378 ovex 
 |-  ( ( ( F ` X ) - ( F ` u ) ) / ( ( G ` X ) - ( G ` u ) ) ) e. _V
379 376 377 378 fvmpt 
 |-  ( u e. ( A (,) X ) -> ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) ` u ) = ( ( ( F ` X ) - ( F ` u ) ) / ( ( G ` X ) - ( G ` u ) ) ) )
380 379 fvoveq1d 
 |-  ( u e. ( A (,) X ) -> ( abs ` ( ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) ` u ) - C ) ) = ( abs ` ( ( ( ( F ` X ) - ( F ` u ) ) / ( ( G ` X ) - ( G ` u ) ) ) - C ) ) )
381 380 breq1d 
 |-  ( u e. ( A (,) X ) -> ( ( abs ` ( ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) ` u ) - C ) ) <_ E <-> ( abs ` ( ( ( ( F ` X ) - ( F ` u ) ) / ( ( G ` X ) - ( G ` u ) ) ) - C ) ) <_ E ) )
382 371 381 syl 
 |-  ( u e. ( v i^i ( ( A (,) X ) \ { A } ) ) -> ( ( abs ` ( ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) ` u ) - C ) ) <_ E <-> ( abs ` ( ( ( ( F ` X ) - ( F ` u ) ) / ( ( G ` X ) - ( G ` u ) ) ) - C ) ) <_ E ) )
383 382 rexbiia 
 |-  ( E. u e. ( v i^i ( ( A (,) X ) \ { A } ) ) ( abs ` ( ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) ` u ) - C ) ) <_ E <-> E. u e. ( v i^i ( ( A (,) X ) \ { A } ) ) ( abs ` ( ( ( ( F ` X ) - ( F ` u ) ) / ( ( G ` X ) - ( G ` u ) ) ) - C ) ) <_ E )
384 367 383 sylibr 
 |-  ( ( ph /\ ( v e. ( TopOpen ` CCfld ) /\ A e. v ) ) -> E. u e. ( v i^i ( ( A (,) X ) \ { A } ) ) ( abs ` ( ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) ` u ) - C ) ) <_ E )
385 ovex 
 |-  ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) e. _V
386 385 377 fnmpti 
 |-  ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) Fn ( A (,) X )
387 fvoveq1 
 |-  ( x = ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) ` u ) -> ( abs ` ( x - C ) ) = ( abs ` ( ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) ` u ) - C ) ) )
388 387 breq1d 
 |-  ( x = ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) ` u ) -> ( ( abs ` ( x - C ) ) <_ E <-> ( abs ` ( ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) ` u ) - C ) ) <_ E ) )
389 388 rexima 
 |-  ( ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) Fn ( A (,) X ) /\ ( v i^i ( ( A (,) X ) \ { A } ) ) C_ ( A (,) X ) ) -> ( E. x e. ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) ( abs ` ( x - C ) ) <_ E <-> E. u e. ( v i^i ( ( A (,) X ) \ { A } ) ) ( abs ` ( ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) ` u ) - C ) ) <_ E ) )
390 386 370 389 mp2an 
 |-  ( E. x e. ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) ( abs ` ( x - C ) ) <_ E <-> E. u e. ( v i^i ( ( A (,) X ) \ { A } ) ) ( abs ` ( ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) ` u ) - C ) ) <_ E )
391 384 390 sylibr 
 |-  ( ( ph /\ ( v e. ( TopOpen ` CCfld ) /\ A e. v ) ) -> E. x e. ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) ( abs ` ( x - C ) ) <_ E )
392 dfrex2 
 |-  ( E. x e. ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) ( abs ` ( x - C ) ) <_ E <-> -. A. x e. ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) -. ( abs ` ( x - C ) ) <_ E )
393 391 392 sylib 
 |-  ( ( ph /\ ( v e. ( TopOpen ` CCfld ) /\ A e. v ) ) -> -. A. x e. ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) -. ( abs ` ( x - C ) ) <_ E )
394 ssrab 
 |-  ( ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) C_ { x e. CC | -. ( abs ` ( x - C ) ) <_ E } <-> ( ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) C_ CC /\ A. x e. ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) -. ( abs ` ( x - C ) ) <_ E ) )
395 394 simprbi 
 |-  ( ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) C_ { x e. CC | -. ( abs ` ( x - C ) ) <_ E } -> A. x e. ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) -. ( abs ` ( x - C ) ) <_ E )
396 393 395 nsyl 
 |-  ( ( ph /\ ( v e. ( TopOpen ` CCfld ) /\ A e. v ) ) -> -. ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) C_ { x e. CC | -. ( abs ` ( x - C ) ) <_ E } )
397 396 expr 
 |-  ( ( ph /\ v e. ( TopOpen ` CCfld ) ) -> ( A e. v -> -. ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) C_ { x e. CC | -. ( abs ` ( x - C ) ) <_ E } ) )
398 397 ralrimiva 
 |-  ( ph -> A. v e. ( TopOpen ` CCfld ) ( A e. v -> -. ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) C_ { x e. CC | -. ( abs ` ( x - C ) ) <_ E } ) )
399 ralinexa 
 |-  ( A. v e. ( TopOpen ` CCfld ) ( A e. v -> -. ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) C_ { x e. CC | -. ( abs ` ( x - C ) ) <_ E } ) <-> -. E. v e. ( TopOpen ` CCfld ) ( A e. v /\ ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) C_ { x e. CC | -. ( abs ` ( x - C ) ) <_ E } ) )
400 398 399 sylib 
 |-  ( ph -> -. E. v e. ( TopOpen ` CCfld ) ( A e. v /\ ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) C_ { x e. CC | -. ( abs ` ( x - C ) ) <_ E } ) )
401 fvoveq1 
 |-  ( x = ( ( F ` X ) / ( G ` X ) ) -> ( abs ` ( x - C ) ) = ( abs ` ( ( ( F ` X ) / ( G ` X ) ) - C ) ) )
402 401 breq1d 
 |-  ( x = ( ( F ` X ) / ( G ` X ) ) -> ( ( abs ` ( x - C ) ) <_ E <-> ( abs ` ( ( ( F ` X ) / ( G ` X ) ) - C ) ) <_ E ) )
403 402 notbid 
 |-  ( x = ( ( F ` X ) / ( G ` X ) ) -> ( -. ( abs ` ( x - C ) ) <_ E <-> -. ( abs ` ( ( ( F ` X ) / ( G ` X ) ) - C ) ) <_ E ) )
404 403 elrab3 
 |-  ( ( ( F ` X ) / ( G ` X ) ) e. CC -> ( ( ( F ` X ) / ( G ` X ) ) e. { x e. CC | -. ( abs ` ( x - C ) ) <_ E } <-> -. ( abs ` ( ( ( F ` X ) / ( G ` X ) ) - C ) ) <_ E ) )
405 33 404 syl 
 |-  ( ph -> ( ( ( F ` X ) / ( G ` X ) ) e. { x e. CC | -. ( abs ` ( x - C ) ) <_ E } <-> -. ( abs ` ( ( ( F ` X ) / ( G ` X ) ) - C ) ) <_ E ) )
406 eleq2 
 |-  ( u = { x e. CC | -. ( abs ` ( x - C ) ) <_ E } -> ( ( ( F ` X ) / ( G ` X ) ) e. u <-> ( ( F ` X ) / ( G ` X ) ) e. { x e. CC | -. ( abs ` ( x - C ) ) <_ E } ) )
407 sseq2 
 |-  ( u = { x e. CC | -. ( abs ` ( x - C ) ) <_ E } -> ( ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) C_ u <-> ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) C_ { x e. CC | -. ( abs ` ( x - C ) ) <_ E } ) )
408 407 anbi2d 
 |-  ( u = { x e. CC | -. ( abs ` ( x - C ) ) <_ E } -> ( ( A e. v /\ ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) C_ u ) <-> ( A e. v /\ ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) C_ { x e. CC | -. ( abs ` ( x - C ) ) <_ E } ) ) )
409 408 rexbidv 
 |-  ( u = { x e. CC | -. ( abs ` ( x - C ) ) <_ E } -> ( E. v e. ( TopOpen ` CCfld ) ( A e. v /\ ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) C_ u ) <-> E. v e. ( TopOpen ` CCfld ) ( A e. v /\ ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) C_ { x e. CC | -. ( abs ` ( x - C ) ) <_ E } ) ) )
410 406 409 imbi12d 
 |-  ( u = { x e. CC | -. ( abs ` ( x - C ) ) <_ E } -> ( ( ( ( F ` X ) / ( G ` X ) ) e. u -> E. v e. ( TopOpen ` CCfld ) ( A e. v /\ ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) C_ u ) ) <-> ( ( ( F ` X ) / ( G ` X ) ) e. { x e. CC | -. ( abs ` ( x - C ) ) <_ E } -> E. v e. ( TopOpen ` CCfld ) ( A e. v /\ ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) C_ { x e. CC | -. ( abs ` ( x - C ) ) <_ E } ) ) ) )
411 23 adantr 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> ( F ` X ) e. CC )
412 4 ffvelrnda 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( F ` z ) e. RR )
413 137 412 syldan 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> ( F ` z ) e. RR )
414 413 recnd 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> ( F ` z ) e. CC )
415 411 414 subcld 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> ( ( F ` X ) - ( F ` z ) ) e. CC )
416 136 140 subcld 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> ( ( G ` X ) - ( G ` z ) ) e. CC )
417 eldifsn 
 |-  ( ( ( G ` X ) - ( G ` z ) ) e. ( CC \ { 0 } ) <-> ( ( ( G ` X ) - ( G ` z ) ) e. CC /\ ( ( G ` X ) - ( G ` z ) ) =/= 0 ) )
418 416 225 417 sylanbrc 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> ( ( G ` X ) - ( G ` z ) ) e. ( CC \ { 0 } ) )
419 ssidd 
 |-  ( ph -> CC C_ CC )
420 difss 
 |-  ( CC \ { 0 } ) C_ CC
421 420 a1i 
 |-  ( ph -> ( CC \ { 0 } ) C_ CC )
422 55 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
423 cnex 
 |-  CC e. _V
424 423 difexi 
 |-  ( CC \ { 0 } ) e. _V
425 txrest 
 |-  ( ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) /\ ( CC e. _V /\ ( CC \ { 0 } ) e. _V ) ) -> ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) |`t ( CC X. ( CC \ { 0 } ) ) ) = ( ( ( TopOpen ` CCfld ) |`t CC ) tX ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) ) )
426 422 422 423 424 425 mp4an 
 |-  ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) |`t ( CC X. ( CC \ { 0 } ) ) ) = ( ( ( TopOpen ` CCfld ) |`t CC ) tX ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) )
427 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
428 427 restid 
 |-  ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) -> ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld ) )
429 422 428 ax-mp 
 |-  ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld )
430 429 oveq1i 
 |-  ( ( ( TopOpen ` CCfld ) |`t CC ) tX ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) ) = ( ( TopOpen ` CCfld ) tX ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) )
431 426 430 eqtr2i 
 |-  ( ( TopOpen ` CCfld ) tX ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) ) = ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) |`t ( CC X. ( CC \ { 0 } ) ) )
432 23 subid1d 
 |-  ( ph -> ( ( F ` X ) - 0 ) = ( F ` X ) )
433 txtopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) -> ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) e. ( TopOn ` ( CC X. CC ) ) )
434 422 422 433 mp2an 
 |-  ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) e. ( TopOn ` ( CC X. CC ) )
435 434 toponrestid 
 |-  ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) = ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) |`t ( CC X. CC ) )
436 limcresi 
 |-  ( ( z e. RR |-> ( F ` X ) ) limCC A ) C_ ( ( ( z e. RR |-> ( F ` X ) ) |` ( A (,) X ) ) limCC A )
437 ioossre 
 |-  ( A (,) X ) C_ RR
438 resmpt 
 |-  ( ( A (,) X ) C_ RR -> ( ( z e. RR |-> ( F ` X ) ) |` ( A (,) X ) ) = ( z e. ( A (,) X ) |-> ( F ` X ) ) )
439 437 438 ax-mp 
 |-  ( ( z e. RR |-> ( F ` X ) ) |` ( A (,) X ) ) = ( z e. ( A (,) X ) |-> ( F ` X ) )
440 439 oveq1i 
 |-  ( ( ( z e. RR |-> ( F ` X ) ) |` ( A (,) X ) ) limCC A ) = ( ( z e. ( A (,) X ) |-> ( F ` X ) ) limCC A )
441 436 440 sseqtri 
 |-  ( ( z e. RR |-> ( F ` X ) ) limCC A ) C_ ( ( z e. ( A (,) X ) |-> ( F ` X ) ) limCC A )
442 cncfmptc 
 |-  ( ( ( F ` X ) e. RR /\ RR C_ CC /\ RR C_ CC ) -> ( z e. RR |-> ( F ` X ) ) e. ( RR -cn-> RR ) )
443 22 160 160 442 syl3anc 
 |-  ( ph -> ( z e. RR |-> ( F ` X ) ) e. ( RR -cn-> RR ) )
444 eqidd 
 |-  ( z = A -> ( F ` X ) = ( F ` X ) )
445 443 1 444 cnmptlimc 
 |-  ( ph -> ( F ` X ) e. ( ( z e. RR |-> ( F ` X ) ) limCC A ) )
446 441 445 sseldi 
 |-  ( ph -> ( F ` X ) e. ( ( z e. ( A (,) X ) |-> ( F ` X ) ) limCC A ) )
447 limcresi 
 |-  ( F limCC A ) C_ ( ( F |` ( A (,) X ) ) limCC A )
448 4 121 feqresmpt 
 |-  ( ph -> ( F |` ( A (,) X ) ) = ( z e. ( A (,) X ) |-> ( F ` z ) ) )
449 448 oveq1d 
 |-  ( ph -> ( ( F |` ( A (,) X ) ) limCC A ) = ( ( z e. ( A (,) X ) |-> ( F ` z ) ) limCC A ) )
450 447 449 sseqtrid 
 |-  ( ph -> ( F limCC A ) C_ ( ( z e. ( A (,) X ) |-> ( F ` z ) ) limCC A ) )
451 450 8 sseldd 
 |-  ( ph -> 0 e. ( ( z e. ( A (,) X ) |-> ( F ` z ) ) limCC A ) )
452 55 subcn 
 |-  - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
453 0cn 
 |-  0 e. CC
454 opelxpi 
 |-  ( ( ( F ` X ) e. CC /\ 0 e. CC ) -> <. ( F ` X ) , 0 >. e. ( CC X. CC ) )
455 23 453 454 sylancl 
 |-  ( ph -> <. ( F ` X ) , 0 >. e. ( CC X. CC ) )
456 434 toponunii 
 |-  ( CC X. CC ) = U. ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) )
457 456 cncnpi 
 |-  ( ( - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) /\ <. ( F ` X ) , 0 >. e. ( CC X. CC ) ) -> - e. ( ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) CnP ( TopOpen ` CCfld ) ) ` <. ( F ` X ) , 0 >. ) )
458 452 455 457 sylancr 
 |-  ( ph -> - e. ( ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) CnP ( TopOpen ` CCfld ) ) ` <. ( F ` X ) , 0 >. ) )
459 411 414 419 419 55 435 446 451 458 limccnp2 
 |-  ( ph -> ( ( F ` X ) - 0 ) e. ( ( z e. ( A (,) X ) |-> ( ( F ` X ) - ( F ` z ) ) ) limCC A ) )
460 432 459 eqeltrrd 
 |-  ( ph -> ( F ` X ) e. ( ( z e. ( A (,) X ) |-> ( ( F ` X ) - ( F ` z ) ) ) limCC A ) )
461 25 subid1d 
 |-  ( ph -> ( ( G ` X ) - 0 ) = ( G ` X ) )
462 limcresi 
 |-  ( ( z e. RR |-> ( G ` X ) ) limCC A ) C_ ( ( ( z e. RR |-> ( G ` X ) ) |` ( A (,) X ) ) limCC A )
463 resmpt 
 |-  ( ( A (,) X ) C_ RR -> ( ( z e. RR |-> ( G ` X ) ) |` ( A (,) X ) ) = ( z e. ( A (,) X ) |-> ( G ` X ) ) )
464 437 463 ax-mp 
 |-  ( ( z e. RR |-> ( G ` X ) ) |` ( A (,) X ) ) = ( z e. ( A (,) X ) |-> ( G ` X ) )
465 464 oveq1i 
 |-  ( ( ( z e. RR |-> ( G ` X ) ) |` ( A (,) X ) ) limCC A ) = ( ( z e. ( A (,) X ) |-> ( G ` X ) ) limCC A )
466 462 465 sseqtri 
 |-  ( ( z e. RR |-> ( G ` X ) ) limCC A ) C_ ( ( z e. ( A (,) X ) |-> ( G ` X ) ) limCC A )
467 cncfmptc 
 |-  ( ( ( G ` X ) e. RR /\ RR C_ CC /\ RR C_ CC ) -> ( z e. RR |-> ( G ` X ) ) e. ( RR -cn-> RR ) )
468 24 160 160 467 syl3anc 
 |-  ( ph -> ( z e. RR |-> ( G ` X ) ) e. ( RR -cn-> RR ) )
469 eqidd 
 |-  ( z = A -> ( G ` X ) = ( G ` X ) )
470 468 1 469 cnmptlimc 
 |-  ( ph -> ( G ` X ) e. ( ( z e. RR |-> ( G ` X ) ) limCC A ) )
471 466 470 sseldi 
 |-  ( ph -> ( G ` X ) e. ( ( z e. ( A (,) X ) |-> ( G ` X ) ) limCC A ) )
472 limcresi 
 |-  ( G limCC A ) C_ ( ( G |` ( A (,) X ) ) limCC A )
473 5 121 feqresmpt 
 |-  ( ph -> ( G |` ( A (,) X ) ) = ( z e. ( A (,) X ) |-> ( G ` z ) ) )
474 473 oveq1d 
 |-  ( ph -> ( ( G |` ( A (,) X ) ) limCC A ) = ( ( z e. ( A (,) X ) |-> ( G ` z ) ) limCC A ) )
475 472 474 sseqtrid 
 |-  ( ph -> ( G limCC A ) C_ ( ( z e. ( A (,) X ) |-> ( G ` z ) ) limCC A ) )
476 475 9 sseldd 
 |-  ( ph -> 0 e. ( ( z e. ( A (,) X ) |-> ( G ` z ) ) limCC A ) )
477 opelxpi 
 |-  ( ( ( G ` X ) e. CC /\ 0 e. CC ) -> <. ( G ` X ) , 0 >. e. ( CC X. CC ) )
478 25 453 477 sylancl 
 |-  ( ph -> <. ( G ` X ) , 0 >. e. ( CC X. CC ) )
479 456 cncnpi 
 |-  ( ( - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) /\ <. ( G ` X ) , 0 >. e. ( CC X. CC ) ) -> - e. ( ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) CnP ( TopOpen ` CCfld ) ) ` <. ( G ` X ) , 0 >. ) )
480 452 478 479 sylancr 
 |-  ( ph -> - e. ( ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) CnP ( TopOpen ` CCfld ) ) ` <. ( G ` X ) , 0 >. ) )
481 136 140 419 419 55 435 471 476 480 limccnp2 
 |-  ( ph -> ( ( G ` X ) - 0 ) e. ( ( z e. ( A (,) X ) |-> ( ( G ` X ) - ( G ` z ) ) ) limCC A ) )
482 461 481 eqeltrrd 
 |-  ( ph -> ( G ` X ) e. ( ( z e. ( A (,) X ) |-> ( ( G ` X ) - ( G ` z ) ) ) limCC A ) )
483 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) = ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) )
484 55 483 divcn 
 |-  / e. ( ( ( TopOpen ` CCfld ) tX ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) ) Cn ( TopOpen ` CCfld ) )
485 eldifsn 
 |-  ( ( G ` X ) e. ( CC \ { 0 } ) <-> ( ( G ` X ) e. CC /\ ( G ` X ) =/= 0 ) )
486 25 32 485 sylanbrc 
 |-  ( ph -> ( G ` X ) e. ( CC \ { 0 } ) )
487 23 486 opelxpd 
 |-  ( ph -> <. ( F ` X ) , ( G ` X ) >. e. ( CC X. ( CC \ { 0 } ) ) )
488 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( CC \ { 0 } ) C_ CC ) -> ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) e. ( TopOn ` ( CC \ { 0 } ) ) )
489 422 420 488 mp2an 
 |-  ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) e. ( TopOn ` ( CC \ { 0 } ) )
490 txtopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) e. ( TopOn ` ( CC \ { 0 } ) ) ) -> ( ( TopOpen ` CCfld ) tX ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) ) e. ( TopOn ` ( CC X. ( CC \ { 0 } ) ) ) )
491 422 489 490 mp2an 
 |-  ( ( TopOpen ` CCfld ) tX ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) ) e. ( TopOn ` ( CC X. ( CC \ { 0 } ) ) )
492 491 toponunii 
 |-  ( CC X. ( CC \ { 0 } ) ) = U. ( ( TopOpen ` CCfld ) tX ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) )
493 492 cncnpi 
 |-  ( ( / e. ( ( ( TopOpen ` CCfld ) tX ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) ) Cn ( TopOpen ` CCfld ) ) /\ <. ( F ` X ) , ( G ` X ) >. e. ( CC X. ( CC \ { 0 } ) ) ) -> / e. ( ( ( ( TopOpen ` CCfld ) tX ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) ) CnP ( TopOpen ` CCfld ) ) ` <. ( F ` X ) , ( G ` X ) >. ) )
494 484 487 493 sylancr 
 |-  ( ph -> / e. ( ( ( ( TopOpen ` CCfld ) tX ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) ) CnP ( TopOpen ` CCfld ) ) ` <. ( F ` X ) , ( G ` X ) >. ) )
495 415 418 419 421 55 431 460 482 494 limccnp2 
 |-  ( ph -> ( ( F ` X ) / ( G ` X ) ) e. ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) limCC A ) )
496 415 416 225 divcld 
 |-  ( ( ph /\ z e. ( A (,) X ) ) -> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) e. CC )
497 496 fmpttd 
 |-  ( ph -> ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) : ( A (,) X ) --> CC )
498 437 159 sstri 
 |-  ( A (,) X ) C_ CC
499 498 a1i 
 |-  ( ph -> ( A (,) X ) C_ CC )
500 497 499 74 55 ellimc2 
 |-  ( ph -> ( ( ( F ` X ) / ( G ` X ) ) e. ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) limCC A ) <-> ( ( ( F ` X ) / ( G ` X ) ) e. CC /\ A. u e. ( TopOpen ` CCfld ) ( ( ( F ` X ) / ( G ` X ) ) e. u -> E. v e. ( TopOpen ` CCfld ) ( A e. v /\ ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) C_ u ) ) ) ) )
501 495 500 mpbid 
 |-  ( ph -> ( ( ( F ` X ) / ( G ` X ) ) e. CC /\ A. u e. ( TopOpen ` CCfld ) ( ( ( F ` X ) / ( G ` X ) ) e. u -> E. v e. ( TopOpen ` CCfld ) ( A e. v /\ ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) C_ u ) ) ) )
502 501 simprd 
 |-  ( ph -> A. u e. ( TopOpen ` CCfld ) ( ( ( F ` X ) / ( G ` X ) ) e. u -> E. v e. ( TopOpen ` CCfld ) ( A e. v /\ ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) C_ u ) ) )
503 notrab 
 |-  ( CC \ { x e. CC | ( abs ` ( x - C ) ) <_ E } ) = { x e. CC | -. ( abs ` ( x - C ) ) <_ E }
504 76 cnmetdval 
 |-  ( ( C e. CC /\ x e. CC ) -> ( C ( abs o. - ) x ) = ( abs ` ( C - x ) ) )
505 abssub 
 |-  ( ( C e. CC /\ x e. CC ) -> ( abs ` ( C - x ) ) = ( abs ` ( x - C ) ) )
506 504 505 eqtrd 
 |-  ( ( C e. CC /\ x e. CC ) -> ( C ( abs o. - ) x ) = ( abs ` ( x - C ) ) )
507 35 506 sylan 
 |-  ( ( ph /\ x e. CC ) -> ( C ( abs o. - ) x ) = ( abs ` ( x - C ) ) )
508 507 breq1d 
 |-  ( ( ph /\ x e. CC ) -> ( ( C ( abs o. - ) x ) <_ E <-> ( abs ` ( x - C ) ) <_ E ) )
509 508 rabbidva 
 |-  ( ph -> { x e. CC | ( C ( abs o. - ) x ) <_ E } = { x e. CC | ( abs ` ( x - C ) ) <_ E } )
510 42 a1i 
 |-  ( ph -> ( abs o. - ) e. ( *Met ` CC ) )
511 38 rexrd 
 |-  ( ph -> E e. RR* )
512 eqid 
 |-  { x e. CC | ( C ( abs o. - ) x ) <_ E } = { x e. CC | ( C ( abs o. - ) x ) <_ E }
513 56 512 blcld 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ C e. CC /\ E e. RR* ) -> { x e. CC | ( C ( abs o. - ) x ) <_ E } e. ( Clsd ` ( TopOpen ` CCfld ) ) )
514 510 35 511 513 syl3anc 
 |-  ( ph -> { x e. CC | ( C ( abs o. - ) x ) <_ E } e. ( Clsd ` ( TopOpen ` CCfld ) ) )
515 509 514 eqeltrrd 
 |-  ( ph -> { x e. CC | ( abs ` ( x - C ) ) <_ E } e. ( Clsd ` ( TopOpen ` CCfld ) ) )
516 427 cldopn 
 |-  ( { x e. CC | ( abs ` ( x - C ) ) <_ E } e. ( Clsd ` ( TopOpen ` CCfld ) ) -> ( CC \ { x e. CC | ( abs ` ( x - C ) ) <_ E } ) e. ( TopOpen ` CCfld ) )
517 515 516 syl 
 |-  ( ph -> ( CC \ { x e. CC | ( abs ` ( x - C ) ) <_ E } ) e. ( TopOpen ` CCfld ) )
518 503 517 eqeltrrid 
 |-  ( ph -> { x e. CC | -. ( abs ` ( x - C ) ) <_ E } e. ( TopOpen ` CCfld ) )
519 410 502 518 rspcdva 
 |-  ( ph -> ( ( ( F ` X ) / ( G ` X ) ) e. { x e. CC | -. ( abs ` ( x - C ) ) <_ E } -> E. v e. ( TopOpen ` CCfld ) ( A e. v /\ ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) C_ { x e. CC | -. ( abs ` ( x - C ) ) <_ E } ) ) )
520 405 519 sylbird 
 |-  ( ph -> ( -. ( abs ` ( ( ( F ` X ) / ( G ` X ) ) - C ) ) <_ E -> E. v e. ( TopOpen ` CCfld ) ( A e. v /\ ( ( z e. ( A (,) X ) |-> ( ( ( F ` X ) - ( F ` z ) ) / ( ( G ` X ) - ( G ` z ) ) ) ) " ( v i^i ( ( A (,) X ) \ { A } ) ) ) C_ { x e. CC | -. ( abs ` ( x - C ) ) <_ E } ) ) )
521 400 520 mt3d 
 |-  ( ph -> ( abs ` ( ( ( F ` X ) / ( G ` X ) ) - C ) ) <_ E )
522 38 recnd 
 |-  ( ph -> E e. CC )
523 522 mulid2d 
 |-  ( ph -> ( 1 x. E ) = E )
524 1red 
 |-  ( ph -> 1 e. RR )
525 1lt2 
 |-  1 < 2
526 525 a1i 
 |-  ( ph -> 1 < 2 )
527 524 40 13 526 ltmul1dd 
 |-  ( ph -> ( 1 x. E ) < ( 2 x. E ) )
528 523 527 eqbrtrrd 
 |-  ( ph -> E < ( 2 x. E ) )
529 37 38 41 521 528 lelttrd 
 |-  ( ph -> ( abs ` ( ( ( F ` X ) / ( G ` X ) ) - C ) ) < ( 2 x. E ) )