Metamath Proof Explorer

Theorem limciccioolb

Description: The limit of a function at the lower bound of a closed interval only depends on the values in the inner open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses limciccioolb.1 
|- ( ph -> A e. RR )
limciccioolb.2 
|- ( ph -> B e. RR )
limciccioolb.3 
|- ( ph -> A < B )
limciccioolb.4 
|- ( ph -> F : ( A [,] B ) --> CC )
Assertion limciccioolb 
|- ( ph -> ( ( F |` ( A (,) B ) ) limCC A ) = ( F limCC A ) )

Proof

Step Hyp Ref Expression
1 limciccioolb.1 
 |-  ( ph -> A e. RR )
2 limciccioolb.2 
 |-  ( ph -> B e. RR )
3 limciccioolb.3 
 |-  ( ph -> A < B )
4 limciccioolb.4 
 |-  ( ph -> F : ( A [,] B ) --> CC )
5 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
6 5 a1i 
 |-  ( ph -> ( A (,) B ) C_ ( A [,] B ) )
7 1 2 iccssred 
 |-  ( ph -> ( A [,] B ) C_ RR )
8 ax-resscn 
 |-  RR C_ CC
9 7 8 sstrdi 
 |-  ( ph -> ( A [,] B ) C_ CC )
10 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
11 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( ( A [,] B ) u. { A } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( A [,] B ) u. { A } ) )
12 retop 
 |-  ( topGen ` ran (,) ) e. Top
13 12 a1i 
 |-  ( ph -> ( topGen ` ran (,) ) e. Top )
14 2 rexrd 
 |-  ( ph -> B e. RR* )
15 icossre 
 |-  ( ( A e. RR /\ B e. RR* ) -> ( A [,) B ) C_ RR )
16 1 14 15 syl2anc 
 |-  ( ph -> ( A [,) B ) C_ RR )
17 difssd 
 |-  ( ph -> ( RR \ ( A [,] B ) ) C_ RR )
18 16 17 unssd 
 |-  ( ph -> ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) C_ RR )
19 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
20 18 19 sseqtrdi 
 |-  ( ph -> ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) C_ U. ( topGen ` ran (,) ) )
21 elioore 
 |-  ( x e. ( -oo (,) B ) -> x e. RR )
22 21 ad2antlr 
 |-  ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ A <_ x ) -> x e. RR )
23 simpr 
 |-  ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ A <_ x ) -> A <_ x )
24 simpr 
 |-  ( ( ph /\ x e. ( -oo (,) B ) ) -> x e. ( -oo (,) B ) )
25 mnfxr 
 |-  -oo e. RR*
26 25 a1i 
 |-  ( ( ph /\ x e. ( -oo (,) B ) ) -> -oo e. RR* )
27 14 adantr 
 |-  ( ( ph /\ x e. ( -oo (,) B ) ) -> B e. RR* )
28 elioo2 
 |-  ( ( -oo e. RR* /\ B e. RR* ) -> ( x e. ( -oo (,) B ) <-> ( x e. RR /\ -oo < x /\ x < B ) ) )
29 26 27 28 syl2anc 
 |-  ( ( ph /\ x e. ( -oo (,) B ) ) -> ( x e. ( -oo (,) B ) <-> ( x e. RR /\ -oo < x /\ x < B ) ) )
30 24 29 mpbid 
 |-  ( ( ph /\ x e. ( -oo (,) B ) ) -> ( x e. RR /\ -oo < x /\ x < B ) )
31 30 simp3d 
 |-  ( ( ph /\ x e. ( -oo (,) B ) ) -> x < B )
32 31 adantr 
 |-  ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ A <_ x ) -> x < B )
33 1 ad2antrr 
 |-  ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ A <_ x ) -> A e. RR )
34 14 ad2antrr 
 |-  ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ A <_ x ) -> B e. RR* )
35 elico2 
 |-  ( ( A e. RR /\ B e. RR* ) -> ( x e. ( A [,) B ) <-> ( x e. RR /\ A <_ x /\ x < B ) ) )
36 33 34 35 syl2anc 
 |-  ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ A <_ x ) -> ( x e. ( A [,) B ) <-> ( x e. RR /\ A <_ x /\ x < B ) ) )
37 22 23 32 36 mpbir3and 
 |-  ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ A <_ x ) -> x e. ( A [,) B ) )
38 37 orcd 
 |-  ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ A <_ x ) -> ( x e. ( A [,) B ) \/ x e. ( RR \ ( A [,] B ) ) ) )
39 21 ad2antlr 
 |-  ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. A <_ x ) -> x e. RR )
40 simpr 
 |-  ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. A <_ x ) -> -. A <_ x )
41 40 intnanrd 
 |-  ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. A <_ x ) -> -. ( A <_ x /\ x <_ B ) )
42 1 rexrd 
 |-  ( ph -> A e. RR* )
43 42 ad2antrr 
 |-  ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. A <_ x ) -> A e. RR* )
44 14 ad2antrr 
 |-  ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. A <_ x ) -> B e. RR* )
45 39 rexrd 
 |-  ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. A <_ x ) -> x e. RR* )
46 elicc4 
 |-  ( ( A e. RR* /\ B e. RR* /\ x e. RR* ) -> ( x e. ( A [,] B ) <-> ( A <_ x /\ x <_ B ) ) )
47 43 44 45 46 syl3anc 
 |-  ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. A <_ x ) -> ( x e. ( A [,] B ) <-> ( A <_ x /\ x <_ B ) ) )
48 41 47 mtbird 
 |-  ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. A <_ x ) -> -. x e. ( A [,] B ) )
49 39 48 eldifd 
 |-  ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. A <_ x ) -> x e. ( RR \ ( A [,] B ) ) )
50 49 olcd 
 |-  ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. A <_ x ) -> ( x e. ( A [,) B ) \/ x e. ( RR \ ( A [,] B ) ) ) )
51 38 50 pm2.61dan 
 |-  ( ( ph /\ x e. ( -oo (,) B ) ) -> ( x e. ( A [,) B ) \/ x e. ( RR \ ( A [,] B ) ) ) )
52 elun 
 |-  ( x e. ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) <-> ( x e. ( A [,) B ) \/ x e. ( RR \ ( A [,] B ) ) ) )
53 51 52 sylibr 
 |-  ( ( ph /\ x e. ( -oo (,) B ) ) -> x e. ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) )
54 53 ralrimiva 
 |-  ( ph -> A. x e. ( -oo (,) B ) x e. ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) )
55 dfss3 
 |-  ( ( -oo (,) B ) C_ ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) <-> A. x e. ( -oo (,) B ) x e. ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) )
56 54 55 sylibr 
 |-  ( ph -> ( -oo (,) B ) C_ ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) )
57 eqid 
 |-  U. ( topGen ` ran (,) ) = U. ( topGen ` ran (,) )
58 57 ntrss 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) C_ U. ( topGen ` ran (,) ) /\ ( -oo (,) B ) C_ ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( -oo (,) B ) ) C_ ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
59 13 20 56 58 syl3anc 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( -oo (,) B ) ) C_ ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
60 25 a1i 
 |-  ( ph -> -oo e. RR* )
61 1 mnfltd 
 |-  ( ph -> -oo < A )
62 60 14 1 61 3 eliood 
 |-  ( ph -> A e. ( -oo (,) B ) )
63 iooretop 
 |-  ( -oo (,) B ) e. ( topGen ` ran (,) )
64 63 a1i 
 |-  ( ph -> ( -oo (,) B ) e. ( topGen ` ran (,) ) )
65 isopn3i 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( -oo (,) B ) e. ( topGen ` ran (,) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( -oo (,) B ) ) = ( -oo (,) B ) )
66 13 64 65 syl2anc 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( -oo (,) B ) ) = ( -oo (,) B ) )
67 62 66 eleqtrrd 
 |-  ( ph -> A e. ( ( int ` ( topGen ` ran (,) ) ) ` ( -oo (,) B ) ) )
68 59 67 sseldd 
 |-  ( ph -> A e. ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
69 1 leidd 
 |-  ( ph -> A <_ A )
70 1 2 3 ltled 
 |-  ( ph -> A <_ B )
71 1 2 1 69 70 eliccd 
 |-  ( ph -> A e. ( A [,] B ) )
72 68 71 elind 
 |-  ( ph -> A e. ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) i^i ( A [,] B ) ) )
73 icossicc 
 |-  ( A [,) B ) C_ ( A [,] B )
74 73 a1i 
 |-  ( ph -> ( A [,) B ) C_ ( A [,] B ) )
75 eqid 
 |-  ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) = ( ( topGen ` ran (,) ) |`t ( A [,] B ) )
76 19 75 restntr 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( A [,] B ) C_ RR /\ ( A [,) B ) C_ ( A [,] B ) ) -> ( ( int ` ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) ) ` ( A [,) B ) ) = ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) i^i ( A [,] B ) ) )
77 13 7 74 76 syl3anc 
 |-  ( ph -> ( ( int ` ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) ) ` ( A [,) B ) ) = ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) i^i ( A [,] B ) ) )
78 72 77 eleqtrrd 
 |-  ( ph -> A e. ( ( int ` ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) ) ` ( A [,) B ) ) )
79 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
80 10 79 rerest 
 |-  ( ( A [,] B ) C_ RR -> ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) = ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) )
81 7 80 syl 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) = ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) )
82 81 eqcomd 
 |-  ( ph -> ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) = ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) )
83 82 fveq2d 
 |-  ( ph -> ( int ` ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) ) = ( int ` ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) ) )
84 83 fveq1d 
 |-  ( ph -> ( ( int ` ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) ) ` ( A [,) B ) ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) ) ` ( A [,) B ) ) )
85 78 84 eleqtrd 
 |-  ( ph -> A e. ( ( int ` ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) ) ` ( A [,) B ) ) )
86 71 snssd 
 |-  ( ph -> { A } C_ ( A [,] B ) )
87 ssequn2 
 |-  ( { A } C_ ( A [,] B ) <-> ( ( A [,] B ) u. { A } ) = ( A [,] B ) )
88 86 87 sylib 
 |-  ( ph -> ( ( A [,] B ) u. { A } ) = ( A [,] B ) )
89 88 eqcomd 
 |-  ( ph -> ( A [,] B ) = ( ( A [,] B ) u. { A } ) )
90 89 oveq2d 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) = ( ( TopOpen ` CCfld ) |`t ( ( A [,] B ) u. { A } ) ) )
91 90 fveq2d 
 |-  ( ph -> ( int ` ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) ) = ( int ` ( ( TopOpen ` CCfld ) |`t ( ( A [,] B ) u. { A } ) ) ) )
92 uncom 
 |-  ( ( A (,) B ) u. { A } ) = ( { A } u. ( A (,) B ) )
93 snunioo 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( { A } u. ( A (,) B ) ) = ( A [,) B ) )
94 42 14 3 93 syl3anc 
 |-  ( ph -> ( { A } u. ( A (,) B ) ) = ( A [,) B ) )
95 92 94 syl5req 
 |-  ( ph -> ( A [,) B ) = ( ( A (,) B ) u. { A } ) )
96 91 95 fveq12d 
 |-  ( ph -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) ) ` ( A [,) B ) ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( A [,] B ) u. { A } ) ) ) ` ( ( A (,) B ) u. { A } ) ) )
97 85 96 eleqtrd 
 |-  ( ph -> A e. ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( A [,] B ) u. { A } ) ) ) ` ( ( A (,) B ) u. { A } ) ) )
98 4 6 9 10 11 97 limcres 
 |-  ( ph -> ( ( F |` ( A (,) B ) ) limCC A ) = ( F limCC A ) )