Metamath Proof Explorer

Theorem limcrecl

Description: If F is a real-valued function, B is a limit point of its domain, and the limit of F at B exists, then this limit is real. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses limcrecl.1 
|- ( ph -> F : A --> RR )
limcrecl.2 
|- ( ph -> A C_ CC )
limcrecl.3 
|- ( ph -> B e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` A ) )
limcrecl.4 
|- ( ph -> L e. ( F limCC B ) )
Assertion limcrecl 
|- ( ph -> L e. RR )

Proof

Step Hyp Ref Expression
1 limcrecl.1 
 |-  ( ph -> F : A --> RR )
2 limcrecl.2 
 |-  ( ph -> A C_ CC )
3 limcrecl.3 
 |-  ( ph -> B e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` A ) )
4 limcrecl.4 
 |-  ( ph -> L e. ( F limCC B ) )
5 4 adantr 
 |-  ( ( ph /\ -. L e. RR ) -> L e. ( F limCC B ) )
6 limccl 
 |-  ( F limCC B ) C_ CC
7 6 4 sselid 
 |-  ( ph -> L e. CC )
8 7 adantr 
 |-  ( ( ph /\ -. L e. RR ) -> L e. CC )
9 simpr 
 |-  ( ( ph /\ -. L e. RR ) -> -. L e. RR )
10 8 9 eldifd 
 |-  ( ( ph /\ -. L e. RR ) -> L e. ( CC \ RR ) )
11 10 dstregt0 
 |-  ( ( ph /\ -. L e. RR ) -> E. x e. RR+ A. w e. RR x < ( abs ` ( L - w ) ) )
12 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
13 12 a1i 
 |-  ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) -> ( abs o. - ) e. ( *Met ` CC ) )
14 2 ad4antr 
 |-  ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) -> A C_ CC )
15 14 ssdifssd 
 |-  ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) -> ( A \ { B } ) C_ CC )
16 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
17 16 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
18 17 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. Top )
19 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
20 2 19 sseqtrdi 
 |-  ( ph -> A C_ U. ( TopOpen ` CCfld ) )
21 eqid 
 |-  U. ( TopOpen ` CCfld ) = U. ( TopOpen ` CCfld )
22 21 lpdifsn 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ A C_ U. ( TopOpen ` CCfld ) ) -> ( B e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` A ) <-> B e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( A \ { B } ) ) ) )
23 18 20 22 syl2anc 
 |-  ( ph -> ( B e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` A ) <-> B e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( A \ { B } ) ) ) )
24 3 23 mpbid 
 |-  ( ph -> B e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( A \ { B } ) ) )
25 24 ad4antr 
 |-  ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) -> B e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( A \ { B } ) ) )
26 simpr 
 |-  ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) -> y e. RR+ )
27 16 cnfldtopn 
 |-  ( TopOpen ` CCfld ) = ( MetOpen ` ( abs o. - ) )
28 27 lpbl 
 |-  ( ( ( ( abs o. - ) e. ( *Met ` CC ) /\ ( A \ { B } ) C_ CC /\ B e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( A \ { B } ) ) ) /\ y e. RR+ ) -> E. z e. ( A \ { B } ) z e. ( B ( ball ` ( abs o. - ) ) y ) )
29 13 15 25 26 28 syl31anc 
 |-  ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) -> E. z e. ( A \ { B } ) z e. ( B ( ball ` ( abs o. - ) ) y ) )
30 eldif 
 |-  ( z e. ( A \ { B } ) <-> ( z e. A /\ -. z e. { B } ) )
31 30 anbi1i 
 |-  ( ( z e. ( A \ { B } ) /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) <-> ( ( z e. A /\ -. z e. { B } ) /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) )
32 anass 
 |-  ( ( ( z e. A /\ -. z e. { B } ) /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) <-> ( z e. A /\ ( -. z e. { B } /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) ) )
33 31 32 bitri 
 |-  ( ( z e. ( A \ { B } ) /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) <-> ( z e. A /\ ( -. z e. { B } /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) ) )
34 33 rexbii2 
 |-  ( E. z e. ( A \ { B } ) z e. ( B ( ball ` ( abs o. - ) ) y ) <-> E. z e. A ( -. z e. { B } /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) )
35 29 34 sylib 
 |-  ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) -> E. z e. A ( -. z e. { B } /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) )
36 simprl 
 |-  ( ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) /\ ( -. z e. { B } /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) ) -> -. z e. { B } )
37 velsn 
 |-  ( z e. { B } <-> z = B )
38 37 necon3bbii 
 |-  ( -. z e. { B } <-> z =/= B )
39 36 38 sylib 
 |-  ( ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) /\ ( -. z e. { B } /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) ) -> z =/= B )
40 simp-5l 
 |-  ( ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) /\ ( -. z e. { B } /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) ) -> ph )
41 simplr 
 |-  ( ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) /\ ( -. z e. { B } /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) ) -> y e. RR+ )
42 simprr 
 |-  ( ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) /\ ( -. z e. { B } /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) ) -> z e. ( B ( ball ` ( abs o. - ) ) y ) )
43 simp3 
 |-  ( ( ph /\ y e. RR+ /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) -> z e. ( B ( ball ` ( abs o. - ) ) y ) )
44 12 a1i 
 |-  ( ( ph /\ y e. RR+ /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) -> ( abs o. - ) e. ( *Met ` CC ) )
45 19 lpss 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ A C_ CC ) -> ( ( limPt ` ( TopOpen ` CCfld ) ) ` A ) C_ CC )
46 18 2 45 syl2anc 
 |-  ( ph -> ( ( limPt ` ( TopOpen ` CCfld ) ) ` A ) C_ CC )
47 46 3 sseldd 
 |-  ( ph -> B e. CC )
48 47 3ad2ant1 
 |-  ( ( ph /\ y e. RR+ /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) -> B e. CC )
49 rpxr 
 |-  ( y e. RR+ -> y e. RR* )
50 49 3ad2ant2 
 |-  ( ( ph /\ y e. RR+ /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) -> y e. RR* )
51 elbl 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ B e. CC /\ y e. RR* ) -> ( z e. ( B ( ball ` ( abs o. - ) ) y ) <-> ( z e. CC /\ ( B ( abs o. - ) z ) < y ) ) )
52 44 48 50 51 syl3anc 
 |-  ( ( ph /\ y e. RR+ /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) -> ( z e. ( B ( ball ` ( abs o. - ) ) y ) <-> ( z e. CC /\ ( B ( abs o. - ) z ) < y ) ) )
53 43 52 mpbid 
 |-  ( ( ph /\ y e. RR+ /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) -> ( z e. CC /\ ( B ( abs o. - ) z ) < y ) )
54 53 simpld 
 |-  ( ( ph /\ y e. RR+ /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) -> z e. CC )
55 54 48 abssubd 
 |-  ( ( ph /\ y e. RR+ /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) -> ( abs ` ( z - B ) ) = ( abs ` ( B - z ) ) )
56 eqid 
 |-  ( abs o. - ) = ( abs o. - )
57 56 cnmetdval 
 |-  ( ( B e. CC /\ z e. CC ) -> ( B ( abs o. - ) z ) = ( abs ` ( B - z ) ) )
58 48 54 57 syl2anc 
 |-  ( ( ph /\ y e. RR+ /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) -> ( B ( abs o. - ) z ) = ( abs ` ( B - z ) ) )
59 53 simprd 
 |-  ( ( ph /\ y e. RR+ /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) -> ( B ( abs o. - ) z ) < y )
60 58 59 eqbrtrrd 
 |-  ( ( ph /\ y e. RR+ /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) -> ( abs ` ( B - z ) ) < y )
61 55 60 eqbrtrd 
 |-  ( ( ph /\ y e. RR+ /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) -> ( abs ` ( z - B ) ) < y )
62 40 41 42 61 syl3anc 
 |-  ( ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) /\ ( -. z e. { B } /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) ) -> ( abs ` ( z - B ) ) < y )
63 39 62 jca 
 |-  ( ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) /\ ( -. z e. { B } /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) ) -> ( z =/= B /\ ( abs ` ( z - B ) ) < y ) )
64 63 adantlr 
 |-  ( ( ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) /\ z e. A ) /\ ( -. z e. { B } /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) ) -> ( z =/= B /\ ( abs ` ( z - B ) ) < y ) )
65 40 adantlr 
 |-  ( ( ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) /\ z e. A ) /\ ( -. z e. { B } /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) ) -> ph )
66 simplr 
 |-  ( ( ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) /\ z e. A ) /\ ( -. z e. { B } /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) ) -> z e. A )
67 65 66 jca 
 |-  ( ( ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) /\ z e. A ) /\ ( -. z e. { B } /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) ) -> ( ph /\ z e. A ) )
68 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) /\ z e. A ) /\ ( -. z e. { B } /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) ) -> x e. RR+ )
69 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) /\ z e. A ) /\ ( -. z e. { B } /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) ) -> A. w e. RR x < ( abs ` ( L - w ) ) )
70 rpre 
 |-  ( x e. RR+ -> x e. RR )
71 70 ad2antlr 
 |-  ( ( ( ( ph /\ z e. A ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) -> x e. RR )
72 1 ffvelcdmda 
 |-  ( ( ph /\ z e. A ) -> ( F ` z ) e. RR )
73 72 recnd 
 |-  ( ( ph /\ z e. A ) -> ( F ` z ) e. CC )
74 73 ad2antrr 
 |-  ( ( ( ( ph /\ z e. A ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) -> ( F ` z ) e. CC )
75 7 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. A ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) -> L e. CC )
76 74 75 subcld 
 |-  ( ( ( ( ph /\ z e. A ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) -> ( ( F ` z ) - L ) e. CC )
77 76 abscld 
 |-  ( ( ( ( ph /\ z e. A ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) -> ( abs ` ( ( F ` z ) - L ) ) e. RR )
78 72 adantr 
 |-  ( ( ( ph /\ z e. A ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) -> ( F ` z ) e. RR )
79 nfv 
 |-  F/ w ph
80 nfra1 
 |-  F/ w A. w e. RR x < ( abs ` ( L - w ) )
81 79 80 nfan 
 |-  F/ w ( ph /\ A. w e. RR x < ( abs ` ( L - w ) ) )
82 rspa 
 |-  ( ( A. w e. RR x < ( abs ` ( L - w ) ) /\ w e. RR ) -> x < ( abs ` ( L - w ) ) )
83 82 adantll 
 |-  ( ( ( ph /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ w e. RR ) -> x < ( abs ` ( L - w ) ) )
84 7 adantr 
 |-  ( ( ph /\ w e. RR ) -> L e. CC )
85 ax-resscn 
 |-  RR C_ CC
86 85 a1i 
 |-  ( ph -> RR C_ CC )
87 86 sselda 
 |-  ( ( ph /\ w e. RR ) -> w e. CC )
88 84 87 abssubd 
 |-  ( ( ph /\ w e. RR ) -> ( abs ` ( L - w ) ) = ( abs ` ( w - L ) ) )
89 88 adantlr 
 |-  ( ( ( ph /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ w e. RR ) -> ( abs ` ( L - w ) ) = ( abs ` ( w - L ) ) )
90 83 89 breqtrd 
 |-  ( ( ( ph /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ w e. RR ) -> x < ( abs ` ( w - L ) ) )
91 90 ex 
 |-  ( ( ph /\ A. w e. RR x < ( abs ` ( L - w ) ) ) -> ( w e. RR -> x < ( abs ` ( w - L ) ) ) )
92 81 91 ralrimi 
 |-  ( ( ph /\ A. w e. RR x < ( abs ` ( L - w ) ) ) -> A. w e. RR x < ( abs ` ( w - L ) ) )
93 92 adantlr 
 |-  ( ( ( ph /\ z e. A ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) -> A. w e. RR x < ( abs ` ( w - L ) ) )
94 fvoveq1 
 |-  ( w = ( F ` z ) -> ( abs ` ( w - L ) ) = ( abs ` ( ( F ` z ) - L ) ) )
95 94 breq2d 
 |-  ( w = ( F ` z ) -> ( x < ( abs ` ( w - L ) ) <-> x < ( abs ` ( ( F ` z ) - L ) ) ) )
96 95 rspcv 
 |-  ( ( F ` z ) e. RR -> ( A. w e. RR x < ( abs ` ( w - L ) ) -> x < ( abs ` ( ( F ` z ) - L ) ) ) )
97 78 93 96 sylc 
 |-  ( ( ( ph /\ z e. A ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) -> x < ( abs ` ( ( F ` z ) - L ) ) )
98 97 adantlr 
 |-  ( ( ( ( ph /\ z e. A ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) -> x < ( abs ` ( ( F ` z ) - L ) ) )
99 71 77 98 ltnsymd 
 |-  ( ( ( ( ph /\ z e. A ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) -> -. ( abs ` ( ( F ` z ) - L ) ) < x )
100 67 68 69 99 syl21anc 
 |-  ( ( ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) /\ z e. A ) /\ ( -. z e. { B } /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) ) -> -. ( abs ` ( ( F ` z ) - L ) ) < x )
101 64 100 jcnd 
 |-  ( ( ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) /\ z e. A ) /\ ( -. z e. { B } /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) ) -> -. ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - L ) ) < x ) )
102 101 ex 
 |-  ( ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) /\ z e. A ) -> ( ( -. z e. { B } /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) -> -. ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - L ) ) < x ) ) )
103 102 reximdva 
 |-  ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) -> ( E. z e. A ( -. z e. { B } /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) -> E. z e. A -. ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - L ) ) < x ) ) )
104 35 103 mpd 
 |-  ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) -> E. z e. A -. ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - L ) ) < x ) )
105 rexnal 
 |-  ( E. z e. A -. ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - L ) ) < x ) <-> -. A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - L ) ) < x ) )
106 104 105 sylib 
 |-  ( ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) /\ y e. RR+ ) -> -. A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - L ) ) < x ) )
107 106 nrexdv 
 |-  ( ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) /\ A. w e. RR x < ( abs ` ( L - w ) ) ) -> -. E. y e. RR+ A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - L ) ) < x ) )
108 107 ex 
 |-  ( ( ( ph /\ -. L e. RR ) /\ x e. RR+ ) -> ( A. w e. RR x < ( abs ` ( L - w ) ) -> -. E. y e. RR+ A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - L ) ) < x ) ) )
109 108 reximdva 
 |-  ( ( ph /\ -. L e. RR ) -> ( E. x e. RR+ A. w e. RR x < ( abs ` ( L - w ) ) -> E. x e. RR+ -. E. y e. RR+ A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - L ) ) < x ) ) )
110 11 109 mpd 
 |-  ( ( ph /\ -. L e. RR ) -> E. x e. RR+ -. E. y e. RR+ A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - L ) ) < x ) )
111 rexnal 
 |-  ( E. x e. RR+ -. E. y e. RR+ A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - L ) ) < x ) <-> -. A. x e. RR+ E. y e. RR+ A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - L ) ) < x ) )
112 110 111 sylib 
 |-  ( ( ph /\ -. L e. RR ) -> -. A. x e. RR+ E. y e. RR+ A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - L ) ) < x ) )
113 112 intnand 
 |-  ( ( ph /\ -. L e. RR ) -> -. ( 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 ) ) )
114 1 86 fssd 
 |-  ( ph -> F : A --> CC )
115 114 2 47 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 ) ) ) )
116 115 adantr 
 |-  ( ( ph /\ -. L e. RR ) -> ( 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 ) ) ) )
117 113 116 mtbird 
 |-  ( ( ph /\ -. L e. RR ) -> -. L e. ( F limCC B ) )
118 5 117 condan 
 |-  ( ph -> L e. RR )