Metamath Proof Explorer

Theorem lhop1

Description: L'Hôpital's Rule for limits from the right. If F and G are differentiable real functions on ( A , B ) , and F and G both approach 0 at A , and G ( x ) and G ' ( x ) are not zero on ( A , B ) , and the limit of F ' ( x ) / G ' ( x ) at A is C , then the limit F ( x ) / G ( x ) at A also exists and equals C . (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 ) )
Assertion lhop1 
|- ( ph -> C e. ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) limCC A ) )

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 simpr 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR+ )
14 13 rphalfcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( x / 2 ) e. RR+ )
15 breq2 
 |-  ( e = ( x / 2 ) -> ( ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < e <-> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < ( x / 2 ) ) )
16 15 imbi2d 
 |-  ( e = ( x / 2 ) -> ( ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < e ) <-> ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < ( x / 2 ) ) ) )
17 16 rexralbidv 
 |-  ( e = ( x / 2 ) -> ( E. d e. RR+ A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < e ) <-> E. d e. RR+ A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < ( x / 2 ) ) ) )
18 17 rspcv 
 |-  ( ( x / 2 ) e. RR+ -> ( A. e e. RR+ E. d e. RR+ A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < e ) -> E. d e. RR+ A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < ( x / 2 ) ) ) )
19 14 18 syl 
 |-  ( ( ph /\ x e. RR+ ) -> ( A. e e. RR+ E. d e. RR+ A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < e ) -> E. d e. RR+ A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < ( x / 2 ) ) ) )
20 rabid 
 |-  ( v e. { v e. ( A (,) B ) | ( abs ` ( v - A ) ) < d } <-> ( v e. ( A (,) B ) /\ ( abs ` ( v - A ) ) < d ) )
21 eliooord 
 |-  ( v e. ( A (,) B ) -> ( A < v /\ v < B ) )
22 21 adantl 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> ( A < v /\ v < B ) )
23 22 simprd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> v < B )
24 23 biantrurd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> ( v < ( d + A ) <-> ( v < B /\ v < ( d + A ) ) ) )
25 ioossre 
 |-  ( A (,) B ) C_ RR
26 simpr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> v e. ( A (,) B ) )
27 25 26 sseldi 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> v e. RR )
28 1 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> A e. RR )
29 simpr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) -> d e. RR+ )
30 29 rpred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) -> d e. RR )
31 30 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> d e. RR )
32 27 28 31 ltsubaddd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> ( ( v - A ) < d <-> v < ( d + A ) ) )
33 27 rexrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> v e. RR* )
34 2 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> B e. RR* )
35 1 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) -> A e. RR )
36 30 35 readdcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) -> ( d + A ) e. RR )
37 36 rexrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) -> ( d + A ) e. RR* )
38 37 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> ( d + A ) e. RR* )
39 xrltmin 
 |-  ( ( v e. RR* /\ B e. RR* /\ ( d + A ) e. RR* ) -> ( v < if ( B <_ ( d + A ) , B , ( d + A ) ) <-> ( v < B /\ v < ( d + A ) ) ) )
40 33 34 38 39 syl3anc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> ( v < if ( B <_ ( d + A ) , B , ( d + A ) ) <-> ( v < B /\ v < ( d + A ) ) ) )
41 24 32 40 3bitr4rd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> ( v < if ( B <_ ( d + A ) , B , ( d + A ) ) <-> ( v - A ) < d ) )
42 28 rexrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> A e. RR* )
43 34 38 ifcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> if ( B <_ ( d + A ) , B , ( d + A ) ) e. RR* )
44 22 simpld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> A < v )
45 elioo5 
 |-  ( ( A e. RR* /\ if ( B <_ ( d + A ) , B , ( d + A ) ) e. RR* /\ v e. RR* ) -> ( v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) <-> ( A < v /\ v < if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) )
46 45 baibd 
 |-  ( ( ( A e. RR* /\ if ( B <_ ( d + A ) , B , ( d + A ) ) e. RR* /\ v e. RR* ) /\ A < v ) -> ( v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) <-> v < if ( B <_ ( d + A ) , B , ( d + A ) ) ) )
47 42 43 33 44 46 syl31anc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> ( v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) <-> v < if ( B <_ ( d + A ) , B , ( d + A ) ) ) )
48 28 27 44 ltled 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> A <_ v )
49 28 27 48 abssubge0d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> ( abs ` ( v - A ) ) = ( v - A ) )
50 49 breq1d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> ( ( abs ` ( v - A ) ) < d <-> ( v - A ) < d ) )
51 41 47 50 3bitr4d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> ( v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) <-> ( abs ` ( v - A ) ) < d ) )
52 51 rabbi2dva 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) -> ( ( A (,) B ) i^i ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) = { v e. ( A (,) B ) | ( abs ` ( v - A ) ) < d } )
53 2 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) -> B e. RR* )
54 xrmin1 
 |-  ( ( B e. RR* /\ ( d + A ) e. RR* ) -> if ( B <_ ( d + A ) , B , ( d + A ) ) <_ B )
55 53 37 54 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) -> if ( B <_ ( d + A ) , B , ( d + A ) ) <_ B )
56 iooss2 
 |-  ( ( B e. RR* /\ if ( B <_ ( d + A ) , B , ( d + A ) ) <_ B ) -> ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) C_ ( A (,) B ) )
57 53 55 56 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) -> ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) C_ ( A (,) B ) )
58 sseqin2 
 |-  ( ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) C_ ( A (,) B ) <-> ( ( A (,) B ) i^i ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) = ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) )
59 57 58 sylib 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) -> ( ( A (,) B ) i^i ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) = ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) )
60 52 59 eqtr3d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) -> { v e. ( A (,) B ) | ( abs ` ( v - A ) ) < d } = ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) )
61 60 eleq2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) -> ( v e. { v e. ( A (,) B ) | ( abs ` ( v - A ) ) < d } <-> v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) )
62 20 61 bitr3id 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) -> ( ( v e. ( A (,) B ) /\ ( abs ` ( v - A ) ) < d ) <-> v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) )
63 lbioo 
 |-  -. A e. ( A (,) B )
64 eleq1 
 |-  ( y = A -> ( y e. ( A (,) B ) <-> A e. ( A (,) B ) ) )
65 63 64 mtbiri 
 |-  ( y = A -> -. y e. ( A (,) B ) )
66 65 necon2ai 
 |-  ( y e. ( A (,) B ) -> y =/= A )
67 66 biantrurd 
 |-  ( y e. ( A (,) B ) -> ( ( abs ` ( y - A ) ) < d <-> ( y =/= A /\ ( abs ` ( y - A ) ) < d ) ) )
68 67 bicomd 
 |-  ( y e. ( A (,) B ) -> ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) <-> ( abs ` ( y - A ) ) < d ) )
69 fveq2 
 |-  ( z = y -> ( ( RR _D F ) ` z ) = ( ( RR _D F ) ` y ) )
70 fveq2 
 |-  ( z = y -> ( ( RR _D G ) ` z ) = ( ( RR _D G ) ` y ) )
71 69 70 oveq12d 
 |-  ( z = y -> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) = ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) )
72 eqid 
 |-  ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) = ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) )
73 ovex 
 |-  ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) e. _V
74 71 72 73 fvmpt3i 
 |-  ( y e. ( A (,) B ) -> ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) = ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) )
75 74 fvoveq1d 
 |-  ( y e. ( A (,) B ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) = ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) )
76 75 breq1d 
 |-  ( y e. ( A (,) B ) -> ( ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < ( x / 2 ) <-> ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) )
77 68 76 imbi12d 
 |-  ( y e. ( A (,) B ) -> ( ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < ( x / 2 ) ) <-> ( ( abs ` ( y - A ) ) < d -> ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) )
78 77 ralbiia 
 |-  ( A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < ( x / 2 ) ) <-> A. y e. ( A (,) B ) ( ( abs ` ( y - A ) ) < d -> ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) )
79 fvoveq1 
 |-  ( v = y -> ( abs ` ( v - A ) ) = ( abs ` ( y - A ) ) )
80 79 breq1d 
 |-  ( v = y -> ( ( abs ` ( v - A ) ) < d <-> ( abs ` ( y - A ) ) < d ) )
81 80 ralrab 
 |-  ( A. y e. { v e. ( A (,) B ) | ( abs ` ( v - A ) ) < d } ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) <-> A. y e. ( A (,) B ) ( ( abs ` ( y - A ) ) < d -> ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) )
82 78 81 bitr4i 
 |-  ( A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < ( x / 2 ) ) <-> A. y e. { v e. ( A (,) B ) | ( abs ` ( v - A ) ) < d } ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) )
83 60 adantrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) ) -> { v e. ( A (,) B ) | ( abs ` ( v - A ) ) < d } = ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) )
84 83 raleqdv 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) ) -> ( A. y e. { v e. ( A (,) B ) | ( abs ` ( v - A ) ) < d } ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) <-> A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) )
85 1 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> A e. RR )
86 2 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> B e. RR* )
87 3 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> A < B )
88 4 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> F : ( A (,) B ) --> RR )
89 5 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> G : ( A (,) B ) --> RR )
90 6 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> dom ( RR _D F ) = ( A (,) B ) )
91 7 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> dom ( RR _D G ) = ( A (,) B ) )
92 8 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> 0 e. ( F limCC A ) )
93 9 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> 0 e. ( G limCC A ) )
94 10 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> -. 0 e. ran G )
95 11 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> -. 0 e. ran ( RR _D G ) )
96 12 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> C e. ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) limCC A ) )
97 14 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> ( x / 2 ) e. RR+ )
98 85 rexrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> A e. RR* )
99 simprll 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> d e. RR+ )
100 99 rpred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> d e. RR )
101 100 85 readdcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> ( d + A ) e. RR )
102 iocssre 
 |-  ( ( A e. RR* /\ ( d + A ) e. RR ) -> ( A (,] ( d + A ) ) C_ RR )
103 98 101 102 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> ( A (,] ( d + A ) ) C_ RR )
104 86 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) /\ B <_ ( d + A ) ) -> B e. RR* )
105 100 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) /\ -. B <_ ( d + A ) ) -> d e. RR )
106 85 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) /\ -. B <_ ( d + A ) ) -> A e. RR )
107 105 106 readdcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) /\ -. B <_ ( d + A ) ) -> ( d + A ) e. RR )
108 107 rexrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) /\ -. B <_ ( d + A ) ) -> ( d + A ) e. RR* )
109 104 108 ifclda 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> if ( B <_ ( d + A ) , B , ( d + A ) ) e. RR* )
110 85 99 ltaddrp2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> A < ( d + A ) )
111 101 rexrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> ( d + A ) e. RR* )
112 xrltmin 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( d + A ) e. RR* ) -> ( A < if ( B <_ ( d + A ) , B , ( d + A ) ) <-> ( A < B /\ A < ( d + A ) ) ) )
113 98 86 111 112 syl3anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> ( A < if ( B <_ ( d + A ) , B , ( d + A ) ) <-> ( A < B /\ A < ( d + A ) ) ) )
114 87 110 113 mpbir2and 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> A < if ( B <_ ( d + A ) , B , ( d + A ) ) )
115 xrmin2 
 |-  ( ( B e. RR* /\ ( d + A ) e. RR* ) -> if ( B <_ ( d + A ) , B , ( d + A ) ) <_ ( d + A ) )
116 86 111 115 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> if ( B <_ ( d + A ) , B , ( d + A ) ) <_ ( d + A ) )
117 elioc1 
 |-  ( ( A e. RR* /\ ( d + A ) e. RR* ) -> ( if ( B <_ ( d + A ) , B , ( d + A ) ) e. ( A (,] ( d + A ) ) <-> ( if ( B <_ ( d + A ) , B , ( d + A ) ) e. RR* /\ A < if ( B <_ ( d + A ) , B , ( d + A ) ) /\ if ( B <_ ( d + A ) , B , ( d + A ) ) <_ ( d + A ) ) ) )
118 98 111 117 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> ( if ( B <_ ( d + A ) , B , ( d + A ) ) e. ( A (,] ( d + A ) ) <-> ( if ( B <_ ( d + A ) , B , ( d + A ) ) e. RR* /\ A < if ( B <_ ( d + A ) , B , ( d + A ) ) /\ if ( B <_ ( d + A ) , B , ( d + A ) ) <_ ( d + A ) ) ) )
119 109 114 116 118 mpbir3and 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> if ( B <_ ( d + A ) , B , ( d + A ) ) e. ( A (,] ( d + A ) ) )
120 103 119 sseldd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> if ( B <_ ( d + A ) , B , ( d + A ) ) e. RR )
121 86 111 54 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> if ( B <_ ( d + A ) , B , ( d + A ) ) <_ B )
122 simprlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) )
123 simprr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) )
124 eqid 
 |-  ( A + ( r / 2 ) ) = ( A + ( r / 2 ) )
125 85 86 87 88 89 90 91 92 93 94 95 96 97 120 121 122 123 124 lhop1lem 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> ( abs ` ( ( ( F ` v ) / ( G ` v ) ) - C ) ) < ( 2 x. ( x / 2 ) ) )
126 13 rpcnd 
 |-  ( ( ph /\ x e. RR+ ) -> x e. CC )
127 2cnd 
 |-  ( ( ph /\ x e. RR+ ) -> 2 e. CC )
128 2ne0 
 |-  2 =/= 0
129 128 a1i 
 |-  ( ( ph /\ x e. RR+ ) -> 2 =/= 0 )
130 126 127 129 divcan2d 
 |-  ( ( ph /\ x e. RR+ ) -> ( 2 x. ( x / 2 ) ) = x )
131 130 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> ( 2 x. ( x / 2 ) ) = x )
132 125 131 breqtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) /\ A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) ) ) -> ( abs ` ( ( ( F ` v ) / ( G ` v ) ) - C ) ) < x )
133 132 expr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) ) -> ( A. y e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) -> ( abs ` ( ( ( F ` v ) / ( G ` v ) ) - C ) ) < x ) )
134 84 133 sylbid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) ) -> ( A. y e. { v e. ( A (,) B ) | ( abs ` ( v - A ) ) < d } ( abs ` ( ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) - C ) ) < ( x / 2 ) -> ( abs ` ( ( ( F ` v ) / ( G ` v ) ) - C ) ) < x ) )
135 82 134 syl5bi 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. RR+ /\ v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) ) ) -> ( A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < ( x / 2 ) ) -> ( abs ` ( ( ( F ` v ) / ( G ` v ) ) - C ) ) < x ) )
136 135 expr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) -> ( v e. ( A (,) if ( B <_ ( d + A ) , B , ( d + A ) ) ) -> ( A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < ( x / 2 ) ) -> ( abs ` ( ( ( F ` v ) / ( G ` v ) ) - C ) ) < x ) ) )
137 62 136 sylbid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) -> ( ( v e. ( A (,) B ) /\ ( abs ` ( v - A ) ) < d ) -> ( A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < ( x / 2 ) ) -> ( abs ` ( ( ( F ` v ) / ( G ` v ) ) - C ) ) < x ) ) )
138 137 expdimp 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> ( ( abs ` ( v - A ) ) < d -> ( A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < ( x / 2 ) ) -> ( abs ` ( ( ( F ` v ) / ( G ` v ) ) - C ) ) < x ) ) )
139 fveq2 
 |-  ( z = v -> ( F ` z ) = ( F ` v ) )
140 fveq2 
 |-  ( z = v -> ( G ` z ) = ( G ` v ) )
141 139 140 oveq12d 
 |-  ( z = v -> ( ( F ` z ) / ( G ` z ) ) = ( ( F ` v ) / ( G ` v ) ) )
142 eqid 
 |-  ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) = ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) )
143 ovex 
 |-  ( ( F ` z ) / ( G ` z ) ) e. _V
144 141 142 143 fvmpt3i 
 |-  ( v e. ( A (,) B ) -> ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) ` v ) = ( ( F ` v ) / ( G ` v ) ) )
145 144 fvoveq1d 
 |-  ( v e. ( A (,) B ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) ` v ) - C ) ) = ( abs ` ( ( ( F ` v ) / ( G ` v ) ) - C ) ) )
146 145 breq1d 
 |-  ( v e. ( A (,) B ) -> ( ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) ` v ) - C ) ) < x <-> ( abs ` ( ( ( F ` v ) / ( G ` v ) ) - C ) ) < x ) )
147 146 imbi2d 
 |-  ( v e. ( A (,) B ) -> ( ( A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < ( x / 2 ) ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) ` v ) - C ) ) < x ) <-> ( A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < ( x / 2 ) ) -> ( abs ` ( ( ( F ` v ) / ( G ` v ) ) - C ) ) < x ) ) )
148 147 adantl 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> ( ( A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < ( x / 2 ) ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) ` v ) - C ) ) < x ) <-> ( A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < ( x / 2 ) ) -> ( abs ` ( ( ( F ` v ) / ( G ` v ) ) - C ) ) < x ) ) )
149 138 148 sylibrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> ( ( abs ` ( v - A ) ) < d -> ( A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < ( x / 2 ) ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) ` v ) - C ) ) < x ) ) )
150 149 adantld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> ( ( v =/= A /\ ( abs ` ( v - A ) ) < d ) -> ( A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < ( x / 2 ) ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) ` v ) - C ) ) < x ) ) )
151 150 com23 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) /\ v e. ( A (,) B ) ) -> ( A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < ( x / 2 ) ) -> ( ( v =/= A /\ ( abs ` ( v - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) ` v ) - C ) ) < x ) ) )
152 151 ralrimdva 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. RR+ ) -> ( A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < ( x / 2 ) ) -> A. v e. ( A (,) B ) ( ( v =/= A /\ ( abs ` ( v - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) ` v ) - C ) ) < x ) ) )
153 152 reximdva 
 |-  ( ( ph /\ x e. RR+ ) -> ( E. d e. RR+ A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < ( x / 2 ) ) -> E. d e. RR+ A. v e. ( A (,) B ) ( ( v =/= A /\ ( abs ` ( v - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) ` v ) - C ) ) < x ) ) )
154 19 153 syld 
 |-  ( ( ph /\ x e. RR+ ) -> ( A. e e. RR+ E. d e. RR+ A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < e ) -> E. d e. RR+ A. v e. ( A (,) B ) ( ( v =/= A /\ ( abs ` ( v - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) ` v ) - C ) ) < x ) ) )
155 154 ralrimdva 
 |-  ( ph -> ( A. e e. RR+ E. d e. RR+ A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < e ) -> A. x e. RR+ E. d e. RR+ A. v e. ( A (,) B ) ( ( v =/= A /\ ( abs ` ( v - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) ` v ) - C ) ) < x ) ) )
156 155 anim2d 
 |-  ( ph -> ( ( C e. CC /\ A. e e. RR+ E. d e. RR+ A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < e ) ) -> ( C e. CC /\ A. x e. RR+ E. d e. RR+ A. v e. ( A (,) B ) ( ( v =/= A /\ ( abs ` ( v - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) ` v ) - C ) ) < x ) ) ) )
157 dvf 
 |-  ( RR _D F ) : dom ( RR _D F ) --> CC
158 6 feq2d 
 |-  ( ph -> ( ( RR _D F ) : dom ( RR _D F ) --> CC <-> ( RR _D F ) : ( A (,) B ) --> CC ) )
159 157 158 mpbii 
 |-  ( ph -> ( RR _D F ) : ( A (,) B ) --> CC )
160 159 ffvelrnda 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( RR _D F ) ` z ) e. CC )
161 dvf 
 |-  ( RR _D G ) : dom ( RR _D G ) --> CC
162 7 feq2d 
 |-  ( ph -> ( ( RR _D G ) : dom ( RR _D G ) --> CC <-> ( RR _D G ) : ( A (,) B ) --> CC ) )
163 161 162 mpbii 
 |-  ( ph -> ( RR _D G ) : ( A (,) B ) --> CC )
164 163 ffvelrnda 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( RR _D G ) ` z ) e. CC )
165 11 adantr 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> -. 0 e. ran ( RR _D G ) )
166 163 ffnd 
 |-  ( ph -> ( RR _D G ) Fn ( A (,) B ) )
167 fnfvelrn 
 |-  ( ( ( RR _D G ) Fn ( A (,) B ) /\ z e. ( A (,) B ) ) -> ( ( RR _D G ) ` z ) e. ran ( RR _D G ) )
168 166 167 sylan 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( RR _D G ) ` z ) e. ran ( RR _D G ) )
169 eleq1 
 |-  ( ( ( RR _D G ) ` z ) = 0 -> ( ( ( RR _D G ) ` z ) e. ran ( RR _D G ) <-> 0 e. ran ( RR _D G ) ) )
170 168 169 syl5ibcom 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( ( RR _D G ) ` z ) = 0 -> 0 e. ran ( RR _D G ) ) )
171 170 necon3bd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( -. 0 e. ran ( RR _D G ) -> ( ( RR _D G ) ` z ) =/= 0 ) )
172 165 171 mpd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( RR _D G ) ` z ) =/= 0 )
173 160 164 172 divcld 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) e. CC )
174 173 fmpttd 
 |-  ( ph -> ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) : ( A (,) B ) --> CC )
175 ax-resscn 
 |-  RR C_ CC
176 25 175 sstri 
 |-  ( A (,) B ) C_ CC
177 176 a1i 
 |-  ( ph -> ( A (,) B ) C_ CC )
178 1 recnd 
 |-  ( ph -> A e. CC )
179 174 177 178 ellimc3 
 |-  ( ph -> ( C e. ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) limCC A ) <-> ( C e. CC /\ A. e e. RR+ E. d e. RR+ A. y e. ( A (,) B ) ( ( y =/= A /\ ( abs ` ( y - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) ` y ) - C ) ) < e ) ) ) )
180 4 ffvelrnda 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( F ` z ) e. RR )
181 180 recnd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( F ` z ) e. CC )
182 5 ffvelrnda 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( G ` z ) e. RR )
183 182 recnd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( G ` z ) e. CC )
184 10 adantr 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> -. 0 e. ran G )
185 5 ffnd 
 |-  ( ph -> G Fn ( A (,) B ) )
186 fnfvelrn 
 |-  ( ( G Fn ( A (,) B ) /\ z e. ( A (,) B ) ) -> ( G ` z ) e. ran G )
187 185 186 sylan 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( G ` z ) e. ran G )
188 eleq1 
 |-  ( ( G ` z ) = 0 -> ( ( G ` z ) e. ran G <-> 0 e. ran G ) )
189 187 188 syl5ibcom 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( G ` z ) = 0 -> 0 e. ran G ) )
190 189 necon3bd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( -. 0 e. ran G -> ( G ` z ) =/= 0 ) )
191 184 190 mpd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( G ` z ) =/= 0 )
192 181 183 191 divcld 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( F ` z ) / ( G ` z ) ) e. CC )
193 192 fmpttd 
 |-  ( ph -> ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) : ( A (,) B ) --> CC )
194 193 177 178 ellimc3 
 |-  ( ph -> ( C e. ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) limCC A ) <-> ( C e. CC /\ A. x e. RR+ E. d e. RR+ A. v e. ( A (,) B ) ( ( v =/= A /\ ( abs ` ( v - A ) ) < d ) -> ( abs ` ( ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) ` v ) - C ) ) < x ) ) ) )
195 156 179 194 3imtr4d 
 |-  ( ph -> ( C e. ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) limCC A ) -> C e. ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) limCC A ) ) )
196 12 195 mpd 
 |-  ( ph -> C e. ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) limCC A ) )