Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  limclner Structured version   Unicode version

Theorem limclner 31860
Description: For a limit point, both from the left and from the right, of the domain, the limit of the function exits only if the left and the right limits are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
limclner.k  |-  K  =  ( TopOpen ` fld )
limclner.a  |-  ( ph  ->  A  C_  RR )
limclner.j  |-  J  =  ( topGen `  ran  (,) )
limclner.f  |-  ( ph  ->  F : A --> CC )
limclner.blp1  |-  ( ph  ->  B  e.  ( (
limPt `  J ) `  ( A  i^i  ( -oo (,) B ) ) ) )
limclner.blp2  |-  ( ph  ->  B  e.  ( (
limPt `  J ) `  ( A  i^i  ( B (,) +oo ) ) ) )
limclner.l  |-  ( ph  ->  L  e.  ( ( F  |`  ( -oo (,) B ) ) lim CC  B ) )
limclner.r  |-  ( ph  ->  R  e.  ( ( F  |`  ( B (,) +oo ) ) lim CC  B ) )
limclner.lner  |-  ( ph  ->  L  =/=  R )
Assertion
Ref Expression
limclner  |-  ( ph  ->  ( F lim CC  B
)  =  (/) )

Proof of Theorem limclner
Dummy variables  a 
b  u  v  z  w  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 limccl 22405 . . . . . . . . . . . . 13  |-  ( ( F  |`  ( B (,) +oo ) ) lim CC  B )  C_  CC
2 limclner.r . . . . . . . . . . . . 13  |-  ( ph  ->  R  e.  ( ( F  |`  ( B (,) +oo ) ) lim CC  B ) )
31, 2sseldi 3497 . . . . . . . . . . . 12  |-  ( ph  ->  R  e.  CC )
43ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  CC )  /\  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( ( w  =/=  B  /\  ( abs `  ( w  -  B ) )  < 
z )  ->  ( abs `  ( ( F `
 w )  -  x ) )  < 
y ) )  ->  R  e.  CC )
5 limccl 22405 . . . . . . . . . . . . 13  |-  ( ( F  |`  ( -oo (,) B ) ) lim CC  B )  C_  CC
6 limclner.l . . . . . . . . . . . . 13  |-  ( ph  ->  L  e.  ( ( F  |`  ( -oo (,) B ) ) lim CC  B ) )
75, 6sseldi 3497 . . . . . . . . . . . 12  |-  ( ph  ->  L  e.  CC )
87ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  CC )  /\  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( ( w  =/=  B  /\  ( abs `  ( w  -  B ) )  < 
z )  ->  ( abs `  ( ( F `
 w )  -  x ) )  < 
y ) )  ->  L  e.  CC )
94, 8subcld 9950 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  CC )  /\  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( ( w  =/=  B  /\  ( abs `  ( w  -  B ) )  < 
z )  ->  ( abs `  ( ( F `
 w )  -  x ) )  < 
y ) )  -> 
( R  -  L
)  e.  CC )
10 limclner.lner . . . . . . . . . . . . 13  |-  ( ph  ->  L  =/=  R )
1110necomd 2728 . . . . . . . . . . . 12  |-  ( ph  ->  R  =/=  L )
1211ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  CC )  /\  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( ( w  =/=  B  /\  ( abs `  ( w  -  B ) )  < 
z )  ->  ( abs `  ( ( F `
 w )  -  x ) )  < 
y ) )  ->  R  =/=  L )
134, 8, 12subne0d 9959 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  CC )  /\  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( ( w  =/=  B  /\  ( abs `  ( w  -  B ) )  < 
z )  ->  ( abs `  ( ( F `
 w )  -  x ) )  < 
y ) )  -> 
( R  -  L
)  =/=  0 )
149, 13absrpcld 13291 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  CC )  /\  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( ( w  =/=  B  /\  ( abs `  ( w  -  B ) )  < 
z )  ->  ( abs `  ( ( F `
 w )  -  x ) )  < 
y ) )  -> 
( abs `  ( R  -  L )
)  e.  RR+ )
15 4re 10633 . . . . . . . . . . 11  |-  4  e.  RR
16 4pos 10652 . . . . . . . . . . 11  |-  0  <  4
1715, 16elrpii 11248 . . . . . . . . . 10  |-  4  e.  RR+
1817a1i 11 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  CC )  /\  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( ( w  =/=  B  /\  ( abs `  ( w  -  B ) )  < 
z )  ->  ( abs `  ( ( F `
 w )  -  x ) )  < 
y ) )  -> 
4  e.  RR+ )
1914, 18rpdivcld 11298 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  CC )  /\  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( ( w  =/=  B  /\  ( abs `  ( w  -  B ) )  < 
z )  ->  ( abs `  ( ( F `
 w )  -  x ) )  < 
y ) )  -> 
( ( abs `  ( R  -  L )
)  /  4 )  e.  RR+ )
20 nfv 1708 . . . . . . . . . . 11  |-  F/ y ( ph  /\  x  e.  CC )
21 nfra1 2838 . . . . . . . . . . 11  |-  F/ y A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( (
w  =/=  B  /\  ( abs `  ( w  -  B ) )  <  z )  -> 
( abs `  (
( F `  w
)  -  x ) )  <  y )
2220, 21nfan 1929 . . . . . . . . . 10  |-  F/ y ( ( ph  /\  x  e.  CC )  /\  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( (
w  =/=  B  /\  ( abs `  ( w  -  B ) )  <  z )  -> 
( abs `  (
( F `  w
)  -  x ) )  <  y ) )
23 nfv 1708 . . . . . . . . . 10  |-  F/ y ( ( ( abs `  ( R  -  L
) )  /  4
)  e.  RR+  ->  E. a  e.  A  E. b  e.  A  ( abs `  ( R  -  L ) )  < 
( 4  x.  (
( abs `  ( R  -  L )
)  /  4 ) ) )
2422, 23nfim 1921 . . . . . . . . 9  |-  F/ y ( ( ( ph  /\  x  e.  CC )  /\  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( ( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  ->  ( (
( abs `  ( R  -  L )
)  /  4 )  e.  RR+  ->  E. a  e.  A  E. b  e.  A  ( abs `  ( R  -  L
) )  <  (
4  x.  ( ( abs `  ( R  -  L ) )  /  4 ) ) ) )
25 ovex 6324 . . . . . . . . 9  |-  ( ( abs `  ( R  -  L ) )  /  4 )  e. 
_V
26 eleq1 2529 . . . . . . . . . . 11  |-  ( y  =  ( ( abs `  ( R  -  L
) )  /  4
)  ->  ( y  e.  RR+  <->  ( ( abs `  ( R  -  L
) )  /  4
)  e.  RR+ )
)
27 oveq2 6304 . . . . . . . . . . . . 13  |-  ( y  =  ( ( abs `  ( R  -  L
) )  /  4
)  ->  ( 4  x.  y )  =  ( 4  x.  (
( abs `  ( R  -  L )
)  /  4 ) ) )
2827breq2d 4468 . . . . . . . . . . . 12  |-  ( y  =  ( ( abs `  ( R  -  L
) )  /  4
)  ->  ( ( abs `  ( R  -  L ) )  < 
( 4  x.  y
)  <->  ( abs `  ( R  -  L )
)  <  ( 4  x.  ( ( abs `  ( R  -  L
) )  /  4
) ) ) )
29282rexbidv 2975 . . . . . . . . . . 11  |-  ( y  =  ( ( abs `  ( R  -  L
) )  /  4
)  ->  ( E. a  e.  A  E. b  e.  A  ( abs `  ( R  -  L ) )  < 
( 4  x.  y
)  <->  E. a  e.  A  E. b  e.  A  ( abs `  ( R  -  L ) )  <  ( 4  x.  ( ( abs `  ( R  -  L )
)  /  4 ) ) ) )
3026, 29imbi12d 320 . . . . . . . . . 10  |-  ( y  =  ( ( abs `  ( R  -  L
) )  /  4
)  ->  ( (
y  e.  RR+  ->  E. a  e.  A  E. b  e.  A  ( abs `  ( R  -  L ) )  < 
( 4  x.  y
) )  <->  ( (
( abs `  ( R  -  L )
)  /  4 )  e.  RR+  ->  E. a  e.  A  E. b  e.  A  ( abs `  ( R  -  L
) )  <  (
4  x.  ( ( abs `  ( R  -  L ) )  /  4 ) ) ) ) )
3130imbi2d 316 . . . . . . . . 9  |-  ( y  =  ( ( abs `  ( R  -  L
) )  /  4
)  ->  ( (
( ( ph  /\  x  e.  CC )  /\  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( (
w  =/=  B  /\  ( abs `  ( w  -  B ) )  <  z )  -> 
( abs `  (
( F `  w
)  -  x ) )  <  y ) )  ->  ( y  e.  RR+  ->  E. a  e.  A  E. b  e.  A  ( abs `  ( R  -  L
) )  <  (
4  x.  y ) ) )  <->  ( (
( ph  /\  x  e.  CC )  /\  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( ( w  =/=  B  /\  ( abs `  ( w  -  B ) )  < 
z )  ->  ( abs `  ( ( F `
 w )  -  x ) )  < 
y ) )  -> 
( ( ( abs `  ( R  -  L
) )  /  4
)  e.  RR+  ->  E. a  e.  A  E. b  e.  A  ( abs `  ( R  -  L ) )  < 
( 4  x.  (
( abs `  ( R  -  L )
)  /  4 ) ) ) ) ) )
32 simpll 753 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  CC )  /\  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( (
w  =/=  B  /\  ( abs `  ( w  -  B ) )  <  z )  -> 
( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  y  e.  RR+ )  ->  ( ph  /\  x  e.  CC ) )
33 simpr 461 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  CC )  /\  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( (
w  =/=  B  /\  ( abs `  ( w  -  B ) )  <  z )  -> 
( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  y  e.  RR+ )  ->  y  e.  RR+ )
34 rspa 2824 . . . . . . . . . . . 12  |-  ( ( A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( (
w  =/=  B  /\  ( abs `  ( w  -  B ) )  <  z )  -> 
( abs `  (
( F `  w
)  -  x ) )  <  y )  /\  y  e.  RR+ )  ->  E. z  e.  RR+  A. w  e.  A  ( ( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )
3534adantll 713 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  CC )  /\  A. y  e.  RR+  E. z  e.  RR+  A. w  e.  A  ( (
w  =/=  B  /\  ( abs `  ( w  -  B ) )  <  z )  -> 
( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  y  e.  RR+ )  ->  E. z  e.  RR+  A. w  e.  A  ( ( w  =/=  B  /\  ( abs `  ( w  -  B ) )  < 
z )  ->  ( abs `  ( ( F `
 w )  -  x ) )  < 
y ) )
36 limclner.f . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  F : A --> CC )
37 fresin 5760 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F : A --> CC  ->  ( F  |`  ( -oo (,) B ) ) : ( A  i^i  ( -oo (,) B ) ) --> CC )
3836, 37syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( F  |`  ( -oo (,) B ) ) : ( A  i^i  ( -oo (,) B ) ) --> CC )
39 inss2 3715 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( A  i^i  ( -oo (,) B ) )  C_  ( -oo (,) B )
40 ioosscn 31730 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( -oo (,) B )  C_  CC
4139, 40sstri 3508 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A  i^i  ( -oo (,) B ) )  C_  CC
4241a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( A  i^i  ( -oo (,) B ) ) 
C_  CC )
43 limclner.j . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  J  =  ( topGen `  ran  (,) )
44 retop 21394 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( topGen ` 
ran  (,) )  e.  Top
4543, 44eqeltri 2541 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  J  e. 
Top
46 ioossre 11611 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( -oo (,) B )  C_  RR
4739, 46sstri 3508 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A  i^i  ( -oo (,) B ) )  C_  RR
48 uniretop 21395 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  RR  =  U. ( topGen `  ran  (,) )
4943unieqi 4260 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  U. J  =  U. ( topGen `  ran  (,) )
5048, 49eqtr4i 2489 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  RR  =  U. J
5150lpss 19770 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( J  e.  Top  /\  ( A  i^i  ( -oo (,) B ) ) 
C_  RR )  -> 
( ( limPt `  J
) `  ( A  i^i  ( -oo (,) B
) ) )  C_  RR )
5245, 47, 51mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
limPt `  J ) `  ( A  i^i  ( -oo (,) B ) ) )  C_  RR
53 limclner.blp1 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  B  e.  ( (
limPt `  J ) `  ( A  i^i  ( -oo (,) B ) ) ) )
5452, 53sseldi 3497 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  B  e.  RR )
5554recnd 9639 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  B  e.  CC )
5638, 42, 55ellimc3 22409 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( L  e.  ( ( F  |`  ( -oo (,) B ) ) lim
CC  B )  <->  ( L  e.  CC  /\  A. y  e.  RR+  E. v  e.  RR+  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  v )  ->  ( abs `  (
( ( F  |`  ( -oo (,) B ) ) `  w )  -  L ) )  <  y ) ) ) )
576, 56mpbid 210 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( L  e.  CC  /\ 
A. y  e.  RR+  E. v  e.  RR+  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) ) )
5857simprd 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A. y  e.  RR+  E. v  e.  RR+  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )
5958r19.21bi 2826 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  RR+ )  ->  E. v  e.  RR+  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )
60593ad2ant1 1017 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  ( (
w  =/=  B  /\  ( abs `  ( w  -  B ) )  <  z )  -> 
( abs `  (
( F `  w
)  -  x ) )  <  y ) )  ->  E. v  e.  RR+  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )
61 simp11l 1107 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )  ->  ph )
62 simp12 1027 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )  ->  z  e.  RR+ )
63 simp2 997 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )  ->  v  e.  RR+ )
64 ifcl 3986 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( z  e.  RR+  /\  v  e.  RR+ )  ->  if ( z  <_  v ,  z ,  v )  e.  RR+ )
65643adant1 1014 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  if ( z  <_  v ,  z ,  v )  e.  RR+ )
66 inss1 3714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( limPt `  K ) `  ( A  i^i  ( -oo (,) B ) ) )  i^i  RR ) 
C_  ( ( limPt `  K ) `  ( A  i^i  ( -oo (,) B ) ) )
6766a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( ( ( limPt `  K ) `  ( A  i^i  ( -oo (,) B ) ) )  i^i  RR )  C_  ( ( limPt `  K
) `  ( A  i^i  ( -oo (,) B
) ) ) )
68 limclner.k . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  K  =  ( TopOpen ` fld )
6968cnfldtop 21417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  K  e. 
Top
7069a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  K  e.  Top )
71 ax-resscn 9566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  RR  C_  CC
7271a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  RR  C_  CC )
7347a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( A  i^i  ( -oo (,) B ) ) 
C_  RR )
74 unicntop 31634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  CC  =  U. ( TopOpen ` fld )
7568unieqi 4260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  U. K  =  U. ( TopOpen ` fld )
7674, 75eqtr4i 2489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  CC  =  U. K
7768tgioo2 21434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( topGen ` 
ran  (,) )  =  ( Kt  RR )
7843, 77eqtri 2486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  J  =  ( Kt  RR )
7976, 78restlp 19811 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( K  e.  Top  /\  RR  C_  CC  /\  ( A  i^i  ( -oo (,) B ) )  C_  RR )  ->  ( (
limPt `  J ) `  ( A  i^i  ( -oo (,) B ) ) )  =  ( ( ( limPt `  K ) `  ( A  i^i  ( -oo (,) B ) ) )  i^i  RR ) )
8070, 72, 73, 79syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( ( limPt `  J
) `  ( A  i^i  ( -oo (,) B
) ) )  =  ( ( ( limPt `  K ) `  ( A  i^i  ( -oo (,) B ) ) )  i^i  RR ) )
8168eqcomi 2470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( TopOpen ` fld )  =  K
8281fveq2i 5875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( limPt `  ( TopOpen ` fld ) )  =  (
limPt `  K )
8382fveq1i 5873 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
limPt `  ( TopOpen ` fld ) ) `  ( A  i^i  ( -oo (,) B ) ) )  =  ( ( limPt `  K ) `  ( A  i^i  ( -oo (,) B ) ) )
8483a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( ( limPt `  ( TopOpen
` fld
) ) `  ( A  i^i  ( -oo (,) B ) ) )  =  ( ( limPt `  K ) `  ( A  i^i  ( -oo (,) B ) ) ) )
8567, 80, 843sstr4d 3542 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( limPt `  J
) `  ( A  i^i  ( -oo (,) B
) ) )  C_  ( ( limPt `  ( TopOpen
` fld
) ) `  ( A  i^i  ( -oo (,) B ) ) ) )
8685, 53sseldd 3500 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  B  e.  ( (
limPt `  ( TopOpen ` fld ) ) `  ( A  i^i  ( -oo (,) B ) ) ) )
8742, 55islpcn 31848 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( B  e.  ( ( limPt `  ( TopOpen ` fld ) ) `  ( A  i^i  ( -oo (,) B ) ) )  <->  A. u  e.  RR+  E. a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } ) ( abs `  ( a  -  B
) )  <  u
) )
8886, 87mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  A. u  e.  RR+  E. a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } ) ( abs `  ( a  -  B ) )  <  u )
89883ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  A. u  e.  RR+  E. a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } ) ( abs `  ( a  -  B ) )  <  u )
90 breq2 4460 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( u  =  if ( z  <_  v ,  z ,  v )  -> 
( ( abs `  (
a  -  B ) )  <  u  <->  ( abs `  ( a  -  B
) )  <  if ( z  <_  v ,  z ,  v ) ) )
9190rexbidv 2968 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( u  =  if ( z  <_  v ,  z ,  v )  -> 
( E. a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } ) ( abs `  ( a  -  B
) )  <  u  <->  E. a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } ) ( abs `  ( a  -  B ) )  <  if ( z  <_  v ,  z ,  v ) ) )
9291rspcva 3208 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( if ( z  <_ 
v ,  z ,  v )  e.  RR+  /\ 
A. u  e.  RR+  E. a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } ) ( abs `  ( a  -  B ) )  <  u )  ->  E. a  e.  (
( A  i^i  ( -oo (,) B ) ) 
\  { B }
) ( abs `  (
a  -  B ) )  <  if ( z  <_  v , 
z ,  v ) )
9365, 89, 92syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  E. a  e.  ( ( A  i^i  ( -oo (,) B ) ) 
\  { B }
) ( abs `  (
a  -  B ) )  <  if ( z  <_  v , 
z ,  v ) )
94 eldifi 3622 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  -> 
a  e.  ( A  i^i  ( -oo (,) B ) ) )
9547, 94sseldi 3497 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  -> 
a  e.  RR )
9672sselda 3499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  a  e.  RR )  ->  a  e.  CC )
9755adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  a  e.  RR )  ->  B  e.  CC )
9896, 97subcld 9950 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  a  e.  RR )  ->  ( a  -  B )  e.  CC )
9998abscld 13279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  a  e.  RR )  ->  ( abs `  ( a  -  B
) )  e.  RR )
100993ad2antl1 1158 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  ->  ( abs `  ( a  -  B ) )  e.  RR )
101100adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  /\  ( abs `  ( a  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
( abs `  (
a  -  B ) )  e.  RR )
10265rpred 11281 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  if ( z  <_  v ,  z ,  v )  e.  RR )
103102ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  /\  ( abs `  ( a  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  ->  if ( z  <_  v ,  z ,  v )  e.  RR )
104 rpre 11251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  e.  RR+  ->  z  e.  RR )
1051043ad2ant2 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  z  e.  RR )
106105ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  /\  ( abs `  ( a  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
z  e.  RR )
107 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  /\  ( abs `  ( a  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
( abs `  (
a  -  B ) )  <  if ( z  <_  v , 
z ,  v ) )
108 rpre 11251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( v  e.  RR+  ->  v  e.  RR )
109 min1 11414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( z  e.  RR  /\  v  e.  RR )  ->  if ( z  <_ 
v ,  z ,  v )  <_  z
)
110104, 108, 109syl2an 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( z  e.  RR+  /\  v  e.  RR+ )  ->  if ( z  <_  v ,  z ,  v )  <_  z )
1111103adant1 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  if ( z  <_  v ,  z ,  v )  <_ 
z )
112111ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  /\  ( abs `  ( a  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  ->  if ( z  <_  v ,  z ,  v )  <_  z )
113101, 103, 106, 107, 112ltletrd 9759 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  /\  ( abs `  ( a  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
( abs `  (
a  -  B ) )  <  z )
114108adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( z  e.  RR+  /\  v  e.  RR+ )  ->  v  e.  RR )
1151143adant1 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  v  e.  RR )
116115ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  /\  ( abs `  ( a  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
v  e.  RR )
117 min2 11415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( z  e.  RR  /\  v  e.  RR )  ->  if ( z  <_ 
v ,  z ,  v )  <_  v
)
118104, 108, 117syl2an 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( z  e.  RR+  /\  v  e.  RR+ )  ->  if ( z  <_  v ,  z ,  v )  <_  v )
1191183adant1 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  if ( z  <_  v ,  z ,  v )  <_ 
v )
120119ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  /\  ( abs `  ( a  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  ->  if ( z  <_  v ,  z ,  v )  <_  v )
121101, 103, 116, 107, 120ltletrd 9759 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  /\  ( abs `  ( a  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
( abs `  (
a  -  B ) )  <  v )
122113, 121jca 532 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  /\  ( abs `  ( a  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
( ( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v ) )
123122ex 434 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  ->  (
( abs `  (
a  -  B ) )  <  if ( z  <_  v , 
z ,  v )  ->  ( ( abs `  ( a  -  B
) )  <  z  /\  ( abs `  (
a  -  B ) )  <  v ) ) )
12495, 123sylan2 474 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } ) )  -> 
( ( abs `  (
a  -  B ) )  <  if ( z  <_  v , 
z ,  v )  ->  ( ( abs `  ( a  -  B
) )  <  z  /\  ( abs `  (
a  -  B ) )  <  v ) ) )
125124reximdva 2932 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  ( E. a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } ) ( abs `  ( a  -  B
) )  <  if ( z  <_  v ,  z ,  v )  ->  E. a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } ) ( ( abs `  ( a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  < 
v ) ) )
12693, 125mpd 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  E. a  e.  ( ( A  i^i  ( -oo (,) B ) ) 
\  { B }
) ( ( abs `  ( a  -  B
) )  <  z  /\  ( abs `  (
a  -  B ) )  <  v ) )
12761, 62, 63, 126syl3anc 1228 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )  ->  E. a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } ) ( ( abs `  ( a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  < 
v ) )
128 nfv 1708 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ a ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )
129 nfre1 2918 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ a E. a  e.  A  ( ( abs `  (
( F `  a
)  -  x ) )  <  y  /\  ( abs `  ( ( F `  a )  -  L ) )  <  y )
130 inss1 3714 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A  i^i  ( -oo (,) B ) )  C_  A
131130, 94sseldi 3497 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  -> 
a  e.  A )
1321313ad2ant2 1018 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )  /\  a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  (
( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v ) )  ->  a  e.  A
)
133 simp113 1127 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )  /\  a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  (
( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v ) )  ->  A. w  e.  A  ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  z
)  ->  ( abs `  ( ( F `  w )  -  x
) )  <  y
) )
134 eldifsni 4158 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  -> 
a  =/=  B )
135134adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  ( ( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v ) )  ->  a  =/=  B
)
136 simprl 756 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  ( ( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v ) )  ->  ( abs `  (
a  -  B ) )  <  z )
137135, 136jca 532 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  ( ( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v ) )  ->  ( a  =/= 
B  /\  ( abs `  ( a  -  B
) )  <  z
) )
1381373adant1 1014 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )  /\  a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  (
( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v ) )  ->  ( a  =/= 
B  /\  ( abs `  ( a  -  B
) )  <  z
) )
139 neeq1 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w  =  a  ->  (
w  =/=  B  <->  a  =/=  B ) )
140 oveq1 6303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( w  =  a  ->  (
w  -  B )  =  ( a  -  B ) )
141140fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( w  =  a  ->  ( abs `  ( w  -  B ) )  =  ( abs `  (
a  -  B ) ) )
142141breq1d 4466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w  =  a  ->  (
( abs `  (
w  -  B ) )  <  z  <->  ( abs `  ( a  -  B
) )  <  z
) )
143139, 142anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( w  =  a  ->  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  <-> 
( a  =/=  B  /\  ( abs `  (
a  -  B ) )  <  z ) ) )
144 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( w  =  a  ->  ( F `  w )  =  ( F `  a ) )
145144oveq1d 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( w  =  a  ->  (
( F `  w
)  -  x )  =  ( ( F `
 a )  -  x ) )
146145fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w  =  a  ->  ( abs `  ( ( F `
 w )  -  x ) )  =  ( abs `  (
( F `  a
)  -  x ) ) )
147146breq1d 4466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( w  =  a  ->  (
( abs `  (
( F `  w
)  -  x ) )  <  y  <->  ( abs `  ( ( F `  a )  -  x
) )  <  y
) )
148143, 147imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  =  a  ->  (
( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  z
)  ->  ( abs `  ( ( F `  w )  -  x
) )  <  y
)  <->  ( ( a  =/=  B  /\  ( abs `  ( a  -  B ) )  < 
z )  ->  ( abs `  ( ( F `
 a )  -  x ) )  < 
y ) ) )
149148rspcva 3208 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( a  e.  A  /\  A. w  e.  A  ( ( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  ->  ( (
a  =/=  B  /\  ( abs `  ( a  -  B ) )  <  z )  -> 
( abs `  (
( F `  a
)  -  x ) )  <  y ) )
150149imp 429 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( a  e.  A  /\  A. w  e.  A  ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  z
)  ->  ( abs `  ( ( F `  w )  -  x
) )  <  y
) )  /\  (
a  =/=  B  /\  ( abs `  ( a  -  B ) )  <  z ) )  ->  ( abs `  (
( F `  a
)  -  x ) )  <  y )
151132, 133, 138, 150syl21anc 1227 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )  /\  a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  (
( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v ) )  ->  ( abs `  (
( F `  a
)  -  x ) )  <  y )
152943ad2ant2 1018 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )  /\  a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  (
( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v ) )  ->  a  e.  ( A  i^i  ( -oo (,) B ) ) )
153613ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )  /\  a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  (
( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v ) )  ->  ph )
154 simp13 1028 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )  /\  a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  (
( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v ) )  ->  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  v )  ->  ( abs `  (
( ( F  |`  ( -oo (,) B ) ) `  w )  -  L ) )  <  y ) )
155 nfv 1708 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  F/ w ph
156 nfra1 2838 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  F/ w A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  v )  ->  ( abs `  (
( ( F  |`  ( -oo (,) B ) ) `  w )  -  L ) )  <  y )
157155, 156nfan 1929 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/ w
( ph  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )
158 elinel2 31626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( w  e.  ( A  i^i  ( -oo (,) B ) )  ->  w  e.  ( -oo (,) B ) )
159 fvres 5886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( w  e.  ( -oo (,) B )  ->  (
( F  |`  ( -oo (,) B ) ) `
 w )  =  ( F `  w
) )
160158, 159syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( w  e.  ( A  i^i  ( -oo (,) B ) )  ->  ( ( F  |`  ( -oo (,) B ) ) `  w )  =  ( F `  w ) )
161160eqcomd 2465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( w  e.  ( A  i^i  ( -oo (,) B ) )  ->  ( F `  w )  =  ( ( F  |`  ( -oo (,) B ) ) `
 w ) )
162161oveq1d 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( w  e.  ( A  i^i  ( -oo (,) B ) )  ->  ( ( F `  w )  -  L )  =  ( ( ( F  |`  ( -oo (,) B ) ) `  w )  -  L ) )
163162fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( w  e.  ( A  i^i  ( -oo (,) B ) )  ->  ( abs `  ( ( F `  w )  -  L
) )  =  ( abs `  ( ( ( F  |`  ( -oo (,) B ) ) `
 w )  -  L ) ) )
1641633ad2ant2 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  A. w  e.  ( A  i^i  ( -oo (,) B
) ) ( ( w  =/=  B  /\  ( abs `  ( w  -  B ) )  <  v )  -> 
( abs `  (
( ( F  |`  ( -oo (,) B ) ) `  w )  -  L ) )  <  y ) )  /\  w  e.  ( A  i^i  ( -oo (,) B ) )  /\  ( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  v ) )  ->  ( abs `  ( ( F `  w )  -  L
) )  =  ( abs `  ( ( ( F  |`  ( -oo (,) B ) ) `
 w )  -  L ) ) )
165 rspa 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  v )  ->  ( abs `  (
( ( F  |`  ( -oo (,) B ) ) `  w )  -  L ) )  <  y )  /\  w  e.  ( A  i^i  ( -oo (,) B
) ) )  -> 
( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )
1661653impia 1193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  v )  ->  ( abs `  (
( ( F  |`  ( -oo (,) B ) ) `  w )  -  L ) )  <  y )  /\  w  e.  ( A  i^i  ( -oo (,) B
) )  /\  (
w  =/=  B  /\  ( abs `  ( w  -  B ) )  <  v ) )  ->  ( abs `  (
( ( F  |`  ( -oo (,) B ) ) `  w )  -  L ) )  <  y )
1671663adant1l 1220 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  A. w  e.  ( A  i^i  ( -oo (,) B
) ) ( ( w  =/=  B  /\  ( abs `  ( w  -  B ) )  <  v )  -> 
( abs `  (
( ( F  |`  ( -oo (,) B ) ) `  w )  -  L ) )  <  y ) )  /\  w  e.  ( A  i^i  ( -oo (,) B ) )  /\  ( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  v ) )  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y )
168164, 167eqbrtrd 4476 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  A. w  e.  ( A  i^i  ( -oo (,) B
) ) ( ( w  =/=  B  /\  ( abs `  ( w  -  B ) )  <  v )  -> 
( abs `  (
( ( F  |`  ( -oo (,) B ) ) `  w )  -  L ) )  <  y ) )  /\  w  e.  ( A  i^i  ( -oo (,) B ) )  /\  ( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  v ) )  ->  ( abs `  ( ( F `  w )  -  L
) )  <  y
)
1691683exp 1195 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )  ->  ( w  e.  ( A  i^i  ( -oo (,) B ) )  ->  ( ( w  =/=  B  /\  ( abs `  ( w  -  B ) )  < 
v )  ->  ( abs `  ( ( F `
 w )  -  L ) )  < 
y ) ) )
170157, 169ralrimi 2857 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )  ->  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( F `  w )  -  L
) )  <  y
) )
171153, 154, 170syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )  /\  a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  (
( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v ) )  ->  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  v )  ->  ( abs `  (
( F `  w
)  -  L ) )  <  y ) )
172134anim1i 568 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  ( abs `  ( a  -  B ) )  <  v )  -> 
( a  =/=  B  /\  ( abs `  (
a  -  B ) )  <  v ) )
173172adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  ( ( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v ) )  ->  ( a  =/= 
B  /\  ( abs `  ( a  -  B
) )  <  v
) )
1741733adant1 1014 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )  /\  a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  (
( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v ) )  ->  ( a  =/= 
B  /\  ( abs `  ( a  -  B
) )  <  v
) )
175141breq1d 4466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w  =  a  ->  (
( abs `  (
w  -  B ) )  <  v  <->  ( abs `  ( a  -  B
) )  <  v
) )
176139, 175anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( w  =  a  ->  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  v )  <-> 
( a  =/=  B  /\  ( abs `  (
a  -  B ) )  <  v ) ) )
177144oveq1d 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( w  =  a  ->  (
( F `  w
)  -  L )  =  ( ( F `
 a )  -  L ) )
178177fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w  =  a  ->  ( abs `  ( ( F `
 w )  -  L ) )  =  ( abs `  (
( F `  a
)  -  L ) ) )
179178breq1d 4466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( w  =  a  ->  (
( abs `  (
( F `  w
)  -  L ) )  <  y  <->  ( abs `  ( ( F `  a )  -  L
) )  <  y
) )
180176, 179imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  =  a  ->  (
( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( F `  w )  -  L
) )  <  y
)  <->  ( ( a  =/=  B  /\  ( abs `  ( a  -  B ) )  < 
v )  ->  ( abs `  ( ( F `
 a )  -  L ) )  < 
y ) ) )
181180rspcva 3208 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( a  e.  ( A  i^i  ( -oo (,) B ) )  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  v )  ->  ( abs `  (
( F `  w
)  -  L ) )  <  y ) )  ->  ( (
a  =/=  B  /\  ( abs `  ( a  -  B ) )  <  v )  -> 
( abs `  (
( F `  a
)  -  L ) )  <  y ) )
182181imp 429 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( a  e.  ( A  i^i  ( -oo (,) B ) )  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  v )  ->  ( abs `  (
( F `  w
)  -  L ) )  <  y ) )  /\  ( a  =/=  B  /\  ( abs `  ( a  -  B ) )  < 
v ) )  -> 
( abs `  (
( F `  a
)  -  L ) )  <  y )
183152, 171, 174, 182syl21anc 1227 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )  /\  a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  (
( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v ) )  ->  ( abs `  (
( F `  a
)  -  L ) )  <  y )
184 rspe 2915 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( a  e.  A  /\  ( ( abs `  (
( F `  a
)  -  x ) )  <  y  /\  ( abs `  ( ( F `  a )  -  L ) )  <  y ) )  ->  E. a  e.  A  ( ( abs `  (
( F `  a
)  -  x ) )  <  y  /\  ( abs `  ( ( F `  a )  -  L ) )  <  y ) )
185132, 151, 183, 184syl12anc 1226 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )  /\  a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  (
( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v ) )  ->  E. a  e.  A  ( ( abs `  (
( F `  a
)  -  x ) )  <  y  /\  ( abs `  ( ( F `  a )  -  L ) )  <  y ) )
1861853exp 1195 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )  ->  ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  ->  (
( ( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v )  ->  E. a  e.  A  ( ( abs `  (
( F `  a
)  -  x ) )  <  y  /\  ( abs `  ( ( F `  a )  -  L ) )  <  y ) ) ) )
187128, 129, 186rexlimd 2941 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )  ->  ( E. a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } ) ( ( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v )  ->  E. a  e.  A  ( ( abs `  (
( F `  a
)  -  x ) )  <  y  /\  ( abs `  ( ( F `  a )  -  L ) )  <  y ) ) )
188127, 187mpd 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )  ->  E. a  e.  A  ( ( abs `  ( ( F `
 a )  -  x ) )  < 
y  /\  ( abs `  ( ( F `  a )  -  L
) )  <  y
) )
1891883exp 1195 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  ( (
w  =/=  B  /\  ( abs `  ( w  -  B ) )  <  z )  -> 
( abs `  (
( F `  w
)  -  x ) )  <  y ) )  ->  ( v  e.  RR+  ->  ( A. w  e.  ( A  i^i  ( -oo (,) B
) ) ( ( w  =/=  B  /\  ( abs `  ( w  -  B ) )  <  v )  -> 
( abs `  (
( ( F  |`  ( -oo (,) B ) ) `  w )  -  L ) )  <  y )  ->  E. a  e.  A  ( ( abs `  (
( F `  a
)  -  x ) )  <  y  /\  ( abs `  ( ( F `  a )  -  L ) )  <  y ) ) ) )
190189rexlimdv 2947 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  ( (
w  =/=  B  /\  ( abs `  ( w  -  B ) )  <  z )  -> 
( abs `  (
( F `  w
)  -  x ) )  <  y ) )  ->  ( E. v  e.  RR+  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y )  ->  E. a  e.  A  ( ( abs `  (
( F `  a
)  -  x ) )  <  y  /\  ( abs `  ( ( F `  a )  -  L ) )  <  y ) ) )
19160, 190mpd 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  ( (
w  =/=  B  /\  ( abs `  ( w  -  B ) )  <  z )  -> 
( abs `  (
( F `  w
)  -  x ) )  <  y ) )  ->  E. a  e.  A  ( ( abs `  ( ( F `
 a )  -  x ) )  < 
y  /\  ( abs `  ( ( F `  a )  -  L
) )  <  y
) )
1921913exp 1195 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  RR+ )  ->  ( z  e.  RR+  ->  ( A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y )  ->  E. a  e.  A  ( ( abs `  (
( F `  a
)  -  x ) )  <  y  /\  ( abs `  ( ( F `  a )  -  L ) )  <  y ) ) ) )
193192rexlimdv 2947 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  RR+ )  ->  ( E. z  e.  RR+  A. w  e.  A  ( (
w  =/=  B  /\  ( abs `  ( w  -  B ) )  <  z )  -> 
( abs `  (
( F `  w
)  -  x ) )  <  y )  ->  E. a  e.  A  ( ( abs `  (
( F `  a
)  -  x ) )  <  y  /\  ( abs `  ( ( F `  a )  -  L ) )  <  y ) ) )
194193imp 429 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  E. z  e.  RR+  A. w  e.  A  ( (
w  =/=  B  /\  ( abs `  ( w  -  B ) )  <  z )  -> 
( abs `  (
( F `  w
)  -  x ) )  <  y ) )  ->  E. a  e.  A  ( ( abs `  ( ( F `
 a )  -  x ) )  < 
y  /\  ( abs `  ( ( F `  a )  -  L
) )  <  y
) )
195194adantllr 718 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  CC )  /\  y  e.  RR+ )  /\  E. z  e.  RR+  A. w  e.  A  ( ( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  ->  E. a  e.  A  ( ( abs `  ( ( F `
 a )  -  x ) )  < 
y  /\  ( abs `  ( ( F `  a )  -  L
) )  <  y
) )
196 fresin 5760 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( F : A --> CC  ->  ( F  |`  ( B (,) +oo ) ) : ( A  i^i  ( B (,) +oo ) ) --> CC )
19736, 196syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( F  |`  ( B (,) +oo ) ) : ( A  i^i  ( B (,) +oo )
) --> CC )
198 inss2 3715 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( A  i^i  ( B (,) +oo ) )  C_  ( B (,) +oo )
199 ioosscn 31730 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( B (,) +oo )  C_  CC
200198, 199sstri 3508 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( A  i^i  ( B (,) +oo ) )  C_  CC
201200a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( A  i^i  ( B (,) +oo ) ) 
C_  CC )
202197, 201, 55ellimc3 22409 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( R  e.  ( ( F  |`  ( B (,) +oo ) ) lim
CC  B )  <->  ( R  e.  CC  /\  A. y  e.  RR+  E. v  e.  RR+  A. w  e.  ( A  i^i  ( B (,) +oo ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( B (,) +oo ) ) `  w
)  -  R ) )  <  y ) ) ) )
2032, 202mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( R  e.  CC  /\ 
A. y  e.  RR+  E. v  e.  RR+  A. w  e.  ( A  i^i  ( B (,) +oo ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( B (,) +oo ) ) `  w
)  -  R ) )  <  y ) ) )
204203simprd 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  A. y  e.  RR+  E. v  e.  RR+  A. w  e.  ( A  i^i  ( B (,) +oo ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( B (,) +oo ) ) `  w
)  -  R ) )  <  y ) )
205204r19.21bi 2826 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  RR+ )  ->  E. v  e.  RR+  A. w  e.  ( A  i^i  ( B (,) +oo ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( B (,) +oo ) ) `  w
)  -  R ) )  <  y ) )
2062053ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  ( (
w  =/=  B  /\  ( abs `  ( w  -  B ) )  <  z )  -> 
( abs `  (
( F `  w
)  -  x ) )  <  y ) )  ->  E. v  e.  RR+  A. w  e.  ( A  i^i  ( B (,) +oo ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( B (,) +oo ) ) `  w
)  -  R ) )  <  y ) )
207 simp11l 1107 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( B (,) +oo ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( B (,) +oo ) ) `  w
)  -  R ) )  <  y ) )  ->  ph )
208 simp12 1027 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( B (,) +oo ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( B (,) +oo ) ) `  w
)  -  R ) )  <  y ) )  ->  z  e.  RR+ )
209 simp2 997 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( B (,) +oo ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( B (,) +oo ) ) `  w
)  -  R ) )  <  y ) )  ->  v  e.  RR+ )
210 inss1 3714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( limPt `  K ) `  ( A  i^i  ( B (,) +oo ) ) )  i^i  RR ) 
C_  ( ( limPt `  K ) `  ( A  i^i  ( B (,) +oo ) ) )
211210a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ( ( ( limPt `  K ) `  ( A  i^i  ( B (,) +oo ) ) )  i^i 
RR )  C_  (
( limPt `  K ) `  ( A  i^i  ( B (,) +oo ) ) ) )
212 ioossre 11611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( B (,) +oo )  C_  RR
213198, 212sstri 3508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( A  i^i  ( B (,) +oo ) )  C_  RR
214213a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  ( A  i^i  ( B (,) +oo ) ) 
C_  RR )
21576, 78restlp 19811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( K  e.  Top  /\  RR  C_  CC  /\  ( A  i^i  ( B (,) +oo ) )  C_  RR )  ->  ( ( limPt `  J ) `  ( A  i^i  ( B (,) +oo ) ) )  =  ( ( ( limPt `  K ) `  ( A  i^i  ( B (,) +oo ) ) )  i^i 
RR ) )
21670, 72, 214, 215syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ( ( limPt `  J
) `  ( A  i^i  ( B (,) +oo ) ) )  =  ( ( ( limPt `  K ) `  ( A  i^i  ( B (,) +oo ) ) )  i^i 
RR ) )
21782fveq1i 5873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
limPt `  ( TopOpen ` fld ) ) `  ( A  i^i  ( B (,) +oo ) ) )  =  ( ( limPt `  K
) `  ( A  i^i  ( B (,) +oo ) ) )
218217a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ( ( limPt `  ( TopOpen
` fld
) ) `  ( A  i^i  ( B (,) +oo ) ) )  =  ( ( limPt `  K
) `  ( A  i^i  ( B (,) +oo ) ) ) )
219211, 216, 2183sstr4d 3542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ( ( limPt `  J
) `  ( A  i^i  ( B (,) +oo ) ) )  C_  ( ( limPt `  ( TopOpen
` fld
) ) `  ( A  i^i  ( B (,) +oo ) ) ) )
220 limclner.blp2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  B  e.  ( (
limPt `  J ) `  ( A  i^i  ( B (,) +oo ) ) ) )
221219, 220sseldd 3500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  B  e.  ( (
limPt `  ( TopOpen ` fld ) ) `  ( A  i^i  ( B (,) +oo ) ) ) )
222201, 55islpcn 31848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( B  e.  ( ( limPt `  ( TopOpen ` fld ) ) `  ( A  i^i  ( B (,) +oo ) ) )  <->  A. u  e.  RR+  E. b  e.  ( ( A  i^i  ( B (,) +oo )
)  \  { B } ) ( abs `  ( b  -  B
) )  <  u
) )
223221, 222mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  A. u  e.  RR+  E. b  e.  ( ( A  i^i  ( B (,) +oo ) ) 
\  { B }
) ( abs `  (
b  -  B ) )  <  u )
2242233ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  A. u  e.  RR+  E. b  e.  ( ( A  i^i  ( B (,) +oo ) ) 
\  { B }
) ( abs `  (
b  -  B ) )  <  u )
225 breq2 4460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( u  =  if ( z  <_  v ,  z ,  v )  -> 
( ( abs `  (
b  -  B ) )  <  u  <->  ( abs `  ( b  -  B
) )  <  if ( z  <_  v ,  z ,  v ) ) )
226225rexbidv 2968 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( u  =  if ( z  <_  v ,  z ,  v )  -> 
( E. b  e.  ( ( A  i^i  ( B (,) +oo )
)  \  { B } ) ( abs `  ( b  -  B
) )  <  u  <->  E. b  e.  ( ( A  i^i  ( B (,) +oo ) ) 
\  { B }
) ( abs `  (
b  -  B ) )  <  if ( z  <_  v , 
z ,  v ) ) )
227226rspcva 3208 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( if ( z  <_ 
v ,  z ,  v )  e.  RR+  /\ 
A. u  e.  RR+  E. b  e.  ( ( A  i^i  ( B (,) +oo ) ) 
\  { B }
) ( abs `  (
b  -  B ) )  <  u )  ->  E. b  e.  ( ( A  i^i  ( B (,) +oo ) ) 
\  { B }
) ( abs `  (
b  -  B ) )  <  if ( z  <_  v , 
z ,  v ) )
22865, 224, 227syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  E. b  e.  ( ( A  i^i  ( B (,) +oo ) ) 
\  { B }
) ( abs `  (
b  -  B ) )  <  if ( z  <_  v , 
z ,  v ) )
229 eldifi 3622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( b  e.  ( ( A  i^i  ( B (,) +oo ) )  \  { B } )  ->  b  e.  ( A  i^i  ( B (,) +oo ) ) )
230213, 229sseldi 3497 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( b  e.  ( ( A  i^i  ( B (,) +oo ) )  \  { B } )  ->  b  e.  RR )
23172sselda 3499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  b  e.  RR )  ->  b  e.  CC )
23255adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  b  e.  RR )  ->  B  e.  CC )
233231, 232subcld 9950 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  b  e.  RR )  ->  ( b  -  B )  e.  CC )
234233abscld 13279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  b  e.  RR )  ->  ( abs `  ( b  -  B
) )  e.  RR )
2352343ad2antl1 1158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  RR )  ->  ( abs `  ( b  -  B ) )  e.  RR )
236235adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  RR )  /\  ( abs `  ( b  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
( abs `  (
b  -  B ) )  e.  RR )
237102ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  RR )  /\  ( abs `  ( b  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  ->  if ( z  <_  v ,  z ,  v )  e.  RR )
238105ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  RR )  /\  ( abs `  ( b  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
z  e.  RR )
239 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  RR )  /\  ( abs `  ( b  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
( abs `  (
b  -  B ) )  <  if ( z  <_  v , 
z ,  v ) )
240111ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  RR )  /\  ( abs `  ( b  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  ->  if ( z  <_  v ,  z ,  v )  <_  z )
241236, 237, 238, 239, 240ltletrd 9759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  RR )  /\  ( abs `  ( b  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
( abs `  (
b  -  B ) )  <  z )
242115ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  RR )  /\  ( abs `  ( b  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
v  e.  RR )
243238, 242, 117syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  RR )  /\  ( abs `  ( b  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  ->  if ( z  <_  v ,  z ,  v )  <_  v )
244236, 237, 242, 239, 243ltletrd 9759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  RR )  /\  ( abs `  ( b  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
( abs `  (
b  -  B ) )  <  v )
245241, 244jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  RR )  /\  ( abs `  ( b  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
( ( abs `  (
b  -  B ) )  <  z  /\  ( abs `  ( b  -  B ) )  <  v ) )
246245ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  RR )  ->  (
( abs `  (
b  -  B ) )  <  if ( z  <_  v , 
z ,  v )  ->  ( ( abs `  ( b  -  B
) )  <  z  /\  ( abs `  (
b  -  B ) )  <  v ) ) )
247230, 246sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  ( ( A  i^i  ( B (,) +oo )
)  \  { B } ) )  -> 
( ( abs `  (
b  -  B ) )  <  if ( z  <_  v , 
z ,  v )  ->  ( ( abs `  ( b  -  B
) )  <  z  /\  ( abs `  (
b  -  B ) )  <  v ) ) )
248247reximdva 2932 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  ( E. b  e.  ( ( A  i^i  ( B (,) +oo )
)  \  { B } ) ( abs `  ( b  -  B
) )  <  if ( z  <_  v ,  z ,  v )  ->  E. b  e.  ( ( A  i^i  ( B (,) +oo )
)  \  { B } ) ( ( abs `  ( b  -  B ) )  <  z  /\  ( abs `  ( b  -  B ) )  < 
v ) ) )
249228, 248mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  E. b  e.  ( ( A  i^i  ( B (,) +oo ) ) 
\  { B }
) ( ( abs `  ( b  -  B
) )  <  z  /\  ( abs `  (
b  -  B ) )  <  v ) )
250207, 208, 209, 249syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( B (,) +oo ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( B (,) +oo ) ) `  w
)  -  R ) )  <  y ) )  ->  E. b  e.  ( ( A  i^i  ( B (,) +oo )
)  \  { B } ) ( ( abs `  ( b  -  B ) )  <  z  /\  ( abs `  ( b  -  B ) )  < 
v ) )
251 nfv 1708 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/ b ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( B (,) +oo ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( B (,) +oo ) ) `  w
)  -  R ) )  <  y ) )
252 nfre1 2918 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/ b E. b  e.  A  ( ( abs `  (
( F `  b
)  -  x ) )  <  y  /\  ( abs `  ( ( F `  b )  -  R ) )  <  y )
253 inss1 3714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( A  i^i  ( B (,) +oo ) )  C_  A
254253, 229sseldi 3497 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( b  e.  ( ( A  i^i  ( B (,) +oo ) )  \  { B } )  ->  b  e.  A )
2552543ad2ant2 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( B (,) +oo ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( B (,) +oo ) ) `  w
)  -  R ) )  <  y ) )  /\  b  e.  ( ( A  i^i  ( B (,) +oo )
)  \  { B } )  /\  (
( abs `  (
b  -  B ) )  <  z  /\  ( abs `  ( b  -  B ) )  <  v ) )  ->  b  e.  A
)
256 simp113 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( B (,) +oo ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( B (,) +oo ) ) `  w
)  -  R ) )  <  y ) )  /\  b  e.  ( ( A  i^i  ( B (,) +oo )
)  \  { B } )  /\  (
( abs `  (
b  -  B ) )  <  z  /\  ( abs `  ( b  -  B ) )  <  v ) )  ->  A. w  e.  A  ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  z
)  ->  ( abs `  ( ( F `  w )  -  x
) )  <  y
) )
257 eldifsni 4158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( b  e.  ( ( A  i^i  ( B (,) +oo ) )  \  { B } )  ->  b  =/=  B )
258257adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( b  e.  ( ( A  i^i  ( B (,) +oo ) ) 
\  { B }
)  /\  ( ( abs `  ( b  -  B ) )  < 
z  /\  ( abs `  ( b  -  B
) )  <  v
) )  ->  b  =/=  B )
259 simprl 756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( b  e.  ( ( A  i^i  ( B (,) +oo ) ) 
\  { B }
)  /\  ( ( abs `  ( b  -  B ) )  < 
z  /\  ( abs `  ( b  -  B
) )  <  v
) )  ->  ( abs `  ( b  -  B ) )  < 
z )
260258, 259jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( b  e.  ( ( A  i^i  ( B (,) +oo ) ) 
\  { B }
)  /\  ( ( abs `  ( b  -  B ) )  < 
z  /\  ( abs `  ( b  -  B
) )  <  v
) )  ->  (
b  =/=  B  /\  ( abs `  ( b  -  B ) )  <  z ) )
2612603adant1 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( B (,) +oo ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( B (,) +oo ) ) `  w
)  -  R ) )  <  y ) )  /\  b  e.  ( ( A  i^i  ( B (,) +oo )
)  \  { B } )  /\  (
( abs `  (
b  -  B ) )  <  z  /\  ( abs `  ( b  -  B ) )  <  v ) )  ->  ( b  =/= 
B  /\  ( abs `  ( b  -  B
) )  <  z
) )
262 neeq1 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( w  =  b  ->  (
w  =/=  B  <->  b  =/=  B ) )
263 oveq1 6303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( w  =  b  ->  (
w  -  B )  =  ( b  -  B ) )
264263fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( w  =  b  ->  ( abs `  ( w  -  B ) )  =  ( abs `  (
b  -  B ) ) )
265264breq1d 4466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( w  =  b  ->  (
( abs `  (
w  -  B ) )  <  z  <->  ( abs `  ( b  -  B
) )  <  z
) )
266262, 265anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( w  =  b  ->  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  <-> 
( b  =/=  B  /\  ( abs `  (
b  -  B ) )  <  z ) ) )
267 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( w  =  b  ->  ( F `  w )  =  ( F `  b ) )
268267oveq1d 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( w  =  b  ->  (
( F `  w
)  -  x )  =  ( ( F `
 b )  -  x ) )
269268fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( w  =  b  ->  ( abs `  ( ( F `
 w )  -  x ) )  =  ( abs `  (
( F `  b
)  -  x ) ) )
270269breq1d 4466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( w  =  b  ->  (
( abs `  (
( F `  w
)  -  x ) )  <  y  <->  ( abs `  ( ( F `  b )  -  x
) )  <  y
) )
271266, 270imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( w  =  b  ->  (
( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  z
)  ->  ( abs `  ( ( F `  w )  -  x
) )  <  y
)  <->  ( ( b  =/=  B  /\  ( abs `  ( b  -  B ) )  < 
z )  ->  ( abs `  ( ( F `
 b )  -  x ) )  < 
y ) ) )
272271rspcva 3208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( b  e.  A  /\  A. w  e.  A  ( ( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  ->  ( (
b  =/=  B  /\  ( abs `  ( b  -  B ) )  <  z )  -> 
( abs `  (
( F `  b
)  -  x ) )  <  y ) )
273272imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( b  e.  A  /\  A. w  e.  A  ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  z
)  ->  ( abs `  ( ( F `  w )  -  x
) )  <  y
) )  /\  (
b  =/=  B  /\  ( abs `  ( b  -  B ) )  <  z ) )  ->  ( abs `  (
( F `  b
)  -  x ) )  <  y )
274255, 256, 261, 273syl21anc 1227 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( B (,) +oo ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( B (,) +oo ) ) `  w
)  -  R ) )  <  y ) )  /\  b  e.  ( ( A  i^i  ( B (,) +oo )
)  \  { B } )  /\  (
( abs `  (
b  -  B ) )  <  z  /\  ( abs `  ( b  -  B ) )  <  v ) )  ->  ( abs `  (
( F `  b
)  -  x ) )  <  y )
2752293ad2ant2 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. w  e.  A  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  ->  ( abs `  (
( F `  w
)  -  x ) )  <  y ) )  /\  v  e.  RR+  /\  A. w  e.  ( A  i^i  ( B (,) +oo ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( B (,) +oo ) ) `  w
)  -  R ) )