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