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

Theorem limclner 37672
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 22828 . . . . . . . . . . . . 13  |-  ( ( F  |`  ( B (,) +oo ) ) lim CC  B )  C_  CC
2 limclner.r . . . . . . . . . . . . 13  |-  ( ph  ->  R  e.  ( ( F  |`  ( B (,) +oo ) ) lim CC  B ) )
31, 2sseldi 3462 . . . . . . . . . . . 12  |-  ( ph  ->  R  e.  CC )
43ad2antrr 730 . . . . . . . . . . 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 22828 . . . . . . . . . . . . 13  |-  ( ( F  |`  ( -oo (,) B ) ) lim CC  B )  C_  CC
6 limclner.l . . . . . . . . . . . . 13  |-  ( ph  ->  L  e.  ( ( F  |`  ( -oo (,) B ) ) lim CC  B ) )
75, 6sseldi 3462 . . . . . . . . . . . 12  |-  ( ph  ->  L  e.  CC )
87ad2antrr 730 . . . . . . . . . . 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 9993 . . . . . . . . . 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 2691 . . . . . . . . . . . 12  |-  ( ph  ->  R  =/=  L )
1211ad2antrr 730 . . . . . . . . . . 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 10002 . . . . . . . . . 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 13509 . . . . . . . . 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 10693 . . . . . . . . . . 11  |-  4  e.  RR
16 4pos 10712 . . . . . . . . . . 11  |-  0  <  4
1715, 16elrpii 11312 . . . . . . . . . 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 11365 . . . . . . . 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 1755 . . . . . . . . . . 11  |-  F/ y ( ph  /\  x  e.  CC )
21 nfra1 2803 . . . . . . . . . . 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 1988 . . . . . . . . . 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 1755 . . . . . . . . . 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 1980 . . . . . . . . 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 6333 . . . . . . . . 9  |-  ( ( abs `  ( R  -  L ) )  /  4 )  e. 
_V
26 eleq1 2495 . . . . . . . . . . 11  |-  ( y  =  ( ( abs `  ( R  -  L
) )  /  4
)  ->  ( y  e.  RR+  <->  ( ( abs `  ( R  -  L
) )  /  4
)  e.  RR+ )
)
27 oveq2 6313 . . . . . . . . . . . . 13  |-  ( y  =  ( ( abs `  ( R  -  L
) )  /  4
)  ->  ( 4  x.  y )  =  ( 4  x.  (
( abs `  ( R  -  L )
)  /  4 ) ) )
2827breq2d 4435 . . . . . . . . . . . 12  |-  ( y  =  ( ( abs `  ( R  -  L
) )  /  4
)  ->  ( ( abs `  ( R  -  L ) )  < 
( 4  x.  y
)  <->  ( abs `  ( R  -  L )
)  <  ( 4  x.  ( ( abs `  ( R  -  L
) )  /  4
) ) ) )
29282rexbidv 2943 . . . . . . . . . . 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 321 . . . . . . . . . 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 317 . . . . . . . . 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 758 . . . . . . . . . . 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 462 . . . . . . . . . . 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 2789 . . . . . . . . . . . 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 718 . . . . . . . . . . 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 5769 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F : A --> CC  ->  ( F  |`  ( -oo (,) B ) ) : ( A  i^i  ( -oo (,) B ) ) --> CC )
3836, 37syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( F  |`  ( -oo (,) B ) ) : ( A  i^i  ( -oo (,) B ) ) --> CC )
39 inss2 3683 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( A  i^i  ( -oo (,) B ) )  C_  ( -oo (,) B )
40 ioosscn 37540 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( -oo (,) B )  C_  CC
4139, 40sstri 3473 . . . . . . . . . . . . . . . . . . . . . . 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 21780 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( topGen ` 
ran  (,) )  e.  Top
4543, 44eqeltri 2503 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  J  e. 
Top
46 ioossre 11703 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( -oo (,) B )  C_  RR
4739, 46sstri 3473 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A  i^i  ( -oo (,) B ) )  C_  RR
48 uniretop 21781 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  RR  =  U. ( topGen `  ran  (,) )
4943unieqi 4228 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  U. J  =  U. ( topGen `  ran  (,) )
5048, 49eqtr4i 2454 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  RR  =  U. J
5150lpss 20156 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( J  e.  Top  /\  ( A  i^i  ( -oo (,) B ) ) 
C_  RR )  -> 
( ( limPt `  J
) `  ( A  i^i  ( -oo (,) B
) ) )  C_  RR )
5245, 47, 51mp2an 676 . . . . . . . . . . . . . . . . . . . . . . . 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 3462 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  B  e.  RR )
5554recnd 9676 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  B  e.  CC )
5638, 42, 55ellimc3 22832 . . . . . . . . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . . . . . . 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 2791 . . . . . . . . . . . . . . . . . 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 1026 . . . . . . . . . . . . . . . . 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 1116 . . . . . . . . . . . . . . . . . . . . 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 1036 . . . . . . . . . . . . . . . . . . . . 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 1006 . . . . . . . . . . . . . . . . . . . . 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 3953 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( z  e.  RR+  /\  v  e.  RR+ )  ->  if ( z  <_  v ,  z ,  v )  e.  RR+ )
65643adant1 1023 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  if ( z  <_  v ,  z ,  v )  e.  RR+ )
66 inss1 3682 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 21802 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  K  e. 
Top
7069a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  K  e.  Top )
71 ax-resscn 9603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  RR  C_  CC
7271a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  RR  C_  CC )
7347a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( A  i^i  ( -oo (,) B ) ) 
C_  RR )
74 unicntop 37344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  CC  =  U. ( TopOpen ` fld )
7568unieqi 4228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  U. K  =  U. ( TopOpen ` fld )
7674, 75eqtr4i 2454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  CC  =  U. K
7768tgioo2 21819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( topGen ` 
ran  (,) )  =  ( Kt  RR )
7843, 77eqtri 2451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  J  =  ( Kt  RR )
7976, 78restlp 20197 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( ( limPt `  J
) `  ( A  i^i  ( -oo (,) B
) ) )  =  ( ( ( limPt `  K ) `  ( A  i^i  ( -oo (,) B ) ) )  i^i  RR ) )
8168eqcomi 2435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( TopOpen ` fld )  =  K
8281fveq2i 5884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( limPt `  ( TopOpen ` fld ) )  =  (
limPt `  K )
8382fveq1i 5882 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3507 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( limPt `  J
) `  ( A  i^i  ( -oo (,) B
) ) )  C_  ( ( limPt `  ( TopOpen
` fld
) ) `  ( A  i^i  ( -oo (,) B ) ) ) )
8685, 53sseldd 3465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  B  e.  ( (
limPt `  ( TopOpen ` fld ) ) `  ( A  i^i  ( -oo (,) B ) ) ) )
8742, 55islpcn 37659 . . . . . . . . . . . . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  A. u  e.  RR+  E. a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } ) ( abs `  ( a  -  B ) )  <  u )
89883ad2ant1 1026 . . . . . . . . . . . . . . . . . . . . . . 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 4427 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( u  =  if ( z  <_  v ,  z ,  v )  -> 
( ( abs `  (
a  -  B ) )  <  u  <->  ( abs `  ( a  -  B
) )  <  if ( z  <_  v ,  z ,  v ) ) )
9190rexbidv 2936 . . . . . . . . . . . . . . . . . . . . . . . 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 3180 . . . . . . . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . . . . . . 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 3587 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  -> 
a  e.  ( A  i^i  ( -oo (,) B ) ) )
9547, 94sseldi 3462 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  -> 
a  e.  RR )
9672sselda 3464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  a  e.  RR )  ->  a  e.  CC )
9755adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  a  e.  RR )  ->  B  e.  CC )
9896, 97subcld 9993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  a  e.  RR )  ->  ( a  -  B )  e.  CC )
9998abscld 13497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  a  e.  RR )  ->  ( abs `  ( a  -  B
) )  e.  RR )
100993ad2antl1 1167 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  ->  ( abs `  ( a  -  B ) )  e.  RR )
101100adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11348 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  if ( z  <_  v ,  z ,  v )  e.  RR )
103102ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  e.  RR+  ->  z  e.  RR )
1051043ad2ant2 1027 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  z  e.  RR )
106105ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  /\  ( abs `  ( a  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
z  e.  RR )
107 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( v  e.  RR+  ->  v  e.  RR )
109 min1 11490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( z  e.  RR  /\  v  e.  RR )  ->  if ( z  <_ 
v ,  z ,  v )  <_  z
)
110104, 108, 109syl2an 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( z  e.  RR+  /\  v  e.  RR+ )  ->  if ( z  <_  v ,  z ,  v )  <_  z )
1111103adant1 1023 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  if ( z  <_  v ,  z ,  v )  <_ 
z )
112111ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9802 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  /\  ( abs `  ( a  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
( abs `  (
a  -  B ) )  <  z )
114108adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( z  e.  RR+  /\  v  e.  RR+ )  ->  v  e.  RR )
1151143adant1 1023 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  v  e.  RR )
116115ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  /\  ( abs `  ( a  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
v  e.  RR )
117 min2 11491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( z  e.  RR  /\  v  e.  RR )  ->  if ( z  <_ 
v ,  z ,  v )  <_  v
)
118104, 108, 117syl2an 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( z  e.  RR+  /\  v  e.  RR+ )  ->  if ( z  <_  v ,  z ,  v )  <_  v )
1191183adant1 1023 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  if ( z  <_  v ,  z ,  v )  <_ 
v )
120119ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9802 . . . . . . . . . . . . . . . . . . . . . . . . . 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 534 . . . . . . . . . . . . . . . . . . . . . . . . 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 435 . . . . . . . . . . . . . . . . . . . . . . . 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 476 . . . . . . . . . . . . . . . . . . . . . . 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 2897 . . . . . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . . . . 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 1755 . . . . . . . . . . . . . . . . . . . . 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 2883 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ a E. a  e.  A  ( ( abs `  (
( F `  a
)  -  x ) )  <  y  /\  ( abs `  ( ( F `  a )  -  L ) )  <  y )
130 inss1 3682 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A  i^i  ( -oo (,) B ) )  C_  A
131130, 94sseldi 3462 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  -> 
a  e.  A )
1321313ad2ant2 1027 . . . . . . . . . . . . . . . . . . . . . . 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 1136 . . . . . . . . . . . . . . . . . . . . . . . 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 4126 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  -> 
a  =/=  B )
135134adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  ( ( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v ) )  ->  a  =/=  B
)
136 simprl 762 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  ( ( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v ) )  ->  ( abs `  (
a  -  B ) )  <  z )
137135, 136jca 534 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  ( ( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v ) )  ->  ( a  =/= 
B  /\  ( abs `  ( a  -  B
) )  <  z
) )
1381373adant1 1023 . . . . . . . . . . . . . . . . . . . . . . . 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 2701 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w  =  a  ->  (
w  =/=  B  <->  a  =/=  B ) )
140 oveq1 6312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( w  =  a  ->  (
w  -  B )  =  ( a  -  B ) )
141140fveq2d 5885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( w  =  a  ->  ( abs `  ( w  -  B ) )  =  ( abs `  (
a  -  B ) ) )
142141breq1d 4433 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w  =  a  ->  (
( abs `  (
w  -  B ) )  <  z  <->  ( abs `  ( a  -  B
) )  <  z
) )
143139, 142anbi12d 715 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( w  =  a  ->  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  <-> 
( a  =/=  B  /\  ( abs `  (
a  -  B ) )  <  z ) ) )
144 fveq2 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( w  =  a  ->  ( F `  w )  =  ( F `  a ) )
145144oveq1d 6320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( w  =  a  ->  (
( F `  w
)  -  x )  =  ( ( F `
 a )  -  x ) )
146145fveq2d 5885 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w  =  a  ->  ( abs `  ( ( F `
 w )  -  x ) )  =  ( abs `  (
( F `  a
)  -  x ) ) )
147146breq1d 4433 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( w  =  a  ->  (
( abs `  (
( F `  w
)  -  x ) )  <  y  <->  ( abs `  ( ( F `  a )  -  x
) )  <  y
) )
148143, 147imbi12d 321 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3180 . . . . . . . . . . . . . . . . . . . . . . . . 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 430 . . . . . . . . . . . . . . . . . . . . . . . 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 1263 . . . . . . . . . . . . . . . . . . . . . . 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 1027 . . . . . . . . . . . . . . . . . . . . . . . 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 1026 . . . . . . . . . . . . . . . . . . . . . . . . 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 1037 . . . . . . . . . . . . . . . . . . . . . . . . 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 1755 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  F/ w ph
156 nfra1 2803 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1988 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3652 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( w  e.  ( A  i^i  ( -oo (,) B ) )  ->  w  e.  ( -oo (,) B ) )
159 fvres 5895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( w  e.  ( -oo (,) B )  ->  (
( F  |`  ( -oo (,) B ) ) `
 w )  =  ( F `  w
) )
160158, 159syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( w  e.  ( A  i^i  ( -oo (,) B ) )  ->  ( ( F  |`  ( -oo (,) B ) ) `  w )  =  ( F `  w ) )
161160eqcomd 2430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( w  e.  ( A  i^i  ( -oo (,) B ) )  ->  ( F `  w )  =  ( ( F  |`  ( -oo (,) B ) ) `
 w ) )
162161oveq1d 6320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( w  e.  ( A  i^i  ( -oo (,) B ) )  ->  ( ( F `  w )  -  L )  =  ( ( ( F  |`  ( -oo (,) B ) ) `  w )  -  L ) )
163162fveq2d 5885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( w  e.  ( A  i^i  ( -oo (,) B ) )  ->  ( abs `  ( ( F `  w )  -  L
) )  =  ( abs `  ( ( ( F  |`  ( -oo (,) B ) ) `
 w )  -  L ) ) )
1641633ad2ant2 1027 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1256 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4444 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1204 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2822 . . . . . . . . . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . . . . . . . . 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 570 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  ( abs `  ( a  -  B ) )  <  v )  -> 
( a  =/=  B  /\  ( abs `  (
a  -  B ) )  <  v ) )
173172adantrl 720 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  ( ( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v ) )  ->  ( a  =/= 
B  /\  ( abs `  ( a  -  B
) )  <  v
) )
1741733adant1 1023 . . . . . . . . . . . . . . . . . . . . . . . 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 4433 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w  =  a  ->  (
( abs `  (
w  -  B ) )  <  v  <->  ( abs `  ( a  -  B
) )  <  v
) )
176139, 175anbi12d 715 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( w  =  a  ->  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  v )  <-> 
( a  =/=  B  /\  ( abs `  (
a  -  B ) )  <  v ) ) )
177144oveq1d 6320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( w  =  a  ->  (
( F `  w
)  -  L )  =  ( ( F `
 a )  -  L ) )
178177fveq2d 5885 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w  =  a  ->  ( abs `  ( ( F `
 w )  -  L ) )  =  ( abs `  (
( F `  a
)  -  L ) ) )
179178breq1d 4433 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( w  =  a  ->  (
( abs `  (
( F `  w
)  -  L ) )  <  y  <->  ( abs `  ( ( F `  a )  -  L
) )  <  y
) )
180176, 179imbi12d 321 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3180 . . . . . . . . . . . . . . . . . . . . . . . . 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 430 . . . . . . . . . . . . . . . . . . . . . . . 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 1263 . . . . . . . . . . . . . . . . . . . . . . 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 2880 . . . . . . . . . . . . . . . . . . . . . . 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 1262 . . . . . . . . . . . . . . . . . . . . . 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 1204 . . . . . . . . . . . . . . . . . . . . 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 2906 . . . . . . . . . . . . . . . . . . . 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 1204 . . . . . . . . . . . . . . . . . 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 2912 . . . . . . . . . . . . . . . . 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 1204 . . . . . . . . . . . . . . 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 2912 . . . . . . . . . . . . . 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 430 . . . . . . . . . . . . 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 723 . . . . . . . . . . . 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 5769 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( F : A --> CC  ->  ( F  |`  ( B (,) +oo ) ) : ( A  i^i  ( B (,) +oo ) ) --> CC )
19736, 196syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( F  |`  ( B (,) +oo ) ) : ( A  i^i  ( B (,) +oo )
) --> CC )
198 inss2 3683 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( A  i^i  ( B (,) +oo ) )  C_  ( B (,) +oo )
199 ioosscn 37540 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( B (,) +oo )  C_  CC
200198, 199sstri 3473 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( A  i^i  ( B (,) +oo ) )  C_  CC
201200a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( A  i^i  ( B (,) +oo ) ) 
C_  CC )
202197, 201, 55ellimc3 22832 . . . . . . . . . . . . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . . . . . . . . . . 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 2791 . . . . . . . . . . . . . . . . . . . . . 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 1026 . . . . . . . . . . . . . . . . . . . . 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 1116 . . . . . . . . . . . . . . . . . . . . . . . . 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 1036 . . . . . . . . . . . . . . . . . . . . . . . . 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 1006 . . . . . . . . . . . . . . . . . . . . . . . . 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 3682 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( B (,) +oo )  C_  RR
213198, 212sstri 3473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( A  i^i  ( B (,) +oo ) )  C_  RR
214213a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  ( A  i^i  ( B (,) +oo ) ) 
C_  RR )
21576, 78restlp 20197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ( ( limPt `  J
) `  ( A  i^i  ( B (,) +oo ) ) )  =  ( ( ( limPt `  K ) `  ( A  i^i  ( B (,) +oo ) ) )  i^i 
RR ) )
21782fveq1i 5882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  B  e.  ( (
limPt `  ( TopOpen ` fld ) ) `  ( A  i^i  ( B (,) +oo ) ) ) )
222201, 55islpcn 37659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  A. u  e.  RR+  E. b  e.  ( ( A  i^i  ( B (,) +oo ) ) 
\  { B }
) ( abs `  (
b  -  B ) )  <  u )
2242233ad2ant1 1026 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( u  =  if ( z  <_  v ,  z ,  v )  -> 
( ( abs `  (
b  -  B ) )  <  u  <->  ( abs `  ( b  -  B
) )  <  if ( z  <_  v ,  z ,  v ) ) )
226225rexbidv 2936 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3180 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( b  e.  ( ( A  i^i  ( B (,) +oo ) )  \  { B } )  ->  b  e.  ( A  i^i  ( B (,) +oo ) ) )
230213, 229sseldi 3462 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( b  e.  ( ( A  i^i  ( B (,) +oo ) )  \  { B } )  ->  b  e.  RR )
23172sselda 3464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  b  e.  RR )  ->  b  e.  CC )
23255adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  b  e.  RR )  ->  B  e.  CC )
233231, 232subcld 9993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  b  e.  RR )  ->  ( b  -  B )  e.  CC )
234233abscld 13497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  b  e.  RR )  ->  ( abs `  ( b  -  B
) )  e.  RR )
2352343ad2antl1 1167 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  RR )  ->  ( abs `  ( b  -  B ) )  e.  RR )
236235adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  RR )  /\  ( abs `  ( b  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
z  e.  RR )
239 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9802 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  RR )  /\  ( abs `  ( b  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
( abs `  (
b  -  B ) )  <  z )
242115ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9802 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 476 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2897 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . . . . . . . . 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 1755 . . . . . . . . . . . . . . . . . . . . . . . . 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 2883 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/ b E. b  e.  A  ( ( abs `  (
( F `  b
)  -  x ) )  <  y  /\  ( abs `  ( ( F `  b )  -  R ) )  <  y )
253 inss1 3682 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( A  i^i  ( B (,) +oo ) )  C_  A
254253, 229sseldi 3462 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( b  e.  ( ( A  i^i  ( B (,) +oo ) )  \  { B } )  ->  b  e.  A )
2552543ad2ant2 1027 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1136 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( b  e.  ( ( A  i^i  ( B (,) +oo ) )  \  { B } )  ->  b  =/=  B )
258257adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( b  e.  ( ( A  i^i  ( B (,) +oo ) ) 
\  { B }
)  /\  ( ( abs `  ( b  -  B ) )  < 
z  /\  ( abs `  ( b  -  B
) )  <  v
) )  ->  b  =/=  B )
259 simprl 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( b  e.  ( ( A  i^i  ( B (,) +oo ) ) 
\  { B }
)  /\  ( ( abs `  ( b  -  B ) )  < 
z  /\  ( abs `  ( b  -  B
) )  <  v
) )  ->  ( abs `  ( b  -  B ) )  < 
z )
260258, 259jca 534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( b  e.  ( ( A  i^i  ( B (,) +oo ) ) 
\  { B }
)  /\  ( ( abs `  ( b  -  B ) )  < 
z  /\  ( abs `  ( b  -  B
) )  <  v
) )  ->  (
b  =/=  B  /\  ( abs `  ( b  -  B ) )  <  z ) )
2612603adant1 1023 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( w  =  b  ->  (
w  =/=  B  <->  b  =/=  B ) )
263 oveq1 6312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( w  =  b  ->  (
w  -  B )  =  ( b  -  B ) )
264263fveq2d 5885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( w  =  b  ->  ( abs `  ( w  -  B ) )  =  ( abs `  (
b  -  B ) ) )
265264breq1d 4433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( w  =  b  ->  (
( abs `  (
w  -  B ) )  <  z  <->  ( abs `  ( b  -  B
) )  <  z
) )
266262, 265anbi12d 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( w  =  b  ->  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  <-> 
( b  =/=  B  /\  ( abs `  (
b  -  B ) )  <  z ) ) )
267 fveq2 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( w  =  b  ->  ( F `  w )  =  ( F `  b ) )
268267oveq1d 6320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( w  =  b  ->  (
( F `  w
)  -  x )  =  ( ( F `
 b )  -  x ) )
269268fveq2d 5885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( w  =  b  ->  ( abs `  ( ( F `
 w )  -  x ) )  =  ( abs `  (
( F `  b
)  -  x ) ) )
270269breq1d 4433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( w  =  b  ->  (
( abs `  (
( F `  w
)  -  x ) )  <  y  <->  ( abs `  ( ( F `  b )  -  x
) )  <  y
) )
271266, 270imbi12d 321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 430 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1263 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1027 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )  <