Metamath Proof Explorer

Theorem limsupbnd1

Description: If a sequence is eventually at most A , then the limsup is also at most A . (The converse is only true if the less or equal is replaced by strictly less than; consider the sequence 1 / n which is never less or equal to zero even though the limsup is.) (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 12-Sep-2020)

Ref Expression
Hypotheses limsupbnd.1 
|- ( ph -> B C_ RR )
limsupbnd.2 
|- ( ph -> F : B --> RR* )
limsupbnd.3 
|- ( ph -> A e. RR* )
limsupbnd1.4 
|- ( ph -> E. k e. RR A. j e. B ( k <_ j -> ( F ` j ) <_ A ) )
Assertion limsupbnd1 
|- ( ph -> ( limsup ` F ) <_ A )

Proof

Step Hyp Ref Expression
1 limsupbnd.1 
 |-  ( ph -> B C_ RR )
2 limsupbnd.2 
 |-  ( ph -> F : B --> RR* )
3 limsupbnd.3 
 |-  ( ph -> A e. RR* )
4 limsupbnd1.4 
 |-  ( ph -> E. k e. RR A. j e. B ( k <_ j -> ( F ` j ) <_ A ) )
5 1 adantr 
 |-  ( ( ph /\ k e. RR ) -> B C_ RR )
6 2 adantr 
 |-  ( ( ph /\ k e. RR ) -> F : B --> RR* )
7 simpr 
 |-  ( ( ph /\ k e. RR ) -> k e. RR )
8 3 adantr 
 |-  ( ( ph /\ k e. RR ) -> A e. RR* )
9 eqid 
 |-  ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) )
10 9 limsupgle 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ k e. RR /\ A e. RR* ) -> ( ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` k ) <_ A <-> A. j e. B ( k <_ j -> ( F ` j ) <_ A ) ) )
11 5 6 7 8 10 syl211anc 
 |-  ( ( ph /\ k e. RR ) -> ( ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` k ) <_ A <-> A. j e. B ( k <_ j -> ( F ` j ) <_ A ) ) )
12 reex 
 |-  RR e. _V
13 12 ssex 
 |-  ( B C_ RR -> B e. _V )
14 1 13 syl 
 |-  ( ph -> B e. _V )
15 xrex 
 |-  RR* e. _V
16 15 a1i 
 |-  ( ph -> RR* e. _V )
17 fex2 
 |-  ( ( F : B --> RR* /\ B e. _V /\ RR* e. _V ) -> F e. _V )
18 2 14 16 17 syl3anc 
 |-  ( ph -> F e. _V )
19 limsupcl 
 |-  ( F e. _V -> ( limsup ` F ) e. RR* )
20 18 19 syl 
 |-  ( ph -> ( limsup ` F ) e. RR* )
21 20 xrleidd 
 |-  ( ph -> ( limsup ` F ) <_ ( limsup ` F ) )
22 9 limsuple 
 |-  ( ( B C_ RR /\ F : B --> RR* /\ ( limsup ` F ) e. RR* ) -> ( ( limsup ` F ) <_ ( limsup ` F ) <-> A. k e. RR ( limsup ` F ) <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` k ) ) )
23 1 2 20 22 syl3anc 
 |-  ( ph -> ( ( limsup ` F ) <_ ( limsup ` F ) <-> A. k e. RR ( limsup ` F ) <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` k ) ) )
24 21 23 mpbid 
 |-  ( ph -> A. k e. RR ( limsup ` F ) <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` k ) )
25 24 r19.21bi 
 |-  ( ( ph /\ k e. RR ) -> ( limsup ` F ) <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` k ) )
26 20 adantr 
 |-  ( ( ph /\ k e. RR ) -> ( limsup ` F ) e. RR* )
27 9 limsupgf 
 |-  ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) : RR --> RR*
28 27 a1i 
 |-  ( ph -> ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) : RR --> RR* )
29 28 ffvelcdmda 
 |-  ( ( ph /\ k e. RR ) -> ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` k ) e. RR* )
30 xrletr 
 |-  ( ( ( limsup ` F ) e. RR* /\ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` k ) e. RR* /\ A e. RR* ) -> ( ( ( limsup ` F ) <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` k ) /\ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` k ) <_ A ) -> ( limsup ` F ) <_ A ) )
31 26 29 8 30 syl3anc 
 |-  ( ( ph /\ k e. RR ) -> ( ( ( limsup ` F ) <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` k ) /\ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` k ) <_ A ) -> ( limsup ` F ) <_ A ) )
32 25 31 mpand 
 |-  ( ( ph /\ k e. RR ) -> ( ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` k ) <_ A -> ( limsup ` F ) <_ A ) )
33 11 32 sylbird 
 |-  ( ( ph /\ k e. RR ) -> ( A. j e. B ( k <_ j -> ( F ` j ) <_ A ) -> ( limsup ` F ) <_ A ) )
34 33 rexlimdva 
 |-  ( ph -> ( E. k e. RR A. j e. B ( k <_ j -> ( F ` j ) <_ A ) -> ( limsup ` F ) <_ A ) )
35 4 34 mpd 
 |-  ( ph -> ( limsup ` F ) <_ A )