Metamath Proof Explorer

Theorem limclr

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. In this case, the three limits coincide. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses limclr.k 
|- K = ( TopOpen ` CCfld )
limclr.a 
|- ( ph -> A C_ RR )
limclr.j 
|- J = ( topGen ` ran (,) )
limclr.f 
|- ( ph -> F : A --> CC )
limclr.lp1 
|- ( ph -> B e. ( ( limPt ` J ) ` ( A i^i ( -oo (,) B ) ) ) )
limclr.lp2 
|- ( ph -> B e. ( ( limPt ` J ) ` ( A i^i ( B (,) +oo ) ) ) )
limclr.l 
|- ( ph -> L e. ( ( F |` ( -oo (,) B ) ) limCC B ) )
limclr.r 
|- ( ph -> R e. ( ( F |` ( B (,) +oo ) ) limCC B ) )
Assertion limclr 
|- ( ph -> ( ( ( F limCC B ) =/= (/) <-> L = R ) /\ ( L = R -> L e. ( F limCC B ) ) ) )

Proof

Step Hyp Ref Expression
1 limclr.k 
 |-  K = ( TopOpen ` CCfld )
2 limclr.a 
 |-  ( ph -> A C_ RR )
3 limclr.j 
 |-  J = ( topGen ` ran (,) )
4 limclr.f 
 |-  ( ph -> F : A --> CC )
5 limclr.lp1 
 |-  ( ph -> B e. ( ( limPt ` J ) ` ( A i^i ( -oo (,) B ) ) ) )
6 limclr.lp2 
 |-  ( ph -> B e. ( ( limPt ` J ) ` ( A i^i ( B (,) +oo ) ) ) )
7 limclr.l 
 |-  ( ph -> L e. ( ( F |` ( -oo (,) B ) ) limCC B ) )
8 limclr.r 
 |-  ( ph -> R e. ( ( F |` ( B (,) +oo ) ) limCC B ) )
9 neqne 
 |-  ( -. L = R -> L =/= R )
10 2 adantr 
 |-  ( ( ph /\ L =/= R ) -> A C_ RR )
11 4 adantr 
 |-  ( ( ph /\ L =/= R ) -> F : A --> CC )
12 5 adantr 
 |-  ( ( ph /\ L =/= R ) -> B e. ( ( limPt ` J ) ` ( A i^i ( -oo (,) B ) ) ) )
13 6 adantr 
 |-  ( ( ph /\ L =/= R ) -> B e. ( ( limPt ` J ) ` ( A i^i ( B (,) +oo ) ) ) )
14 7 adantr 
 |-  ( ( ph /\ L =/= R ) -> L e. ( ( F |` ( -oo (,) B ) ) limCC B ) )
15 8 adantr 
 |-  ( ( ph /\ L =/= R ) -> R e. ( ( F |` ( B (,) +oo ) ) limCC B ) )
16 simpr 
 |-  ( ( ph /\ L =/= R ) -> L =/= R )
17 1 10 3 11 12 13 14 15 16 limclner 
 |-  ( ( ph /\ L =/= R ) -> ( F limCC B ) = (/) )
18 nne 
 |-  ( -. ( F limCC B ) =/= (/) <-> ( F limCC B ) = (/) )
19 17 18 sylibr 
 |-  ( ( ph /\ L =/= R ) -> -. ( F limCC B ) =/= (/) )
20 9 19 sylan2 
 |-  ( ( ph /\ -. L = R ) -> -. ( F limCC B ) =/= (/) )
21 20 ex 
 |-  ( ph -> ( -. L = R -> -. ( F limCC B ) =/= (/) ) )
22 21 con4d 
 |-  ( ph -> ( ( F limCC B ) =/= (/) -> L = R ) )
23 2 adantr 
 |-  ( ( ph /\ L = R ) -> A C_ RR )
24 4 adantr 
 |-  ( ( ph /\ L = R ) -> F : A --> CC )
25 retop 
 |-  ( topGen ` ran (,) ) e. Top
26 3 25 eqeltri 
 |-  J e. Top
27 inss2 
 |-  ( A i^i ( -oo (,) B ) ) C_ ( -oo (,) B )
28 ioossre 
 |-  ( -oo (,) B ) C_ RR
29 27 28 sstri 
 |-  ( A i^i ( -oo (,) B ) ) C_ RR
30 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
31 3 eqcomi 
 |-  ( topGen ` ran (,) ) = J
32 31 unieqi 
 |-  U. ( topGen ` ran (,) ) = U. J
33 30 32 eqtri 
 |-  RR = U. J
34 33 lpss 
 |-  ( ( J e. Top /\ ( A i^i ( -oo (,) B ) ) C_ RR ) -> ( ( limPt ` J ) ` ( A i^i ( -oo (,) B ) ) ) C_ RR )
35 26 29 34 mp2an 
 |-  ( ( limPt ` J ) ` ( A i^i ( -oo (,) B ) ) ) C_ RR
36 35 5 sselid 
 |-  ( ph -> B e. RR )
37 36 adantr 
 |-  ( ( ph /\ L = R ) -> B e. RR )
38 7 adantr 
 |-  ( ( ph /\ L = R ) -> L e. ( ( F |` ( -oo (,) B ) ) limCC B ) )
39 8 adantr 
 |-  ( ( ph /\ L = R ) -> R e. ( ( F |` ( B (,) +oo ) ) limCC B ) )
40 simpr 
 |-  ( ( ph /\ L = R ) -> L = R )
41 1 23 3 24 37 38 39 40 limcleqr 
 |-  ( ( ph /\ L = R ) -> L e. ( F limCC B ) )
42 41 ne0d 
 |-  ( ( ph /\ L = R ) -> ( F limCC B ) =/= (/) )
43 42 ex 
 |-  ( ph -> ( L = R -> ( F limCC B ) =/= (/) ) )
44 22 43 impbid 
 |-  ( ph -> ( ( F limCC B ) =/= (/) <-> L = R ) )
45 41 ex 
 |-  ( ph -> ( L = R -> L e. ( F limCC B ) ) )
46 44 45 jca 
 |-  ( ph -> ( ( ( F limCC B ) =/= (/) <-> L = R ) /\ ( L = R -> L e. ( F limCC B ) ) ) )