Metamath Proof Explorer

Theorem limsupgtlem

Description: For any positive real, the superior limit of F is larger than any of its values at large enough arguments, up to that positive real. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses limsupgtlem.m 
|- ( ph -> M e. ZZ )
limsupgtlem.z 
|- Z = ( ZZ>= ` M )
limsupgtlem.f 
|- ( ph -> F : Z --> RR )
limsupgtlem.r 
|- ( ph -> ( limsup ` F ) e. RR )
limsupgtlem.x 
|- ( ph -> X e. RR+ )
Assertion limsupgtlem 
|- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) - X ) < ( limsup ` F ) )

Proof

Step Hyp Ref Expression
1 limsupgtlem.m 
 |-  ( ph -> M e. ZZ )
2 limsupgtlem.z 
 |-  Z = ( ZZ>= ` M )
3 limsupgtlem.f 
 |-  ( ph -> F : Z --> RR )
4 limsupgtlem.r 
 |-  ( ph -> ( limsup ` F ) e. RR )
5 limsupgtlem.x 
 |-  ( ph -> X e. RR+ )
6 nfv 
 |-  F/ j ph
7 1 2 uzn0d 
 |-  ( ph -> Z =/= (/) )
8 rnresss 
 |-  ran ( F |` ( ZZ>= ` j ) ) C_ ran F
9 8 a1i 
 |-  ( ph -> ran ( F |` ( ZZ>= ` j ) ) C_ ran F )
10 3 frexr 
 |-  ( ph -> F : Z --> RR* )
11 10 frnd 
 |-  ( ph -> ran F C_ RR* )
12 9 11 sstrd 
 |-  ( ph -> ran ( F |` ( ZZ>= ` j ) ) C_ RR* )
13 12 supxrcld 
 |-  ( ph -> sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) e. RR* )
14 13 adantr 
 |-  ( ( ph /\ j e. Z ) -> sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) e. RR* )
15 nfcv 
 |-  F/_ k F
16 15 1 2 3 limsupreuz 
 |-  ( ph -> ( ( limsup ` F ) e. RR <-> ( E. x e. RR A. j e. Z E. k e. ( ZZ>= ` j ) x <_ ( F ` k ) /\ E. x e. RR A. k e. Z ( F ` k ) <_ x ) ) )
17 4 16 mpbid 
 |-  ( ph -> ( E. x e. RR A. j e. Z E. k e. ( ZZ>= ` j ) x <_ ( F ` k ) /\ E. x e. RR A. k e. Z ( F ` k ) <_ x ) )
18 17 simpld 
 |-  ( ph -> E. x e. RR A. j e. Z E. k e. ( ZZ>= ` j ) x <_ ( F ` k ) )
19 rexr 
 |-  ( x e. RR -> x e. RR* )
20 19 ad4antlr 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ x <_ ( F ` k ) ) -> x e. RR* )
21 3 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> F : Z --> RR )
22 2 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
23 22 adantll 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
24 21 23 ffvelrnd 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. RR )
25 24 rexrd 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. RR* )
26 25 3impa 
 |-  ( ( ph /\ j e. Z /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. RR* )
27 26 ad5ant134 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ x <_ ( F ` k ) ) -> ( F ` k ) e. RR* )
28 13 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ x <_ ( F ` k ) ) -> sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) e. RR* )
29 simpr 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ x <_ ( F ` k ) ) -> x <_ ( F ` k ) )
30 12 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ran ( F |` ( ZZ>= ` j ) ) C_ RR* )
31 fvres 
 |-  ( k e. ( ZZ>= ` j ) -> ( ( F |` ( ZZ>= ` j ) ) ` k ) = ( F ` k ) )
32 31 eqcomd 
 |-  ( k e. ( ZZ>= ` j ) -> ( F ` k ) = ( ( F |` ( ZZ>= ` j ) ) ` k ) )
33 32 adantl 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) = ( ( F |` ( ZZ>= ` j ) ) ` k ) )
34 3 ffnd 
 |-  ( ph -> F Fn Z )
35 34 adantr 
 |-  ( ( ph /\ j e. Z ) -> F Fn Z )
36 23 ssd 
 |-  ( ( ph /\ j e. Z ) -> ( ZZ>= ` j ) C_ Z )
37 fnssres 
 |-  ( ( F Fn Z /\ ( ZZ>= ` j ) C_ Z ) -> ( F |` ( ZZ>= ` j ) ) Fn ( ZZ>= ` j ) )
38 35 36 37 syl2anc 
 |-  ( ( ph /\ j e. Z ) -> ( F |` ( ZZ>= ` j ) ) Fn ( ZZ>= ` j ) )
39 38 adantr 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( F |` ( ZZ>= ` j ) ) Fn ( ZZ>= ` j ) )
40 simpr 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> k e. ( ZZ>= ` j ) )
41 39 40 fnfvelrnd 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F |` ( ZZ>= ` j ) ) ` k ) e. ran ( F |` ( ZZ>= ` j ) ) )
42 33 41 eqeltrd 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. ran ( F |` ( ZZ>= ` j ) ) )
43 eqid 
 |-  sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < )
44 30 42 43 supxrubd 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) <_ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) )
45 44 3impa 
 |-  ( ( ph /\ j e. Z /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) <_ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) )
46 45 ad5ant134 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ x <_ ( F ` k ) ) -> ( F ` k ) <_ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) )
47 20 27 28 29 46 xrletrd 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ x <_ ( F ` k ) ) -> x <_ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) )
48 47 rexlimdva2 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. Z ) -> ( E. k e. ( ZZ>= ` j ) x <_ ( F ` k ) -> x <_ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) ) )
49 48 ralimdva 
 |-  ( ( ph /\ x e. RR ) -> ( A. j e. Z E. k e. ( ZZ>= ` j ) x <_ ( F ` k ) -> A. j e. Z x <_ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) ) )
50 49 reximdva 
 |-  ( ph -> ( E. x e. RR A. j e. Z E. k e. ( ZZ>= ` j ) x <_ ( F ` k ) -> E. x e. RR A. j e. Z x <_ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) ) )
51 18 50 mpd 
 |-  ( ph -> E. x e. RR A. j e. Z x <_ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) )
52 5 rphalfcld 
 |-  ( ph -> ( X / 2 ) e. RR+ )
53 6 7 14 51 52 infrpgernmpt 
 |-  ( ph -> E. j e. Z sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) <_ ( inf ( ran ( j e. Z |-> sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) ) , RR* , < ) +e ( X / 2 ) ) )
54 simp3 
 |-  ( ( ph /\ j e. Z /\ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) <_ ( inf ( ran ( j e. Z |-> sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) ) , RR* , < ) +e ( X / 2 ) ) ) -> sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) <_ ( inf ( ran ( j e. Z |-> sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) ) , RR* , < ) +e ( X / 2 ) ) )
55 1 2 10 limsupvaluz 
 |-  ( ph -> ( limsup ` F ) = inf ( ran ( j e. Z |-> sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) ) , RR* , < ) )
56 55 eqcomd 
 |-  ( ph -> inf ( ran ( j e. Z |-> sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) ) , RR* , < ) = ( limsup ` F ) )
57 56 oveq1d 
 |-  ( ph -> ( inf ( ran ( j e. Z |-> sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) ) , RR* , < ) +e ( X / 2 ) ) = ( ( limsup ` F ) +e ( X / 2 ) ) )
58 57 3ad2ant1 
 |-  ( ( ph /\ j e. Z /\ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) <_ ( inf ( ran ( j e. Z |-> sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) ) , RR* , < ) +e ( X / 2 ) ) ) -> ( inf ( ran ( j e. Z |-> sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) ) , RR* , < ) +e ( X / 2 ) ) = ( ( limsup ` F ) +e ( X / 2 ) ) )
59 54 58 breqtrd 
 |-  ( ( ph /\ j e. Z /\ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) <_ ( inf ( ran ( j e. Z |-> sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) ) , RR* , < ) +e ( X / 2 ) ) ) -> sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) <_ ( ( limsup ` F ) +e ( X / 2 ) ) )
60 25 3adantl3 
 |-  ( ( ( ph /\ j e. Z /\ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) <_ ( ( limsup ` F ) +e ( X / 2 ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. RR* )
61 simpl1 
 |-  ( ( ( ph /\ j e. Z /\ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) <_ ( ( limsup ` F ) +e ( X / 2 ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ph )
62 61 13 syl 
 |-  ( ( ( ph /\ j e. Z /\ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) <_ ( ( limsup ` F ) +e ( X / 2 ) ) ) /\ k e. ( ZZ>= ` j ) ) -> sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) e. RR* )
63 2 fvexi 
 |-  Z e. _V
64 63 a1i 
 |-  ( ph -> Z e. _V )
65 3 64 fexd 
 |-  ( ph -> F e. _V )
66 65 limsupcld 
 |-  ( ph -> ( limsup ` F ) e. RR* )
67 5 rpred 
 |-  ( ph -> X e. RR )
68 67 rehalfcld 
 |-  ( ph -> ( X / 2 ) e. RR )
69 68 rexrd 
 |-  ( ph -> ( X / 2 ) e. RR* )
70 66 69 xaddcld 
 |-  ( ph -> ( ( limsup ` F ) +e ( X / 2 ) ) e. RR* )
71 61 70 syl 
 |-  ( ( ( ph /\ j e. Z /\ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) <_ ( ( limsup ` F ) +e ( X / 2 ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ( ( limsup ` F ) +e ( X / 2 ) ) e. RR* )
72 44 3adantl3 
 |-  ( ( ( ph /\ j e. Z /\ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) <_ ( ( limsup ` F ) +e ( X / 2 ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) <_ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) )
73 simpl3 
 |-  ( ( ( ph /\ j e. Z /\ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) <_ ( ( limsup ` F ) +e ( X / 2 ) ) ) /\ k e. ( ZZ>= ` j ) ) -> sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) <_ ( ( limsup ` F ) +e ( X / 2 ) ) )
74 60 62 71 72 73 xrletrd 
 |-  ( ( ( ph /\ j e. Z /\ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) <_ ( ( limsup ` F ) +e ( X / 2 ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) <_ ( ( limsup ` F ) +e ( X / 2 ) ) )
75 4 68 rexaddd 
 |-  ( ph -> ( ( limsup ` F ) +e ( X / 2 ) ) = ( ( limsup ` F ) + ( X / 2 ) ) )
76 61 75 syl 
 |-  ( ( ( ph /\ j e. Z /\ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) <_ ( ( limsup ` F ) +e ( X / 2 ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ( ( limsup ` F ) +e ( X / 2 ) ) = ( ( limsup ` F ) + ( X / 2 ) ) )
77 74 76 breqtrd 
 |-  ( ( ( ph /\ j e. Z /\ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) <_ ( ( limsup ` F ) +e ( X / 2 ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) <_ ( ( limsup ` F ) + ( X / 2 ) ) )
78 68 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( X / 2 ) e. RR )
79 4 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( limsup ` F ) e. RR )
80 24 78 79 lesubaddd 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) - ( X / 2 ) ) <_ ( limsup ` F ) <-> ( F ` k ) <_ ( ( limsup ` F ) + ( X / 2 ) ) ) )
81 80 3adantl3 
 |-  ( ( ( ph /\ j e. Z /\ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) <_ ( ( limsup ` F ) +e ( X / 2 ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) - ( X / 2 ) ) <_ ( limsup ` F ) <-> ( F ` k ) <_ ( ( limsup ` F ) + ( X / 2 ) ) ) )
82 77 81 mpbird 
 |-  ( ( ( ph /\ j e. Z /\ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) <_ ( ( limsup ` F ) +e ( X / 2 ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` k ) - ( X / 2 ) ) <_ ( limsup ` F ) )
83 82 ralrimiva 
 |-  ( ( ph /\ j e. Z /\ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) <_ ( ( limsup ` F ) +e ( X / 2 ) ) ) -> A. k e. ( ZZ>= ` j ) ( ( F ` k ) - ( X / 2 ) ) <_ ( limsup ` F ) )
84 59 83 syld3an3 
 |-  ( ( ph /\ j e. Z /\ sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) <_ ( inf ( ran ( j e. Z |-> sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) ) , RR* , < ) +e ( X / 2 ) ) ) -> A. k e. ( ZZ>= ` j ) ( ( F ` k ) - ( X / 2 ) ) <_ ( limsup ` F ) )
85 84 3exp 
 |-  ( ph -> ( j e. Z -> ( sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) <_ ( inf ( ran ( j e. Z |-> sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) ) , RR* , < ) +e ( X / 2 ) ) -> A. k e. ( ZZ>= ` j ) ( ( F ` k ) - ( X / 2 ) ) <_ ( limsup ` F ) ) ) )
86 6 85 reximdai 
 |-  ( ph -> ( E. j e. Z sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) <_ ( inf ( ran ( j e. Z |-> sup ( ran ( F |` ( ZZ>= ` j ) ) , RR* , < ) ) , RR* , < ) +e ( X / 2 ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) - ( X / 2 ) ) <_ ( limsup ` F ) ) )
87 53 86 mpd 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) - ( X / 2 ) ) <_ ( limsup ` F ) )
88 simpll 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ph )
89 3 ffvelrnda 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
90 67 adantr 
 |-  ( ( ph /\ k e. Z ) -> X e. RR )
91 89 90 resubcld 
 |-  ( ( ph /\ k e. Z ) -> ( ( F ` k ) - X ) e. RR )
92 91 adantr 
 |-  ( ( ( ph /\ k e. Z ) /\ ( ( F ` k ) - ( X / 2 ) ) <_ ( limsup ` F ) ) -> ( ( F ` k ) - X ) e. RR )
93 68 adantr 
 |-  ( ( ph /\ k e. Z ) -> ( X / 2 ) e. RR )
94 89 93 resubcld 
 |-  ( ( ph /\ k e. Z ) -> ( ( F ` k ) - ( X / 2 ) ) e. RR )
95 94 adantr 
 |-  ( ( ( ph /\ k e. Z ) /\ ( ( F ` k ) - ( X / 2 ) ) <_ ( limsup ` F ) ) -> ( ( F ` k ) - ( X / 2 ) ) e. RR )
96 4 ad2antrr 
 |-  ( ( ( ph /\ k e. Z ) /\ ( ( F ` k ) - ( X / 2 ) ) <_ ( limsup ` F ) ) -> ( limsup ` F ) e. RR )
97 5 rphalfltd 
 |-  ( ph -> ( X / 2 ) < X )
98 97 adantr 
 |-  ( ( ph /\ k e. Z ) -> ( X / 2 ) < X )
99 93 90 89 98 ltsub2dd 
 |-  ( ( ph /\ k e. Z ) -> ( ( F ` k ) - X ) < ( ( F ` k ) - ( X / 2 ) ) )
100 99 adantr 
 |-  ( ( ( ph /\ k e. Z ) /\ ( ( F ` k ) - ( X / 2 ) ) <_ ( limsup ` F ) ) -> ( ( F ` k ) - X ) < ( ( F ` k ) - ( X / 2 ) ) )
101 simpr 
 |-  ( ( ( ph /\ k e. Z ) /\ ( ( F ` k ) - ( X / 2 ) ) <_ ( limsup ` F ) ) -> ( ( F ` k ) - ( X / 2 ) ) <_ ( limsup ` F ) )
102 92 95 96 100 101 ltletrd 
 |-  ( ( ( ph /\ k e. Z ) /\ ( ( F ` k ) - ( X / 2 ) ) <_ ( limsup ` F ) ) -> ( ( F ` k ) - X ) < ( limsup ` F ) )
103 102 ex 
 |-  ( ( ph /\ k e. Z ) -> ( ( ( F ` k ) - ( X / 2 ) ) <_ ( limsup ` F ) -> ( ( F ` k ) - X ) < ( limsup ` F ) ) )
104 88 23 103 syl2anc 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) - ( X / 2 ) ) <_ ( limsup ` F ) -> ( ( F ` k ) - X ) < ( limsup ` F ) ) )
105 104 ralimdva 
 |-  ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) - ( X / 2 ) ) <_ ( limsup ` F ) -> A. k e. ( ZZ>= ` j ) ( ( F ` k ) - X ) < ( limsup ` F ) ) )
106 105 reximdva 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) - ( X / 2 ) ) <_ ( limsup ` F ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) - X ) < ( limsup ` F ) ) )
107 87 106 mpd 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) - X ) < ( limsup ` F ) )