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

Theorem limclner 31516
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 limclner.r . . . . . . . . . . . . . 14  |-  ( ph  ->  R  e.  ( ( F  |`  ( B (,) +oo ) ) lim CC  B ) )
2 limccl 22147 . . . . . . . . . . . . . . 15  |-  ( ( F  |`  ( B (,) +oo ) ) lim CC  B )  C_  CC
32sseli 3505 . . . . . . . . . . . . . 14  |-  ( R  e.  ( ( F  |`  ( B (,) +oo ) ) lim CC  B )  ->  R  e.  CC )
41, 3syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  R  e.  CC )
54ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( 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 )
6 limclner.l . . . . . . . . . . . . . 14  |-  ( ph  ->  L  e.  ( ( F  |`  ( -oo (,) B ) ) lim CC  B ) )
7 limccl 22147 . . . . . . . . . . . . . . 15  |-  ( ( F  |`  ( -oo (,) B ) ) lim CC  B )  C_  CC
87sseli 3505 . . . . . . . . . . . . . 14  |-  ( L  e.  ( ( F  |`  ( -oo (,) B
) ) lim CC  B
)  ->  L  e.  CC )
96, 8syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  L  e.  CC )
109ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( 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 )
115, 10subcld 9942 . . . . . . . . . . 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
)  e.  CC )
12 limclner.lner . . . . . . . . . . . . . 14  |-  ( ph  ->  L  =/=  R )
1312necomd 2738 . . . . . . . . . . . . 13  |-  ( ph  ->  R  =/=  L )
1413ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( 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 )
155, 10, 14subne0d 9951 . . . . . . . . . . 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
)  =/=  0 )
1611, 15absrpcld 13259 . . . . . . . . . 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 ) )  -> 
( abs `  ( R  -  L )
)  e.  RR+ )
17 4re 10624 . . . . . . . . . . . 12  |-  4  e.  RR
18 4pos 10643 . . . . . . . . . . . 12  |-  0  <  4
19 elrp 11234 . . . . . . . . . . . 12  |-  ( 4  e.  RR+  <->  ( 4  e.  RR  /\  0  <  4 ) )
2017, 18, 19mpbir2an 918 . . . . . . . . . . 11  |-  4  e.  RR+
2120a1i 11 . . . . . . . . . 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 ) )  -> 
4  e.  RR+ )
2216, 21rpdivcld 11285 . . . . . . . . 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 )
)  /  4 )  e.  RR+ )
23 nfv 1683 . . . . . . . . . . . 12  |-  F/ y ( ph  /\  x  e.  CC )
24 nfra1 2848 . . . . . . . . . . . 12  |-  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 )
2523, 24nfan 1875 . . . . . . . . . . 11  |-  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 ) )
26 nfv 1683 . . . . . . . . . . 11  |-  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 ) ) )
2725, 26nfim 1867 . . . . . . . . . 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 ) )  ->  ( (
( abs `  ( R  -  L )
)  /  4 )  e.  RR+  ->  E. a  e.  A  E. b  e.  A  ( abs `  ( R  -  L
) )  <  (
4  x.  ( ( abs `  ( R  -  L ) )  /  4 ) ) ) )
28 ovex 6320 . . . . . . . . . 10  |-  ( ( abs `  ( R  -  L ) )  /  4 )  e. 
_V
29 eleq1 2539 . . . . . . . . . . . 12  |-  ( y  =  ( ( abs `  ( R  -  L
) )  /  4
)  ->  ( y  e.  RR+  <->  ( ( abs `  ( R  -  L
) )  /  4
)  e.  RR+ )
)
30 oveq2 6303 . . . . . . . . . . . . . . 15  |-  ( y  =  ( ( abs `  ( R  -  L
) )  /  4
)  ->  ( 4  x.  y )  =  ( 4  x.  (
( abs `  ( R  -  L )
)  /  4 ) ) )
3130breq2d 4465 . . . . . . . . . . . . . 14  |-  ( y  =  ( ( abs `  ( R  -  L
) )  /  4
)  ->  ( ( abs `  ( R  -  L ) )  < 
( 4  x.  y
)  <->  ( abs `  ( R  -  L )
)  <  ( 4  x.  ( ( abs `  ( R  -  L
) )  /  4
) ) ) )
3231rexbidv 2978 . . . . . . . . . . . . 13  |-  ( y  =  ( ( abs `  ( R  -  L
) )  /  4
)  ->  ( E. b  e.  A  ( abs `  ( R  -  L ) )  < 
( 4  x.  y
)  <->  E. b  e.  A  ( abs `  ( R  -  L ) )  <  ( 4  x.  ( ( abs `  ( R  -  L )
)  /  4 ) ) ) )
3332rexbidv 2978 . . . . . . . . . . . 12  |-  ( 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 ) ) ) )
3429, 33imbi12d 320 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) )
3534imbi2d 316 . . . . . . . . . 10  |-  ( 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 ) ) ) ) ) )
36 simpll 753 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) )
37 simpr 461 . . . . . . . . . . . 12  |-  ( ( ( ( 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+ )
38 rspa 2834 . . . . . . . . . . . . 13  |-  ( ( 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 ) )
3938adantll 713 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) )
40 limclner.f . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  F : A --> CC )
41 fresin 5760 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( F : A --> CC  ->  ( F  |`  ( -oo (,) B ) ) : ( A  i^i  ( -oo (,) B ) ) --> CC )
4240, 41syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( F  |`  ( -oo (,) B ) ) : ( A  i^i  ( -oo (,) B ) ) --> CC )
43 inss2 3724 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A  i^i  ( -oo (,) B ) )  C_  ( -oo (,) B )
44 ioosscn 31414 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( -oo (,) B )  C_  CC
4543, 44sstri 3518 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( A  i^i  ( -oo (,) B ) )  C_  CC
4645a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( A  i^i  ( -oo (,) B ) ) 
C_  CC )
47 ax-resscn 9561 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  RR  C_  CC
4847a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  RR  C_  CC )
49 limclner.j . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  J  =  ( topGen `  ran  (,) )
50 retop 21136 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( topGen ` 
ran  (,) )  e.  Top
5149, 50eqeltri 2551 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  J  e. 
Top
52 ioossre 11598 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -oo (,) B )  C_  RR
5343, 52sstri 3518 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( A  i^i  ( -oo (,) B ) )  C_  RR
54 uniretop 21137 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  RR  =  U. ( topGen `  ran  (,) )
5549unieqi 4260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  U. J  =  U. ( topGen `  ran  (,) )
5655eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  U. ( topGen `
 ran  (,) )  =  U. J
5754, 56eqtri 2496 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  RR  =  U. J
5857lpss 19511 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( J  e.  Top  /\  ( A  i^i  ( -oo (,) B ) ) 
C_  RR )  -> 
( ( limPt `  J
) `  ( A  i^i  ( -oo (,) B
) ) )  C_  RR )
5951, 53, 58mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
limPt `  J ) `  ( A  i^i  ( -oo (,) B ) ) )  C_  RR
60 limclner.blp1 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  B  e.  ( (
limPt `  J ) `  ( A  i^i  ( -oo (,) B ) ) ) )
6159, 60sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  B  e.  RR )
6248, 61sseldd 3510 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  B  e.  CC )
6342, 46, 62ellimc3 22151 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 ) ) ) )
646, 63mpbid 210 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) ) )
6564simprd 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 ) )
6665r19.21bi 2836 . . . . . . . . . . . . . . . . . . 19  |-  ( (
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 ) )
67663ad2ant1 1017 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 ) )
68 simp11l 1107 . . . . . . . . . . . . . . . . . . . . . 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 ) )  ->  ph )
69 simp12 1027 . . . . . . . . . . . . . . . . . . . . . 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 ) )  ->  z  e.  RR+ )
70 simp2 997 . . . . . . . . . . . . . . . . . . . . . 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 ) )  ->  v  e.  RR+ )
71 ifcl 3987 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( z  e.  RR+  /\  v  e.  RR+ )  ->  if ( z  <_  v ,  z ,  v )  e.  RR+ )
72713adant1 1014 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  if ( z  <_  v ,  z ,  v )  e.  RR+ )
73 inss1 3723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( limPt `  K ) `  ( A  i^i  ( -oo (,) B ) ) )  i^i  RR ) 
C_  ( ( limPt `  K ) `  ( A  i^i  ( -oo (,) B ) ) )
7473a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( ( ( limPt `  K ) `  ( A  i^i  ( -oo (,) B ) ) )  i^i  RR )  C_  ( ( limPt `  K
) `  ( A  i^i  ( -oo (,) B
) ) ) )
75 limclner.k . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  K  =  ( TopOpen ` fld )
7675cnfldtop 21159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  K  e. 
Top
7776a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  K  e.  Top )
7853a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ( A  i^i  ( -oo (,) B ) ) 
C_  RR )
79 unicntop 31336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  CC  =  U. ( TopOpen ` fld )
8075unieqi 4260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  U. K  =  U. ( TopOpen ` fld )
8180eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  U. ( TopOpen
` fld
)  =  U. K
8279, 81eqtri 2496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  CC  =  U. K
8375tgioo2 21176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( topGen ` 
ran  (,) )  =  ( Kt  RR )
8449, 83eqtri 2496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  J  =  ( Kt  RR )
8582, 84restlp 19552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 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 ) )
8677, 48, 78, 85syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( ( limPt `  J
) `  ( A  i^i  ( -oo (,) B
) ) )  =  ( ( ( limPt `  K ) `  ( A  i^i  ( -oo (,) B ) ) )  i^i  RR ) )
8775eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( TopOpen ` fld )  =  K
8887fveq2i 5875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( limPt `  ( TopOpen ` fld ) )  =  (
limPt `  K )
8988fveq1i 5873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
limPt `  ( TopOpen ` fld ) ) `  ( A  i^i  ( -oo (,) B ) ) )  =  ( ( limPt `  K ) `  ( A  i^i  ( -oo (,) B ) ) )
9089a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( ( limPt `  ( TopOpen
` fld
) ) `  ( A  i^i  ( -oo (,) B ) ) )  =  ( ( limPt `  K ) `  ( A  i^i  ( -oo (,) B ) ) ) )
9186, 90sseq12d 3538 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( ( ( limPt `  J ) `  ( A  i^i  ( -oo (,) B ) ) ) 
C_  ( ( limPt `  ( TopOpen ` fld ) ) `  ( A  i^i  ( -oo (,) B ) ) )  <-> 
( ( ( limPt `  K ) `  ( A  i^i  ( -oo (,) B ) ) )  i^i  RR )  C_  ( ( limPt `  K
) `  ( A  i^i  ( -oo (,) B
) ) ) ) )
9274, 91mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( ( limPt `  J
) `  ( A  i^i  ( -oo (,) B
) ) )  C_  ( ( limPt `  ( TopOpen
` fld
) ) `  ( A  i^i  ( -oo (,) B ) ) ) )
9392, 60sseldd 3510 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  B  e.  ( (
limPt `  ( TopOpen ` fld ) ) `  ( A  i^i  ( -oo (,) B ) ) ) )
9446, 62islpcn 31504 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 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
) )
9593, 94mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  A. u  e.  RR+  E. a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } ) ( abs `  ( a  -  B ) )  <  u )
96953ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  A. u  e.  RR+  E. a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } ) ( abs `  ( a  -  B ) )  <  u )
97 breq2 4457 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( u  =  if ( z  <_  v ,  z ,  v )  -> 
( ( abs `  (
a  -  B ) )  <  u  <->  ( abs `  ( a  -  B
) )  <  if ( z  <_  v ,  z ,  v ) ) )
9897rexbidv 2978 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 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 ) ) )
9998rspcva 3217 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 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 ) )
10072, 96, 99syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  E. a  e.  ( ( A  i^i  ( -oo (,) B ) ) 
\  { B }
) ( abs `  (
a  -  B ) )  <  if ( z  <_  v , 
z ,  v ) )
101 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } ) )  -> 
( ph  /\  z  e.  RR+  /\  v  e.  RR+ ) )
10253a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  -> 
( A  i^i  ( -oo (,) B ) ) 
C_  RR )
103 eldifi 3631 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  -> 
a  e.  ( A  i^i  ( -oo (,) B ) ) )
104102, 103sseldd 3510 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  -> 
a  e.  RR )
105104adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } ) )  -> 
a  e.  RR )
10648sselda 3509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  a  e.  RR )  ->  a  e.  CC )
10762adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  a  e.  RR )  ->  B  e.  CC )
108106, 107subcld 9942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  a  e.  RR )  ->  ( a  -  B )  e.  CC )
109108abscld 13247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  a  e.  RR )  ->  ( abs `  ( a  -  B
) )  e.  RR )
1101093ad2antl1 1158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  ->  ( abs `  ( a  -  B ) )  e.  RR )
111110adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  /\  ( abs `  ( a  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
( abs `  (
a  -  B ) )  e.  RR )
11272rpred 11268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  if ( z  <_  v ,  z ,  v )  e.  RR )
113112adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  ->  if ( z  <_  v ,  z ,  v )  e.  RR )
114113adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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 )
115 rpre 11238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( z  e.  RR+  ->  z  e.  RR )
1161153ad2ant2 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  z  e.  RR )
117116ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  /\  ( abs `  ( a  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
z  e.  RR )
118 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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 ) )
119115adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( z  e.  RR+  /\  v  e.  RR+ )  ->  z  e.  RR )
120 rpre 11238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( v  e.  RR+  ->  v  e.  RR )
121120adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( z  e.  RR+  /\  v  e.  RR+ )  ->  v  e.  RR )
122 min1 11401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( z  e.  RR  /\  v  e.  RR )  ->  if ( z  <_ 
v ,  z ,  v )  <_  z
)
123119, 121, 122syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( z  e.  RR+  /\  v  e.  RR+ )  ->  if ( z  <_  v ,  z ,  v )  <_  z )
1241233adant1 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  if ( z  <_  v ,  z ,  v )  <_ 
z )
125124ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  /\  ( abs `  ( a  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  ->  if ( z  <_  v ,  z ,  v )  <_  z )
126111, 114, 117, 118, 125ltletrd 9753 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  /\  ( abs `  ( a  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
( abs `  (
a  -  B ) )  <  z )
1271213adant1 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  v  e.  RR )
128127ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  /\  ( abs `  ( a  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
v  e.  RR )
129 min2 11402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( z  e.  RR  /\  v  e.  RR )  ->  if ( z  <_ 
v ,  z ,  v )  <_  v
)
130119, 121, 129syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( z  e.  RR+  /\  v  e.  RR+ )  ->  if ( z  <_  v ,  z ,  v )  <_  v )
1311303adant1 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  if ( z  <_  v ,  z ,  v )  <_ 
v )
132131ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  /\  ( abs `  ( a  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  ->  if ( z  <_  v ,  z ,  v )  <_  v )
133111, 114, 128, 118, 132ltletrd 9753 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  a  e.  RR )  /\  ( abs `  ( a  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
( abs `  (
a  -  B ) )  <  v )
134126, 133jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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 ) )
135134ex 434 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
136101, 105, 135syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 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 ) ) )
137136reximdva 2942 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
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 ) ) )
138100, 137mpd 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  E. a  e.  ( ( A  i^i  ( -oo (,) B ) ) 
\  { B }
) ( ( abs `  ( a  -  B
) )  <  z  /\  ( abs `  (
a  -  B ) )  <  v ) )
13968, 69, 70, 138syl3anc 1228 . . . . . . . . . . . . . . . . . . . . 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 ) )  ->  E. a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } ) ( ( abs `  ( a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  < 
v ) )
140 nfv 1683 . . . . . . . . . . . . . . . . . . . . . 22  |-  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 ) )
141 nfre1 2928 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ a E. a  e.  A  ( ( abs `  (
( F `  a
)  -  x ) )  <  y  /\  ( abs `  ( ( F `  a )  -  L ) )  <  y )
142 inss1 3723 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( A  i^i  ( -oo (,) B ) )  C_  A
143142, 103sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  -> 
a  e.  A )
1441433ad2ant2 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
)
145 simp113 1127 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( 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
) )
146 eldifsni 4159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  -> 
a  =/=  B )
147146adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  ( ( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v ) )  ->  a  =/=  B
)
148 simprl 755 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  ( ( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v ) )  ->  ( abs `  (
a  -  B ) )  <  z )
149147, 148jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  ( ( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v ) )  ->  ( a  =/= 
B  /\  ( abs `  ( a  -  B
) )  <  z
) )
1501493adant1 1014 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( 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
) )
151 neeq1 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( w  =  a  ->  (
w  =/=  B  <->  a  =/=  B ) )
152 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( w  =  a  ->  (
w  -  B )  =  ( a  -  B ) )
153152fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( w  =  a  ->  ( abs `  ( w  -  B ) )  =  ( abs `  (
a  -  B ) ) )
154153breq1d 4463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( w  =  a  ->  (
( abs `  (
w  -  B ) )  <  z  <->  ( abs `  ( a  -  B
) )  <  z
) )
155151, 154anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( w  =  a  ->  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  z )  <-> 
( a  =/=  B  /\  ( abs `  (
a  -  B ) )  <  z ) ) )
156 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( w  =  a  ->  ( F `  w )  =  ( F `  a ) )
157156oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( w  =  a  ->  (
( F `  w
)  -  x )  =  ( ( F `
 a )  -  x ) )
158157fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( w  =  a  ->  ( abs `  ( ( F `
 w )  -  x ) )  =  ( abs `  (
( F `  a
)  -  x ) ) )
159158breq1d 4463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( w  =  a  ->  (
( abs `  (
( F `  w
)  -  x ) )  <  y  <->  ( abs `  ( ( F `  a )  -  x
) )  <  y
) )
160155, 159imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w  =  a  ->  (
( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  z
)  ->  ( abs `  ( ( F `  w )  -  x
) )  <  y
)  <->  ( ( a  =/=  B  /\  ( abs `  ( a  -  B ) )  < 
z )  ->  ( abs `  ( ( F `
 a )  -  x ) )  < 
y ) ) )
161160rspcva 3217 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 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 ) )
162161imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 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 )
163144, 145, 150, 162syl21anc 1227 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )  ->  ( abs `  (
( F `  a
)  -  x ) )  <  y )
1641033ad2ant2 1018 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( 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 ) ) )
165683ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . 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  ( -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 )
166 simp13 1028 . . . . . . . . . . . . . . . . . . . . . . . . . . 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  ( -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 ) )
167 nfv 1683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  F/ w ph
168 nfra1 2848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  F/ w A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  v )  ->  ( abs `  (
( ( F  |`  ( -oo (,) B ) ) `  w )  -  L ) )  <  y )
169167, 168nfan 1875 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  F/ w
( ph  /\  A. w  e.  ( A  i^i  ( -oo (,) B ) ) ( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) )  <  y ) )
17043sseli 3505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( w  e.  ( A  i^i  ( -oo (,) B ) )  ->  w  e.  ( -oo (,) B ) )
171 fvres 5886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( w  e.  ( -oo (,) B )  ->  (
( F  |`  ( -oo (,) B ) ) `
 w )  =  ( F `  w
) )
172170, 171syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( w  e.  ( A  i^i  ( -oo (,) B ) )  ->  ( ( F  |`  ( -oo (,) B ) ) `  w )  =  ( F `  w ) )
173172eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( w  e.  ( A  i^i  ( -oo (,) B ) )  ->  ( F `  w )  =  ( ( F  |`  ( -oo (,) B ) ) `
 w ) )
174173oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( w  e.  ( A  i^i  ( -oo (,) B ) )  ->  ( ( F `  w )  -  L )  =  ( ( ( F  |`  ( -oo (,) B ) ) `  w )  -  L ) )
175174fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( w  e.  ( A  i^i  ( -oo (,) B ) )  ->  ( abs `  ( ( F `  w )  -  L
) )  =  ( abs `  ( ( ( F  |`  ( -oo (,) B ) ) `
 w )  -  L ) ) )
176175adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( 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 ) ) )  ->  ( abs `  (
( F `  w
)  -  L ) )  =  ( abs `  ( ( ( F  |`  ( -oo (,) B
) ) `  w
)  -  L ) ) )
1771763adant3 1016 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( 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 ) ) )
178 simp3 998 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( 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 ) )  ->  ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
) )
179 rspa 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( 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 ) )
1801793adant3 1016 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( 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 ) )  ->  ( ( w  =/=  B  /\  ( abs `  ( w  -  B ) )  < 
v )  ->  ( abs `  ( ( ( F  |`  ( -oo (,) B ) ) `  w )  -  L
) )  <  y
) )
181178, 180mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( 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 )
1821813adant1l 1220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( 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 )
183177, 182eqbrtrd 4473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( 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
)
1841833exp 1195 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )  < 
y ) ) )
185169, 184ralrimi 2867 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
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
) )
186165, 166, 185syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( 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 ) )
187146anim1i 568 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  ( abs `  ( a  -  B ) )  <  v )  -> 
( a  =/=  B  /\  ( abs `  (
a  -  B ) )  <  v ) )
188187adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( a  e.  ( ( A  i^i  ( -oo (,) B ) )  \  { B } )  /\  ( ( abs `  (
a  -  B ) )  <  z  /\  ( abs `  ( a  -  B ) )  <  v ) )  ->  ( a  =/= 
B  /\  ( abs `  ( a  -  B
) )  <  v
) )
1891883adant1 1014 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( 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
) )
190153breq1d 4463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( w  =  a  ->  (
( abs `  (
w  -  B ) )  <  v  <->  ( abs `  ( a  -  B
) )  <  v
) )
191151, 190anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( w  =  a  ->  (
( w  =/=  B  /\  ( abs `  (
w  -  B ) )  <  v )  <-> 
( a  =/=  B  /\  ( abs `  (
a  -  B ) )  <  v ) ) )
192156oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( w  =  a  ->  (
( F `  w
)  -  L )  =  ( ( F `
 a )  -  L ) )
193192fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( w  =  a  ->  ( abs `  ( ( F `
 w )  -  L ) )  =  ( abs `  (
( F `  a
)  -  L ) ) )
194193breq1d 4463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( w  =  a  ->  (
( abs `  (
( F `  w
)  -  L ) )  <  y  <->  ( abs `  ( ( F `  a )  -  L
) )  <  y
) )
195191, 194imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w  =  a  ->  (
( ( w  =/= 
B  /\  ( abs `  ( w  -  B
) )  <  v
)  ->  ( abs `  ( ( F `  w )  -  L
) )  <  y
)  <->  ( ( a  =/=  B  /\  ( abs `  ( a  -  B ) )  < 
v )  ->  ( abs `  ( ( F `
 a )  -  L ) )  < 
y ) ) )
196195rspcva 3217 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 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 ) )
197196imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 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 )
198164, 186, 189, 197syl21anc 1227 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )  ->  ( abs `  (
( F `  a
)  -  L ) )  <  y )
199163, 198jca 532 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )  ->  ( ( abs `  ( ( F `  a )  -  x
) )  <  y  /\  ( abs `  (
( F `  a
)  -  L ) )  <  y ) )
200 rspe 2925 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 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 ) )
201144, 199, 200syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 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 ) )  ->  E. a  e.  A  ( ( abs `  (
( F `  a
)  -  x ) )  <  y  /\  ( abs `  ( ( F `  a )  -  L ) )  <  y ) )
2022013exp 1195 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
203140, 141, 202rexlimd 2951 . . . . . . . . . . . . . . . . . . . . 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 ) )  ->  ( 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 ) ) )
204139, 203mpd 15 . . . . . . . . . . . . . . . . . . . 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  ( ( abs `  ( ( F `
 a )  -  x ) )  < 
y  /\  ( abs `  ( ( F `  a )  -  L
) )  <  y
) )
2052043exp 1195 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
206205rexlimdv 2957 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 ) ) )
20767, 206mpd 15 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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
) )
2082073exp 1195 . . . . . . . . . . . . . . . 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 ) ) ) )
209208rexlimdv 2957 . . . . . . . . . . . . . . 15  |-  ( (
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 ) ) )
210209imp 429 . . . . . . . . . . . . . 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
) )
211210adantllr 718 . . . . . . . . . . . . 13  |-  ( ( ( ( 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
) )
212 fresin 5760 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( F : A --> CC  ->  ( F  |`  ( B (,) +oo ) ) : ( A  i^i  ( B (,) +oo ) ) --> CC )
21340, 212syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( F  |`  ( B (,) +oo ) ) : ( A  i^i  ( B (,) +oo )
) --> CC )
214 inss2 3724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( A  i^i  ( B (,) +oo ) )  C_  ( B (,) +oo )
215 ioosscn 31414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( B (,) +oo )  C_  CC
216214, 215sstri 3518 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( A  i^i  ( B (,) +oo ) )  C_  CC
217216a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( A  i^i  ( B (,) +oo ) ) 
C_  CC )
218213, 217, 62ellimc3 22151 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 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 ) ) ) )
2191, 218mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 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 ) ) )
220219simprd 463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 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 ) )
221220r19.21bi 2836 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
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 ) )
2222213ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 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 ) )
223 simp11l 1107 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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 )
224 simp12 1027 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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+ )
225 simp2 997 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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+ )
226 inss1 3723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( limPt `  K ) `  ( A  i^i  ( B (,) +oo ) ) )  i^i  RR ) 
C_  ( ( limPt `  K ) `  ( A  i^i  ( B (,) +oo ) ) )
227226a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  ( ( ( limPt `  K ) `  ( A  i^i  ( B (,) +oo ) ) )  i^i 
RR )  C_  (
( limPt `  K ) `  ( A  i^i  ( B (,) +oo ) ) ) )
228 ioossre 11598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( B (,) +oo )  C_  RR
229214, 228sstri 3518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( A  i^i  ( B (,) +oo ) )  C_  RR
230229a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  ( A  i^i  ( B (,) +oo ) ) 
C_  RR )
23182, 84restlp 19552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( 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 ) )
23277, 48, 230, 231syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  ( ( limPt `  J
) `  ( A  i^i  ( B (,) +oo ) ) )  =  ( ( ( limPt `  K ) `  ( A  i^i  ( B (,) +oo ) ) )  i^i 
RR ) )
23388fveq1i 5873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
limPt `  ( TopOpen ` fld ) ) `  ( A  i^i  ( B (,) +oo ) ) )  =  ( ( limPt `  K
) `  ( A  i^i  ( B (,) +oo ) ) )
234233a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  ( ( limPt `  ( TopOpen
` fld
) ) `  ( A  i^i  ( B (,) +oo ) ) )  =  ( ( limPt `  K
) `  ( A  i^i  ( B (,) +oo ) ) ) )
235232, 234sseq12d 3538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  ( ( ( limPt `  J ) `  ( A  i^i  ( B (,) +oo ) ) )  C_  ( ( limPt `  ( TopOpen
` fld
) ) `  ( A  i^i  ( B (,) +oo ) ) )  <->  ( (
( limPt `  K ) `  ( A  i^i  ( B (,) +oo ) ) )  i^i  RR ) 
C_  ( ( limPt `  K ) `  ( A  i^i  ( B (,) +oo ) ) ) ) )
236227, 235mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ( ( limPt `  J
) `  ( A  i^i  ( B (,) +oo ) ) )  C_  ( ( limPt `  ( TopOpen
` fld
) ) `  ( A  i^i  ( B (,) +oo ) ) ) )
237 limclner.blp2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  B  e.  ( (
limPt `  J ) `  ( A  i^i  ( B (,) +oo ) ) ) )
238236, 237sseldd 3510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  B  e.  ( (
limPt `  ( TopOpen ` fld ) ) `  ( A  i^i  ( B (,) +oo ) ) ) )
239217, 62islpcn 31504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 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
) )
240238, 239mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  A. u  e.  RR+  E. b  e.  ( ( A  i^i  ( B (,) +oo ) ) 
\  { B }
) ( abs `  (
b  -  B ) )  <  u )
2412403ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  A. u  e.  RR+  E. b  e.  ( ( A  i^i  ( B (,) +oo ) ) 
\  { B }
) ( abs `  (
b  -  B ) )  <  u )
242 breq2 4457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( u  =  if ( z  <_  v ,  z ,  v )  -> 
( ( abs `  (
b  -  B ) )  <  u  <->  ( abs `  ( b  -  B
) )  <  if ( z  <_  v ,  z ,  v ) ) )
243242rexbidv 2978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 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 ) ) )
244243rspcva 3217 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 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 ) )
24572, 241, 244syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  E. b  e.  ( ( A  i^i  ( B (,) +oo ) ) 
\  { B }
) ( abs `  (
b  -  B ) )  <  if ( z  <_  v , 
z ,  v ) )
246 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  ( ( A  i^i  ( B (,) +oo )
)  \  { B } ) )  -> 
( ph  /\  z  e.  RR+  /\  v  e.  RR+ ) )
247 eldifi 3631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( b  e.  ( ( A  i^i  ( B (,) +oo ) )  \  { B } )  ->  b  e.  ( A  i^i  ( B (,) +oo ) ) )
248229, 247sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( b  e.  ( ( A  i^i  ( B (,) +oo ) )  \  { B } )  ->  b  e.  RR )
249248adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  ( ( A  i^i  ( B (,) +oo )
)  \  { B } ) )  -> 
b  e.  RR )
25048sselda 3509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  b  e.  RR )  ->  b  e.  CC )
25162adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  b  e.  RR )  ->  B  e.  CC )
252250, 251subcld 9942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  b  e.  RR )  ->  ( b  -  B )  e.  CC )
253252abscld 13247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  b  e.  RR )  ->  ( abs `  ( b  -  B
) )  e.  RR )
2542533ad2antl1 1158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  RR )  ->  ( abs `  ( b  -  B ) )  e.  RR )
255254adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  RR )  /\  ( abs `  ( b  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
( abs `  (
b  -  B ) )  e.  RR )
256112ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( 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 )
257116ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  RR )  /\  ( abs `  ( b  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
z  e.  RR )
258 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( 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 ) )
259124ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  RR )  /\  ( abs `  ( b  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  ->  if ( z  <_  v ,  z ,  v )  <_  z )
260255, 256, 257, 258, 259ltletrd 9753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  RR )  /\  ( abs `  ( b  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
( abs `  (
b  -  B ) )  <  z )
261127ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  RR )  /\  ( abs `  ( b  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
v  e.  RR )
262257, 261, 129syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  RR )  /\  ( abs `  ( b  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  ->  if ( z  <_  v ,  z ,  v )  <_  v )
263255, 256, 261, 258, 262ltletrd 9753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  z  e.  RR+  /\  v  e.  RR+ )  /\  b  e.  RR )  /\  ( abs `  ( b  -  B ) )  < 
if ( z  <_ 
v ,  z ,  v ) )  -> 
( abs `  (
b  -  B ) )  <  v )
264260, 263jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( 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 ) )
265264ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
266246, 249, 265syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( 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 ) ) )
267266reximdva 2942 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
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 ) ) )
268245, 267mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  z  e.  RR+ 
/\  v  e.  RR+ )  ->  E. b  e.  ( ( A  i^i  ( B (,) +oo ) ) 
\  { B }
) ( ( abs `  ( b  -  B
) )  <  z  /\  ( abs `  (
b  -  B ) )  <  v ) )
269223, 224, 225, 268syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )  ->  E. b  e.  ( ( A  i^i  ( B (,) +oo )
)  \  { B } ) ( ( abs `  ( b  -  B ) )  <  z  /\  ( abs `  ( b  -  B ) )  < 
v ) )
270 nfv 1683 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  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 ) )
271 nfre1 2928 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/ b E. b  e.  A  ( ( abs `  (
( F `  b
)  -  x ) )  <  y  /\  ( abs `  ( ( F `  b )  -  R ) )  <  y )
272 inss1 3723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( A  i^i  ( B (,) +oo ) )  C_  A
273272, 247sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( b  e.  ( ( A  i^i  ( B (,) +oo ) )  \  { B } )  ->  b  e.  A )
2742733ad2ant2 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 ) )  <  y ) )  /\  b  e.  ( ( A  i^i  ( B (,) +oo )
)  \  { B } )  /\  (
( abs `  (
b  -  B ) )  <  z  /\  ( abs `  ( b  -  B ) )  <  v ) )  ->  b  e.  A
)
275 simp113 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( 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
) )
276 eldifsni 4159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( b  e.  ( ( A  i^i  ( B (,) +oo ) )  \  { B } )  ->  b  =/=  B )
277276adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (