Metamath Proof Explorer

Theorem limsupvaluz2

Description: The superior limit, when the domain of a real-valued function is a set of upper integers, and the superior limit is real. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 limsupvaluz2.m 
 |-  ( ph -> M e. ZZ )
2 limsupvaluz2.z 
 |-  Z = ( ZZ>= ` M )
3 limsupvaluz2.f 
 |-  ( ph -> F : Z --> RR )
4 limsupvaluz2.r 
 |-  ( ph -> ( limsup ` F ) e. RR )
5 3 frexr 
 |-  ( ph -> F : Z --> RR* )
6 1 2 5 limsupvaluz 
 |-  ( ph -> ( limsup ` F ) = inf ( ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) , RR* , < ) )
7 3 adantr 
 |-  ( ( ph /\ n e. Z ) -> F : Z --> RR )
8 2 uzssd3 
 |-  ( n e. Z -> ( ZZ>= ` n ) C_ Z )
9 8 adantl 
 |-  ( ( ph /\ n e. Z ) -> ( ZZ>= ` n ) C_ Z )
10 7 9 feqresmpt 
 |-  ( ( ph /\ n e. Z ) -> ( F |` ( ZZ>= ` n ) ) = ( m e. ( ZZ>= ` n ) |-> ( F ` m ) ) )
11 10 rneqd 
 |-  ( ( ph /\ n e. Z ) -> ran ( F |` ( ZZ>= ` n ) ) = ran ( m e. ( ZZ>= ` n ) |-> ( F ` m ) ) )
12 11 supeq1d 
 |-  ( ( ph /\ n e. Z ) -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( m e. ( ZZ>= ` n ) |-> ( F ` m ) ) , RR* , < ) )
13 nfcv 
 |-  F/_ m F
14 4 renepnfd 
 |-  ( ph -> ( limsup ` F ) =/= +oo )
15 13 2 3 14 limsupubuz 
 |-  ( ph -> E. x e. RR A. m e. Z ( F ` m ) <_ x )
16 15 adantr 
 |-  ( ( ph /\ n e. Z ) -> E. x e. RR A. m e. Z ( F ` m ) <_ x )
17 ssralv 
 |-  ( ( ZZ>= ` n ) C_ Z -> ( A. m e. Z ( F ` m ) <_ x -> A. m e. ( ZZ>= ` n ) ( F ` m ) <_ x ) )
18 8 17 syl 
 |-  ( n e. Z -> ( A. m e. Z ( F ` m ) <_ x -> A. m e. ( ZZ>= ` n ) ( F ` m ) <_ x ) )
19 18 adantl 
 |-  ( ( ph /\ n e. Z ) -> ( A. m e. Z ( F ` m ) <_ x -> A. m e. ( ZZ>= ` n ) ( F ` m ) <_ x ) )
20 19 reximdv 
 |-  ( ( ph /\ n e. Z ) -> ( E. x e. RR A. m e. Z ( F ` m ) <_ x -> E. x e. RR A. m e. ( ZZ>= ` n ) ( F ` m ) <_ x ) )
21 16 20 mpd 
 |-  ( ( ph /\ n e. Z ) -> E. x e. RR A. m e. ( ZZ>= ` n ) ( F ` m ) <_ x )
22 nfv 
 |-  F/ m ( ph /\ n e. Z )
23 2 eluzelz2 
 |-  ( n e. Z -> n e. ZZ )
24 uzid 
 |-  ( n e. ZZ -> n e. ( ZZ>= ` n ) )
25 ne0i 
 |-  ( n e. ( ZZ>= ` n ) -> ( ZZ>= ` n ) =/= (/) )
26 23 24 25 3syl 
 |-  ( n e. Z -> ( ZZ>= ` n ) =/= (/) )
27 26 adantl 
 |-  ( ( ph /\ n e. Z ) -> ( ZZ>= ` n ) =/= (/) )
28 7 adantr 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> F : Z --> RR )
29 9 sselda 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
30 28 29 ffvelcdmd 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> ( F ` m ) e. RR )
31 22 27 30 supxrre3rnmpt 
 |-  ( ( ph /\ n e. Z ) -> ( sup ( ran ( m e. ( ZZ>= ` n ) |-> ( F ` m ) ) , RR* , < ) e. RR <-> E. x e. RR A. m e. ( ZZ>= ` n ) ( F ` m ) <_ x ) )
32 21 31 mpbird 
 |-  ( ( ph /\ n e. Z ) -> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( F ` m ) ) , RR* , < ) e. RR )
33 12 32 eqeltrd 
 |-  ( ( ph /\ n e. Z ) -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) e. RR )
34 33 fmpttd 
 |-  ( ph -> ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) : Z --> RR )
35 34 frnd 
 |-  ( ph -> ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) C_ RR )
36 nfv 
 |-  F/ n ph
37 eqid 
 |-  ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) = ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) )
38 1 2 uzn0d 
 |-  ( ph -> Z =/= (/) )
39 36 33 37 38 rnmptn0 
 |-  ( ph -> ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) =/= (/) )
40 nfcv 
 |-  F/_ j F
41 40 1 2 5 limsupre3uz 
 |-  ( ph -> ( ( limsup ` F ) e. RR <-> ( E. x e. RR A. i e. Z E. j e. ( ZZ>= ` i ) x <_ ( F ` j ) /\ E. x e. RR E. i e. Z A. j e. ( ZZ>= ` i ) ( F ` j ) <_ x ) ) )
42 4 41 mpbid 
 |-  ( ph -> ( E. x e. RR A. i e. Z E. j e. ( ZZ>= ` i ) x <_ ( F ` j ) /\ E. x e. RR E. i e. Z A. j e. ( ZZ>= ` i ) ( F ` j ) <_ x ) )
43 42 simpld 
 |-  ( ph -> E. x e. RR A. i e. Z E. j e. ( ZZ>= ` i ) x <_ ( F ` j ) )
44 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> x e. RR )
45 44 rexrd 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> x e. RR* )
46 5 3ad2ant1 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> F : Z --> RR* )
47 2 uztrn2 
 |-  ( ( i e. Z /\ j e. ( ZZ>= ` i ) ) -> j e. Z )
48 47 3adant1 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> j e. Z )
49 46 48 ffvelcdmd 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( F ` j ) e. RR* )
50 49 ad5ant134 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> ( F ` j ) e. RR* )
51 rnresss 
 |-  ran ( F |` ( ZZ>= ` i ) ) C_ ran F
52 3 frnd 
 |-  ( ph -> ran F C_ RR )
53 52 adantr 
 |-  ( ( ph /\ i e. Z ) -> ran F C_ RR )
54 51 53 sstrid 
 |-  ( ( ph /\ i e. Z ) -> ran ( F |` ( ZZ>= ` i ) ) C_ RR )
55 54 ssrexr 
 |-  ( ( ph /\ i e. Z ) -> ran ( F |` ( ZZ>= ` i ) ) C_ RR* )
56 55 supxrcld 
 |-  ( ( ph /\ i e. Z ) -> sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) e. RR* )
57 56 ad5ant13 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) e. RR* )
58 simpr 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> x <_ ( F ` j ) )
59 55 3adant3 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ran ( F |` ( ZZ>= ` i ) ) C_ RR* )
60 fvres 
 |-  ( j e. ( ZZ>= ` i ) -> ( ( F |` ( ZZ>= ` i ) ) ` j ) = ( F ` j ) )
61 60 eqcomd 
 |-  ( j e. ( ZZ>= ` i ) -> ( F ` j ) = ( ( F |` ( ZZ>= ` i ) ) ` j ) )
62 61 3ad2ant3 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( F ` j ) = ( ( F |` ( ZZ>= ` i ) ) ` j ) )
63 3 ffnd 
 |-  ( ph -> F Fn Z )
64 2 uzssd3 
 |-  ( i e. Z -> ( ZZ>= ` i ) C_ Z )
65 fnssres 
 |-  ( ( F Fn Z /\ ( ZZ>= ` i ) C_ Z ) -> ( F |` ( ZZ>= ` i ) ) Fn ( ZZ>= ` i ) )
66 63 64 65 syl2an 
 |-  ( ( ph /\ i e. Z ) -> ( F |` ( ZZ>= ` i ) ) Fn ( ZZ>= ` i ) )
67 fnfvelrn 
 |-  ( ( ( F |` ( ZZ>= ` i ) ) Fn ( ZZ>= ` i ) /\ j e. ( ZZ>= ` i ) ) -> ( ( F |` ( ZZ>= ` i ) ) ` j ) e. ran ( F |` ( ZZ>= ` i ) ) )
68 66 67 stoic3 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( ( F |` ( ZZ>= ` i ) ) ` j ) e. ran ( F |` ( ZZ>= ` i ) ) )
69 62 68 eqeltrd 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( F ` j ) e. ran ( F |` ( ZZ>= ` i ) ) )
70 eqid 
 |-  sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < )
71 59 69 70 supxrubd 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( F ` j ) <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
72 71 ad5ant134 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> ( F ` j ) <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
73 45 50 57 58 72 xrletrd 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
74 73 rexlimdva2 
 |-  ( ( ( ph /\ x e. RR ) /\ i e. Z ) -> ( E. j e. ( ZZ>= ` i ) x <_ ( F ` j ) -> x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) ) )
75 74 ralimdva 
 |-  ( ( ph /\ x e. RR ) -> ( A. i e. Z E. j e. ( ZZ>= ` i ) x <_ ( F ` j ) -> A. i e. Z x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) ) )
76 75 reximdva 
 |-  ( ph -> ( E. x e. RR A. i e. Z E. j e. ( ZZ>= ` i ) x <_ ( F ` j ) -> E. x e. RR A. i e. Z x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) ) )
77 43 76 mpd 
 |-  ( ph -> E. x e. RR A. i e. Z x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
78 fveq2 
 |-  ( n = i -> ( ZZ>= ` n ) = ( ZZ>= ` i ) )
79 78 reseq2d 
 |-  ( n = i -> ( F |` ( ZZ>= ` n ) ) = ( F |` ( ZZ>= ` i ) ) )
80 79 rneqd 
 |-  ( n = i -> ran ( F |` ( ZZ>= ` n ) ) = ran ( F |` ( ZZ>= ` i ) ) )
81 80 supeq1d 
 |-  ( n = i -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
82 eqcom 
 |-  ( n = i <-> i = n )
83 eqcom 
 |-  ( sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) <-> sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) )
84 81 82 83 3imtr3i 
 |-  ( i = n -> sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) )
85 84 breq2d 
 |-  ( i = n -> ( x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) <-> x <_ sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) )
86 85 cbvralvw 
 |-  ( A. i e. Z x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) <-> A. n e. Z x <_ sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) )
87 86 rexbii 
 |-  ( E. x e. RR A. i e. Z x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) <-> E. x e. RR A. n e. Z x <_ sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) )
88 77 87 sylib 
 |-  ( ph -> E. x e. RR A. n e. Z x <_ sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) )
89 36 33 rnmptbd2 
 |-  ( ph -> ( E. x e. RR A. n e. Z x <_ sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) <-> E. x e. RR A. y e. ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) x <_ y ) )
90 88 89 mpbid 
 |-  ( ph -> E. x e. RR A. y e. ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) x <_ y )
91 infxrre 
 |-  ( ( ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) C_ RR /\ ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) =/= (/) /\ E. x e. RR A. y e. ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) x <_ y ) -> inf ( ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) , RR* , < ) = inf ( ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) , RR , < ) )
92 35 39 90 91 syl3anc 
 |-  ( ph -> inf ( ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) , RR* , < ) = inf ( ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) , RR , < ) )
93 fveq2 
 |-  ( n = k -> ( ZZ>= ` n ) = ( ZZ>= ` k ) )
94 93 reseq2d 
 |-  ( n = k -> ( F |` ( ZZ>= ` n ) ) = ( F |` ( ZZ>= ` k ) ) )
95 94 rneqd 
 |-  ( n = k -> ran ( F |` ( ZZ>= ` n ) ) = ran ( F |` ( ZZ>= ` k ) ) )
96 95 supeq1d 
 |-  ( n = k -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) )
97 96 cbvmptv 
 |-  ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) = ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) )
98 97 rneqi 
 |-  ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) = ran ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) )
99 98 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 , < )
100 99 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 , < ) )
101 6 92 100 3eqtrd 
 |-  ( ph -> ( limsup ` F ) = inf ( ran ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) ) , RR , < ) )