Metamath Proof Explorer

Theorem limcicciooub

Description: The limit of a function at the upper 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 limcicciooub.1 
|- ( ph -> A e. RR )
limcicciooub.2 
|- ( ph -> B e. RR )
limcicciooub.3 
|- ( ph -> A < B )
limcicciooub.4 
|- ( ph -> F : ( A [,] B ) --> CC )
Assertion limcicciooub 
|- ( ph -> ( ( F |` ( A (,) B ) ) limCC B ) = ( F limCC B ) )

Proof

Step Hyp Ref Expression
1 limcicciooub.1 
 |-  ( ph -> A e. RR )
2 limcicciooub.2 
 |-  ( ph -> B e. RR )
3 limcicciooub.3 
 |-  ( ph -> A < B )
4 limcicciooub.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. { B } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( A [,] B ) u. { B } ) )
12 retop 
 |-  ( topGen ` ran (,) ) e. Top
13 12 a1i 
 |-  ( ph -> ( topGen ` ran (,) ) e. Top )
14 1 rexrd 
 |-  ( ph -> A e. RR* )
15 iocssre 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
16 14 2 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. ( A (,) +oo ) -> x e. RR )
22 21 ad2antlr 
 |-  ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ x <_ B ) -> x e. RR )
23 simplr 
 |-  ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ x <_ B ) -> x e. ( A (,) +oo ) )
24 14 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ x <_ B ) -> A e. RR* )
25 pnfxr 
 |-  +oo e. RR*
26 elioo2 
 |-  ( ( A e. RR* /\ +oo e. RR* ) -> ( x e. ( A (,) +oo ) <-> ( x e. RR /\ A < x /\ x < +oo ) ) )
27 24 25 26 sylancl 
 |-  ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ x <_ B ) -> ( x e. ( A (,) +oo ) <-> ( x e. RR /\ A < x /\ x < +oo ) ) )
28 23 27 mpbid 
 |-  ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ x <_ B ) -> ( x e. RR /\ A < x /\ x < +oo ) )
29 28 simp2d 
 |-  ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ x <_ B ) -> A < x )
30 simpr 
 |-  ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ x <_ B ) -> x <_ B )
31 2 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ x <_ B ) -> B e. RR )
32 elioc2 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( x e. ( A (,] B ) <-> ( x e. RR /\ A < x /\ x <_ B ) ) )
33 24 31 32 syl2anc 
 |-  ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ x <_ B ) -> ( x e. ( A (,] B ) <-> ( x e. RR /\ A < x /\ x <_ B ) ) )
34 22 29 30 33 mpbir3and 
 |-  ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ x <_ B ) -> x e. ( A (,] B ) )
35 34 orcd 
 |-  ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ x <_ B ) -> ( x e. ( A (,] B ) \/ x e. ( RR \ ( A [,] B ) ) ) )
36 21 ad2antlr 
 |-  ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ -. x <_ B ) -> x e. RR )
37 3mix3 
 |-  ( -. x <_ B -> ( -. x e. RR \/ -. A <_ x \/ -. x <_ B ) )
38 3ianor 
 |-  ( -. ( x e. RR /\ A <_ x /\ x <_ B ) <-> ( -. x e. RR \/ -. A <_ x \/ -. x <_ B ) )
39 37 38 sylibr 
 |-  ( -. x <_ B -> -. ( x e. RR /\ A <_ x /\ x <_ B ) )
40 39 adantl 
 |-  ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ -. x <_ B ) -> -. ( x e. RR /\ A <_ x /\ x <_ B ) )
41 1 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ -. x <_ B ) -> A e. RR )
42 2 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ -. x <_ B ) -> B e. RR )
43 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
44 41 42 43 syl2anc 
 |-  ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ -. x <_ B ) -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
45 40 44 mtbird 
 |-  ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ -. x <_ B ) -> -. x e. ( A [,] B ) )
46 36 45 eldifd 
 |-  ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ -. x <_ B ) -> x e. ( RR \ ( A [,] B ) ) )
47 46 olcd 
 |-  ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ -. x <_ B ) -> ( x e. ( A (,] B ) \/ x e. ( RR \ ( A [,] B ) ) ) )
48 35 47 pm2.61dan 
 |-  ( ( ph /\ x e. ( A (,) +oo ) ) -> ( x e. ( A (,] B ) \/ x e. ( RR \ ( A [,] B ) ) ) )
49 elun 
 |-  ( x e. ( ( A (,] B ) u. ( RR \ ( A [,] B ) ) ) <-> ( x e. ( A (,] B ) \/ x e. ( RR \ ( A [,] B ) ) ) )
50 48 49 sylibr 
 |-  ( ( ph /\ x e. ( A (,) +oo ) ) -> x e. ( ( A (,] B ) u. ( RR \ ( A [,] B ) ) ) )
51 50 ralrimiva 
 |-  ( ph -> A. x e. ( A (,) +oo ) x e. ( ( A (,] B ) u. ( RR \ ( A [,] B ) ) ) )
52 dfss3 
 |-  ( ( A (,) +oo ) C_ ( ( A (,] B ) u. ( RR \ ( A [,] B ) ) ) <-> A. x e. ( A (,) +oo ) x e. ( ( A (,] B ) u. ( RR \ ( A [,] B ) ) ) )
53 51 52 sylibr 
 |-  ( ph -> ( A (,) +oo ) C_ ( ( A (,] B ) u. ( RR \ ( A [,] B ) ) ) )
54 eqid 
 |-  U. ( topGen ` ran (,) ) = U. ( topGen ` ran (,) )
55 54 ntrss 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( ( A (,] B ) u. ( RR \ ( A [,] B ) ) ) C_ U. ( topGen ` ran (,) ) /\ ( A (,) +oo ) C_ ( ( A (,] B ) u. ( RR \ ( A [,] B ) ) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) +oo ) ) C_ ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,] B ) u. ( RR \ ( A [,] B ) ) ) ) )
56 13 20 53 55 syl3anc 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) +oo ) ) C_ ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,] B ) u. ( RR \ ( A [,] B ) ) ) ) )
57 25 a1i 
 |-  ( ph -> +oo e. RR* )
58 2 ltpnfd 
 |-  ( ph -> B < +oo )
59 14 57 2 3 58 eliood 
 |-  ( ph -> B e. ( A (,) +oo ) )
60 iooretop 
 |-  ( A (,) +oo ) e. ( topGen ` ran (,) )
61 isopn3i 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( A (,) +oo ) e. ( topGen ` ran (,) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) +oo ) ) = ( A (,) +oo ) )
62 13 60 61 sylancl 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) +oo ) ) = ( A (,) +oo ) )
63 59 62 eleqtrrd 
 |-  ( ph -> B e. ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) +oo ) ) )
64 56 63 sseldd 
 |-  ( ph -> B e. ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,] B ) u. ( RR \ ( A [,] B ) ) ) ) )
65 2 rexrd 
 |-  ( ph -> B e. RR* )
66 1 2 3 ltled 
 |-  ( ph -> A <_ B )
67 ubicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
68 14 65 66 67 syl3anc 
 |-  ( ph -> B e. ( A [,] B ) )
69 64 68 elind 
 |-  ( ph -> B e. ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,] B ) u. ( RR \ ( A [,] B ) ) ) ) i^i ( A [,] B ) ) )
70 iocssicc 
 |-  ( A (,] B ) C_ ( A [,] B )
71 70 a1i 
 |-  ( ph -> ( A (,] B ) C_ ( A [,] B ) )
72 eqid 
 |-  ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) = ( ( topGen ` ran (,) ) |`t ( A [,] B ) )
73 19 72 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 ) ) )
74 13 7 71 73 syl3anc 
 |-  ( ph -> ( ( int ` ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) ) ` ( A (,] B ) ) = ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,] B ) u. ( RR \ ( A [,] B ) ) ) ) i^i ( A [,] B ) ) )
75 69 74 eleqtrrd 
 |-  ( ph -> B e. ( ( int ` ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) ) ` ( A (,] B ) ) )
76 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
77 10 76 rerest 
 |-  ( ( A [,] B ) C_ RR -> ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) = ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) )
78 7 77 syl 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) = ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) )
79 78 eqcomd 
 |-  ( ph -> ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) = ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) )
80 79 fveq2d 
 |-  ( ph -> ( int ` ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) ) = ( int ` ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) ) )
81 80 fveq1d 
 |-  ( ph -> ( ( int ` ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) ) ` ( A (,] B ) ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) ) ` ( A (,] B ) ) )
82 75 81 eleqtrd 
 |-  ( ph -> B e. ( ( int ` ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) ) ` ( A (,] B ) ) )
83 68 snssd 
 |-  ( ph -> { B } C_ ( A [,] B ) )
84 ssequn2 
 |-  ( { B } C_ ( A [,] B ) <-> ( ( A [,] B ) u. { B } ) = ( A [,] B ) )
85 83 84 sylib 
 |-  ( ph -> ( ( A [,] B ) u. { B } ) = ( A [,] B ) )
86 85 eqcomd 
 |-  ( ph -> ( A [,] B ) = ( ( A [,] B ) u. { B } ) )
87 86 oveq2d 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) = ( ( TopOpen ` CCfld ) |`t ( ( A [,] B ) u. { B } ) ) )
88 87 fveq2d 
 |-  ( ph -> ( int ` ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) ) = ( int ` ( ( TopOpen ` CCfld ) |`t ( ( A [,] B ) u. { B } ) ) ) )
89 ioounsn 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( A (,) B ) u. { B } ) = ( A (,] B ) )
90 14 65 3 89 syl3anc 
 |-  ( ph -> ( ( A (,) B ) u. { B } ) = ( A (,] B ) )
91 90 eqcomd 
 |-  ( ph -> ( A (,] B ) = ( ( A (,) B ) u. { B } ) )
92 88 91 fveq12d 
 |-  ( ph -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) ) ` ( A (,] B ) ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( A [,] B ) u. { B } ) ) ) ` ( ( A (,) B ) u. { B } ) ) )
93 82 92 eleqtrd 
 |-  ( ph -> B e. ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( A [,] B ) u. { B } ) ) ) ` ( ( A (,) B ) u. { B } ) ) )
94 4 6 9 10 11 93 limcres 
 |-  ( ph -> ( ( F |` ( A (,) B ) ) limCC B ) = ( F limCC B ) )