Metamath Proof Explorer

Theorem limsupvaluz

Description: The superior limit, when the domain of the function is a set of upper integers (the first condition is needed, otherwise the l.h.s. would be -oo and the r.h.s. would be +oo ). (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupvaluz.m 
|- ( ph -> M e. ZZ )
limsupvaluz.z 
|- Z = ( ZZ>= ` M )
limsupvaluz.f 
|- ( ph -> F : Z --> RR* )
Assertion limsupvaluz 
|- ( ph -> ( limsup ` F ) = inf ( ran ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) ) , RR* , < ) )

Proof

Step Hyp Ref Expression
1 limsupvaluz.m 
 |-  ( ph -> M e. ZZ )
2 limsupvaluz.z 
 |-  Z = ( ZZ>= ` M )
3 limsupvaluz.f 
 |-  ( ph -> F : Z --> RR* )
4 eqid 
 |-  ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) )
5 2 fvexi 
 |-  Z e. _V
6 5 a1i 
 |-  ( ph -> Z e. _V )
7 3 6 fexd 
 |-  ( ph -> F e. _V )
8 7 elexd 
 |-  ( ph -> F e. _V )
9 uzssre 
 |-  ( ZZ>= ` M ) C_ RR
10 2 9 eqsstri 
 |-  Z C_ RR
11 10 a1i 
 |-  ( ph -> Z C_ RR )
12 2 uzsup 
 |-  ( M e. ZZ -> sup ( Z , RR* , < ) = +oo )
13 1 12 syl 
 |-  ( ph -> sup ( Z , RR* , < ) = +oo )
14 4 8 11 13 limsupval2 
 |-  ( ph -> ( limsup ` F ) = inf ( ( ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) " Z ) , RR* , < ) )
15 11 mptima2 
 |-  ( ph -> ( ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) " Z ) = ran ( i e. Z |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
16 oveq1 
 |-  ( i = n -> ( i [,) +oo ) = ( n [,) +oo ) )
17 16 imaeq2d 
 |-  ( i = n -> ( F " ( i [,) +oo ) ) = ( F " ( n [,) +oo ) ) )
18 17 ineq1d 
 |-  ( i = n -> ( ( F " ( i [,) +oo ) ) i^i RR* ) = ( ( F " ( n [,) +oo ) ) i^i RR* ) )
19 18 supeq1d 
 |-  ( i = n -> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) = sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) )
20 19 cbvmptv 
 |-  ( i e. Z |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( n e. Z |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) )
21 20 a1i 
 |-  ( ph -> ( i e. Z |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( n e. Z |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
22 fimass 
 |-  ( F : Z --> RR* -> ( F " ( n [,) +oo ) ) C_ RR* )
23 3 22 syl 
 |-  ( ph -> ( F " ( n [,) +oo ) ) C_ RR* )
24 df-ss 
 |-  ( ( F " ( n [,) +oo ) ) C_ RR* <-> ( ( F " ( n [,) +oo ) ) i^i RR* ) = ( F " ( n [,) +oo ) ) )
25 24 biimpi 
 |-  ( ( F " ( n [,) +oo ) ) C_ RR* -> ( ( F " ( n [,) +oo ) ) i^i RR* ) = ( F " ( n [,) +oo ) ) )
26 23 25 syl 
 |-  ( ph -> ( ( F " ( n [,) +oo ) ) i^i RR* ) = ( F " ( n [,) +oo ) ) )
27 26 adantr 
 |-  ( ( ph /\ n e. Z ) -> ( ( F " ( n [,) +oo ) ) i^i RR* ) = ( F " ( n [,) +oo ) ) )
28 df-ima 
 |-  ( F " ( n [,) +oo ) ) = ran ( F |` ( n [,) +oo ) )
29 28 a1i 
 |-  ( ( ph /\ n e. Z ) -> ( F " ( n [,) +oo ) ) = ran ( F |` ( n [,) +oo ) ) )
30 3 freld 
 |-  ( ph -> Rel F )
31 resindm 
 |-  ( Rel F -> ( F |` ( ( n [,) +oo ) i^i dom F ) ) = ( F |` ( n [,) +oo ) ) )
32 30 31 syl 
 |-  ( ph -> ( F |` ( ( n [,) +oo ) i^i dom F ) ) = ( F |` ( n [,) +oo ) ) )
33 32 adantr 
 |-  ( ( ph /\ n e. Z ) -> ( F |` ( ( n [,) +oo ) i^i dom F ) ) = ( F |` ( n [,) +oo ) ) )
34 incom 
 |-  ( ( n [,) +oo ) i^i Z ) = ( Z i^i ( n [,) +oo ) )
35 2 ineq1i 
 |-  ( Z i^i ( n [,) +oo ) ) = ( ( ZZ>= ` M ) i^i ( n [,) +oo ) )
36 34 35 eqtri 
 |-  ( ( n [,) +oo ) i^i Z ) = ( ( ZZ>= ` M ) i^i ( n [,) +oo ) )
37 36 a1i 
 |-  ( ( ph /\ n e. Z ) -> ( ( n [,) +oo ) i^i Z ) = ( ( ZZ>= ` M ) i^i ( n [,) +oo ) ) )
38 3 fdmd 
 |-  ( ph -> dom F = Z )
39 38 ineq2d 
 |-  ( ph -> ( ( n [,) +oo ) i^i dom F ) = ( ( n [,) +oo ) i^i Z ) )
40 39 adantr 
 |-  ( ( ph /\ n e. Z ) -> ( ( n [,) +oo ) i^i dom F ) = ( ( n [,) +oo ) i^i Z ) )
41 2 eleq2i 
 |-  ( n e. Z <-> n e. ( ZZ>= ` M ) )
42 41 biimpi 
 |-  ( n e. Z -> n e. ( ZZ>= ` M ) )
43 42 adantl 
 |-  ( ( ph /\ n e. Z ) -> n e. ( ZZ>= ` M ) )
44 43 uzinico2 
 |-  ( ( ph /\ n e. Z ) -> ( ZZ>= ` n ) = ( ( ZZ>= ` M ) i^i ( n [,) +oo ) ) )
45 37 40 44 3eqtr4d 
 |-  ( ( ph /\ n e. Z ) -> ( ( n [,) +oo ) i^i dom F ) = ( ZZ>= ` n ) )
46 45 reseq2d 
 |-  ( ( ph /\ n e. Z ) -> ( F |` ( ( n [,) +oo ) i^i dom F ) ) = ( F |` ( ZZ>= ` n ) ) )
47 33 46 eqtr3d 
 |-  ( ( ph /\ n e. Z ) -> ( F |` ( n [,) +oo ) ) = ( F |` ( ZZ>= ` n ) ) )
48 47 rneqd 
 |-  ( ( ph /\ n e. Z ) -> ran ( F |` ( n [,) +oo ) ) = ran ( F |` ( ZZ>= ` n ) ) )
49 27 29 48 3eqtrd 
 |-  ( ( ph /\ n e. Z ) -> ( ( F " ( n [,) +oo ) ) i^i RR* ) = ran ( F |` ( ZZ>= ` n ) ) )
50 49 supeq1d 
 |-  ( ( ph /\ n e. Z ) -> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) )
51 50 mpteq2dva 
 |-  ( ph -> ( n e. Z |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) )
52 21 51 eqtrd 
 |-  ( ph -> ( i e. Z |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) )
53 52 rneqd 
 |-  ( ph -> ran ( i e. Z |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) )
54 15 53 eqtrd 
 |-  ( ph -> ( ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) " Z ) = ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) )
55 54 infeq1d 
 |-  ( ph -> inf ( ( ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) " Z ) , RR* , < ) = inf ( ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) , RR* , < ) )
56 fveq2 
 |-  ( n = k -> ( ZZ>= ` n ) = ( ZZ>= ` k ) )
57 56 reseq2d 
 |-  ( n = k -> ( F |` ( ZZ>= ` n ) ) = ( F |` ( ZZ>= ` k ) ) )
58 57 rneqd 
 |-  ( n = k -> ran ( F |` ( ZZ>= ` n ) ) = ran ( F |` ( ZZ>= ` k ) ) )
59 58 supeq1d 
 |-  ( n = k -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) )
60 59 cbvmptv 
 |-  ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) = ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) )
61 60 rneqi 
 |-  ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) = ran ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) )
62 61 infeq1i 
 |-  inf ( ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) , RR* , < ) = inf ( ran ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) ) , RR* , < )
63 62 a1i 
 |-  ( ph -> inf ( ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) , RR* , < ) = inf ( ran ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) ) , RR* , < ) )
64 14 55 63 3eqtrd 
 |-  ( ph -> ( limsup ` F ) = inf ( ran ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) ) , RR* , < ) )