Metamath Proof Explorer

Theorem limcleqr

Description: If the left and the right limits are equal, the limit of the function exits and the three limits coincide. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses limcleqr.k 
|- K = ( TopOpen ` CCfld )
limcleqr.a 
|- ( ph -> A C_ RR )
limcleqr.j 
|- J = ( topGen ` ran (,) )
limcleqr.f 
|- ( ph -> F : A --> CC )
limcleqr.b 
|- ( ph -> B e. RR )
limcleqr.l 
|- ( ph -> L e. ( ( F |` ( -oo (,) B ) ) limCC B ) )
limcleqr.r 
|- ( ph -> R e. ( ( F |` ( B (,) +oo ) ) limCC B ) )
limcleqr.leqr 
|- ( ph -> L = R )
Assertion limcleqr 
|- ( ph -> L e. ( F limCC B ) )

Proof

Step Hyp Ref Expression
1 limcleqr.k 
 |-  K = ( TopOpen ` CCfld )
2 limcleqr.a 
 |-  ( ph -> A C_ RR )
3 limcleqr.j 
 |-  J = ( topGen ` ran (,) )
4 limcleqr.f 
 |-  ( ph -> F : A --> CC )
5 limcleqr.b 
 |-  ( ph -> B e. RR )
6 limcleqr.l 
 |-  ( ph -> L e. ( ( F |` ( -oo (,) B ) ) limCC B ) )
7 limcleqr.r 
 |-  ( ph -> R e. ( ( F |` ( B (,) +oo ) ) limCC B ) )
8 limcleqr.leqr 
 |-  ( ph -> L = R )
9 limccl 
 |-  ( ( F |` ( -oo (,) B ) ) limCC B ) C_ CC
10 9 6 sseldi 
 |-  ( ph -> L e. CC )
11 simp-4r 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) -> a e. RR+ )
12 simplr 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) -> b e. RR+ )
13 11 12 ifcld 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) -> if ( a <_ b , a , b ) e. RR+ )
14 nfv 
 |-  F/ z ( ph /\ x e. RR+ )
15 nfv 
 |-  F/ z a e. RR+
16 14 15 nfan 
 |-  F/ z ( ( ph /\ x e. RR+ ) /\ a e. RR+ )
17 nfra1 
 |-  F/ z A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x )
18 16 17 nfan 
 |-  F/ z ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) )
19 nfv 
 |-  F/ z b e. RR+
20 18 19 nfan 
 |-  F/ z ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ )
21 nfra1 
 |-  F/ z A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x )
22 20 21 nfan 
 |-  F/ z ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) )
23 simp-6l 
 |-  ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z < B ) -> ph )
24 23 3ad2antl1 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ z < B ) -> ph )
25 simpl2 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ z < B ) -> z e. A )
26 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ z < B ) -> z < B )
27 mnfxr 
 |-  -oo e. RR*
28 27 a1i 
 |-  ( ( ph /\ z e. A /\ z < B ) -> -oo e. RR* )
29 5 rexrd 
 |-  ( ph -> B e. RR* )
30 29 3ad2ant1 
 |-  ( ( ph /\ z e. A /\ z < B ) -> B e. RR* )
31 2 sselda 
 |-  ( ( ph /\ z e. A ) -> z e. RR )
32 31 3adant3 
 |-  ( ( ph /\ z e. A /\ z < B ) -> z e. RR )
33 32 mnfltd 
 |-  ( ( ph /\ z e. A /\ z < B ) -> -oo < z )
34 simp3 
 |-  ( ( ph /\ z e. A /\ z < B ) -> z < B )
35 28 30 32 33 34 eliood 
 |-  ( ( ph /\ z e. A /\ z < B ) -> z e. ( -oo (,) B ) )
36 24 25 26 35 syl3anc 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ z < B ) -> z e. ( -oo (,) B ) )
37 fvres 
 |-  ( z e. ( -oo (,) B ) -> ( ( F |` ( -oo (,) B ) ) ` z ) = ( F ` z ) )
38 37 oveq1d 
 |-  ( z e. ( -oo (,) B ) -> ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) = ( ( F ` z ) - L ) )
39 38 eqcomd 
 |-  ( z e. ( -oo (,) B ) -> ( ( F ` z ) - L ) = ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) )
40 39 fveq2d 
 |-  ( z e. ( -oo (,) B ) -> ( abs ` ( ( F ` z ) - L ) ) = ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) )
41 36 40 syl 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ z < B ) -> ( abs ` ( ( F ` z ) - L ) ) = ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) )
42 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z < B ) -> A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) )
43 42 3ad2antl1 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ z < B ) -> A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) )
44 25 36 elind 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ z < B ) -> z e. ( A i^i ( -oo (,) B ) ) )
45 43 44 jca 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ z < B ) -> ( A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) /\ z e. ( A i^i ( -oo (,) B ) ) ) )
46 simpl3l 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ z < B ) -> z =/= B )
47 11 adantr 
 |-  ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z < B ) -> a e. RR+ )
48 47 3ad2antl1 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ z < B ) -> a e. RR+ )
49 12 adantr 
 |-  ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z < B ) -> b e. RR+ )
50 49 3ad2antl1 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ z < B ) -> b e. RR+ )
51 simpl3r 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ z < B ) -> ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) )
52 simpl1 
 |-  ( ( ( ph /\ a e. RR+ /\ b e. RR+ ) /\ ( ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) /\ z e. A ) ) -> ph )
53 simprr 
 |-  ( ( ( ph /\ a e. RR+ /\ b e. RR+ ) /\ ( ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) /\ z e. A ) ) -> z e. A )
54 31 recnd 
 |-  ( ( ph /\ z e. A ) -> z e. CC )
55 5 recnd 
 |-  ( ph -> B e. CC )
56 55 adantr 
 |-  ( ( ph /\ z e. A ) -> B e. CC )
57 54 56 subcld 
 |-  ( ( ph /\ z e. A ) -> ( z - B ) e. CC )
58 57 abscld 
 |-  ( ( ph /\ z e. A ) -> ( abs ` ( z - B ) ) e. RR )
59 52 53 58 syl2anc 
 |-  ( ( ( ph /\ a e. RR+ /\ b e. RR+ ) /\ ( ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) /\ z e. A ) ) -> ( abs ` ( z - B ) ) e. RR )
60 rpre 
 |-  ( a e. RR+ -> a e. RR )
61 60 adantr 
 |-  ( ( a e. RR+ /\ b e. RR+ ) -> a e. RR )
62 rpre 
 |-  ( b e. RR+ -> b e. RR )
63 62 adantl 
 |-  ( ( a e. RR+ /\ b e. RR+ ) -> b e. RR )
64 61 63 ifcld 
 |-  ( ( a e. RR+ /\ b e. RR+ ) -> if ( a <_ b , a , b ) e. RR )
65 64 3adant1 
 |-  ( ( ph /\ a e. RR+ /\ b e. RR+ ) -> if ( a <_ b , a , b ) e. RR )
66 65 adantr 
 |-  ( ( ( ph /\ a e. RR+ /\ b e. RR+ ) /\ ( ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) /\ z e. A ) ) -> if ( a <_ b , a , b ) e. RR )
67 61 3adant1 
 |-  ( ( ph /\ a e. RR+ /\ b e. RR+ ) -> a e. RR )
68 67 adantr 
 |-  ( ( ( ph /\ a e. RR+ /\ b e. RR+ ) /\ ( ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) /\ z e. A ) ) -> a e. RR )
69 simprl 
 |-  ( ( ( ph /\ a e. RR+ /\ b e. RR+ ) /\ ( ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) /\ z e. A ) ) -> ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) )
70 63 3adant1 
 |-  ( ( ph /\ a e. RR+ /\ b e. RR+ ) -> b e. RR )
71 min1 
 |-  ( ( a e. RR /\ b e. RR ) -> if ( a <_ b , a , b ) <_ a )
72 67 70 71 syl2anc 
 |-  ( ( ph /\ a e. RR+ /\ b e. RR+ ) -> if ( a <_ b , a , b ) <_ a )
73 72 adantr 
 |-  ( ( ( ph /\ a e. RR+ /\ b e. RR+ ) /\ ( ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) /\ z e. A ) ) -> if ( a <_ b , a , b ) <_ a )
74 59 66 68 69 73 ltletrd 
 |-  ( ( ( ph /\ a e. RR+ /\ b e. RR+ ) /\ ( ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) /\ z e. A ) ) -> ( abs ` ( z - B ) ) < a )
75 24 48 50 51 25 74 syl32anc 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ z < B ) -> ( abs ` ( z - B ) ) < a )
76 46 75 jca 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ z < B ) -> ( z =/= B /\ ( abs ` ( z - B ) ) < a ) )
77 rspa 
 |-  ( ( A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) /\ z e. ( A i^i ( -oo (,) B ) ) ) -> ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) )
78 45 76 77 sylc 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ z < B ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x )
79 41 78 eqbrtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ z < B ) -> ( abs ` ( ( F ` z ) - L ) ) < x )
80 simp-6l 
 |-  ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ -. z < B ) -> ph )
81 80 3ad2antl1 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ -. z < B ) -> ph )
82 81 5 syl 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ -. z < B ) -> B e. RR )
83 simpl2 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ -. z < B ) -> z e. A )
84 81 83 31 syl2anc 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ -. z < B ) -> z e. RR )
85 id 
 |-  ( z =/= B -> z =/= B )
86 85 necomd 
 |-  ( z =/= B -> B =/= z )
87 86 ad2antrr 
 |-  ( ( ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) /\ -. z < B ) -> B =/= z )
88 87 3ad2antl3 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ -. z < B ) -> B =/= z )
89 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ -. z < B ) -> -. z < B )
90 82 84 88 89 lttri5d 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ -. z < B ) -> B < z )
91 simp-6l 
 |-  ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ B < z ) -> ph )
92 91 3ad2antl1 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ B < z ) -> ph )
93 simpl2 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ B < z ) -> z e. A )
94 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ B < z ) -> B < z )
95 29 3ad2ant1 
 |-  ( ( ph /\ z e. A /\ B < z ) -> B e. RR* )
96 pnfxr 
 |-  +oo e. RR*
97 96 a1i 
 |-  ( ( ph /\ z e. A /\ B < z ) -> +oo e. RR* )
98 31 3adant3 
 |-  ( ( ph /\ z e. A /\ B < z ) -> z e. RR )
99 simp3 
 |-  ( ( ph /\ z e. A /\ B < z ) -> B < z )
100 98 ltpnfd 
 |-  ( ( ph /\ z e. A /\ B < z ) -> z < +oo )
101 95 97 98 99 100 eliood 
 |-  ( ( ph /\ z e. A /\ B < z ) -> z e. ( B (,) +oo ) )
102 92 93 94 101 syl3anc 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ B < z ) -> z e. ( B (,) +oo ) )
103 fvres 
 |-  ( z e. ( B (,) +oo ) -> ( ( F |` ( B (,) +oo ) ) ` z ) = ( F ` z ) )
104 103 eqcomd 
 |-  ( z e. ( B (,) +oo ) -> ( F ` z ) = ( ( F |` ( B (,) +oo ) ) ` z ) )
105 104 fvoveq1d 
 |-  ( z e. ( B (,) +oo ) -> ( abs ` ( ( F ` z ) - L ) ) = ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) )
106 102 105 syl 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ B < z ) -> ( abs ` ( ( F ` z ) - L ) ) = ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) )
107 simpl1r 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ B < z ) -> A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) )
108 93 102 elind 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ B < z ) -> z e. ( A i^i ( B (,) +oo ) ) )
109 107 108 jca 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ B < z ) -> ( A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) /\ z e. ( A i^i ( B (,) +oo ) ) ) )
110 simpl3l 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ B < z ) -> z =/= B )
111 11 adantr 
 |-  ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ B < z ) -> a e. RR+ )
112 111 3ad2antl1 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ B < z ) -> a e. RR+ )
113 12 adantr 
 |-  ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ B < z ) -> b e. RR+ )
114 113 3ad2antl1 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ B < z ) -> b e. RR+ )
115 simpl3r 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ B < z ) -> ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) )
116 70 adantr 
 |-  ( ( ( ph /\ a e. RR+ /\ b e. RR+ ) /\ ( ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) /\ z e. A ) ) -> b e. RR )
117 min2 
 |-  ( ( a e. RR /\ b e. RR ) -> if ( a <_ b , a , b ) <_ b )
118 67 70 117 syl2anc 
 |-  ( ( ph /\ a e. RR+ /\ b e. RR+ ) -> if ( a <_ b , a , b ) <_ b )
119 118 adantr 
 |-  ( ( ( ph /\ a e. RR+ /\ b e. RR+ ) /\ ( ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) /\ z e. A ) ) -> if ( a <_ b , a , b ) <_ b )
120 59 66 116 69 119 ltletrd 
 |-  ( ( ( ph /\ a e. RR+ /\ b e. RR+ ) /\ ( ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) /\ z e. A ) ) -> ( abs ` ( z - B ) ) < b )
121 92 112 114 115 93 120 syl32anc 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ B < z ) -> ( abs ` ( z - B ) ) < b )
122 110 121 jca 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ B < z ) -> ( z =/= B /\ ( abs ` ( z - B ) ) < b ) )
123 rspa 
 |-  ( ( A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) /\ z e. ( A i^i ( B (,) +oo ) ) ) -> ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) )
124 109 122 123 sylc 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ B < z ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x )
125 106 124 eqbrtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ B < z ) -> ( abs ` ( ( F ` z ) - L ) ) < x )
126 90 125 syldan 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) /\ -. z < B ) -> ( abs ` ( ( F ` z ) - L ) ) < x )
127 79 126 pm2.61dan 
 |-  ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) /\ z e. A /\ ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) ) -> ( abs ` ( ( F ` z ) - L ) ) < x )
128 127 3exp 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) -> ( z e. A -> ( ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) -> ( abs ` ( ( F ` z ) - L ) ) < x ) ) )
129 22 128 ralrimi 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) -> A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) -> ( abs ` ( ( F ` z ) - L ) ) < x ) )
130 brimralrspcev 
 |-  ( ( if ( a <_ b , a , b ) e. RR+ /\ A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < if ( a <_ b , a , b ) ) -> ( abs ` ( ( F ` z ) - L ) ) < x ) ) -> E. y e. RR+ A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - L ) ) < x ) )
131 13 129 130 syl2anc 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) /\ b e. RR+ ) /\ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) ) -> E. y e. RR+ A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - L ) ) < x ) )
132 fresin 
 |-  ( F : A --> CC -> ( F |` ( B (,) +oo ) ) : ( A i^i ( B (,) +oo ) ) --> CC )
133 4 132 syl 
 |-  ( ph -> ( F |` ( B (,) +oo ) ) : ( A i^i ( B (,) +oo ) ) --> CC )
134 inss2 
 |-  ( A i^i ( B (,) +oo ) ) C_ ( B (,) +oo )
135 ioosscn 
 |-  ( B (,) +oo ) C_ CC
136 134 135 sstri 
 |-  ( A i^i ( B (,) +oo ) ) C_ CC
137 136 a1i 
 |-  ( ph -> ( A i^i ( B (,) +oo ) ) C_ CC )
138 133 137 55 ellimc3 
 |-  ( ph -> ( R e. ( ( F |` ( B (,) +oo ) ) limCC B ) <-> ( R e. CC /\ A. x e. RR+ E. b e. RR+ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - R ) ) < x ) ) ) )
139 7 138 mpbid 
 |-  ( ph -> ( R e. CC /\ A. x e. RR+ E. b e. RR+ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - R ) ) < x ) ) )
140 139 simprd 
 |-  ( ph -> A. x e. RR+ E. b e. RR+ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - R ) ) < x ) )
141 140 r19.21bi 
 |-  ( ( ph /\ x e. RR+ ) -> E. b e. RR+ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - R ) ) < x ) )
142 8 oveq2d 
 |-  ( ph -> ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) = ( ( ( F |` ( B (,) +oo ) ) ` z ) - R ) )
143 142 fveq2d 
 |-  ( ph -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) = ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - R ) ) )
144 143 breq1d 
 |-  ( ph -> ( ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x <-> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - R ) ) < x ) )
145 144 imbi2d 
 |-  ( ph -> ( ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) <-> ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - R ) ) < x ) ) )
146 145 rexralbidv 
 |-  ( ph -> ( E. b e. RR+ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) <-> E. b e. RR+ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - R ) ) < x ) ) )
147 146 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> ( E. b e. RR+ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) <-> E. b e. RR+ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - R ) ) < x ) ) )
148 141 147 mpbird 
 |-  ( ( ph /\ x e. RR+ ) -> E. b e. RR+ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) )
149 148 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) -> E. b e. RR+ A. z e. ( A i^i ( B (,) +oo ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < b ) -> ( abs ` ( ( ( F |` ( B (,) +oo ) ) ` z ) - L ) ) < x ) )
150 131 149 r19.29a 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ a e. RR+ ) /\ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) -> E. y e. RR+ A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - L ) ) < x ) )
151 fresin 
 |-  ( F : A --> CC -> ( F |` ( -oo (,) B ) ) : ( A i^i ( -oo (,) B ) ) --> CC )
152 4 151 syl 
 |-  ( ph -> ( F |` ( -oo (,) B ) ) : ( A i^i ( -oo (,) B ) ) --> CC )
153 inss2 
 |-  ( A i^i ( -oo (,) B ) ) C_ ( -oo (,) B )
154 ioossre 
 |-  ( -oo (,) B ) C_ RR
155 153 154 sstri 
 |-  ( A i^i ( -oo (,) B ) ) C_ RR
156 ax-resscn 
 |-  RR C_ CC
157 156 a1i 
 |-  ( ph -> RR C_ CC )
158 155 157 sstrid 
 |-  ( ph -> ( A i^i ( -oo (,) B ) ) C_ CC )
159 152 158 55 ellimc3 
 |-  ( ph -> ( L e. ( ( F |` ( -oo (,) B ) ) limCC B ) <-> ( L e. CC /\ A. x e. RR+ E. a e. RR+ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) ) )
160 6 159 mpbid 
 |-  ( ph -> ( L e. CC /\ A. x e. RR+ E. a e. RR+ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) ) )
161 160 simprd 
 |-  ( ph -> A. x e. RR+ E. a e. RR+ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) )
162 161 r19.21bi 
 |-  ( ( ph /\ x e. RR+ ) -> E. a e. RR+ A. z e. ( A i^i ( -oo (,) B ) ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < a ) -> ( abs ` ( ( ( F |` ( -oo (,) B ) ) ` z ) - L ) ) < x ) )
163 150 162 r19.29a 
 |-  ( ( ph /\ x e. RR+ ) -> E. y e. RR+ A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - L ) ) < x ) )
164 163 ralrimiva 
 |-  ( ph -> A. x e. RR+ E. y e. RR+ A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - L ) ) < x ) )
165 2 156 sstrdi 
 |-  ( ph -> A C_ CC )
166 4 165 55 ellimc3 
 |-  ( ph -> ( L e. ( F limCC B ) <-> ( L e. CC /\ A. x e. RR+ E. y e. RR+ A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - L ) ) < x ) ) ) )
167 10 164 166 mpbir2and 
 |-  ( ph -> L e. ( F limCC B ) )