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 id 
 |-  ( n e. Z -> n e. Z )
9 2 8 uzssd2 
 |-  ( n e. Z -> ( ZZ>= ` n ) C_ Z )
10 9 adantl 
 |-  ( ( ph /\ n e. Z ) -> ( ZZ>= ` n ) C_ Z )
11 7 10 feqresmpt 
 |-  ( ( ph /\ n e. Z ) -> ( F |` ( ZZ>= ` n ) ) = ( m e. ( ZZ>= ` n ) |-> ( F ` m ) ) )
12 11 rneqd 
 |-  ( ( ph /\ n e. Z ) -> ran ( F |` ( ZZ>= ` n ) ) = ran ( m e. ( ZZ>= ` n ) |-> ( F ` m ) ) )
13 12 supeq1d 
 |-  ( ( ph /\ n e. Z ) -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( m e. ( ZZ>= ` n ) |-> ( F ` m ) ) , RR* , < ) )
14 nfcv 
 |-  F/_ m F
15 4 renepnfd 
 |-  ( ph -> ( limsup ` F ) =/= +oo )
16 14 2 3 15 limsupubuz 
 |-  ( ph -> E. x e. RR A. m e. Z ( F ` m ) <_ x )
17 16 adantr 
 |-  ( ( ph /\ n e. Z ) -> E. x e. RR A. m e. Z ( F ` m ) <_ x )
18 ssralv 
 |-  ( ( ZZ>= ` n ) C_ Z -> ( A. m e. Z ( F ` m ) <_ x -> A. m e. ( ZZ>= ` n ) ( F ` m ) <_ x ) )
19 9 18 syl 
 |-  ( n e. Z -> ( A. m e. Z ( F ` m ) <_ x -> A. m e. ( ZZ>= ` n ) ( F ` m ) <_ x ) )
20 19 adantl 
 |-  ( ( ph /\ n e. Z ) -> ( A. m e. Z ( F ` m ) <_ x -> A. m e. ( ZZ>= ` n ) ( F ` m ) <_ x ) )
21 20 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 ) )
22 17 21 mpd 
 |-  ( ( ph /\ n e. Z ) -> E. x e. RR A. m e. ( ZZ>= ` n ) ( F ` m ) <_ x )
23 nfv 
 |-  F/ m ( ph /\ n e. Z )
24 2 eluzelz2 
 |-  ( n e. Z -> n e. ZZ )
25 uzid 
 |-  ( n e. ZZ -> n e. ( ZZ>= ` n ) )
26 ne0i 
 |-  ( n e. ( ZZ>= ` n ) -> ( ZZ>= ` n ) =/= (/) )
27 24 25 26 3syl 
 |-  ( n e. Z -> ( ZZ>= ` n ) =/= (/) )
28 27 adantl 
 |-  ( ( ph /\ n e. Z ) -> ( ZZ>= ` n ) =/= (/) )
29 7 adantr 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> F : Z --> RR )
30 10 sselda 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
31 29 30 ffvelrnd 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> ( F ` m ) e. RR )
32 23 28 31 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 ) )
33 22 32 mpbird 
 |-  ( ( ph /\ n e. Z ) -> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( F ` m ) ) , RR* , < ) e. RR )
34 13 33 eqeltrd 
 |-  ( ( ph /\ n e. Z ) -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) e. RR )
35 34 fmpttd 
 |-  ( ph -> ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) : Z --> RR )
36 35 frnd 
 |-  ( ph -> ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) C_ RR )
37 nfv 
 |-  F/ n ph
38 eqid 
 |-  ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) = ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) )
39 1 2 uzn0d 
 |-  ( ph -> Z =/= (/) )
40 37 34 38 39 rnmptn0 
 |-  ( ph -> ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) =/= (/) )
41 nfcv 
 |-  F/_ j F
42 41 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 ) ) )
43 4 42 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 ) )
44 43 simpld 
 |-  ( ph -> E. x e. RR A. i e. Z E. j e. ( ZZ>= ` i ) x <_ ( F ` j ) )
45 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> x e. RR )
46 45 rexrd 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> x e. RR* )
47 5 3ad2ant1 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> F : Z --> RR* )
48 2 uztrn2 
 |-  ( ( i e. Z /\ j e. ( ZZ>= ` i ) ) -> j e. Z )
49 48 3adant1 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> j e. Z )
50 47 49 ffvelrnd 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( F ` j ) e. RR* )
51 50 ad5ant134 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> ( F ` j ) e. RR* )
52 rnresss 
 |-  ran ( F |` ( ZZ>= ` i ) ) C_ ran F
53 52 a1i 
 |-  ( ( ph /\ i e. Z ) -> ran ( F |` ( ZZ>= ` i ) ) C_ ran F )
54 3 frnd 
 |-  ( ph -> ran F C_ RR )
55 54 adantr 
 |-  ( ( ph /\ i e. Z ) -> ran F C_ RR )
56 53 55 sstrd 
 |-  ( ( ph /\ i e. Z ) -> ran ( F |` ( ZZ>= ` i ) ) C_ RR )
57 ressxr 
 |-  RR C_ RR*
58 57 a1i 
 |-  ( ( ph /\ i e. Z ) -> RR C_ RR* )
59 56 58 sstrd 
 |-  ( ( ph /\ i e. Z ) -> ran ( F |` ( ZZ>= ` i ) ) C_ RR* )
60 59 supxrcld 
 |-  ( ( ph /\ i e. Z ) -> sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) e. RR* )
61 60 ad5ant13 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) e. RR* )
62 simpr 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> x <_ ( F ` j ) )
63 59 3adant3 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ran ( F |` ( ZZ>= ` i ) ) C_ RR* )
64 fvres 
 |-  ( j e. ( ZZ>= ` i ) -> ( ( F |` ( ZZ>= ` i ) ) ` j ) = ( F ` j ) )
65 64 eqcomd 
 |-  ( j e. ( ZZ>= ` i ) -> ( F ` j ) = ( ( F |` ( ZZ>= ` i ) ) ` j ) )
66 65 3ad2ant3 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( F ` j ) = ( ( F |` ( ZZ>= ` i ) ) ` j ) )
67 3 ffnd 
 |-  ( ph -> F Fn Z )
68 67 adantr 
 |-  ( ( ph /\ i e. Z ) -> F Fn Z )
69 id 
 |-  ( i e. Z -> i e. Z )
70 2 69 uzssd2 
 |-  ( i e. Z -> ( ZZ>= ` i ) C_ Z )
71 70 adantl 
 |-  ( ( ph /\ i e. Z ) -> ( ZZ>= ` i ) C_ Z )
72 fnssres 
 |-  ( ( F Fn Z /\ ( ZZ>= ` i ) C_ Z ) -> ( F |` ( ZZ>= ` i ) ) Fn ( ZZ>= ` i ) )
73 68 71 72 syl2anc 
 |-  ( ( ph /\ i e. Z ) -> ( F |` ( ZZ>= ` i ) ) Fn ( ZZ>= ` i ) )
74 73 3adant3 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( F |` ( ZZ>= ` i ) ) Fn ( ZZ>= ` i ) )
75 simp3 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> j e. ( ZZ>= ` i ) )
76 fnfvelrn 
 |-  ( ( ( F |` ( ZZ>= ` i ) ) Fn ( ZZ>= ` i ) /\ j e. ( ZZ>= ` i ) ) -> ( ( F |` ( ZZ>= ` i ) ) ` j ) e. ran ( F |` ( ZZ>= ` i ) ) )
77 74 75 76 syl2anc 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( ( F |` ( ZZ>= ` i ) ) ` j ) e. ran ( F |` ( ZZ>= ` i ) ) )
78 66 77 eqeltrd 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( F ` j ) e. ran ( F |` ( ZZ>= ` i ) ) )
79 eqid 
 |-  sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < )
80 63 78 79 supxrubd 
 |-  ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( F ` j ) <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
81 80 ad5ant134 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> ( F ` j ) <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
82 46 51 61 62 81 xrletrd 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
83 82 rexlimdva2 
 |-  ( ( ( ph /\ x e. RR ) /\ i e. Z ) -> ( E. j e. ( ZZ>= ` i ) x <_ ( F ` j ) -> x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) ) )
84 83 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* , < ) ) )
85 84 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* , < ) ) )
86 44 85 mpd 
 |-  ( ph -> E. x e. RR A. i e. Z x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
87 86 idi 
 |-  ( ph -> E. x e. RR A. i e. Z x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
88 fveq2 
 |-  ( n = i -> ( ZZ>= ` n ) = ( ZZ>= ` i ) )
89 88 reseq2d 
 |-  ( n = i -> ( F |` ( ZZ>= ` n ) ) = ( F |` ( ZZ>= ` i ) ) )
90 89 rneqd 
 |-  ( n = i -> ran ( F |` ( ZZ>= ` n ) ) = ran ( F |` ( ZZ>= ` i ) ) )
91 90 supeq1d 
 |-  ( n = i -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) )
92 eqcom 
 |-  ( n = i <-> i = n )
93 92 imbi1i 
 |-  ( ( n = i -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) ) <-> ( i = n -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) ) )
94 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* , < ) )
95 94 imbi2i 
 |-  ( ( i = n -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) ) <-> ( i = n -> sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) )
96 93 95 bitri 
 |-  ( ( n = i -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) ) <-> ( i = n -> sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) )
97 91 96 mpbi 
 |-  ( i = n -> sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) )
98 97 breq2d 
 |-  ( i = n -> ( x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) <-> x <_ sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) )
99 98 cbvralvw 
 |-  ( A. i e. Z x <_ sup ( ran ( F |` ( ZZ>= ` i ) ) , RR* , < ) <-> A. n e. Z x <_ sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) )
100 99 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* , < ) )
101 87 100 sylib 
 |-  ( ph -> E. x e. RR A. n e. Z x <_ sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) )
102 34 elexd 
 |-  ( ( ph /\ n e. Z ) -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) e. _V )
103 37 102 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 ) )
104 101 103 mpbid 
 |-  ( ph -> E. x e. RR A. y e. ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) x <_ y )
105 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 , < ) )
106 36 40 104 105 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 , < ) )
107 fveq2 
 |-  ( n = k -> ( ZZ>= ` n ) = ( ZZ>= ` k ) )
108 107 reseq2d 
 |-  ( n = k -> ( F |` ( ZZ>= ` n ) ) = ( F |` ( ZZ>= ` k ) ) )
109 108 rneqd 
 |-  ( n = k -> ran ( F |` ( ZZ>= ` n ) ) = ran ( F |` ( ZZ>= ` k ) ) )
110 109 supeq1d 
 |-  ( n = k -> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) )
111 110 cbvmptv 
 |-  ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) = ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) )
112 111 rneqi 
 |-  ran ( n e. Z |-> sup ( ran ( F |` ( ZZ>= ` n ) ) , RR* , < ) ) = ran ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) )
113 112 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 , < )
114 113 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 , < ) )
115 6 106 114 3eqtrd 
 |-  ( ph -> ( limsup ` F ) = inf ( ran ( k e. Z |-> sup ( ran ( F |` ( ZZ>= ` k ) ) , RR* , < ) ) , RR , < ) )