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 bilani 
 |-  ( ( ( ( ( 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 ) )
36 simp-4r 
 |-  ( ( ( ( ( ph /\ M e. ZZ ) /\ y e. RR ) /\ k e. RR ) /\ A. i e. Z ( k <_ i -> ( F ` i ) <_ y ) ) -> M e. ZZ )
37 35 36 syldan 
 |-  ( ( ( ( ( ph /\ M e. ZZ ) /\ y e. RR ) /\ k e. RR ) /\ A. l e. Z ( k <_ l -> ( F ` l ) <_ y ) ) -> M e. ZZ )
38 3 ad4antr 
 |-  ( ( ( ( ( ph /\ M e. ZZ ) /\ y e. RR ) /\ k e. RR ) /\ A. i e. Z ( k <_ i -> ( F ` i ) <_ y ) ) -> F : Z --> RR )
39 35 38 syldan 
 |-  ( ( ( ( ( ph /\ M e. ZZ ) /\ y e. RR ) /\ k e. RR ) /\ A. l e. Z ( k <_ l -> ( F ` l ) <_ y ) ) -> F : Z --> RR )
40 simpllr 
 |-  ( ( ( ( ( ph /\ M e. ZZ ) /\ y e. RR ) /\ k e. RR ) /\ A. i e. Z ( k <_ i -> ( F ` i ) <_ y ) ) -> y e. RR )
41 35 40 syldan 
 |-  ( ( ( ( ( ph /\ M e. ZZ ) /\ y e. RR ) /\ k e. RR ) /\ A. l e. Z ( k <_ l -> ( F ` l ) <_ y ) ) -> y e. RR )
42 simplr 
 |-  ( ( ( ( ( ph /\ M e. ZZ ) /\ y e. RR ) /\ k e. RR ) /\ A. i e. Z ( k <_ i -> ( F ` i ) <_ y ) ) -> k e. RR )
43 35 42 syldan 
 |-  ( ( ( ( ( ph /\ M e. ZZ ) /\ y e. RR ) /\ k e. RR ) /\ A. l e. Z ( k <_ l -> ( F ` l ) <_ y ) ) -> k e. RR )
44 34 biimpri 
 |-  ( A. i e. Z ( k <_ i -> ( F ` i ) <_ y ) -> A. l e. Z ( k <_ l -> ( F ` l ) <_ y ) )
45 35 44 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 ) )
46 eqid 
 |-  if ( ( |^ ` k ) <_ M , M , ( |^ ` k ) ) = if ( ( |^ ` k ) <_ M , M , ( |^ ` k ) )
47 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 , < )
48 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 , < ) )
49 20 29 37 2 39 41 43 45 46 47 48 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 )
50 49 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 ) )
51 50 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 ) )
52 12 51 mpd 
 |-  ( ( ph /\ M e. ZZ ) -> E. x e. RR A. l e. Z ( F ` l ) <_ x )
53 2 a1i 
 |-  ( -. M e. ZZ -> Z = ( ZZ>= ` M ) )
54 uz0 
 |-  ( -. M e. ZZ -> ( ZZ>= ` M ) = (/) )
55 53 54 eqtrd 
 |-  ( -. M e. ZZ -> Z = (/) )
56 0red 
 |-  ( Z = (/) -> 0 e. RR )
57 rzal 
 |-  ( Z = (/) -> A. l e. Z ( F ` l ) <_ 0 )
58 brralrspcev 
 |-  ( ( 0 e. RR /\ A. l e. Z ( F ` l ) <_ 0 ) -> E. x e. RR A. l e. Z ( F ` l ) <_ x )
59 56 57 58 syl2anc 
 |-  ( Z = (/) -> E. x e. RR A. l e. Z ( F ` l ) <_ x )
60 55 59 syl 
 |-  ( -. M e. ZZ -> E. x e. RR A. l e. Z ( F ` l ) <_ x )
61 60 adantl 
 |-  ( ( ph /\ -. M e. ZZ ) -> E. x e. RR A. l e. Z ( F ` l ) <_ x )
62 52 61 pm2.61dan 
 |-  ( ph -> E. x e. RR A. l e. Z ( F ` l ) <_ x )
63 nfcv 
 |-  F/_ j l
64 1 63 nffv 
 |-  F/_ j ( F ` l )
65 nfcv 
 |-  F/_ j <_
66 nfcv 
 |-  F/_ j x
67 64 65 66 nfbr 
 |-  F/ j ( F ` l ) <_ x
68 nfv 
 |-  F/ l ( F ` j ) <_ x
69 fveq2 
 |-  ( l = j -> ( F ` l ) = ( F ` j ) )
70 69 breq1d 
 |-  ( l = j -> ( ( F ` l ) <_ x <-> ( F ` j ) <_ x ) )
71 67 68 70 cbvralw 
 |-  ( A. l e. Z ( F ` l ) <_ x <-> A. j e. Z ( F ` j ) <_ x )
72 71 rexbii 
 |-  ( E. x e. RR A. l e. Z ( F ` l ) <_ x <-> E. x e. RR A. j e. Z ( F ` j ) <_ x )
73 62 72 sylib 
 |-  ( ph -> E. x e. RR A. j e. Z ( F ` j ) <_ x )