lhop1lem

	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	ffvelcdmd	\|- ( ph -> ( F ` X ) e. RR )
23	22	recnd	\|- ( ph -> ( F ` X ) e. CC )
24	5 21	ffvelcdmd	\|- ( 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	sselid	\|- ( 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	sselid	\|- ( 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	eqtrid	\|- ( ( 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	ffvelcdmd	\|- ( ( 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	ffvelcdmd	\|- ( ( 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	ffvelcdmda	\|- ( ( 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	sselid	\|- ( ( 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		cncfcdm	\|- ( ( 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		tgioo4	\|- ( 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		cncfcdm	\|- ( ( 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	ffvelcdmd	\|- ( ( ( 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	ffvelcdmd	\|- ( ( ( 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	ffvelcdmda	\|- ( ( 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	sselid	\|- ( 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	sselid	\|- ( 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	mullidd	\|- ( 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 ) )

Metamath Proof Explorer

Theorem lhop1lem

Proof