Metamath Proof Explorer

Theorem limsupubuz

Description: For a real-valued function on a set of upper integers, if the superior limit is not +oo , then the function is bounded above. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupubuz.j 
|- F/_ j F
limsupubuz.z 
|- Z = ( ZZ>= ` M )
limsupubuz.f 
|- ( ph -> F : Z --> RR )
limsupubuz.n 
|- ( ph -> ( limsup ` F ) =/= +oo )
Assertion limsupubuz 
|- ( ph -> E. x e. RR A. j e. Z ( F ` j ) <_ x )

Proof

Step Hyp Ref Expression
1 limsupubuz.j 
 |-  F/_ j F
2 limsupubuz.z 
 |-  Z = ( ZZ>= ` M )
3 limsupubuz.f 
 |-  ( ph -> F : Z --> RR )
4 limsupubuz.n 
 |-  ( ph -> ( limsup ` F ) =/= +oo )
5 nfv 
 |-  F/ l ph
6 nfcv 
 |-  F/_ l F
7 uzssre 
 |-  ( ZZ>= ` M ) C_ RR
8 2 7 eqsstri 
 |-  Z C_ RR
9 8 a1i 
 |-  ( ph -> Z C_ RR )
10 3 frexr 
 |-  ( ph -> F : Z --> RR* )
11 5 6 9 10 4 limsupub 
 |-  ( ph -> E. y e. RR E. k e. RR A. l e. Z ( k <_ l -> ( F ` l ) <_ y ) )
12 11 adantr 
 |-  ( ( ph /\ M e. ZZ ) -> E. y e. RR E. k e. RR A. l e. Z ( k <_ l -> ( F ` l ) <_ y ) )
13 nfv 
 |-  F/ l M e. ZZ
14 5 13 nfan 
 |-  F/ l ( ph /\ M e. ZZ )
15 nfv 
 |-  F/ l y e. RR
16 14 15 nfan 
 |-  F/ l ( ( ph /\ M e. ZZ ) /\ y e. RR )
17 nfv 
 |-  F/ l k e. RR
18 16 17 nfan 
 |-  F/ l ( ( ( ph /\ M e. ZZ ) /\ y e. RR ) /\ k e. RR )
19 nfra1 
 |-  F/ l A. l e. Z ( k <_ l -> ( F ` l ) <_ y )
20 18 19 nfan 
 |-  F/ l ( ( ( ( ph /\ M e. ZZ ) /\ y e. RR ) /\ k e. RR ) /\ A. l e. Z ( k <_ l -> ( F ` l ) <_ y ) )
21 nfmpt1 
 |-  F/_ l ( l e. ( M ... if ( ( |^ ` k ) <_ M , M , ( |^ ` k ) ) ) |-> ( F ` l ) )
22 21 nfrn 
 |-  F/_ l ran ( l e. ( M ... if ( ( |^ ` k ) <_ M , M , ( |^ ` k ) ) ) |-> ( F ` l ) )
23 nfcv 
 |-  F/_ l RR
24 nfcv 
 |-  F/_ l <
25 22 23 24 nfsup 
 |-  F/_ l sup ( ran ( l e. ( M ... if ( ( |^ ` k ) <_ M , M , ( |^ ` k ) ) ) |-> ( F ` l ) ) , RR , < )
26 nfcv 
 |-  F/_ l <_
27 nfcv 
 |-  F/_ l y
28 25 26 27 nfbr 
 |-  F/ l sup ( ran ( l e. ( M ... if ( ( |^ ` k ) <_ M , M , ( |^ ` k ) ) ) |-> ( F ` l ) ) , RR , < ) <_ y
29 28 27 25 nfif 
 |-  F/_ l if ( sup ( ran ( l e. ( M ... if ( ( |^ ` k ) <_ M , M , ( |^ ` k ) ) ) |-> ( F ` l ) ) , RR , < ) <_ y , y , sup ( ran ( l e. ( M ... if ( ( |^ ` k ) <_ M , M , ( |^ ` k ) ) ) |-> ( F ` l ) ) , RR , < ) )
30 breq2 
 |-  ( l = i -> ( k <_ l <-> k <_ i ) )
31 fveq2 
 |-  ( l = i -> ( F ` l ) = ( F ` i ) )
32 31 breq1d 
 |-  ( l = i -> ( ( F ` l ) <_ y <-> ( F ` i ) <_ y ) )
33 30 32 imbi12d 
 |-  ( l = i -> ( ( k <_ l -> ( F ` l ) <_ y ) <-> ( k <_ i -> ( F ` i ) <_ y ) ) )
34 33 cbvralvw 
 |-  ( A. l e. Z ( k <_ l -> ( F ` l ) <_ y ) <-> A. i e. Z ( k <_ i -> ( F ` i ) <_ y ) )
35 34 biimpi 
 |-  ( A. l e. Z ( k <_ l -> ( F ` l ) <_ y ) -> A. i e. Z ( k <_ i -> ( F ` i ) <_ y ) )
36 35 adantl 
 |-  ( ( ( ( ( ph /\ M e. ZZ ) /\ y e. RR ) /\ k e. RR ) /\ A. l e. Z ( k <_ l -> ( F ` l ) <_ y ) ) -> A. i e. Z ( k <_ i -> ( F ` i ) <_ y ) )
37 simp-4r 
 |-  ( ( ( ( ( ph /\ M e. ZZ ) /\ y e. RR ) /\ k e. RR ) /\ A. i e. Z ( k <_ i -> ( F ` i ) <_ y ) ) -> M e. ZZ )
38 36 37 syldan 
 |-  ( ( ( ( ( ph /\ M e. ZZ ) /\ y e. RR ) /\ k e. RR ) /\ A. l e. Z ( k <_ l -> ( F ` l ) <_ y ) ) -> M e. ZZ )
39 3 ad4antr 
 |-  ( ( ( ( ( ph /\ M e. ZZ ) /\ y e. RR ) /\ k e. RR ) /\ A. i e. Z ( k <_ i -> ( F ` i ) <_ y ) ) -> F : Z --> RR )
40 36 39 syldan 
 |-  ( ( ( ( ( ph /\ M e. ZZ ) /\ y e. RR ) /\ k e. RR ) /\ A. l e. Z ( k <_ l -> ( F ` l ) <_ y ) ) -> F : Z --> RR )
41 simpllr 
 |-  ( ( ( ( ( ph /\ M e. ZZ ) /\ y e. RR ) /\ k e. RR ) /\ A. i e. Z ( k <_ i -> ( F ` i ) <_ y ) ) -> y e. RR )
42 36 41 syldan 
 |-  ( ( ( ( ( ph /\ M e. ZZ ) /\ y e. RR ) /\ k e. RR ) /\ A. l e. Z ( k <_ l -> ( F ` l ) <_ y ) ) -> y e. RR )
43 simplr 
 |-  ( ( ( ( ( ph /\ M e. ZZ ) /\ y e. RR ) /\ k e. RR ) /\ A. i e. Z ( k <_ i -> ( F ` i ) <_ y ) ) -> k e. RR )
44 36 43 syldan 
 |-  ( ( ( ( ( ph /\ M e. ZZ ) /\ y e. RR ) /\ k e. RR ) /\ A. l e. Z ( k <_ l -> ( F ` l ) <_ y ) ) -> k e. RR )
45 34 biimpri 
 |-  ( A. i e. Z ( k <_ i -> ( F ` i ) <_ y ) -> A. l e. Z ( k <_ l -> ( F ` l ) <_ y ) )
46 36 45 syl 
 |-  ( ( ( ( ( ph /\ M e. ZZ ) /\ y e. RR ) /\ k e. RR ) /\ A. l e. Z ( k <_ l -> ( F ` l ) <_ y ) ) -> A. l e. Z ( k <_ l -> ( F ` l ) <_ y ) )
47 eqid 
 |-  if ( ( |^ ` k ) <_ M , M , ( |^ ` k ) ) = if ( ( |^ ` k ) <_ M , M , ( |^ ` k ) )
48 eqid 
 |-  sup ( ran ( l e. ( M ... if ( ( |^ ` k ) <_ M , M , ( |^ ` k ) ) ) |-> ( F ` l ) ) , RR , < ) = sup ( ran ( l e. ( M ... if ( ( |^ ` k ) <_ M , M , ( |^ ` k ) ) ) |-> ( F ` l ) ) , RR , < )
49 eqid 
 |-  if ( sup ( ran ( l e. ( M ... if ( ( |^ ` k ) <_ M , M , ( |^ ` k ) ) ) |-> ( F ` l ) ) , RR , < ) <_ y , y , sup ( ran ( l e. ( M ... if ( ( |^ ` k ) <_ M , M , ( |^ ` k ) ) ) |-> ( F ` l ) ) , RR , < ) ) = if ( sup ( ran ( l e. ( M ... if ( ( |^ ` k ) <_ M , M , ( |^ ` k ) ) ) |-> ( F ` l ) ) , RR , < ) <_ y , y , sup ( ran ( l e. ( M ... if ( ( |^ ` k ) <_ M , M , ( |^ ` k ) ) ) |-> ( F ` l ) ) , RR , < ) )
50 20 29 38 2 40 42 44 46 47 48 49 limsupubuzlem 
 |-  ( ( ( ( ( ph /\ M e. ZZ ) /\ y e. RR ) /\ k e. RR ) /\ A. l e. Z ( k <_ l -> ( F ` l ) <_ y ) ) -> E. x e. RR A. l e. Z ( F ` l ) <_ x )
51 50 rexlimdva2 
 |-  ( ( ( ph /\ M e. ZZ ) /\ y e. RR ) -> ( E. k e. RR A. l e. Z ( k <_ l -> ( F ` l ) <_ y ) -> E. x e. RR A. l e. Z ( F ` l ) <_ x ) )
52 51 rexlimdva 
 |-  ( ( ph /\ M e. ZZ ) -> ( E. y e. RR E. k e. RR A. l e. Z ( k <_ l -> ( F ` l ) <_ y ) -> E. x e. RR A. l e. Z ( F ` l ) <_ x ) )
53 12 52 mpd 
 |-  ( ( ph /\ M e. ZZ ) -> E. x e. RR A. l e. Z ( F ` l ) <_ x )
54 2 a1i 
 |-  ( -. M e. ZZ -> Z = ( ZZ>= ` M ) )
55 uz0 
 |-  ( -. M e. ZZ -> ( ZZ>= ` M ) = (/) )
56 54 55 eqtrd 
 |-  ( -. M e. ZZ -> Z = (/) )
57 0red 
 |-  ( Z = (/) -> 0 e. RR )
58 rzal 
 |-  ( Z = (/) -> A. l e. Z ( F ` l ) <_ 0 )
59 brralrspcev 
 |-  ( ( 0 e. RR /\ A. l e. Z ( F ` l ) <_ 0 ) -> E. x e. RR A. l e. Z ( F ` l ) <_ x )
60 57 58 59 syl2anc 
 |-  ( Z = (/) -> E. x e. RR A. l e. Z ( F ` l ) <_ x )
61 56 60 syl 
 |-  ( -. M e. ZZ -> E. x e. RR A. l e. Z ( F ` l ) <_ x )
62 61 adantl 
 |-  ( ( ph /\ -. M e. ZZ ) -> E. x e. RR A. l e. Z ( F ` l ) <_ x )
63 53 62 pm2.61dan 
 |-  ( ph -> E. x e. RR A. l e. Z ( F ` l ) <_ x )
64 nfcv 
 |-  F/_ j l
65 1 64 nffv 
 |-  F/_ j ( F ` l )
66 nfcv 
 |-  F/_ j <_
67 nfcv 
 |-  F/_ j x
68 65 66 67 nfbr 
 |-  F/ j ( F ` l ) <_ x
69 nfv 
 |-  F/ l ( F ` j ) <_ x
70 fveq2 
 |-  ( l = j -> ( F ` l ) = ( F ` j ) )
71 70 breq1d 
 |-  ( l = j -> ( ( F ` l ) <_ x <-> ( F ` j ) <_ x ) )
72 68 69 71 cbvralw 
 |-  ( A. l e. Z ( F ` l ) <_ x <-> A. j e. Z ( F ` j ) <_ x )
73 72 rexbii 
 |-  ( E. x e. RR A. l e. Z ( F ` l ) <_ x <-> E. x e. RR A. j e. Z ( F ` j ) <_ x )
74 63 73 sylib 
 |-  ( ph -> E. x e. RR A. j e. Z ( F ` j ) <_ x )