Metamath Proof Explorer

Theorem limsupbnd2

Description: If a sequence is eventually greater than A , then the limsup is also greater than A . (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* )
limsupbnd2.4 
|- ( ph -> sup ( B , RR* , < ) = +oo )
limsupbnd2.5 
|- ( ph -> E. k e. RR A. j e. B ( k <_ j -> A <_ ( F ` j ) ) )
Assertion limsupbnd2 
|- ( ph -> A <_ ( limsup ` F ) )

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 limsupbnd2.4 
 |-  ( ph -> sup ( B , RR* , < ) = +oo )
5 limsupbnd2.5 
 |-  ( ph -> E. k e. RR A. j e. B ( k <_ j -> A <_ ( F ` j ) ) )
6 ressxr 
 |-  RR C_ RR*
7 1 6 sstrdi 
 |-  ( ph -> B C_ RR* )
8 supxrunb1 
 |-  ( B C_ RR* -> ( A. n e. RR E. j e. B n <_ j <-> sup ( B , RR* , < ) = +oo ) )
9 7 8 syl 
 |-  ( ph -> ( A. n e. RR E. j e. B n <_ j <-> sup ( B , RR* , < ) = +oo ) )
10 4 9 mpbird 
 |-  ( ph -> A. n e. RR E. j e. B n <_ j )
11 ifcl 
 |-  ( ( m e. RR /\ k e. RR ) -> if ( k <_ m , m , k ) e. RR )
12 breq1 
 |-  ( n = if ( k <_ m , m , k ) -> ( n <_ j <-> if ( k <_ m , m , k ) <_ j ) )
13 12 rexbidv 
 |-  ( n = if ( k <_ m , m , k ) -> ( E. j e. B n <_ j <-> E. j e. B if ( k <_ m , m , k ) <_ j ) )
14 13 rspccva 
 |-  ( ( A. n e. RR E. j e. B n <_ j /\ if ( k <_ m , m , k ) e. RR ) -> E. j e. B if ( k <_ m , m , k ) <_ j )
15 10 11 14 syl2an 
 |-  ( ( ph /\ ( m e. RR /\ k e. RR ) ) -> E. j e. B if ( k <_ m , m , k ) <_ j )
16 r19.29 
 |-  ( ( A. j e. B ( k <_ j -> A <_ ( F ` j ) ) /\ E. j e. B if ( k <_ m , m , k ) <_ j ) -> E. j e. B ( ( k <_ j -> A <_ ( F ` j ) ) /\ if ( k <_ m , m , k ) <_ j ) )
17 simplrr 
 |-  ( ( ( ph /\ ( m e. RR /\ k e. RR ) ) /\ j e. B ) -> k e. RR )
18 simprl 
 |-  ( ( ph /\ ( m e. RR /\ k e. RR ) ) -> m e. RR )
19 18 adantr 
 |-  ( ( ( ph /\ ( m e. RR /\ k e. RR ) ) /\ j e. B ) -> m e. RR )
20 max1 
 |-  ( ( k e. RR /\ m e. RR ) -> k <_ if ( k <_ m , m , k ) )
21 17 19 20 syl2anc 
 |-  ( ( ( ph /\ ( m e. RR /\ k e. RR ) ) /\ j e. B ) -> k <_ if ( k <_ m , m , k ) )
22 19 17 11 syl2anc 
 |-  ( ( ( ph /\ ( m e. RR /\ k e. RR ) ) /\ j e. B ) -> if ( k <_ m , m , k ) e. RR )
23 1 adantr 
 |-  ( ( ph /\ ( m e. RR /\ k e. RR ) ) -> B C_ RR )
24 23 sselda 
 |-  ( ( ( ph /\ ( m e. RR /\ k e. RR ) ) /\ j e. B ) -> j e. RR )
25 letr 
 |-  ( ( k e. RR /\ if ( k <_ m , m , k ) e. RR /\ j e. RR ) -> ( ( k <_ if ( k <_ m , m , k ) /\ if ( k <_ m , m , k ) <_ j ) -> k <_ j ) )
26 17 22 24 25 syl3anc 
 |-  ( ( ( ph /\ ( m e. RR /\ k e. RR ) ) /\ j e. B ) -> ( ( k <_ if ( k <_ m , m , k ) /\ if ( k <_ m , m , k ) <_ j ) -> k <_ j ) )
27 21 26 mpand 
 |-  ( ( ( ph /\ ( m e. RR /\ k e. RR ) ) /\ j e. B ) -> ( if ( k <_ m , m , k ) <_ j -> k <_ j ) )
28 27 imim1d 
 |-  ( ( ( ph /\ ( m e. RR /\ k e. RR ) ) /\ j e. B ) -> ( ( k <_ j -> A <_ ( F ` j ) ) -> ( if ( k <_ m , m , k ) <_ j -> A <_ ( F ` j ) ) ) )
29 28 impd 
 |-  ( ( ( ph /\ ( m e. RR /\ k e. RR ) ) /\ j e. B ) -> ( ( ( k <_ j -> A <_ ( F ` j ) ) /\ if ( k <_ m , m , k ) <_ j ) -> A <_ ( F ` j ) ) )
30 max2 
 |-  ( ( k e. RR /\ m e. RR ) -> m <_ if ( k <_ m , m , k ) )
31 17 19 30 syl2anc 
 |-  ( ( ( ph /\ ( m e. RR /\ k e. RR ) ) /\ j e. B ) -> m <_ if ( k <_ m , m , k ) )
32 letr 
 |-  ( ( m e. RR /\ if ( k <_ m , m , k ) e. RR /\ j e. RR ) -> ( ( m <_ if ( k <_ m , m , k ) /\ if ( k <_ m , m , k ) <_ j ) -> m <_ j ) )
33 19 22 24 32 syl3anc 
 |-  ( ( ( ph /\ ( m e. RR /\ k e. RR ) ) /\ j e. B ) -> ( ( m <_ if ( k <_ m , m , k ) /\ if ( k <_ m , m , k ) <_ j ) -> m <_ j ) )
34 31 33 mpand 
 |-  ( ( ( ph /\ ( m e. RR /\ k e. RR ) ) /\ j e. B ) -> ( if ( k <_ m , m , k ) <_ j -> m <_ j ) )
35 34 adantld 
 |-  ( ( ( ph /\ ( m e. RR /\ k e. RR ) ) /\ j e. B ) -> ( ( ( k <_ j -> A <_ ( F ` j ) ) /\ if ( k <_ m , m , k ) <_ j ) -> m <_ j ) )
36 eqid 
 |-  ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) )
37 36 limsupgf 
 |-  ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) : RR --> RR*
38 37 ffvelrni 
 |-  ( m e. RR -> ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) e. RR* )
39 38 adantl 
 |-  ( ( ph /\ m e. RR ) -> ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) e. RR* )
40 39 xrleidd 
 |-  ( ( ph /\ m e. RR ) -> ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) )
41 40 adantrr 
 |-  ( ( ph /\ ( m e. RR /\ k e. RR ) ) -> ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) )
42 2 adantr 
 |-  ( ( ph /\ ( m e. RR /\ k e. RR ) ) -> F : B --> RR* )
43 18 38 syl 
 |-  ( ( ph /\ ( m e. RR /\ k e. RR ) ) -> ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) e. RR* )
44 36 limsupgle 
 |-  ( ( ( B C_ RR /\ F : B --> RR* ) /\ m e. RR /\ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) e. RR* ) -> ( ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) <-> A. j e. B ( m <_ j -> ( F ` j ) <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) ) ) )
45 23 42 18 43 44 syl211anc 
 |-  ( ( ph /\ ( m e. RR /\ k e. RR ) ) -> ( ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) <-> A. j e. B ( m <_ j -> ( F ` j ) <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) ) ) )
46 41 45 mpbid 
 |-  ( ( ph /\ ( m e. RR /\ k e. RR ) ) -> A. j e. B ( m <_ j -> ( F ` j ) <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) ) )
47 46 r19.21bi 
 |-  ( ( ( ph /\ ( m e. RR /\ k e. RR ) ) /\ j e. B ) -> ( m <_ j -> ( F ` j ) <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) ) )
48 35 47 syld 
 |-  ( ( ( ph /\ ( m e. RR /\ k e. RR ) ) /\ j e. B ) -> ( ( ( k <_ j -> A <_ ( F ` j ) ) /\ if ( k <_ m , m , k ) <_ j ) -> ( F ` j ) <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) ) )
49 29 48 jcad 
 |-  ( ( ( ph /\ ( m e. RR /\ k e. RR ) ) /\ j e. B ) -> ( ( ( k <_ j -> A <_ ( F ` j ) ) /\ if ( k <_ m , m , k ) <_ j ) -> ( A <_ ( F ` j ) /\ ( F ` j ) <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) ) ) )
50 3 ad2antrr 
 |-  ( ( ( ph /\ ( m e. RR /\ k e. RR ) ) /\ j e. B ) -> A e. RR* )
51 42 ffvelrnda 
 |-  ( ( ( ph /\ ( m e. RR /\ k e. RR ) ) /\ j e. B ) -> ( F ` j ) e. RR* )
52 43 adantr 
 |-  ( ( ( ph /\ ( m e. RR /\ k e. RR ) ) /\ j e. B ) -> ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) e. RR* )
53 xrletr 
 |-  ( ( A e. RR* /\ ( F ` j ) e. RR* /\ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) e. RR* ) -> ( ( A <_ ( F ` j ) /\ ( F ` j ) <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) ) -> A <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) ) )
54 50 51 52 53 syl3anc 
 |-  ( ( ( ph /\ ( m e. RR /\ k e. RR ) ) /\ j e. B ) -> ( ( A <_ ( F ` j ) /\ ( F ` j ) <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) ) -> A <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) ) )
55 49 54 syld 
 |-  ( ( ( ph /\ ( m e. RR /\ k e. RR ) ) /\ j e. B ) -> ( ( ( k <_ j -> A <_ ( F ` j ) ) /\ if ( k <_ m , m , k ) <_ j ) -> A <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) ) )
56 55 rexlimdva 
 |-  ( ( ph /\ ( m e. RR /\ k e. RR ) ) -> ( E. j e. B ( ( k <_ j -> A <_ ( F ` j ) ) /\ if ( k <_ m , m , k ) <_ j ) -> A <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) ) )
57 16 56 syl5 
 |-  ( ( ph /\ ( m e. RR /\ k e. RR ) ) -> ( ( A. j e. B ( k <_ j -> A <_ ( F ` j ) ) /\ E. j e. B if ( k <_ m , m , k ) <_ j ) -> A <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) ) )
58 15 57 mpan2d 
 |-  ( ( ph /\ ( m e. RR /\ k e. RR ) ) -> ( A. j e. B ( k <_ j -> A <_ ( F ` j ) ) -> A <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) ) )
59 58 anassrs 
 |-  ( ( ( ph /\ m e. RR ) /\ k e. RR ) -> ( A. j e. B ( k <_ j -> A <_ ( F ` j ) ) -> A <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) ) )
60 59 rexlimdva 
 |-  ( ( ph /\ m e. RR ) -> ( E. k e. RR A. j e. B ( k <_ j -> A <_ ( F ` j ) ) -> A <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) ) )
61 60 ralrimdva 
 |-  ( ph -> ( E. k e. RR A. j e. B ( k <_ j -> A <_ ( F ` j ) ) -> A. m e. RR A <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) ) )
62 5 61 mpd 
 |-  ( ph -> A. m e. RR A <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) )
63 36 limsuple 
 |-  ( ( B C_ RR /\ F : B --> RR* /\ A e. RR* ) -> ( A <_ ( limsup ` F ) <-> A. m e. RR A <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) ) )
64 1 2 3 63 syl3anc 
 |-  ( ph -> ( A <_ ( limsup ` F ) <-> A. m e. RR A <_ ( ( n e. RR |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) ` m ) ) )
65 62 64 mpbird 
 |-  ( ph -> A <_ ( limsup ` F ) )