Metamath Proof Explorer

Theorem limclner

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)

Ref Expression
Hypotheses limclner.k 
|- K = ( TopOpen ` CCfld )
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 ) ) limCC B ) )
limclner.r 
|- ( ph -> R e. ( ( F |` ( B (,) +oo ) ) limCC B ) )
limclner.lner 
|- ( ph -> L =/= R )
Assertion limclner 
|- ( ph -> ( F limCC B ) = (/) )

Proof

Step Hyp Ref Expression
1 limclner.k 
 |-  K = ( TopOpen ` CCfld )
2 limclner.a 
 |-  ( ph -> A C_ RR )
3 limclner.j 
 |-  J = ( topGen ` ran (,) )
4 limclner.f 
 |-  ( ph -> F : A --> CC )
5 limclner.blp1 
 |-  ( ph -> B e. ( ( limPt ` J ) ` ( A i^i ( -oo (,) B ) ) ) )
6 limclner.blp2 
 |-  ( ph -> B e. ( ( limPt ` J ) ` ( A i^i ( B (,) +oo ) ) ) )
7 limclner.l 
 |-  ( ph -> L e. ( ( F |` ( -oo (,) B ) ) limCC B ) )
8 limclner.r 
 |-  ( ph -> R e. ( ( F |` ( B (,) +oo ) ) limCC B ) )
9 limclner.lner 
 |-  ( ph -> L =/= R )
10 limccl 
 |-  ( ( F |` ( B (,) +oo ) ) limCC B ) C_ CC
11 10 8 sselid 
 |-  ( ph -> R e. CC )
12 11 ad2antrr 
 |-  ( ( ( 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 )
13 limccl 
 |-  ( ( F |` ( -oo (,) B ) ) limCC B ) C_ CC
14 13 7 sselid 
 |-  ( ph -> L e. CC )
15 14 ad2antrr 
 |-  ( ( ( 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 )
16 12 15 subcld 
 |-  ( ( ( 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 )
17 9 necomd 
 |-  ( ph -> R =/= L )
18 17 ad2antrr 
 |-  ( ( ( 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 )
19 12 15 18 subne0d 
 |-  ( ( ( 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 )
20 16 19 absrpcld 
 |-  ( ( ( 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+ )
21 4re 
 |-  4 e. RR
22 4pos 
 |-  0 < 4
23 21 22 elrpii 
 |-  4 e. RR+
24 23 a1i 
 |-  ( ( ( 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+ )
25 20 24 rpdivcld 
 |-  ( ( ( 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+ )
26 nfv 
 |-  F/ y ( ph /\ x e. CC )
27 nfra1 
 |-  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 )
28 26 27 nfan 
 |-  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 ) )
29 nfv 
 |-  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 ) ) )
30 28 29 nfim 
 |-  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 ) ) ) )
31 ovex 
 |-  ( ( abs ` ( R - L ) ) / 4 ) e. _V
32 eleq1 
 |-  ( y = ( ( abs ` ( R - L ) ) / 4 ) -> ( y e. RR+ <-> ( ( abs ` ( R - L ) ) / 4 ) e. RR+ ) )
33 oveq2 
 |-  ( y = ( ( abs ` ( R - L ) ) / 4 ) -> ( 4 x. y ) = ( 4 x. ( ( abs ` ( R - L ) ) / 4 ) ) )
34 33 breq2d 
 |-  ( y = ( ( abs ` ( R - L ) ) / 4 ) -> ( ( abs ` ( R - L ) ) < ( 4 x. y ) <-> ( abs ` ( R - L ) ) < ( 4 x. ( ( abs ` ( R - L ) ) / 4 ) ) ) )
35 34 2rexbidv 
 |-  ( 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 ) ) ) )
36 32 35 imbi12d 
 |-  ( 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 ) ) ) ) )
37 36 imbi2d 
 |-  ( 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 ) ) ) ) ) )
38 simpll 
 |-  ( ( ( ( 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 ) )
39 simpr 
 |-  ( ( ( ( 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+ )
40 rspa 
 |-  ( ( 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 ) )
41 40 adantll 
 |-  ( ( ( ( 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 ) )
42 fresin 
 |-  ( F : A --> CC -> ( F |` ( B (,) +oo ) ) : ( A i^i ( B (,) +oo ) ) --> CC )
43 4 42 syl 
 |-  ( ph -> ( F |` ( B (,) +oo ) ) : ( A i^i ( B (,) +oo ) ) --> CC )
44 inss2 
 |-  ( A i^i ( B (,) +oo ) ) C_ ( B (,) +oo )
45 ioosscn 
 |-  ( B (,) +oo ) C_ CC
46 44 45 sstri 
 |-  ( A i^i ( B (,) +oo ) ) C_ CC
47 46 a1i 
 |-  ( ph -> ( A i^i ( B (,) +oo ) ) C_ CC )
48 retop 
 |-  ( topGen ` ran (,) ) e. Top
49 3 48 eqeltri 
 |-  J e. Top
50 inss2 
 |-  ( A i^i ( -oo (,) B ) ) C_ ( -oo (,) B )
51 ioossre 
 |-  ( -oo (,) B ) C_ RR
52 50 51 sstri 
 |-  ( A i^i ( -oo (,) B ) ) C_ RR
53 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
54 3 unieqi 
 |-  U. J = U. ( topGen ` ran (,) )
55 53 54 eqtr4i 
 |-  RR = U. J
56 55 lpss 
 |-  ( ( J e. Top /\ ( A i^i ( -oo (,) B ) ) C_ RR ) -> ( ( limPt ` J ) ` ( A i^i ( -oo (,) B ) ) ) C_ RR )
57 49 52 56 mp2an 
 |-  ( ( limPt ` J ) ` ( A i^i ( -oo (,) B ) ) ) C_ RR
58 57 5 sselid 
 |-  ( ph -> B e. RR )
59 58 recnd 
 |-  ( ph -> B e. CC )
60 43 47 59 ellimc3 
 |-  ( ph -> ( R e. ( ( F |` ( B (,) +oo ) ) limCC 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 ) ) ) )
61 8 60 mpbid 
 |-  ( 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 ) ) )
62 61 simprd 
 |-  ( 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 ) )
63 62 r19.21bi 
 |-  ( ( 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 ) )
64 63 3ad2ant1 
 |-  ( ( ( 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 ) )
65 simp11l 
 |-  ( ( ( ( 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 )
66 simp12 
 |-  ( ( ( ( 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+ )
67 simp2 
 |-  ( ( ( ( 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+ )
68 breq2 
 |-  ( u = if ( z <_ v , z , v ) -> ( ( abs ` ( b - B ) ) < u <-> ( abs ` ( b - B ) ) < if ( z <_ v , z , v ) ) )
69 68 rexbidv 
 |-  ( 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 ) ) )
70 inss1 
 |-  ( ( ( limPt ` K ) ` ( A i^i ( B (,) +oo ) ) ) i^i RR ) C_ ( ( limPt ` K ) ` ( A i^i ( B (,) +oo ) ) )
71 70 a1i 
 |-  ( ph -> ( ( ( limPt ` K ) ` ( A i^i ( B (,) +oo ) ) ) i^i RR ) C_ ( ( limPt ` K ) ` ( A i^i ( B (,) +oo ) ) ) )
72 1 cnfldtop 
 |-  K e. Top
73 72 a1i 
 |-  ( ph -> K e. Top )
74 ax-resscn 
 |-  RR C_ CC
75 74 a1i 
 |-  ( ph -> RR C_ CC )
76 ioossre 
 |-  ( B (,) +oo ) C_ RR
77 44 76 sstri 
 |-  ( A i^i ( B (,) +oo ) ) C_ RR
78 77 a1i 
 |-  ( ph -> ( A i^i ( B (,) +oo ) ) C_ RR )
79 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
80 1 unieqi 
 |-  U. K = U. ( TopOpen ` CCfld )
81 79 80 eqtr4i 
 |-  CC = U. K
82 1 tgioo2 
 |-  ( topGen ` ran (,) ) = ( K |`t RR )
83 3 82 eqtri 
 |-  J = ( K |`t RR )
84 81 83 restlp 
 |-  ( ( 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 ) )
85 73 75 78 84 syl3anc 
 |-  ( ph -> ( ( limPt ` J ) ` ( A i^i ( B (,) +oo ) ) ) = ( ( ( limPt ` K ) ` ( A i^i ( B (,) +oo ) ) ) i^i RR ) )
86 1 eqcomi 
 |-  ( TopOpen ` CCfld ) = K
87 86 fveq2i 
 |-  ( limPt ` ( TopOpen ` CCfld ) ) = ( limPt ` K )
88 87 fveq1i 
 |-  ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( A i^i ( B (,) +oo ) ) ) = ( ( limPt ` K ) ` ( A i^i ( B (,) +oo ) ) )
89 88 a1i 
 |-  ( ph -> ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( A i^i ( B (,) +oo ) ) ) = ( ( limPt ` K ) ` ( A i^i ( B (,) +oo ) ) ) )
90 71 85 89 3sstr4d 
 |-  ( ph -> ( ( limPt ` J ) ` ( A i^i ( B (,) +oo ) ) ) C_ ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( A i^i ( B (,) +oo ) ) ) )
91 90 6 sseldd 
 |-  ( ph -> B e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( A i^i ( B (,) +oo ) ) ) )
92 47 59 islpcn 
 |-  ( ph -> ( B e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( A i^i ( B (,) +oo ) ) ) <-> A. u e. RR+ E. b e. ( ( A i^i ( B (,) +oo ) ) \ { B } ) ( abs ` ( b - B ) ) < u ) )
93 91 92 mpbid 
 |-  ( ph -> A. u e. RR+ E. b e. ( ( A i^i ( B (,) +oo ) ) \ { B } ) ( abs ` ( b - B ) ) < u )
94 93 3ad2ant1 
 |-  ( ( ph /\ z e. RR+ /\ v e. RR+ ) -> A. u e. RR+ E. b e. ( ( A i^i ( B (,) +oo ) ) \ { B } ) ( abs ` ( b - B ) ) < u )
95 ifcl 
 |-  ( ( z e. RR+ /\ v e. RR+ ) -> if ( z <_ v , z , v ) e. RR+ )
96 95 3adant1 
 |-  ( ( ph /\ z e. RR+ /\ v e. RR+ ) -> if ( z <_ v , z , v ) e. RR+ )
97 69 94 96 rspcdva 
 |-  ( ( ph /\ z e. RR+ /\ v e. RR+ ) -> E. b e. ( ( A i^i ( B (,) +oo ) ) \ { B } ) ( abs ` ( b - B ) ) < if ( z <_ v , z , v ) )
98 eldifi 
 |-  ( b e. ( ( A i^i ( B (,) +oo ) ) \ { B } ) -> b e. ( A i^i ( B (,) +oo ) ) )
99 77 98 sselid 
 |-  ( b e. ( ( A i^i ( B (,) +oo ) ) \ { B } ) -> b e. RR )
100 75 sselda 
 |-  ( ( ph /\ b e. RR ) -> b e. CC )
101 59 adantr 
 |-  ( ( ph /\ b e. RR ) -> B e. CC )
102 100 101 subcld 
 |-  ( ( ph /\ b e. RR ) -> ( b - B ) e. CC )
103 102 abscld 
 |-  ( ( ph /\ b e. RR ) -> ( abs ` ( b - B ) ) e. RR )
104 103 3ad2antl1 
 |-  ( ( ( ph /\ z e. RR+ /\ v e. RR+ ) /\ b e. RR ) -> ( abs ` ( b - B ) ) e. RR )
105 104 adantr 
 |-  ( ( ( ( ph /\ z e. RR+ /\ v e. RR+ ) /\ b e. RR ) /\ ( abs ` ( b - B ) ) < if ( z <_ v , z , v ) ) -> ( abs ` ( b - B ) ) e. RR )
106 96 rpred 
 |-  ( ( ph /\ z e. RR+ /\ v e. RR+ ) -> if ( z <_ v , z , v ) e. RR )
107 106 ad2antrr 
 |-  ( ( ( ( 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 )
108 rpre 
 |-  ( z e. RR+ -> z e. RR )
109 108 3ad2ant2 
 |-  ( ( ph /\ z e. RR+ /\ v e. RR+ ) -> z e. RR )
110 109 ad2antrr 
 |-  ( ( ( ( ph /\ z e. RR+ /\ v e. RR+ ) /\ b e. RR ) /\ ( abs ` ( b - B ) ) < if ( z <_ v , z , v ) ) -> z e. RR )
111 simpr 
 |-  ( ( ( ( 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 ) )
112 rpre 
 |-  ( v e. RR+ -> v e. RR )
113 min1 
 |-  ( ( z e. RR /\ v e. RR ) -> if ( z <_ v , z , v ) <_ z )
114 108 112 113 syl2an 
 |-  ( ( z e. RR+ /\ v e. RR+ ) -> if ( z <_ v , z , v ) <_ z )
115 114 3adant1 
 |-  ( ( ph /\ z e. RR+ /\ v e. RR+ ) -> if ( z <_ v , z , v ) <_ z )
116 115 ad2antrr 
 |-  ( ( ( ( ph /\ z e. RR+ /\ v e. RR+ ) /\ b e. RR ) /\ ( abs ` ( b - B ) ) < if ( z <_ v , z , v ) ) -> if ( z <_ v , z , v ) <_ z )
117 105 107 110 111 116 ltletrd 
 |-  ( ( ( ( ph /\ z e. RR+ /\ v e. RR+ ) /\ b e. RR ) /\ ( abs ` ( b - B ) ) < if ( z <_ v , z , v ) ) -> ( abs ` ( b - B ) ) < z )
118 112 3ad2ant3 
 |-  ( ( ph /\ z e. RR+ /\ v e. RR+ ) -> v e. RR )
119 118 ad2antrr 
 |-  ( ( ( ( ph /\ z e. RR+ /\ v e. RR+ ) /\ b e. RR ) /\ ( abs ` ( b - B ) ) < if ( z <_ v , z , v ) ) -> v e. RR )
120 110 119 min2d 
 |-  ( ( ( ( ph /\ z e. RR+ /\ v e. RR+ ) /\ b e. RR ) /\ ( abs ` ( b - B ) ) < if ( z <_ v , z , v ) ) -> if ( z <_ v , z , v ) <_ v )
121 105 107 119 111 120 ltletrd 
 |-  ( ( ( ( ph /\ z e. RR+ /\ v e. RR+ ) /\ b e. RR ) /\ ( abs ` ( b - B ) ) < if ( z <_ v , z , v ) ) -> ( abs ` ( b - B ) ) < v )
122 117 121 jca 
 |-  ( ( ( ( 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 ) )
123 122 ex 
 |-  ( ( ( 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 ) ) )
124 99 123 sylan2 
 |-  ( ( ( 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 ) ) )
125 124 reximdva 
 |-  ( ( 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 ) ) )
126 97 125 mpd 
 |-  ( ( ph /\ z e. RR+ /\ v e. RR+ ) -> E. b e. ( ( A i^i ( B (,) +oo ) ) \ { B } ) ( ( abs ` ( b - B ) ) < z /\ ( abs ` ( b - B ) ) < v ) )
127 65 66 67 126 syl3anc 
 |-  ( ( ( ( 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 ) )
128 nfv 
 |-  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 ) )
129 nfre1 
 |-  F/ b E. b e. A ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y )
130 98 elin1d 
 |-  ( b e. ( ( A i^i ( B (,) +oo ) ) \ { B } ) -> b e. A )
131 130 3ad2ant2 
 |-  ( ( ( ( ( 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 )
132 simp113 
 |-  ( ( ( ( ( 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 ) )
133 eldifsni 
 |-  ( b e. ( ( A i^i ( B (,) +oo ) ) \ { B } ) -> b =/= B )
134 133 adantr 
 |-  ( ( b e. ( ( A i^i ( B (,) +oo ) ) \ { B } ) /\ ( ( abs ` ( b - B ) ) < z /\ ( abs ` ( b - B ) ) < v ) ) -> b =/= B )
135 simprl 
 |-  ( ( b e. ( ( A i^i ( B (,) +oo ) ) \ { B } ) /\ ( ( abs ` ( b - B ) ) < z /\ ( abs ` ( b - B ) ) < v ) ) -> ( abs ` ( b - B ) ) < z )
136 134 135 jca 
 |-  ( ( b e. ( ( A i^i ( B (,) +oo ) ) \ { B } ) /\ ( ( abs ` ( b - B ) ) < z /\ ( abs ` ( b - B ) ) < v ) ) -> ( b =/= B /\ ( abs ` ( b - B ) ) < z ) )
137 136 3adant1 
 |-  ( ( ( ( ( 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 ) )
138 neeq1 
 |-  ( w = b -> ( w =/= B <-> b =/= B ) )
139 fvoveq1 
 |-  ( w = b -> ( abs ` ( w - B ) ) = ( abs ` ( b - B ) ) )
140 139 breq1d 
 |-  ( w = b -> ( ( abs ` ( w - B ) ) < z <-> ( abs ` ( b - B ) ) < z ) )
141 138 140 anbi12d 
 |-  ( w = b -> ( ( w =/= B /\ ( abs ` ( w - B ) ) < z ) <-> ( b =/= B /\ ( abs ` ( b - B ) ) < z ) ) )
142 141 imbrov2fvoveq 
 |-  ( w = b -> ( ( ( w =/= B /\ ( abs ` ( w - B ) ) < z ) -> ( abs ` ( ( F ` w ) - x ) ) < y ) <-> ( ( b =/= B /\ ( abs ` ( b - B ) ) < z ) -> ( abs ` ( ( F ` b ) - x ) ) < y ) ) )
143 142 rspcva 
 |-  ( ( 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 ) )
144 143 imp 
 |-  ( ( ( 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 )
145 131 132 137 144 syl21anc 
 |-  ( ( ( ( ( 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 )
146 98 3ad2ant2 
 |-  ( ( ( ( ( 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 i^i ( B (,) +oo ) ) )
147 65 3ad2ant1 
 |-  ( ( ( ( ( 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 ) ) -> ph )
148 simp13 
 |-  ( ( ( ( ( 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 i^i ( B (,) +oo ) ) ( ( w =/= B /\ ( abs ` ( w - B ) ) < v ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` w ) - R ) ) < y ) )
149 nfv 
 |-  F/ w ph
150 nfra1 
 |-  F/ w A. w e. ( A i^i ( B (,) +oo ) ) ( ( w =/= B /\ ( abs ` ( w - B ) ) < v ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` w ) - R ) ) < y )
151 149 150 nfan 
 |-  F/ w ( ph /\ A. w e. ( A i^i ( B (,) +oo ) ) ( ( w =/= B /\ ( abs ` ( w - B ) ) < v ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` w ) - R ) ) < y ) )
152 elinel2 
 |-  ( w e. ( A i^i ( B (,) +oo ) ) -> w e. ( B (,) +oo ) )
153 152 fvresd 
 |-  ( w e. ( A i^i ( B (,) +oo ) ) -> ( ( F |` ( B (,) +oo ) ) ` w ) = ( F ` w ) )
154 153 eqcomd 
 |-  ( w e. ( A i^i ( B (,) +oo ) ) -> ( F ` w ) = ( ( F |` ( B (,) +oo ) ) ` w ) )
155 154 fvoveq1d 
 |-  ( w e. ( A i^i ( B (,) +oo ) ) -> ( abs ` ( ( F ` w ) - R ) ) = ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` w ) - R ) ) )
156 155 3ad2ant2 
 |-  ( ( ( ph /\ A. w e. ( A i^i ( B (,) +oo ) ) ( ( w =/= B /\ ( abs ` ( w - B ) ) < v ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` w ) - R ) ) < y ) ) /\ w e. ( A i^i ( B (,) +oo ) ) /\ ( w =/= B /\ ( abs ` ( w - B ) ) < v ) ) -> ( abs ` ( ( F ` w ) - R ) ) = ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` w ) - R ) ) )
157 rspa 
 |-  ( ( A. w e. ( A i^i ( B (,) +oo ) ) ( ( w =/= B /\ ( abs ` ( w - B ) ) < v ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` w ) - R ) ) < y ) /\ w e. ( A i^i ( B (,) +oo ) ) ) -> ( ( w =/= B /\ ( abs ` ( w - B ) ) < v ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` w ) - R ) ) < y ) )
158 157 3impia 
 |-  ( ( A. w e. ( A i^i ( B (,) +oo ) ) ( ( w =/= B /\ ( abs ` ( w - B ) ) < v ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` w ) - R ) ) < y ) /\ w e. ( A i^i ( B (,) +oo ) ) /\ ( w =/= B /\ ( abs ` ( w - B ) ) < v ) ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` w ) - R ) ) < y )
159 158 3adant1l 
 |-  ( ( ( ph /\ A. w e. ( A i^i ( B (,) +oo ) ) ( ( w =/= B /\ ( abs ` ( w - B ) ) < v ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` w ) - R ) ) < y ) ) /\ w e. ( A i^i ( B (,) +oo ) ) /\ ( w =/= B /\ ( abs ` ( w - B ) ) < v ) ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` w ) - R ) ) < y )
160 156 159 eqbrtrd 
 |-  ( ( ( ph /\ A. w e. ( A i^i ( B (,) +oo ) ) ( ( w =/= B /\ ( abs ` ( w - B ) ) < v ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` w ) - R ) ) < y ) ) /\ w e. ( A i^i ( B (,) +oo ) ) /\ ( w =/= B /\ ( abs ` ( w - B ) ) < v ) ) -> ( abs ` ( ( F ` w ) - R ) ) < y )
161 160 3exp 
 |-  ( ( ph /\ A. w e. ( A i^i ( B (,) +oo ) ) ( ( w =/= B /\ ( abs ` ( w - B ) ) < v ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` w ) - R ) ) < y ) ) -> ( w e. ( A i^i ( B (,) +oo ) ) -> ( ( w =/= B /\ ( abs ` ( w - B ) ) < v ) -> ( abs ` ( ( F ` w ) - R ) ) < y ) ) )
162 151 161 ralrimi 
 |-  ( ( ph /\ A. w e. ( A i^i ( B (,) +oo ) ) ( ( w =/= B /\ ( abs ` ( w - B ) ) < v ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` w ) - R ) ) < y ) ) -> A. w e. ( A i^i ( B (,) +oo ) ) ( ( w =/= B /\ ( abs ` ( w - B ) ) < v ) -> ( abs ` ( ( F ` w ) - R ) ) < y ) )
163 147 148 162 syl2anc 
 |-  ( ( ( ( ( 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 i^i ( B (,) +oo ) ) ( ( w =/= B /\ ( abs ` ( w - B ) ) < v ) -> ( abs ` ( ( F ` w ) - R ) ) < y ) )
164 133 anim1i 
 |-  ( ( b e. ( ( A i^i ( B (,) +oo ) ) \ { B } ) /\ ( abs ` ( b - B ) ) < v ) -> ( b =/= B /\ ( abs ` ( b - B ) ) < v ) )
165 164 adantrl 
 |-  ( ( b e. ( ( A i^i ( B (,) +oo ) ) \ { B } ) /\ ( ( abs ` ( b - B ) ) < z /\ ( abs ` ( b - B ) ) < v ) ) -> ( b =/= B /\ ( abs ` ( b - B ) ) < v ) )
166 165 3adant1 
 |-  ( ( ( ( ( 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 ) ) < v ) )
167 139 breq1d 
 |-  ( w = b -> ( ( abs ` ( w - B ) ) < v <-> ( abs ` ( b - B ) ) < v ) )
168 138 167 anbi12d 
 |-  ( w = b -> ( ( w =/= B /\ ( abs ` ( w - B ) ) < v ) <-> ( b =/= B /\ ( abs ` ( b - B ) ) < v ) ) )
169 168 imbrov2fvoveq 
 |-  ( w = b -> ( ( ( w =/= B /\ ( abs ` ( w - B ) ) < v ) -> ( abs ` ( ( F ` w ) - R ) ) < y ) <-> ( ( b =/= B /\ ( abs ` ( b - B ) ) < v ) -> ( abs ` ( ( F ` b ) - R ) ) < y ) ) )
170 169 rspcva 
 |-  ( ( b e. ( A i^i ( B (,) +oo ) ) /\ A. w e. ( A i^i ( B (,) +oo ) ) ( ( w =/= B /\ ( abs ` ( w - B ) ) < v ) -> ( abs ` ( ( F ` w ) - R ) ) < y ) ) -> ( ( b =/= B /\ ( abs ` ( b - B ) ) < v ) -> ( abs ` ( ( F ` b ) - R ) ) < y ) )
171 170 imp 
 |-  ( ( ( b e. ( A i^i ( B (,) +oo ) ) /\ A. w e. ( A i^i ( B (,) +oo ) ) ( ( w =/= B /\ ( abs ` ( w - B ) ) < v ) -> ( abs ` ( ( F ` w ) - R ) ) < y ) ) /\ ( b =/= B /\ ( abs ` ( b - B ) ) < v ) ) -> ( abs ` ( ( F ` b ) - R ) ) < y )
172 146 163 166 171 syl21anc 
 |-  ( ( ( ( ( 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 ) - R ) ) < y )
173 rspe 
 |-  ( ( b e. A /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> E. b e. A ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) )
174 131 145 172 173 syl12anc 
 |-  ( ( ( ( ( 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 ) ) -> E. b e. A ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) )
175 174 3exp 
 |-  ( ( ( ( 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 ) -> E. b e. A ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) ) )
176 128 129 175 rexlimd 
 |-  ( ( ( ( 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 ) -> E. b e. A ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) )
177 127 176 mpd 
 |-  ( ( ( ( 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 ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) )
178 177 3exp 
 |-  ( ( ( 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 ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) ) )
179 178 rexlimdv 
 |-  ( ( ( 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 ) -> E. b e. A ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) )
180 64 179 mpd 
 |-  ( ( ( ph /\ y e. RR+ ) /\ z e. RR+ /\ A. w e. A ( ( w =/= B /\ ( abs ` ( w - B ) ) < z ) -> ( abs ` ( ( F ` w ) - x ) ) < y ) ) -> E. b e. A ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) )
181 180 3exp 
 |-  ( ( ph /\ y e. RR+ ) -> ( z e. RR+ -> ( A. w e. A ( ( w =/= B /\ ( abs ` ( w - B ) ) < z ) -> ( abs ` ( ( F ` w ) - x ) ) < y ) -> E. b e. A ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) ) )
182 181 rexlimdv 
 |-  ( ( ph /\ y e. RR+ ) -> ( E. z e. RR+ A. w e. A ( ( w =/= B /\ ( abs ` ( w - B ) ) < z ) -> ( abs ` ( ( F ` w ) - x ) ) < y ) -> E. b e. A ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) )
183 182 imp 
 |-  ( ( ( ph /\ y e. RR+ ) /\ E. z e. RR+ A. w e. A ( ( w =/= B /\ ( abs ` ( w - B ) ) < z ) -> ( abs ` ( ( F ` w ) - x ) ) < y ) ) -> E. b e. A ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) )
184 183 adantllr 
 |-  ( ( ( ( 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. b e. A ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) )
185 184 ad2antrr 
 |-  ( ( ( ( ( ( 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 ) ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) -> E. b e. A ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) )
186 11 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> R e. CC )
187 14 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> L e. CC )
188 186 187 subcld 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( R - L ) e. CC )
189 188 abscld 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( abs ` ( R - L ) ) e. RR )
190 simp-6l 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ph )
191 simplr 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> b e. A )
192 4 ffvelcdmda 
 |-  ( ( ph /\ b e. A ) -> ( F ` b ) e. CC )
193 190 191 192 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( F ` b ) e. CC )
194 186 193 subcld 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( R - ( F ` b ) ) e. CC )
195 194 abscld 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( abs ` ( R - ( F ` b ) ) ) e. RR )
196 simp-6r 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> x e. CC )
197 193 196 subcld 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( ( F ` b ) - x ) e. CC )
198 197 abscld 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( abs ` ( ( F ` b ) - x ) ) e. RR )
199 195 198 readdcld 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( ( abs ` ( R - ( F ` b ) ) ) + ( abs ` ( ( F ` b ) - x ) ) ) e. RR )
200 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> a e. A )
201 4 ffvelcdmda 
 |-  ( ( ph /\ a e. A ) -> ( F ` a ) e. CC )
202 190 200 201 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( F ` a ) e. CC )
203 196 202 subcld 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( x - ( F ` a ) ) e. CC )
204 203 abscld 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( abs ` ( x - ( F ` a ) ) ) e. RR )
205 199 204 readdcld 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( ( ( abs ` ( R - ( F ` b ) ) ) + ( abs ` ( ( F ` b ) - x ) ) ) + ( abs ` ( x - ( F ` a ) ) ) ) e. RR )
206 202 187 subcld 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( ( F ` a ) - L ) e. CC )
207 206 abscld 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( abs ` ( ( F ` a ) - L ) ) e. RR )
208 205 207 readdcld 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( ( ( ( abs ` ( R - ( F ` b ) ) ) + ( abs ` ( ( F ` b ) - x ) ) ) + ( abs ` ( x - ( F ` a ) ) ) ) + ( abs ` ( ( F ` a ) - L ) ) ) e. RR )
209 21 a1i 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> 4 e. RR )
210 rpre 
 |-  ( y e. RR+ -> y e. RR )
211 210 ad5antlr 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> y e. RR )
212 209 211 remulcld 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( 4 x. y ) e. RR )
213 186 193 196 202 187 absnpncan3d 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( abs ` ( R - L ) ) <_ ( ( ( ( abs ` ( R - ( F ` b ) ) ) + ( abs ` ( ( F ` b ) - x ) ) ) + ( abs ` ( x - ( F ` a ) ) ) ) + ( abs ` ( ( F ` a ) - L ) ) ) )
214 186 193 abssubd 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( abs ` ( R - ( F ` b ) ) ) = ( abs ` ( ( F ` b ) - R ) ) )
215 simprr 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( abs ` ( ( F ` b ) - R ) ) < y )
216 214 215 eqbrtrd 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( abs ` ( R - ( F ` b ) ) ) < y )
217 simprl 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( abs ` ( ( F ` b ) - x ) ) < y )
218 simp-5r 
 |-  ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) -> x e. CC )
219 201 ad5ant14 
 |-  ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) -> ( F ` a ) e. CC )
220 219 adantr 
 |-  ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) -> ( F ` a ) e. CC )
221 218 220 abssubd 
 |-  ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) -> ( abs ` ( x - ( F ` a ) ) ) = ( abs ` ( ( F ` a ) - x ) ) )
222 simplrl 
 |-  ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) -> ( abs ` ( ( F ` a ) - x ) ) < y )
223 221 222 eqbrtrd 
 |-  ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) -> ( abs ` ( x - ( F ` a ) ) ) < y )
224 223 adantr 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( abs ` ( x - ( F ` a ) ) ) < y )
225 simplrr 
 |-  ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) -> ( abs ` ( ( F ` a ) - L ) ) < y )
226 225 adantr 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( abs ` ( ( F ` a ) - L ) ) < y )
227 195 198 204 207 211 216 217 224 226 lt4addmuld 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( ( ( ( abs ` ( R - ( F ` b ) ) ) + ( abs ` ( ( F ` b ) - x ) ) ) + ( abs ` ( x - ( F ` a ) ) ) ) + ( abs ` ( ( F ` a ) - L ) ) ) < ( 4 x. y ) )
228 189 208 212 213 227 lelttrd 
 |-  ( ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) /\ ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) ) -> ( abs ` ( R - L ) ) < ( 4 x. y ) )
229 228 ex 
 |-  ( ( ( ( ( ( ph /\ x e. CC ) /\ y e. RR+ ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) -> ( ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) -> ( abs ` ( R - L ) ) < ( 4 x. y ) ) )
230 229 adantl3r 
 |-  ( ( ( ( ( ( ( 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 ) ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) /\ b e. A ) -> ( ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) -> ( abs ` ( R - L ) ) < ( 4 x. y ) ) )
231 230 reximdva 
 |-  ( ( ( ( ( ( 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 ) ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) -> ( E. b e. A ( ( abs ` ( ( F ` b ) - x ) ) < y /\ ( abs ` ( ( F ` b ) - R ) ) < y ) -> E. b e. A ( abs ` ( R - L ) ) < ( 4 x. y ) ) )
232 185 231 mpd 
 |-  ( ( ( ( ( ( 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 ) ) /\ a e. A ) /\ ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y ) ) -> E. b e. A ( abs ` ( R - L ) ) < ( 4 x. y ) )
233 fresin 
 |-  ( F : A --> CC -> ( F |` ( -oo (,) B ) ) : ( A i^i ( -oo (,) B ) ) --> CC )
234 4 233 syl 
 |-  ( ph -> ( F |` ( -oo (,) B ) ) : ( A i^i ( -oo (,) B ) ) --> CC )
235 ioosscn 
 |-  ( -oo (,) B ) C_ CC
236 50 235 sstri 
 |-  ( A i^i ( -oo (,) B ) ) C_ CC
237 236 a1i 
 |-  ( ph -> ( A i^i ( -oo (,) B ) ) C_ CC )
238 234 237 59 ellimc3 
 |-  ( ph -> ( L e. ( ( F |` ( -oo (,) B ) ) limCC 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 ) ) ) )
239 7 238 mpbid 
 |-  ( 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 ) ) )
240 239 simprd 
 |-  ( 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 ) )
241 240 r19.21bi 
 |-  ( ( 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 ) )
242 241 3ad2ant1 
 |-  ( ( ( 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 ) )
243 simp11l 
 |-  ( ( ( ( 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 )
244 simp12 
 |-  ( ( ( ( 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+ )
245 simp2 
 |-  ( ( ( ( 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+ )
246 breq2 
 |-  ( u = if ( z <_ v , z , v ) -> ( ( abs ` ( a - B ) ) < u <-> ( abs ` ( a - B ) ) < if ( z <_ v , z , v ) ) )
247 246 rexbidv 
 |-  ( 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 ) ) )
248 inss1 
 |-  ( ( ( limPt ` K ) ` ( A i^i ( -oo (,) B ) ) ) i^i RR ) C_ ( ( limPt ` K ) ` ( A i^i ( -oo (,) B ) ) )
249 248 a1i 
 |-  ( ph -> ( ( ( limPt ` K ) ` ( A i^i ( -oo (,) B ) ) ) i^i RR ) C_ ( ( limPt ` K ) ` ( A i^i ( -oo (,) B ) ) ) )
250 52 a1i 
 |-  ( ph -> ( A i^i ( -oo (,) B ) ) C_ RR )
251 81 83 restlp 
 |-  ( ( 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 ) )
252 73 75 250 251 syl3anc 
 |-  ( ph -> ( ( limPt ` J ) ` ( A i^i ( -oo (,) B ) ) ) = ( ( ( limPt ` K ) ` ( A i^i ( -oo (,) B ) ) ) i^i RR ) )
253 87 fveq1i 
 |-  ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( A i^i ( -oo (,) B ) ) ) = ( ( limPt ` K ) ` ( A i^i ( -oo (,) B ) ) )
254 253 a1i 
 |-  ( ph -> ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( A i^i ( -oo (,) B ) ) ) = ( ( limPt ` K ) ` ( A i^i ( -oo (,) B ) ) ) )
255 249 252 254 3sstr4d 
 |-  ( ph -> ( ( limPt ` J ) ` ( A i^i ( -oo (,) B ) ) ) C_ ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( A i^i ( -oo (,) B ) ) ) )
256 255 5 sseldd 
 |-  ( ph -> B e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( A i^i ( -oo (,) B ) ) ) )
257 237 59 islpcn 
 |-  ( ph -> ( B e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( A i^i ( -oo (,) B ) ) ) <-> A. u e. RR+ E. a e. ( ( A i^i ( -oo (,) B ) ) \ { B } ) ( abs ` ( a - B ) ) < u ) )
258 256 257 mpbid 
 |-  ( ph -> A. u e. RR+ E. a e. ( ( A i^i ( -oo (,) B ) ) \ { B } ) ( abs ` ( a - B ) ) < u )
259 258 3ad2ant1 
 |-  ( ( ph /\ z e. RR+ /\ v e. RR+ ) -> A. u e. RR+ E. a e. ( ( A i^i ( -oo (,) B ) ) \ { B } ) ( abs ` ( a - B ) ) < u )
260 247 259 96 rspcdva 
 |-  ( ( ph /\ z e. RR+ /\ v e. RR+ ) -> E. a e. ( ( A i^i ( -oo (,) B ) ) \ { B } ) ( abs ` ( a - B ) ) < if ( z <_ v , z , v ) )
261 eldifi 
 |-  ( a e. ( ( A i^i ( -oo (,) B ) ) \ { B } ) -> a e. ( A i^i ( -oo (,) B ) ) )
262 52 261 sselid 
 |-  ( a e. ( ( A i^i ( -oo (,) B ) ) \ { B } ) -> a e. RR )
263 75 sselda 
 |-  ( ( ph /\ a e. RR ) -> a e. CC )
264 59 adantr 
 |-  ( ( ph /\ a e. RR ) -> B e. CC )
265 263 264 subcld 
 |-  ( ( ph /\ a e. RR ) -> ( a - B ) e. CC )
266 265 abscld 
 |-  ( ( ph /\ a e. RR ) -> ( abs ` ( a - B ) ) e. RR )
267 266 3ad2antl1 
 |-  ( ( ( ph /\ z e. RR+ /\ v e. RR+ ) /\ a e. RR ) -> ( abs ` ( a - B ) ) e. RR )
268 267 adantr 
 |-  ( ( ( ( ph /\ z e. RR+ /\ v e. RR+ ) /\ a e. RR ) /\ ( abs ` ( a - B ) ) < if ( z <_ v , z , v ) ) -> ( abs ` ( a - B ) ) e. RR )
269 106 ad2antrr 
 |-  ( ( ( ( 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 )
270 109 ad2antrr 
 |-  ( ( ( ( ph /\ z e. RR+ /\ v e. RR+ ) /\ a e. RR ) /\ ( abs ` ( a - B ) ) < if ( z <_ v , z , v ) ) -> z e. RR )
271 simpr 
 |-  ( ( ( ( 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 ) )
272 115 ad2antrr 
 |-  ( ( ( ( ph /\ z e. RR+ /\ v e. RR+ ) /\ a e. RR ) /\ ( abs ` ( a - B ) ) < if ( z <_ v , z , v ) ) -> if ( z <_ v , z , v ) <_ z )
273 268 269 270 271 272 ltletrd 
 |-  ( ( ( ( ph /\ z e. RR+ /\ v e. RR+ ) /\ a e. RR ) /\ ( abs ` ( a - B ) ) < if ( z <_ v , z , v ) ) -> ( abs ` ( a - B ) ) < z )
274 118 ad2antrr 
 |-  ( ( ( ( ph /\ z e. RR+ /\ v e. RR+ ) /\ a e. RR ) /\ ( abs ` ( a - B ) ) < if ( z <_ v , z , v ) ) -> v e. RR )
275 min2 
 |-  ( ( z e. RR /\ v e. RR ) -> if ( z <_ v , z , v ) <_ v )
276 108 112 275 syl2an 
 |-  ( ( z e. RR+ /\ v e. RR+ ) -> if ( z <_ v , z , v ) <_ v )
277 276 3adant1 
 |-  ( ( ph /\ z e. RR+ /\ v e. RR+ ) -> if ( z <_ v , z , v ) <_ v )
278 277 ad2antrr 
 |-  ( ( ( ( ph /\ z e. RR+ /\ v e. RR+ ) /\ a e. RR ) /\ ( abs ` ( a - B ) ) < if ( z <_ v , z , v ) ) -> if ( z <_ v , z , v ) <_ v )
279 268 269 274 271 278 ltletrd 
 |-  ( ( ( ( ph /\ z e. RR+ /\ v e. RR+ ) /\ a e. RR ) /\ ( abs ` ( a - B ) ) < if ( z <_ v , z , v ) ) -> ( abs ` ( a - B ) ) < v )
280 273 279 jca 
 |-  ( ( ( ( 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 ) )
281 280 ex 
 |-  ( ( ( 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 ) ) )
282 262 281 sylan2 
 |-  ( ( ( 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 ) ) )
283 282 reximdva 
 |-  ( ( 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 ) ) )
284 260 283 mpd 
 |-  ( ( ph /\ z e. RR+ /\ v e. RR+ ) -> E. a e. ( ( A i^i ( -oo (,) B ) ) \ { B } ) ( ( abs ` ( a - B ) ) < z /\ ( abs ` ( a - B ) ) < v ) )
285 243 244 245 284 syl3anc 
 |-  ( ( ( ( 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 ) )
286 nfv 
 |-  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 ) )
287 nfre1 
 |-  F/ a E. a e. A ( ( abs ` ( ( F ` a ) - x ) ) < y /\ ( abs ` ( ( F ` a ) - L ) ) < y )
288 261 elin1d 
 |-  ( a e. ( ( A i^i ( -oo (,) B ) ) \ { B } ) -> a e. A )
289 288 3ad2ant2 
 |-  ( ( ( ( ( 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 )
290 simp113 
 |-  ( ( ( ( ( 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 ) )
291 eldifsni 
 |-  ( a e. ( ( A i^i ( -oo (,) B ) ) \ { B } ) -> a =/= B )
292 291 adantr 
 |-  ( ( a e. ( ( A i^i ( -oo (,) B ) ) \ { B } ) /\ ( ( abs ` ( a - B ) ) < z /\ ( abs ` ( a - B ) ) < v ) ) -> a =/= B )
293 simprl 
 |-  ( ( a e. ( ( A i^i ( -oo (,) B ) ) \ { B } ) /\ ( ( abs ` ( a - B ) ) < z /\ ( abs ` ( a - B ) ) < v ) ) -> ( abs ` ( a - B ) ) < z )
294 292 293 jca 
 |-  ( ( a e. ( ( A i^i ( -oo (,) B ) ) \ { B } ) /\ ( ( abs ` ( a - B ) ) < z /\ ( abs ` ( a - B ) ) < v ) ) -> ( a =/= B /\ ( abs ` ( a - B ) ) < z ) )
295 294 3adant1 
 |-  ( ( ( ( ( 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 ) )
296 neeq1 
 |-  ( w = a -> ( w =/= B <-> a =/= B ) )
297 fvoveq1 
 |-  ( w = a -> ( abs ` ( w - B ) ) = ( abs ` ( a - B ) ) )
298 297 breq1d 
 |-  ( w = a -> ( ( abs ` ( w - B ) ) < z <-> ( abs ` ( a - B ) ) < z ) )
299 296 298 anbi12d 
 |-  ( w = a -> ( ( w =/= B /\ ( abs ` ( w - B ) ) < z ) <-> ( a =/= B /\ ( abs ` ( a - B ) ) < z ) ) )
300 299 imbrov2fvoveq 
 |-  ( w = a -> ( ( ( w =/= B /\ ( abs ` ( w - B ) ) < z ) -> ( abs ` ( ( F ` w ) - x ) ) < y ) <-> ( ( a =/= B /\ ( abs ` ( a - B ) ) < z ) -> ( abs ` ( ( F ` a ) - x ) ) < y ) ) )
301 300 rspcva 
 |-  ( ( 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 ) )
302 301 imp 
 |-  ( ( ( 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 )
303 289 290 295 302 syl21anc 
 |-  ( ( ( ( ( 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 )
304 261 3ad2ant2 
 |-  ( ( ( ( ( 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 ) ) )
305 243 3ad2ant1 
 |-  ( ( ( ( ( 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 )
306 simp13 
 |-  ( ( ( ( ( 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 ) )
307 nfra1 
 |-  F/ w A. w e. ( A i^i ( -oo (,) B ) ) ( ( w =/= B /\ ( abs ` ( w - B ) ) < v ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` w ) - L ) ) < y )
308 149 307 nfan 
 |-  F/ w ( ph /\ A. w e. ( A i^i ( -oo (,) B ) ) ( ( w =/= B /\ ( abs ` ( w - B ) ) < v ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` w ) - L ) ) < y ) )
309 elinel2 
 |-  ( w e. ( A i^i ( -oo (,) B ) ) -> w e. ( -oo (,) B ) )
310 309 fvresd 
 |-  ( w e. ( A i^i ( -oo (,) B ) ) -> ( ( F |` ( -oo (,) B ) ) ` w ) = ( F ` w ) )
311 310 eqcomd 
 |-  ( w e. ( A i^i ( -oo (,) B ) ) -> ( F ` w ) = ( ( F |` ( -oo (,) B ) ) ` w ) )
312 311 fvoveq1d 
 |-  ( w e. ( A i^i ( -oo (,) B ) ) -> ( abs ` ( ( F ` w ) - L ) ) = ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` w ) - L ) ) )
313 312 3ad2ant2 
 |-  ( ( ( 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 ) ) )
314 rspa 
 |-  ( ( 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 ) )
315 314 3impia 
 |-  ( ( 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 )
316 315 3adant1l 
 |-  ( ( ( 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 )
317 313 316 eqbrtrd 
 |-  ( ( ( 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 )
318 317 3exp 
 |-  ( ( 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 ) ) )
319 308 318 ralrimi 
 |-  ( ( 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 ) )
320 305 306 319 syl2anc 
 |-  ( ( ( ( ( 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 ) )
321 291 anim1i 
 |-  ( ( a e. ( ( A i^i ( -oo (,) B ) ) \ { B } ) /\ ( abs ` ( a - B ) ) < v ) -> ( a =/= B /\ ( abs ` ( a - B ) ) < v ) )
322 321 adantrl 
 |-  ( ( a e. ( ( A i^i ( -oo (,) B ) ) \ { B } ) /\ ( ( abs ` ( a - B ) ) < z /\ ( abs ` ( a - B ) ) < v ) ) -> ( a =/= B /\ ( abs ` ( a - B ) ) < v ) )
323 322 3adant1 
 |-  ( ( ( ( ( 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 ) )
324 297 breq1d 
 |-  ( w = a -> ( ( abs ` ( w - B ) ) < v <-> ( abs ` ( a - B ) ) < v ) )
325 296 324 anbi12d 
 |-  ( w = a -> ( ( w =/= B /\ ( abs ` ( w - B ) ) < v ) <-> ( a =/= B /\ ( abs ` ( a - B ) ) < v ) ) )
326 325 imbrov2fvoveq 
 |-  ( w = a -> ( ( ( w =/= B /\ ( abs ` ( w - B ) ) < v ) -> ( abs ` ( ( F ` w ) - L ) ) < y ) <-> ( ( a =/= B /\ ( abs ` ( a - B ) ) < v ) -> ( abs ` ( ( F ` a ) - L ) ) < y ) ) )
327 326 rspcva 
 |-  ( ( 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 ) )
328 327 imp 
 |-  ( ( ( 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 )
329 304 320 323 328 syl21anc 
 |-  ( ( ( ( ( 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 )
330 rspe 
 |-  ( ( 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 ) )
331 289 303 329 330 syl12anc 
 |-  ( ( ( ( ( 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 ) )
332 331 3exp 
 |-  ( ( ( ( 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 ) ) ) )
333 286 287 332 rexlimd 
 |-  ( ( ( ( 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 ) ) )
334 285 333 mpd 
 |-  ( ( ( ( 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 ) )
335 334 3exp 
 |-  ( ( ( 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 ) ) ) )
336 335 rexlimdv 
 |-  ( ( ( 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 ) ) )
337 242 336 mpd 
 |-  ( ( ( 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 ) )
338 337 3exp 
 |-  ( ( 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 ) ) ) )
339 338 rexlimdv 
 |-  ( ( 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 ) ) )
340 339 imp 
 |-  ( ( ( 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 ) )
341 340 adantllr 
 |-  ( ( ( ( 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 ) )
342 232 341 reximddv3 
 |-  ( ( ( ( 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 E. b e. A ( abs ` ( R - L ) ) < ( 4 x. y ) )
343 38 39 41 342 syl21anc 
 |-  ( ( ( ( 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 ) )
344 343 ex 
 |-  ( ( ( 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 ) ) )
345 30 31 37 344 vtoclf 
 |-  ( ( ( 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 ) ) ) )
346 25 345 mpd 
 |-  ( ( ( 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 ) ) -> E. a e. A E. b e. A ( abs ` ( R - L ) ) < ( 4 x. ( ( abs ` ( R - L ) ) / 4 ) ) )
347 simpr 
 |-  ( ( ph /\ ( abs ` ( R - L ) ) < ( 4 x. ( ( abs ` ( R - L ) ) / 4 ) ) ) -> ( abs ` ( R - L ) ) < ( 4 x. ( ( abs ` ( R - L ) ) / 4 ) ) )
348 abssubrp 
 |-  ( ( R e. CC /\ L e. CC /\ R =/= L ) -> ( abs ` ( R - L ) ) e. RR+ )
349 11 14 17 348 syl3anc 
 |-  ( ph -> ( abs ` ( R - L ) ) e. RR+ )
350 349 rpcnd 
 |-  ( ph -> ( abs ` ( R - L ) ) e. CC )
351 350 adantr 
 |-  ( ( ph /\ ( abs ` ( R - L ) ) < ( 4 x. ( ( abs ` ( R - L ) ) / 4 ) ) ) -> ( abs ` ( R - L ) ) e. CC )
352 4cn 
 |-  4 e. CC
353 352 a1i 
 |-  ( ( ph /\ ( abs ` ( R - L ) ) < ( 4 x. ( ( abs ` ( R - L ) ) / 4 ) ) ) -> 4 e. CC )
354 4ne0 
 |-  4 =/= 0
355 354 a1i 
 |-  ( ( ph /\ ( abs ` ( R - L ) ) < ( 4 x. ( ( abs ` ( R - L ) ) / 4 ) ) ) -> 4 =/= 0 )
356 351 353 355 divcan2d 
 |-  ( ( ph /\ ( abs ` ( R - L ) ) < ( 4 x. ( ( abs ` ( R - L ) ) / 4 ) ) ) -> ( 4 x. ( ( abs ` ( R - L ) ) / 4 ) ) = ( abs ` ( R - L ) ) )
357 347 356 breqtrd 
 |-  ( ( ph /\ ( abs ` ( R - L ) ) < ( 4 x. ( ( abs ` ( R - L ) ) / 4 ) ) ) -> ( abs ` ( R - L ) ) < ( abs ` ( R - L ) ) )
358 357 ex 
 |-  ( ph -> ( ( abs ` ( R - L ) ) < ( 4 x. ( ( abs ` ( R - L ) ) / 4 ) ) -> ( abs ` ( R - L ) ) < ( abs ` ( R - L ) ) ) )
359 358 a1d 
 |-  ( ph -> ( ( a e. A /\ b e. A ) -> ( ( abs ` ( R - L ) ) < ( 4 x. ( ( abs ` ( R - L ) ) / 4 ) ) -> ( abs ` ( R - L ) ) < ( abs ` ( R - L ) ) ) ) )
360 359 ad2antrr 
 |-  ( ( ( 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 ) ) -> ( ( a e. A /\ b e. A ) -> ( ( abs ` ( R - L ) ) < ( 4 x. ( ( abs ` ( R - L ) ) / 4 ) ) -> ( abs ` ( R - L ) ) < ( abs ` ( R - L ) ) ) ) )
361 360 rexlimdvv 
 |-  ( ( ( 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 ) ) -> ( E. a e. A E. b e. A ( abs ` ( R - L ) ) < ( 4 x. ( ( abs ` ( R - L ) ) / 4 ) ) -> ( abs ` ( R - L ) ) < ( abs ` ( R - L ) ) ) )
362 346 361 mpd 
 |-  ( ( ( 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 ) ) < ( abs ` ( R - L ) ) )
363 16 abscld 
 |-  ( ( ( 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 )
364 363 ltnrd 
 |-  ( ( ( 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 ) ) < ( abs ` ( R - L ) ) )
365 362 364 pm2.65da 
 |-  ( ( 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 ) )
366 365 ex 
 |-  ( 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 ) ) )
367 imnan 
 |-  ( ( 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 ) ) <-> -. ( 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 ) ) )
368 366 367 sylib 
 |-  ( 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 ) ) )
369 2 75 sstrd 
 |-  ( ph -> A C_ CC )
370 4 369 59 ellimc3 
 |-  ( ph -> ( x e. ( F limCC B ) <-> ( 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 ) ) ) )
371 368 370 mtbird 
 |-  ( ph -> -. x e. ( F limCC B ) )
372 371 eq0rdv 
 |-  ( ph -> ( F limCC B ) = (/) )