Metamath Proof Explorer

Theorem lhop2

Description: L'Hôpital's Rule for limits from the left. If F and G are differentiable real functions on ( A , B ) , and F and G both approach 0 at B , and G ( x ) and G ' ( x ) are not zero on ( A , B ) , and the limit of F ' ( x ) / G ' ( x ) at B is C , then the limit F ( x ) / G ( x ) at B also exists and equals C . (Contributed by Mario Carneiro, 29-Dec-2016)

Ref Expression
Hypotheses lhop2.a 
|- ( ph -> A e. RR* )
lhop2.b 
|- ( ph -> B e. RR )
lhop2.l 
|- ( ph -> A < B )
lhop2.f 
|- ( ph -> F : ( A (,) B ) --> RR )
lhop2.g 
|- ( ph -> G : ( A (,) B ) --> RR )
lhop2.if 
|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
lhop2.ig 
|- ( ph -> dom ( RR _D G ) = ( A (,) B ) )
lhop2.f0 
|- ( ph -> 0 e. ( F limCC B ) )
lhop2.g0 
|- ( ph -> 0 e. ( G limCC B ) )
lhop2.gn0 
|- ( ph -> -. 0 e. ran G )
lhop2.gd0 
|- ( ph -> -. 0 e. ran ( RR _D G ) )
lhop2.c 
|- ( ph -> C e. ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) limCC B ) )
Assertion lhop2 
|- ( ph -> C e. ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) limCC B ) )

Proof

Step Hyp Ref Expression
1 lhop2.a 
 |-  ( ph -> A e. RR* )
2 lhop2.b 
 |-  ( ph -> B e. RR )
3 lhop2.l 
 |-  ( ph -> A < B )
4 lhop2.f 
 |-  ( ph -> F : ( A (,) B ) --> RR )
5 lhop2.g 
 |-  ( ph -> G : ( A (,) B ) --> RR )
6 lhop2.if 
 |-  ( ph -> dom ( RR _D F ) = ( A (,) B ) )
7 lhop2.ig 
 |-  ( ph -> dom ( RR _D G ) = ( A (,) B ) )
8 lhop2.f0 
 |-  ( ph -> 0 e. ( F limCC B ) )
9 lhop2.g0 
 |-  ( ph -> 0 e. ( G limCC B ) )
10 lhop2.gn0 
 |-  ( ph -> -. 0 e. ran G )
11 lhop2.gd0 
 |-  ( ph -> -. 0 e. ran ( RR _D G ) )
12 lhop2.c 
 |-  ( ph -> C e. ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) limCC B ) )
13 qssre 
 |-  QQ C_ RR
14 2 rexrd 
 |-  ( ph -> B e. RR* )
15 qbtwnxr 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> E. a e. QQ ( A < a /\ a < B ) )
16 1 14 3 15 syl3anc 
 |-  ( ph -> E. a e. QQ ( A < a /\ a < B ) )
17 ssrexv 
 |-  ( QQ C_ RR -> ( E. a e. QQ ( A < a /\ a < B ) -> E. a e. RR ( A < a /\ a < B ) ) )
18 13 16 17 mpsyl 
 |-  ( ph -> E. a e. RR ( A < a /\ a < B ) )
19 simpr 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( a (,) B ) ) -> z e. ( a (,) B ) )
20 simprl 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> a e. RR )
21 20 adantr 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( a (,) B ) ) -> a e. RR )
22 2 ad2antrr 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( a (,) B ) ) -> B e. RR )
23 elioore 
 |-  ( z e. ( a (,) B ) -> z e. RR )
24 23 adantl 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( a (,) B ) ) -> z e. RR )
25 iooneg 
 |-  ( ( a e. RR /\ B e. RR /\ z e. RR ) -> ( z e. ( a (,) B ) <-> -u z e. ( -u B (,) -u a ) ) )
26 21 22 24 25 syl3anc 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( a (,) B ) ) -> ( z e. ( a (,) B ) <-> -u z e. ( -u B (,) -u a ) ) )
27 19 26 mpbid 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( a (,) B ) ) -> -u z e. ( -u B (,) -u a ) )
28 27 adantrr 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ ( z e. ( a (,) B ) /\ -u z =/= -u B ) ) -> -u z e. ( -u B (,) -u a ) )
29 4 ad2antrr 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> F : ( A (,) B ) --> RR )
30 elioore 
 |-  ( x e. ( -u B (,) -u a ) -> x e. RR )
31 30 adantl 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> x e. RR )
32 31 recnd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> x e. CC )
33 32 negnegd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> -u -u x = x )
34 simpr 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> x e. ( -u B (,) -u a ) )
35 33 34 eqeltrd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> -u -u x e. ( -u B (,) -u a ) )
36 20 adantr 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> a e. RR )
37 2 ad2antrr 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> B e. RR )
38 31 renegcld 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> -u x e. RR )
39 iooneg 
 |-  ( ( a e. RR /\ B e. RR /\ -u x e. RR ) -> ( -u x e. ( a (,) B ) <-> -u -u x e. ( -u B (,) -u a ) ) )
40 36 37 38 39 syl3anc 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( -u x e. ( a (,) B ) <-> -u -u x e. ( -u B (,) -u a ) ) )
41 35 40 mpbird 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> -u x e. ( a (,) B ) )
42 1 adantr 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> A e. RR* )
43 20 rexrd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> a e. RR* )
44 simprrl 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> A < a )
45 42 43 44 xrltled 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> A <_ a )
46 iooss1 
 |-  ( ( A e. RR* /\ A <_ a ) -> ( a (,) B ) C_ ( A (,) B ) )
47 42 45 46 syl2anc 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( a (,) B ) C_ ( A (,) B ) )
48 47 sselda 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ -u x e. ( a (,) B ) ) -> -u x e. ( A (,) B ) )
49 41 48 syldan 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> -u x e. ( A (,) B ) )
50 29 49 ffvelrnd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( F ` -u x ) e. RR )
51 50 recnd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( F ` -u x ) e. CC )
52 5 ad2antrr 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> G : ( A (,) B ) --> RR )
53 52 49 ffvelrnd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( G ` -u x ) e. RR )
54 53 recnd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( G ` -u x ) e. CC )
55 10 ad2antrr 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> -. 0 e. ran G )
56 5 adantr 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> G : ( A (,) B ) --> RR )
57 ax-resscn 
 |-  RR C_ CC
58 fss 
 |-  ( ( G : ( A (,) B ) --> RR /\ RR C_ CC ) -> G : ( A (,) B ) --> CC )
59 56 57 58 sylancl 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> G : ( A (,) B ) --> CC )
60 59 adantr 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> G : ( A (,) B ) --> CC )
61 60 ffnd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> G Fn ( A (,) B ) )
62 fnfvelrn 
 |-  ( ( G Fn ( A (,) B ) /\ -u x e. ( A (,) B ) ) -> ( G ` -u x ) e. ran G )
63 61 49 62 syl2anc 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( G ` -u x ) e. ran G )
64 eleq1 
 |-  ( ( G ` -u x ) = 0 -> ( ( G ` -u x ) e. ran G <-> 0 e. ran G ) )
65 63 64 syl5ibcom 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( ( G ` -u x ) = 0 -> 0 e. ran G ) )
66 65 necon3bd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( -. 0 e. ran G -> ( G ` -u x ) =/= 0 ) )
67 55 66 mpd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( G ` -u x ) =/= 0 )
68 51 54 67 divcld 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( ( F ` -u x ) / ( G ` -u x ) ) e. CC )
69 limcresi 
 |-  ( ( z e. RR |-> -u z ) limCC B ) C_ ( ( ( z e. RR |-> -u z ) |` ( a (,) B ) ) limCC B )
70 ioossre 
 |-  ( a (,) B ) C_ RR
71 resmpt 
 |-  ( ( a (,) B ) C_ RR -> ( ( z e. RR |-> -u z ) |` ( a (,) B ) ) = ( z e. ( a (,) B ) |-> -u z ) )
72 70 71 ax-mp 
 |-  ( ( z e. RR |-> -u z ) |` ( a (,) B ) ) = ( z e. ( a (,) B ) |-> -u z )
73 72 oveq1i 
 |-  ( ( ( z e. RR |-> -u z ) |` ( a (,) B ) ) limCC B ) = ( ( z e. ( a (,) B ) |-> -u z ) limCC B )
74 69 73 sseqtri 
 |-  ( ( z e. RR |-> -u z ) limCC B ) C_ ( ( z e. ( a (,) B ) |-> -u z ) limCC B )
75 eqid 
 |-  ( z e. RR |-> -u z ) = ( z e. RR |-> -u z )
76 75 negcncf 
 |-  ( RR C_ CC -> ( z e. RR |-> -u z ) e. ( RR -cn-> CC ) )
77 57 76 mp1i 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( z e. RR |-> -u z ) e. ( RR -cn-> CC ) )
78 2 adantr 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> B e. RR )
79 negeq 
 |-  ( z = B -> -u z = -u B )
80 77 78 79 cnmptlimc 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> -u B e. ( ( z e. RR |-> -u z ) limCC B ) )
81 74 80 sseldi 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> -u B e. ( ( z e. ( a (,) B ) |-> -u z ) limCC B ) )
82 78 renegcld 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> -u B e. RR )
83 20 renegcld 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> -u a e. RR )
84 83 rexrd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> -u a e. RR* )
85 simprrr 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> a < B )
86 20 78 ltnegd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( a < B <-> -u B < -u a ) )
87 85 86 mpbid 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> -u B < -u a )
88 50 fmpttd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) : ( -u B (,) -u a ) --> RR )
89 53 fmpttd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) : ( -u B (,) -u a ) --> RR )
90 reelprrecn 
 |-  RR e. { RR , CC }
91 90 a1i 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> RR e. { RR , CC } )
92 neg1cn 
 |-  -u 1 e. CC
93 92 a1i 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> -u 1 e. CC )
94 4 adantr 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> F : ( A (,) B ) --> RR )
95 94 ffvelrnda 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ y e. ( A (,) B ) ) -> ( F ` y ) e. RR )
96 95 recnd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ y e. ( A (,) B ) ) -> ( F ` y ) e. CC )
97 fvexd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ y e. ( A (,) B ) ) -> ( ( RR _D F ) ` y ) e. _V )
98 1cnd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> 1 e. CC )
99 simpr 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. RR ) -> x e. RR )
100 99 recnd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. RR ) -> x e. CC )
101 1cnd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. RR ) -> 1 e. CC )
102 91 dvmptid 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( RR _D ( x e. RR |-> x ) ) = ( x e. RR |-> 1 ) )
103 ioossre 
 |-  ( -u B (,) -u a ) C_ RR
104 103 a1i 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( -u B (,) -u a ) C_ RR )
105 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
106 105 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
107 iooretop 
 |-  ( -u B (,) -u a ) e. ( topGen ` ran (,) )
108 107 a1i 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( -u B (,) -u a ) e. ( topGen ` ran (,) ) )
109 91 100 101 102 104 106 105 108 dvmptres 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( RR _D ( x e. ( -u B (,) -u a ) |-> x ) ) = ( x e. ( -u B (,) -u a ) |-> 1 ) )
110 91 32 98 109 dvmptneg 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( RR _D ( x e. ( -u B (,) -u a ) |-> -u x ) ) = ( x e. ( -u B (,) -u a ) |-> -u 1 ) )
111 94 feqmptd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> F = ( y e. ( A (,) B ) |-> ( F ` y ) ) )
112 111 oveq2d 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( RR _D F ) = ( RR _D ( y e. ( A (,) B ) |-> ( F ` y ) ) ) )
113 dvf 
 |-  ( RR _D F ) : dom ( RR _D F ) --> CC
114 6 adantr 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> dom ( RR _D F ) = ( A (,) B ) )
115 114 feq2d 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( RR _D F ) : dom ( RR _D F ) --> CC <-> ( RR _D F ) : ( A (,) B ) --> CC ) )
116 113 115 mpbii 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( RR _D F ) : ( A (,) B ) --> CC )
117 116 feqmptd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( RR _D F ) = ( y e. ( A (,) B ) |-> ( ( RR _D F ) ` y ) ) )
118 112 117 eqtr3d 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( RR _D ( y e. ( A (,) B ) |-> ( F ` y ) ) ) = ( y e. ( A (,) B ) |-> ( ( RR _D F ) ` y ) ) )
119 fveq2 
 |-  ( y = -u x -> ( F ` y ) = ( F ` -u x ) )
120 fveq2 
 |-  ( y = -u x -> ( ( RR _D F ) ` y ) = ( ( RR _D F ) ` -u x ) )
121 91 91 49 93 96 97 110 118 119 120 dvmptco 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( RR _D ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ) = ( x e. ( -u B (,) -u a ) |-> ( ( ( RR _D F ) ` -u x ) x. -u 1 ) ) )
122 116 adantr 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( RR _D F ) : ( A (,) B ) --> CC )
123 122 49 ffvelrnd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( ( RR _D F ) ` -u x ) e. CC )
124 123 93 mulcomd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( ( ( RR _D F ) ` -u x ) x. -u 1 ) = ( -u 1 x. ( ( RR _D F ) ` -u x ) ) )
125 123 mulm1d 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( -u 1 x. ( ( RR _D F ) ` -u x ) ) = -u ( ( RR _D F ) ` -u x ) )
126 124 125 eqtrd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( ( ( RR _D F ) ` -u x ) x. -u 1 ) = -u ( ( RR _D F ) ` -u x ) )
127 126 mpteq2dva 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( x e. ( -u B (,) -u a ) |-> ( ( ( RR _D F ) ` -u x ) x. -u 1 ) ) = ( x e. ( -u B (,) -u a ) |-> -u ( ( RR _D F ) ` -u x ) ) )
128 121 127 eqtrd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( RR _D ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ) = ( x e. ( -u B (,) -u a ) |-> -u ( ( RR _D F ) ` -u x ) ) )
129 128 dmeqd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> dom ( RR _D ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ) = dom ( x e. ( -u B (,) -u a ) |-> -u ( ( RR _D F ) ` -u x ) ) )
130 negex 
 |-  -u ( ( RR _D F ) ` -u x ) e. _V
131 eqid 
 |-  ( x e. ( -u B (,) -u a ) |-> -u ( ( RR _D F ) ` -u x ) ) = ( x e. ( -u B (,) -u a ) |-> -u ( ( RR _D F ) ` -u x ) )
132 130 131 dmmpti 
 |-  dom ( x e. ( -u B (,) -u a ) |-> -u ( ( RR _D F ) ` -u x ) ) = ( -u B (,) -u a )
133 129 132 eqtrdi 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> dom ( RR _D ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ) = ( -u B (,) -u a ) )
134 56 ffvelrnda 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ y e. ( A (,) B ) ) -> ( G ` y ) e. RR )
135 134 recnd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ y e. ( A (,) B ) ) -> ( G ` y ) e. CC )
136 fvexd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ y e. ( A (,) B ) ) -> ( ( RR _D G ) ` y ) e. _V )
137 56 feqmptd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> G = ( y e. ( A (,) B ) |-> ( G ` y ) ) )
138 137 oveq2d 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( RR _D G ) = ( RR _D ( y e. ( A (,) B ) |-> ( G ` y ) ) ) )
139 dvf 
 |-  ( RR _D G ) : dom ( RR _D G ) --> CC
140 7 adantr 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> dom ( RR _D G ) = ( A (,) B ) )
141 140 feq2d 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( RR _D G ) : dom ( RR _D G ) --> CC <-> ( RR _D G ) : ( A (,) B ) --> CC ) )
142 139 141 mpbii 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( RR _D G ) : ( A (,) B ) --> CC )
143 142 feqmptd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( RR _D G ) = ( y e. ( A (,) B ) |-> ( ( RR _D G ) ` y ) ) )
144 138 143 eqtr3d 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( RR _D ( y e. ( A (,) B ) |-> ( G ` y ) ) ) = ( y e. ( A (,) B ) |-> ( ( RR _D G ) ` y ) ) )
145 fveq2 
 |-  ( y = -u x -> ( G ` y ) = ( G ` -u x ) )
146 fveq2 
 |-  ( y = -u x -> ( ( RR _D G ) ` y ) = ( ( RR _D G ) ` -u x ) )
147 91 91 49 93 135 136 110 144 145 146 dvmptco 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) = ( x e. ( -u B (,) -u a ) |-> ( ( ( RR _D G ) ` -u x ) x. -u 1 ) ) )
148 142 adantr 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( RR _D G ) : ( A (,) B ) --> CC )
149 148 49 ffvelrnd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( ( RR _D G ) ` -u x ) e. CC )
150 149 93 mulcomd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( ( ( RR _D G ) ` -u x ) x. -u 1 ) = ( -u 1 x. ( ( RR _D G ) ` -u x ) ) )
151 149 mulm1d 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( -u 1 x. ( ( RR _D G ) ` -u x ) ) = -u ( ( RR _D G ) ` -u x ) )
152 150 151 eqtrd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( ( ( RR _D G ) ` -u x ) x. -u 1 ) = -u ( ( RR _D G ) ` -u x ) )
153 152 mpteq2dva 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( x e. ( -u B (,) -u a ) |-> ( ( ( RR _D G ) ` -u x ) x. -u 1 ) ) = ( x e. ( -u B (,) -u a ) |-> -u ( ( RR _D G ) ` -u x ) ) )
154 147 153 eqtrd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) = ( x e. ( -u B (,) -u a ) |-> -u ( ( RR _D G ) ` -u x ) ) )
155 154 dmeqd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> dom ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) = dom ( x e. ( -u B (,) -u a ) |-> -u ( ( RR _D G ) ` -u x ) ) )
156 negex 
 |-  -u ( ( RR _D G ) ` -u x ) e. _V
157 eqid 
 |-  ( x e. ( -u B (,) -u a ) |-> -u ( ( RR _D G ) ` -u x ) ) = ( x e. ( -u B (,) -u a ) |-> -u ( ( RR _D G ) ` -u x ) )
158 156 157 dmmpti 
 |-  dom ( x e. ( -u B (,) -u a ) |-> -u ( ( RR _D G ) ` -u x ) ) = ( -u B (,) -u a )
159 155 158 eqtrdi 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> dom ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) = ( -u B (,) -u a ) )
160 49 adantrr 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ ( x e. ( -u B (,) -u a ) /\ -u x =/= B ) ) -> -u x e. ( A (,) B ) )
161 limcresi 
 |-  ( ( x e. RR |-> -u x ) limCC -u B ) C_ ( ( ( x e. RR |-> -u x ) |` ( -u B (,) -u a ) ) limCC -u B )
162 resmpt 
 |-  ( ( -u B (,) -u a ) C_ RR -> ( ( x e. RR |-> -u x ) |` ( -u B (,) -u a ) ) = ( x e. ( -u B (,) -u a ) |-> -u x ) )
163 103 162 ax-mp 
 |-  ( ( x e. RR |-> -u x ) |` ( -u B (,) -u a ) ) = ( x e. ( -u B (,) -u a ) |-> -u x )
164 163 oveq1i 
 |-  ( ( ( x e. RR |-> -u x ) |` ( -u B (,) -u a ) ) limCC -u B ) = ( ( x e. ( -u B (,) -u a ) |-> -u x ) limCC -u B )
165 161 164 sseqtri 
 |-  ( ( x e. RR |-> -u x ) limCC -u B ) C_ ( ( x e. ( -u B (,) -u a ) |-> -u x ) limCC -u B )
166 78 recnd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> B e. CC )
167 166 negnegd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> -u -u B = B )
168 eqid 
 |-  ( x e. RR |-> -u x ) = ( x e. RR |-> -u x )
169 168 negcncf 
 |-  ( RR C_ CC -> ( x e. RR |-> -u x ) e. ( RR -cn-> CC ) )
170 57 169 mp1i 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( x e. RR |-> -u x ) e. ( RR -cn-> CC ) )
171 negeq 
 |-  ( x = -u B -> -u x = -u -u B )
172 170 82 171 cnmptlimc 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> -u -u B e. ( ( x e. RR |-> -u x ) limCC -u B ) )
173 167 172 eqeltrrd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> B e. ( ( x e. RR |-> -u x ) limCC -u B ) )
174 165 173 sseldi 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> B e. ( ( x e. ( -u B (,) -u a ) |-> -u x ) limCC -u B ) )
175 8 adantr 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> 0 e. ( F limCC B ) )
176 111 oveq1d 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( F limCC B ) = ( ( y e. ( A (,) B ) |-> ( F ` y ) ) limCC B ) )
177 175 176 eleqtrd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> 0 e. ( ( y e. ( A (,) B ) |-> ( F ` y ) ) limCC B ) )
178 eliooord 
 |-  ( x e. ( -u B (,) -u a ) -> ( -u B < x /\ x < -u a ) )
179 178 adantl 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( -u B < x /\ x < -u a ) )
180 179 simpld 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> -u B < x )
181 37 31 180 ltnegcon1d 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> -u x < B )
182 38 181 ltned 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> -u x =/= B )
183 182 neneqd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> -. -u x = B )
184 183 pm2.21d 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( -u x = B -> ( F ` -u x ) = 0 ) )
185 184 impr 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ ( x e. ( -u B (,) -u a ) /\ -u x = B ) ) -> ( F ` -u x ) = 0 )
186 160 96 174 177 119 185 limcco 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> 0 e. ( ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) limCC -u B ) )
187 9 adantr 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> 0 e. ( G limCC B ) )
188 137 oveq1d 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( G limCC B ) = ( ( y e. ( A (,) B ) |-> ( G ` y ) ) limCC B ) )
189 187 188 eleqtrd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> 0 e. ( ( y e. ( A (,) B ) |-> ( G ` y ) ) limCC B ) )
190 183 pm2.21d 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( -u x = B -> ( G ` -u x ) = 0 ) )
191 190 impr 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ ( x e. ( -u B (,) -u a ) /\ -u x = B ) ) -> ( G ` -u x ) = 0 )
192 160 135 174 189 145 191 limcco 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> 0 e. ( ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) limCC -u B ) )
193 63 fmpttd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) : ( -u B (,) -u a ) --> ran G )
194 193 frnd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ran ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) C_ ran G )
195 10 adantr 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> -. 0 e. ran G )
196 194 195 ssneldd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> -. 0 e. ran ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) )
197 11 adantr 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> -. 0 e. ran ( RR _D G ) )
198 154 rneqd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ran ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) = ran ( x e. ( -u B (,) -u a ) |-> -u ( ( RR _D G ) ` -u x ) ) )
199 198 eleq2d 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( 0 e. ran ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) <-> 0 e. ran ( x e. ( -u B (,) -u a ) |-> -u ( ( RR _D G ) ` -u x ) ) ) )
200 157 156 elrnmpti 
 |-  ( 0 e. ran ( x e. ( -u B (,) -u a ) |-> -u ( ( RR _D G ) ` -u x ) ) <-> E. x e. ( -u B (,) -u a ) 0 = -u ( ( RR _D G ) ` -u x ) )
201 eqcom 
 |-  ( 0 = -u ( ( RR _D G ) ` -u x ) <-> -u ( ( RR _D G ) ` -u x ) = 0 )
202 149 negeq0d 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( ( ( RR _D G ) ` -u x ) = 0 <-> -u ( ( RR _D G ) ` -u x ) = 0 ) )
203 148 ffnd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( RR _D G ) Fn ( A (,) B ) )
204 fnfvelrn 
 |-  ( ( ( RR _D G ) Fn ( A (,) B ) /\ -u x e. ( A (,) B ) ) -> ( ( RR _D G ) ` -u x ) e. ran ( RR _D G ) )
205 203 49 204 syl2anc 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( ( RR _D G ) ` -u x ) e. ran ( RR _D G ) )
206 eleq1 
 |-  ( ( ( RR _D G ) ` -u x ) = 0 -> ( ( ( RR _D G ) ` -u x ) e. ran ( RR _D G ) <-> 0 e. ran ( RR _D G ) ) )
207 205 206 syl5ibcom 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( ( ( RR _D G ) ` -u x ) = 0 -> 0 e. ran ( RR _D G ) ) )
208 202 207 sylbird 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( -u ( ( RR _D G ) ` -u x ) = 0 -> 0 e. ran ( RR _D G ) ) )
209 201 208 syl5bi 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( 0 = -u ( ( RR _D G ) ` -u x ) -> 0 e. ran ( RR _D G ) ) )
210 209 rexlimdva 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( E. x e. ( -u B (,) -u a ) 0 = -u ( ( RR _D G ) ` -u x ) -> 0 e. ran ( RR _D G ) ) )
211 200 210 syl5bi 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( 0 e. ran ( x e. ( -u B (,) -u a ) |-> -u ( ( RR _D G ) ` -u x ) ) -> 0 e. ran ( RR _D G ) ) )
212 199 211 sylbid 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( 0 e. ran ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) -> 0 e. ran ( RR _D G ) ) )
213 197 212 mtod 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> -. 0 e. ran ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) )
214 116 ffvelrnda 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( A (,) B ) ) -> ( ( RR _D F ) ` z ) e. CC )
215 142 ffvelrnda 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( A (,) B ) ) -> ( ( RR _D G ) ` z ) e. CC )
216 11 ad2antrr 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( A (,) B ) ) -> -. 0 e. ran ( RR _D G ) )
217 142 ffnd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( RR _D G ) Fn ( A (,) B ) )
218 fnfvelrn 
 |-  ( ( ( RR _D G ) Fn ( A (,) B ) /\ z e. ( A (,) B ) ) -> ( ( RR _D G ) ` z ) e. ran ( RR _D G ) )
219 217 218 sylan 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( A (,) B ) ) -> ( ( RR _D G ) ` z ) e. ran ( RR _D G ) )
220 eleq1 
 |-  ( ( ( RR _D G ) ` z ) = 0 -> ( ( ( RR _D G ) ` z ) e. ran ( RR _D G ) <-> 0 e. ran ( RR _D G ) ) )
221 219 220 syl5ibcom 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( A (,) B ) ) -> ( ( ( RR _D G ) ` z ) = 0 -> 0 e. ran ( RR _D G ) ) )
222 221 necon3bd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( A (,) B ) ) -> ( -. 0 e. ran ( RR _D G ) -> ( ( RR _D G ) ` z ) =/= 0 ) )
223 216 222 mpd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( A (,) B ) ) -> ( ( RR _D G ) ` z ) =/= 0 )
224 214 215 223 divcld 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( A (,) B ) ) -> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) e. CC )
225 12 adantr 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> C e. ( ( z e. ( A (,) B ) |-> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) ) limCC B ) )
226 fveq2 
 |-  ( z = -u x -> ( ( RR _D F ) ` z ) = ( ( RR _D F ) ` -u x ) )
227 fveq2 
 |-  ( z = -u x -> ( ( RR _D G ) ` z ) = ( ( RR _D G ) ` -u x ) )
228 226 227 oveq12d 
 |-  ( z = -u x -> ( ( ( RR _D F ) ` z ) / ( ( RR _D G ) ` z ) ) = ( ( ( RR _D F ) ` -u x ) / ( ( RR _D G ) ` -u x ) ) )
229 183 pm2.21d 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( -u x = B -> ( ( ( RR _D F ) ` -u x ) / ( ( RR _D G ) ` -u x ) ) = C ) )
230 229 impr 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ ( x e. ( -u B (,) -u a ) /\ -u x = B ) ) -> ( ( ( RR _D F ) ` -u x ) / ( ( RR _D G ) ` -u x ) ) = C )
231 160 224 174 225 228 230 limcco 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> C e. ( ( x e. ( -u B (,) -u a ) |-> ( ( ( RR _D F ) ` -u x ) / ( ( RR _D G ) ` -u x ) ) ) limCC -u B ) )
232 nfcv 
 |-  F/_ x RR
233 nfcv 
 |-  F/_ x _D
234 nfmpt1 
 |-  F/_ x ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) )
235 232 233 234 nfov 
 |-  F/_ x ( RR _D ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) )
236 nfcv 
 |-  F/_ x y
237 235 236 nffv 
 |-  F/_ x ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ) ` y )
238 nfcv 
 |-  F/_ x /
239 nfmpt1 
 |-  F/_ x ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) )
240 232 233 239 nfov 
 |-  F/_ x ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) )
241 240 236 nffv 
 |-  F/_ x ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) ` y )
242 237 238 241 nfov 
 |-  F/_ x ( ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ) ` y ) / ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) ` y ) )
243 nfcv 
 |-  F/_ y ( ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ) ` x ) / ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) ` x ) )
244 fveq2 
 |-  ( y = x -> ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ) ` y ) = ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ) ` x ) )
245 fveq2 
 |-  ( y = x -> ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) ` y ) = ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) ` x ) )
246 244 245 oveq12d 
 |-  ( y = x -> ( ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ) ` y ) / ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) ` y ) ) = ( ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ) ` x ) / ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) ` x ) ) )
247 242 243 246 cbvmpt 
 |-  ( y e. ( -u B (,) -u a ) |-> ( ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ) ` y ) / ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) ` y ) ) ) = ( x e. ( -u B (,) -u a ) |-> ( ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ) ` x ) / ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) ` x ) ) )
248 128 fveq1d 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ) ` x ) = ( ( x e. ( -u B (,) -u a ) |-> -u ( ( RR _D F ) ` -u x ) ) ` x ) )
249 131 fvmpt2 
 |-  ( ( x e. ( -u B (,) -u a ) /\ -u ( ( RR _D F ) ` -u x ) e. _V ) -> ( ( x e. ( -u B (,) -u a ) |-> -u ( ( RR _D F ) ` -u x ) ) ` x ) = -u ( ( RR _D F ) ` -u x ) )
250 130 249 mpan2 
 |-  ( x e. ( -u B (,) -u a ) -> ( ( x e. ( -u B (,) -u a ) |-> -u ( ( RR _D F ) ` -u x ) ) ` x ) = -u ( ( RR _D F ) ` -u x ) )
251 248 250 sylan9eq 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ) ` x ) = -u ( ( RR _D F ) ` -u x ) )
252 154 fveq1d 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) ` x ) = ( ( x e. ( -u B (,) -u a ) |-> -u ( ( RR _D G ) ` -u x ) ) ` x ) )
253 157 fvmpt2 
 |-  ( ( x e. ( -u B (,) -u a ) /\ -u ( ( RR _D G ) ` -u x ) e. _V ) -> ( ( x e. ( -u B (,) -u a ) |-> -u ( ( RR _D G ) ` -u x ) ) ` x ) = -u ( ( RR _D G ) ` -u x ) )
254 156 253 mpan2 
 |-  ( x e. ( -u B (,) -u a ) -> ( ( x e. ( -u B (,) -u a ) |-> -u ( ( RR _D G ) ` -u x ) ) ` x ) = -u ( ( RR _D G ) ` -u x ) )
255 252 254 sylan9eq 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) ` x ) = -u ( ( RR _D G ) ` -u x ) )
256 251 255 oveq12d 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ) ` x ) / ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) ` x ) ) = ( -u ( ( RR _D F ) ` -u x ) / -u ( ( RR _D G ) ` -u x ) ) )
257 11 ad2antrr 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> -. 0 e. ran ( RR _D G ) )
258 207 necon3bd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( -. 0 e. ran ( RR _D G ) -> ( ( RR _D G ) ` -u x ) =/= 0 ) )
259 257 258 mpd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( ( RR _D G ) ` -u x ) =/= 0 )
260 123 149 259 div2negd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( -u ( ( RR _D F ) ` -u x ) / -u ( ( RR _D G ) ` -u x ) ) = ( ( ( RR _D F ) ` -u x ) / ( ( RR _D G ) ` -u x ) ) )
261 256 260 eqtrd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ) ` x ) / ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) ` x ) ) = ( ( ( RR _D F ) ` -u x ) / ( ( RR _D G ) ` -u x ) ) )
262 261 mpteq2dva 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( x e. ( -u B (,) -u a ) |-> ( ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ) ` x ) / ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) ` x ) ) ) = ( x e. ( -u B (,) -u a ) |-> ( ( ( RR _D F ) ` -u x ) / ( ( RR _D G ) ` -u x ) ) ) )
263 247 262 syl5eq 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( y e. ( -u B (,) -u a ) |-> ( ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ) ` y ) / ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) ` y ) ) ) = ( x e. ( -u B (,) -u a ) |-> ( ( ( RR _D F ) ` -u x ) / ( ( RR _D G ) ` -u x ) ) ) )
264 263 oveq1d 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( y e. ( -u B (,) -u a ) |-> ( ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ) ` y ) / ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) ` y ) ) ) limCC -u B ) = ( ( x e. ( -u B (,) -u a ) |-> ( ( ( RR _D F ) ` -u x ) / ( ( RR _D G ) ` -u x ) ) ) limCC -u B ) )
265 231 264 eleqtrrd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> C e. ( ( y e. ( -u B (,) -u a ) |-> ( ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ) ` y ) / ( ( RR _D ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ) ` y ) ) ) limCC -u B ) )
266 82 84 87 88 89 133 159 186 192 196 213 265 lhop1 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> C e. ( ( y e. ( -u B (,) -u a ) |-> ( ( ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ` y ) / ( ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ` y ) ) ) limCC -u B ) )
267 nffvmpt1 
 |-  F/_ x ( ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ` y )
268 nffvmpt1 
 |-  F/_ x ( ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ` y )
269 267 238 268 nfov 
 |-  F/_ x ( ( ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ` y ) / ( ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ` y ) )
270 nfcv 
 |-  F/_ y ( ( ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ` x ) / ( ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ` x ) )
271 fveq2 
 |-  ( y = x -> ( ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ` y ) = ( ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ` x ) )
272 fveq2 
 |-  ( y = x -> ( ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ` y ) = ( ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ` x ) )
273 271 272 oveq12d 
 |-  ( y = x -> ( ( ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ` y ) / ( ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ` y ) ) = ( ( ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ` x ) / ( ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ` x ) ) )
274 269 270 273 cbvmpt 
 |-  ( y e. ( -u B (,) -u a ) |-> ( ( ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ` y ) / ( ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ` y ) ) ) = ( x e. ( -u B (,) -u a ) |-> ( ( ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ` x ) / ( ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ` x ) ) )
275 fvex 
 |-  ( F ` -u x ) e. _V
276 eqid 
 |-  ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) = ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) )
277 276 fvmpt2 
 |-  ( ( x e. ( -u B (,) -u a ) /\ ( F ` -u x ) e. _V ) -> ( ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ` x ) = ( F ` -u x ) )
278 34 275 277 sylancl 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ` x ) = ( F ` -u x ) )
279 fvex 
 |-  ( G ` -u x ) e. _V
280 eqid 
 |-  ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) = ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) )
281 280 fvmpt2 
 |-  ( ( x e. ( -u B (,) -u a ) /\ ( G ` -u x ) e. _V ) -> ( ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ` x ) = ( G ` -u x ) )
282 34 279 281 sylancl 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ` x ) = ( G ` -u x ) )
283 278 282 oveq12d 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ x e. ( -u B (,) -u a ) ) -> ( ( ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ` x ) / ( ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ` x ) ) = ( ( F ` -u x ) / ( G ` -u x ) ) )
284 283 mpteq2dva 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( x e. ( -u B (,) -u a ) |-> ( ( ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ` x ) / ( ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ` x ) ) ) = ( x e. ( -u B (,) -u a ) |-> ( ( F ` -u x ) / ( G ` -u x ) ) ) )
285 274 284 syl5eq 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( y e. ( -u B (,) -u a ) |-> ( ( ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ` y ) / ( ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ` y ) ) ) = ( x e. ( -u B (,) -u a ) |-> ( ( F ` -u x ) / ( G ` -u x ) ) ) )
286 285 oveq1d 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( y e. ( -u B (,) -u a ) |-> ( ( ( x e. ( -u B (,) -u a ) |-> ( F ` -u x ) ) ` y ) / ( ( x e. ( -u B (,) -u a ) |-> ( G ` -u x ) ) ` y ) ) ) limCC -u B ) = ( ( x e. ( -u B (,) -u a ) |-> ( ( F ` -u x ) / ( G ` -u x ) ) ) limCC -u B ) )
287 266 286 eleqtrd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> C e. ( ( x e. ( -u B (,) -u a ) |-> ( ( F ` -u x ) / ( G ` -u x ) ) ) limCC -u B ) )
288 negeq 
 |-  ( x = -u z -> -u x = -u -u z )
289 288 fveq2d 
 |-  ( x = -u z -> ( F ` -u x ) = ( F ` -u -u z ) )
290 288 fveq2d 
 |-  ( x = -u z -> ( G ` -u x ) = ( G ` -u -u z ) )
291 289 290 oveq12d 
 |-  ( x = -u z -> ( ( F ` -u x ) / ( G ` -u x ) ) = ( ( F ` -u -u z ) / ( G ` -u -u z ) ) )
292 82 adantr 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( a (,) B ) ) -> -u B e. RR )
293 eliooord 
 |-  ( z e. ( a (,) B ) -> ( a < z /\ z < B ) )
294 293 adantl 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( a (,) B ) ) -> ( a < z /\ z < B ) )
295 294 simprd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( a (,) B ) ) -> z < B )
296 24 22 ltnegd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( a (,) B ) ) -> ( z < B <-> -u B < -u z ) )
297 295 296 mpbid 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( a (,) B ) ) -> -u B < -u z )
298 292 297 gtned 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( a (,) B ) ) -> -u z =/= -u B )
299 298 neneqd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( a (,) B ) ) -> -. -u z = -u B )
300 299 pm2.21d 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( a (,) B ) ) -> ( -u z = -u B -> ( ( F ` -u -u z ) / ( G ` -u -u z ) ) = C ) )
301 300 impr 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ ( z e. ( a (,) B ) /\ -u z = -u B ) ) -> ( ( F ` -u -u z ) / ( G ` -u -u z ) ) = C )
302 28 68 81 287 291 301 limcco 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> C e. ( ( z e. ( a (,) B ) |-> ( ( F ` -u -u z ) / ( G ` -u -u z ) ) ) limCC B ) )
303 24 recnd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( a (,) B ) ) -> z e. CC )
304 303 negnegd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( a (,) B ) ) -> -u -u z = z )
305 304 fveq2d 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( a (,) B ) ) -> ( F ` -u -u z ) = ( F ` z ) )
306 304 fveq2d 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( a (,) B ) ) -> ( G ` -u -u z ) = ( G ` z ) )
307 305 306 oveq12d 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( a (,) B ) ) -> ( ( F ` -u -u z ) / ( G ` -u -u z ) ) = ( ( F ` z ) / ( G ` z ) ) )
308 307 mpteq2dva 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( z e. ( a (,) B ) |-> ( ( F ` -u -u z ) / ( G ` -u -u z ) ) ) = ( z e. ( a (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) )
309 308 oveq1d 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( z e. ( a (,) B ) |-> ( ( F ` -u -u z ) / ( G ` -u -u z ) ) ) limCC B ) = ( ( z e. ( a (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) limCC B ) )
310 47 resmptd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) |` ( a (,) B ) ) = ( z e. ( a (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) )
311 310 oveq1d 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) |` ( a (,) B ) ) limCC B ) = ( ( z e. ( a (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) limCC B ) )
312 fss 
 |-  ( ( F : ( A (,) B ) --> RR /\ RR C_ CC ) -> F : ( A (,) B ) --> CC )
313 94 57 312 sylancl 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> F : ( A (,) B ) --> CC )
314 313 ffvelrnda 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( A (,) B ) ) -> ( F ` z ) e. CC )
315 59 ffvelrnda 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( A (,) B ) ) -> ( G ` z ) e. CC )
316 10 ad2antrr 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( A (,) B ) ) -> -. 0 e. ran G )
317 56 ffnd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> G Fn ( A (,) B ) )
318 fnfvelrn 
 |-  ( ( G Fn ( A (,) B ) /\ z e. ( A (,) B ) ) -> ( G ` z ) e. ran G )
319 317 318 sylan 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( A (,) B ) ) -> ( G ` z ) e. ran G )
320 eleq1 
 |-  ( ( G ` z ) = 0 -> ( ( G ` z ) e. ran G <-> 0 e. ran G ) )
321 319 320 syl5ibcom 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( A (,) B ) ) -> ( ( G ` z ) = 0 -> 0 e. ran G ) )
322 321 necon3bd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( A (,) B ) ) -> ( -. 0 e. ran G -> ( G ` z ) =/= 0 ) )
323 316 322 mpd 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( A (,) B ) ) -> ( G ` z ) =/= 0 )
324 314 315 323 divcld 
 |-  ( ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) /\ z e. ( A (,) B ) ) -> ( ( F ` z ) / ( G ` z ) ) e. CC )
325 324 fmpttd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) : ( A (,) B ) --> CC )
326 ioossre 
 |-  ( A (,) B ) C_ RR
327 326 57 sstri 
 |-  ( A (,) B ) C_ CC
328 327 a1i 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( A (,) B ) C_ CC )
329 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( ( A (,) B ) u. { B } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( A (,) B ) u. { B } ) )
330 ssun2 
 |-  { B } C_ ( ( a (,) B ) u. { B } )
331 snssg 
 |-  ( B e. RR -> ( B e. ( ( a (,) B ) u. { B } ) <-> { B } C_ ( ( a (,) B ) u. { B } ) ) )
332 78 331 syl 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( B e. ( ( a (,) B ) u. { B } ) <-> { B } C_ ( ( a (,) B ) u. { B } ) ) )
333 330 332 mpbiri 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> B e. ( ( a (,) B ) u. { B } ) )
334 105 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
335 326 a1i 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( A (,) B ) C_ RR )
336 78 snssd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> { B } C_ RR )
337 335 336 unssd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( A (,) B ) u. { B } ) C_ RR )
338 337 57 sstrdi 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( A (,) B ) u. { B } ) C_ CC )
339 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( ( A (,) B ) u. { B } ) C_ CC ) -> ( ( TopOpen ` CCfld ) |`t ( ( A (,) B ) u. { B } ) ) e. ( TopOn ` ( ( A (,) B ) u. { B } ) ) )
340 334 338 339 sylancr 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( TopOpen ` CCfld ) |`t ( ( A (,) B ) u. { B } ) ) e. ( TopOn ` ( ( A (,) B ) u. { B } ) ) )
341 topontop 
 |-  ( ( ( TopOpen ` CCfld ) |`t ( ( A (,) B ) u. { B } ) ) e. ( TopOn ` ( ( A (,) B ) u. { B } ) ) -> ( ( TopOpen ` CCfld ) |`t ( ( A (,) B ) u. { B } ) ) e. Top )
342 340 341 syl 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( TopOpen ` CCfld ) |`t ( ( A (,) B ) u. { B } ) ) e. Top )
343 indi 
 |-  ( ( a (,) +oo ) i^i ( ( A (,) B ) u. { B } ) ) = ( ( ( a (,) +oo ) i^i ( A (,) B ) ) u. ( ( a (,) +oo ) i^i { B } ) )
344 pnfxr 
 |-  +oo e. RR*
345 344 a1i 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> +oo e. RR* )
346 14 adantr 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> B e. RR* )
347 iooin 
 |-  ( ( ( a e. RR* /\ +oo e. RR* ) /\ ( A e. RR* /\ B e. RR* ) ) -> ( ( a (,) +oo ) i^i ( A (,) B ) ) = ( if ( a <_ A , A , a ) (,) if ( +oo <_ B , +oo , B ) ) )
348 43 345 42 346 347 syl22anc 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( a (,) +oo ) i^i ( A (,) B ) ) = ( if ( a <_ A , A , a ) (,) if ( +oo <_ B , +oo , B ) ) )
349 xrltnle 
 |-  ( ( A e. RR* /\ a e. RR* ) -> ( A < a <-> -. a <_ A ) )
350 42 43 349 syl2anc 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( A < a <-> -. a <_ A ) )
351 44 350 mpbid 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> -. a <_ A )
352 351 iffalsed 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> if ( a <_ A , A , a ) = a )
353 78 ltpnfd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> B < +oo )
354 xrltnle 
 |-  ( ( B e. RR* /\ +oo e. RR* ) -> ( B < +oo <-> -. +oo <_ B ) )
355 346 344 354 sylancl 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( B < +oo <-> -. +oo <_ B ) )
356 353 355 mpbid 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> -. +oo <_ B )
357 356 iffalsed 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> if ( +oo <_ B , +oo , B ) = B )
358 352 357 oveq12d 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( if ( a <_ A , A , a ) (,) if ( +oo <_ B , +oo , B ) ) = ( a (,) B ) )
359 348 358 eqtrd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( a (,) +oo ) i^i ( A (,) B ) ) = ( a (,) B ) )
360 elioopnf 
 |-  ( a e. RR* -> ( B e. ( a (,) +oo ) <-> ( B e. RR /\ a < B ) ) )
361 43 360 syl 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( B e. ( a (,) +oo ) <-> ( B e. RR /\ a < B ) ) )
362 78 85 361 mpbir2and 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> B e. ( a (,) +oo ) )
363 362 snssd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> { B } C_ ( a (,) +oo ) )
364 sseqin2 
 |-  ( { B } C_ ( a (,) +oo ) <-> ( ( a (,) +oo ) i^i { B } ) = { B } )
365 363 364 sylib 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( a (,) +oo ) i^i { B } ) = { B } )
366 359 365 uneq12d 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( ( a (,) +oo ) i^i ( A (,) B ) ) u. ( ( a (,) +oo ) i^i { B } ) ) = ( ( a (,) B ) u. { B } ) )
367 343 366 syl5eq 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( a (,) +oo ) i^i ( ( A (,) B ) u. { B } ) ) = ( ( a (,) B ) u. { B } ) )
368 retop 
 |-  ( topGen ` ran (,) ) e. Top
369 reex 
 |-  RR e. _V
370 369 ssex 
 |-  ( ( ( A (,) B ) u. { B } ) C_ RR -> ( ( A (,) B ) u. { B } ) e. _V )
371 337 370 syl 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( A (,) B ) u. { B } ) e. _V )
372 iooretop 
 |-  ( a (,) +oo ) e. ( topGen ` ran (,) )
373 372 a1i 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( a (,) +oo ) e. ( topGen ` ran (,) ) )
374 elrestr 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( ( A (,) B ) u. { B } ) e. _V /\ ( a (,) +oo ) e. ( topGen ` ran (,) ) ) -> ( ( a (,) +oo ) i^i ( ( A (,) B ) u. { B } ) ) e. ( ( topGen ` ran (,) ) |`t ( ( A (,) B ) u. { B } ) ) )
375 368 371 373 374 mp3an2i 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( a (,) +oo ) i^i ( ( A (,) B ) u. { B } ) ) e. ( ( topGen ` ran (,) ) |`t ( ( A (,) B ) u. { B } ) ) )
376 367 375 eqeltrrd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( a (,) B ) u. { B } ) e. ( ( topGen ` ran (,) ) |`t ( ( A (,) B ) u. { B } ) ) )
377 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
378 105 377 rerest 
 |-  ( ( ( A (,) B ) u. { B } ) C_ RR -> ( ( TopOpen ` CCfld ) |`t ( ( A (,) B ) u. { B } ) ) = ( ( topGen ` ran (,) ) |`t ( ( A (,) B ) u. { B } ) ) )
379 337 378 syl 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( TopOpen ` CCfld ) |`t ( ( A (,) B ) u. { B } ) ) = ( ( topGen ` ran (,) ) |`t ( ( A (,) B ) u. { B } ) ) )
380 376 379 eleqtrrd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( a (,) B ) u. { B } ) e. ( ( TopOpen ` CCfld ) |`t ( ( A (,) B ) u. { B } ) ) )
381 isopn3i 
 |-  ( ( ( ( TopOpen ` CCfld ) |`t ( ( A (,) B ) u. { B } ) ) e. Top /\ ( ( a (,) B ) u. { B } ) e. ( ( TopOpen ` CCfld ) |`t ( ( A (,) B ) u. { B } ) ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( A (,) B ) u. { B } ) ) ) ` ( ( a (,) B ) u. { B } ) ) = ( ( a (,) B ) u. { B } ) )
382 342 380 381 syl2anc 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( A (,) B ) u. { B } ) ) ) ` ( ( a (,) B ) u. { B } ) ) = ( ( a (,) B ) u. { B } ) )
383 333 382 eleqtrrd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> B e. ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( A (,) B ) u. { B } ) ) ) ` ( ( a (,) B ) u. { B } ) ) )
384 325 47 328 105 329 383 limcres 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) |` ( a (,) B ) ) limCC B ) = ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) limCC B ) )
385 309 311 384 3eqtr2d 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> ( ( z e. ( a (,) B ) |-> ( ( F ` -u -u z ) / ( G ` -u -u z ) ) ) limCC B ) = ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) limCC B ) )
386 302 385 eleqtrd 
 |-  ( ( ph /\ ( a e. RR /\ ( A < a /\ a < B ) ) ) -> C e. ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) limCC B ) )
387 18 386 rexlimddv 
 |-  ( ph -> C e. ( ( z e. ( A (,) B ) |-> ( ( F ` z ) / ( G ` z ) ) ) limCC B ) )