Metamath Proof Explorer

Theorem supcnvlimsupmpt

Description: If a function on a set of upper integers has a real superior limit, the supremum of the rightmost parts of the function, converges to that superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses supcnvlimsupmpt.j 
|- F/ j ph
supcnvlimsupmpt.m 
|- ( ph -> M e. ZZ )
supcnvlimsupmpt.z 
|- Z = ( ZZ>= ` M )
supcnvlimsupmpt.b 
|- ( ( ph /\ j e. Z ) -> B e. RR )
supcnvlimsupmpt.r 
|- ( ph -> ( limsup ` ( j e. Z |-> B ) ) e. RR )
Assertion supcnvlimsupmpt 
|- ( ph -> ( k e. Z |-> sup ( ran ( j e. ( ZZ>= ` k ) |-> B ) , RR* , < ) ) ~~> ( limsup ` ( j e. Z |-> B ) ) )

Proof

Step Hyp Ref Expression
1 supcnvlimsupmpt.j 
 |-  F/ j ph
2 supcnvlimsupmpt.m 
 |-  ( ph -> M e. ZZ )
3 supcnvlimsupmpt.z 
 |-  Z = ( ZZ>= ` M )
4 supcnvlimsupmpt.b 
 |-  ( ( ph /\ j e. Z ) -> B e. RR )
5 supcnvlimsupmpt.r 
 |-  ( ph -> ( limsup ` ( j e. Z |-> B ) ) e. RR )
6 fveq2 
 |-  ( k = n -> ( ZZ>= ` k ) = ( ZZ>= ` n ) )
7 6 mpteq1d 
 |-  ( k = n -> ( j e. ( ZZ>= ` k ) |-> B ) = ( j e. ( ZZ>= ` n ) |-> B ) )
8 7 rneqd 
 |-  ( k = n -> ran ( j e. ( ZZ>= ` k ) |-> B ) = ran ( j e. ( ZZ>= ` n ) |-> B ) )
9 8 supeq1d 
 |-  ( k = n -> sup ( ran ( j e. ( ZZ>= ` k ) |-> B ) , RR* , < ) = sup ( ran ( j e. ( ZZ>= ` n ) |-> B ) , RR* , < ) )
10 9 cbvmptv 
 |-  ( k e. Z |-> sup ( ran ( j e. ( ZZ>= ` k ) |-> B ) , RR* , < ) ) = ( n e. Z |-> sup ( ran ( j e. ( ZZ>= ` n ) |-> B ) , RR* , < ) )
11 3 uzssd3 
 |-  ( n e. Z -> ( ZZ>= ` n ) C_ Z )
12 11 adantl 
 |-  ( ( ph /\ n e. Z ) -> ( ZZ>= ` n ) C_ Z )
13 12 resmptd 
 |-  ( ( ph /\ n e. Z ) -> ( ( j e. Z |-> B ) |` ( ZZ>= ` n ) ) = ( j e. ( ZZ>= ` n ) |-> B ) )
14 13 eqcomd 
 |-  ( ( ph /\ n e. Z ) -> ( j e. ( ZZ>= ` n ) |-> B ) = ( ( j e. Z |-> B ) |` ( ZZ>= ` n ) ) )
15 14 rneqd 
 |-  ( ( ph /\ n e. Z ) -> ran ( j e. ( ZZ>= ` n ) |-> B ) = ran ( ( j e. Z |-> B ) |` ( ZZ>= ` n ) ) )
16 15 supeq1d 
 |-  ( ( ph /\ n e. Z ) -> sup ( ran ( j e. ( ZZ>= ` n ) |-> B ) , RR* , < ) = sup ( ran ( ( j e. Z |-> B ) |` ( ZZ>= ` n ) ) , RR* , < ) )
17 16 mpteq2dva 
 |-  ( ph -> ( n e. Z |-> sup ( ran ( j e. ( ZZ>= ` n ) |-> B ) , RR* , < ) ) = ( n e. Z |-> sup ( ran ( ( j e. Z |-> B ) |` ( ZZ>= ` n ) ) , RR* , < ) ) )
18 10 17 syl5eq 
 |-  ( ph -> ( k e. Z |-> sup ( ran ( j e. ( ZZ>= ` k ) |-> B ) , RR* , < ) ) = ( n e. Z |-> sup ( ran ( ( j e. Z |-> B ) |` ( ZZ>= ` n ) ) , RR* , < ) ) )
19 1 4 fmptd2f 
 |-  ( ph -> ( j e. Z |-> B ) : Z --> RR )
20 2 3 19 5 supcnvlimsup 
 |-  ( ph -> ( n e. Z |-> sup ( ran ( ( j e. Z |-> B ) |` ( ZZ>= ` n ) ) , RR* , < ) ) ~~> ( limsup ` ( j e. Z |-> B ) ) )
21 18 20 eqbrtrd 
 |-  ( ph -> ( k e. Z |-> sup ( ran ( j e. ( ZZ>= ` k ) |-> B ) , RR* , < ) ) ~~> ( limsup ` ( j e. Z |-> B ) ) )