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 2 uzssre2 
 |-  Z C_ RR
9 8 a1i 
 |-  ( ph -> Z C_ RR )
10 2 uzsup 
 |-  ( M e. ZZ -> sup ( Z , RR* , < ) = +oo )
11 1 10 syl 
 |-  ( ph -> sup ( Z , RR* , < ) = +oo )
12 4 7 9 11 limsupval2 
 |-  ( ph -> ( limsup ` F ) = inf ( ( ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) " Z ) , RR* , < ) )
13 9 mptimass 
 |-  ( 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* , < ) ) )
14 oveq1 
 |-  ( i = n -> ( i [,) +oo ) = ( n [,) +oo ) )
15 14 imaeq2d 
 |-  ( i = n -> ( F " ( i [,) +oo ) ) = ( F " ( n [,) +oo ) ) )
16 15 ineq1d 
 |-  ( i = n -> ( ( F " ( i [,) +oo ) ) i^i RR* ) = ( ( F " ( n [,) +oo ) ) i^i RR* ) )
17 16 supeq1d 
 |-  ( i = n -> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) = sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) )
18 17 cbvmptv 
 |-  ( i e. Z |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( n e. Z |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) )
19 3 fimassd 
 |-  ( ph -> ( F " ( n [,) +oo ) ) C_ RR* )
20 dfss2 
 |-  ( ( F " ( n [,) +oo ) ) C_ RR* <-> ( ( F " ( n [,) +oo ) ) i^i RR* ) = ( F " ( n [,) +oo ) ) )
21 19 20 sylib 
 |-  ( ph -> ( ( F " ( n [,) +oo ) ) i^i RR* ) = ( F " ( n [,) +oo ) ) )
22 21 adantr 
 |-  ( ( ph /\ n e. Z ) -> ( ( F " ( n [,) +oo ) ) i^i RR* ) = ( F " ( n [,) +oo ) ) )
23 df-ima 
 |-  ( F " ( n [,) +oo ) ) = ran ( F |` ( n [,) +oo ) )
24 23 a1i 
 |-  ( ( ph /\ n e. Z ) -> ( F " ( n [,) +oo ) ) = ran ( F |` ( n [,) +oo ) ) )
25 resindm 
 |-  ( F |` ( ( n [,) +oo ) i^i dom F ) ) = ( F |` ( n [,) +oo ) )
26 2 ineq1i 
 |-  ( Z i^i ( n [,) +oo ) ) = ( ( ZZ>= ` M ) i^i ( n [,) +oo ) )
27 26 ineqcomi 
 |-  ( ( n [,) +oo ) i^i Z ) = ( ( ZZ>= ` M ) i^i ( n [,) +oo ) )
28 3 fdmd 
 |-  ( ph -> dom F = Z )
29 28 ineq2d 
 |-  ( ph -> ( ( n [,) +oo ) i^i dom F ) = ( ( n [,) +oo ) i^i Z ) )
30 29 adantr 
 |-  ( ( ph /\ n e. Z ) -> ( ( n [,) +oo ) i^i dom F ) = ( ( n [,) +oo ) i^i Z ) )
31 2 eleq2i 
 |-  ( n e. Z <-> n e. ( ZZ>= ` M ) )
32 31 bilani 
 |-  ( ( ph /\ n e. Z ) -> n e. ( ZZ>= ` M ) )
33 32 uzinico2 
 |-  ( ( ph /\ n e. Z ) -> ( ZZ>= ` n ) = ( ( ZZ>= ` M ) i^i ( n [,) +oo ) ) )
34 27 30 33 3eqtr4a 
 |-  ( ( ph /\ n e. Z ) -> ( ( n [,) +oo ) i^i dom F ) = ( ZZ>= ` n ) )
35 34 reseq2d 
 |-  ( ( ph /\ n e. Z ) -> ( F |` ( ( n [,) +oo ) i^i dom F ) ) = ( F |` ( ZZ>= ` n ) ) )
36 25 35 eqtr3id 
 |-  ( ( ph /\ n e. Z ) -> ( F |` ( n [,) +oo ) ) = ( F |` ( ZZ>= ` n ) ) )
37 36 rneqd 
 |-  ( ( ph /\ n e. Z ) -> ran ( F |` ( n [,) +oo ) ) = ran ( F |` ( ZZ>= ` n ) ) )
38 22 24 37 3eqtrd 
 |-  ( ( ph /\ n e. Z ) -> ( ( F " ( n [,) +oo ) ) i^i RR* ) = ran ( F |` ( ZZ>= ` n ) ) )
39 38 supeq1d 
 |-  ( ( ph /\ n e. Z ) -> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) )
40 39 mpteq2dva 
 |-  ( ph -> ( n e. Z |-> sup ( ( ( F " ( n [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) )
41 18 40 eqtrid 
 |-  ( ph -> ( i e. Z |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) )
42 41 rneqd 
 |-  ( ph -> ran ( i e. Z |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) )
43 13 42 eqtrd 
 |-  ( ph -> ( ( i e. RR |-> sup ( ( ( F " ( i [,) +oo ) ) i^i RR* ) , RR* , < ) ) " Z ) = ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) )
44 43 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* , < ) )
45 fveq2 
 |-  ( n = k -> ( ZZ>= ` n ) = ( ZZ>= ` k ) )
46 45 reseq2d 
 |-  ( n = k -> ( F |` ( ZZ>= ` n ) ) = ( F |` ( ZZ>= ` k ) ) )
47 46 rneqd 
 |-  ( n = k -> ran ( F |` ( ZZ>= ` n ) ) = ran ( F |` ( ZZ>= ` k ) ) )
48 47 supeq1d 
 |-  ( n = k -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) )
49 48 cbvmptv 
 |-  ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) = ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) )
50 49 rneqi 
 |-  ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) = ran ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) )
51 50 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* , < )
52 51 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* , < ) )
53 12 44 52 3eqtrd 
 |-  ( ph -> ( limsup ` F ) = inf ( ran ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) ) , RR* , < ) )