Metamath Proof Explorer

Theorem limsupubuzlem

Description: If the limsup is not +oo , then the function is bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupubuzlem.j 
|- F/ j ph
limsupubuzlem.e 
|- F/_ j X
limsupubuzlem.m 
|- ( ph -> M e. ZZ )
limsupubuzlem.z 
|- Z = ( ZZ>= ` M )
limsupubuzlem.f 
|- ( ph -> F : Z --> RR )
limsupubuzlem.y 
|- ( ph -> Y e. RR )
limsupubuzlem.k 
|- ( ph -> K e. RR )
limsupubuzlem.b 
|- ( ph -> A. j e. Z ( K <_ j -> ( F ` j ) <_ Y ) )
limsupubuzlem.n 
|- N = if ( ( |^ ` K ) <_ M , M , ( |^ ` K ) )
limsupubuzlem.w 
|- W = sup ( ran ( j e. ( M ... N ) |-> ( F ` j ) ) , RR , < )
limsupubuzlem.x 
|- X = if ( W <_ Y , Y , W )
Assertion limsupubuzlem 
|- ( ph -> E. x e. RR A. j e. Z ( F ` j ) <_ x )

Proof

Step Hyp Ref Expression
1 limsupubuzlem.j 
 |-  F/ j ph
2 limsupubuzlem.e 
 |-  F/_ j X
3 limsupubuzlem.m 
 |-  ( ph -> M e. ZZ )
4 limsupubuzlem.z 
 |-  Z = ( ZZ>= ` M )
5 limsupubuzlem.f 
 |-  ( ph -> F : Z --> RR )
6 limsupubuzlem.y 
 |-  ( ph -> Y e. RR )
7 limsupubuzlem.k 
 |-  ( ph -> K e. RR )
8 limsupubuzlem.b 
 |-  ( ph -> A. j e. Z ( K <_ j -> ( F ` j ) <_ Y ) )
9 limsupubuzlem.n 
 |-  N = if ( ( |^ ` K ) <_ M , M , ( |^ ` K ) )
10 limsupubuzlem.w 
 |-  W = sup ( ran ( j e. ( M ... N ) |-> ( F ` j ) ) , RR , < )
11 limsupubuzlem.x 
 |-  X = if ( W <_ Y , Y , W )
12 10 a1i 
 |-  ( ph -> W = sup ( ran ( j e. ( M ... N ) |-> ( F ` j ) ) , RR , < ) )
13 ltso 
 |-  < Or RR
14 13 a1i 
 |-  ( ph -> < Or RR )
15 fzfid 
 |-  ( ph -> ( M ... N ) e. Fin )
16 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
17 9 a1i 
 |-  ( ph -> N = if ( ( |^ ` K ) <_ M , M , ( |^ ` K ) ) )
18 ceilcl 
 |-  ( K e. RR -> ( |^ ` K ) e. ZZ )
19 7 18 syl 
 |-  ( ph -> ( |^ ` K ) e. ZZ )
20 3 19 ifcld 
 |-  ( ph -> if ( ( |^ ` K ) <_ M , M , ( |^ ` K ) ) e. ZZ )
21 17 20 eqeltrd 
 |-  ( ph -> N e. ZZ )
22 19 zred 
 |-  ( ph -> ( |^ ` K ) e. RR )
23 3 zred 
 |-  ( ph -> M e. RR )
24 max2 
 |-  ( ( ( |^ ` K ) e. RR /\ M e. RR ) -> M <_ if ( ( |^ ` K ) <_ M , M , ( |^ ` K ) ) )
25 22 23 24 syl2anc 
 |-  ( ph -> M <_ if ( ( |^ ` K ) <_ M , M , ( |^ ` K ) ) )
26 17 eqcomd 
 |-  ( ph -> if ( ( |^ ` K ) <_ M , M , ( |^ ` K ) ) = N )
27 25 26 breqtrd 
 |-  ( ph -> M <_ N )
28 16 3 21 27 eluzd 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
29 eluzfz2 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
30 28 29 syl 
 |-  ( ph -> N e. ( M ... N ) )
31 30 ne0d 
 |-  ( ph -> ( M ... N ) =/= (/) )
32 5 adantr 
 |-  ( ( ph /\ j e. ( M ... N ) ) -> F : Z --> RR )
33 3 adantr 
 |-  ( ( ph /\ j e. ( M ... N ) ) -> M e. ZZ )
34 elfzelz 
 |-  ( j e. ( M ... N ) -> j e. ZZ )
35 34 adantl 
 |-  ( ( ph /\ j e. ( M ... N ) ) -> j e. ZZ )
36 elfzle1 
 |-  ( j e. ( M ... N ) -> M <_ j )
37 36 adantl 
 |-  ( ( ph /\ j e. ( M ... N ) ) -> M <_ j )
38 16 33 35 37 eluzd 
 |-  ( ( ph /\ j e. ( M ... N ) ) -> j e. ( ZZ>= ` M ) )
39 38 4 eleqtrrdi 
 |-  ( ( ph /\ j e. ( M ... N ) ) -> j e. Z )
40 32 39 ffvelrnd 
 |-  ( ( ph /\ j e. ( M ... N ) ) -> ( F ` j ) e. RR )
41 1 14 15 31 40 fisupclrnmpt 
 |-  ( ph -> sup ( ran ( j e. ( M ... N ) |-> ( F ` j ) ) , RR , < ) e. RR )
42 12 41 eqeltrd 
 |-  ( ph -> W e. RR )
43 6 42 ifcld 
 |-  ( ph -> if ( W <_ Y , Y , W ) e. RR )
44 11 43 eqeltrid 
 |-  ( ph -> X e. RR )
45 5 ffvelrnda 
 |-  ( ( ph /\ j e. Z ) -> ( F ` j ) e. RR )
46 45 adantr 
 |-  ( ( ( ph /\ j e. Z ) /\ j <_ N ) -> ( F ` j ) e. RR )
47 42 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ j <_ N ) -> W e. RR )
48 44 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ j <_ N ) -> X e. RR )
49 simpll 
 |-  ( ( ( ph /\ j e. Z ) /\ j <_ N ) -> ph )
50 3 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ j <_ N ) -> M e. ZZ )
51 21 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ j <_ N ) -> N e. ZZ )
52 4 eluzelz2 
 |-  ( j e. Z -> j e. ZZ )
53 52 ad2antlr 
 |-  ( ( ( ph /\ j e. Z ) /\ j <_ N ) -> j e. ZZ )
54 4 eleq2i 
 |-  ( j e. Z <-> j e. ( ZZ>= ` M ) )
55 54 biimpi 
 |-  ( j e. Z -> j e. ( ZZ>= ` M ) )
56 eluzle 
 |-  ( j e. ( ZZ>= ` M ) -> M <_ j )
57 55 56 syl 
 |-  ( j e. Z -> M <_ j )
58 57 ad2antlr 
 |-  ( ( ( ph /\ j e. Z ) /\ j <_ N ) -> M <_ j )
59 simpr 
 |-  ( ( ( ph /\ j e. Z ) /\ j <_ N ) -> j <_ N )
60 50 51 53 58 59 elfzd 
 |-  ( ( ( ph /\ j e. Z ) /\ j <_ N ) -> j e. ( M ... N ) )
61 1 15 40 fimaxre4 
 |-  ( ph -> E. b e. RR A. j e. ( M ... N ) ( F ` j ) <_ b )
62 1 40 61 suprubrnmpt 
 |-  ( ( ph /\ j e. ( M ... N ) ) -> ( F ` j ) <_ sup ( ran ( j e. ( M ... N ) |-> ( F ` j ) ) , RR , < ) )
63 62 10 breqtrrdi 
 |-  ( ( ph /\ j e. ( M ... N ) ) -> ( F ` j ) <_ W )
64 49 60 63 syl2anc 
 |-  ( ( ( ph /\ j e. Z ) /\ j <_ N ) -> ( F ` j ) <_ W )
65 max1 
 |-  ( ( W e. RR /\ Y e. RR ) -> W <_ if ( W <_ Y , Y , W ) )
66 42 6 65 syl2anc 
 |-  ( ph -> W <_ if ( W <_ Y , Y , W ) )
67 66 11 breqtrrdi 
 |-  ( ph -> W <_ X )
68 67 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ j <_ N ) -> W <_ X )
69 46 47 48 64 68 letrd 
 |-  ( ( ( ph /\ j e. Z ) /\ j <_ N ) -> ( F ` j ) <_ X )
70 7 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ -. j <_ N ) -> K e. RR )
71 uzssre 
 |-  ( ZZ>= ` M ) C_ RR
72 4 71 eqsstri 
 |-  Z C_ RR
73 72 sseli 
 |-  ( j e. Z -> j e. RR )
74 73 ad2antlr 
 |-  ( ( ( ph /\ j e. Z ) /\ -. j <_ N ) -> j e. RR )
75 71 28 sselid 
 |-  ( ph -> N e. RR )
76 75 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ -. j <_ N ) -> N e. RR )
77 ceilge 
 |-  ( K e. RR -> K <_ ( |^ ` K ) )
78 7 77 syl 
 |-  ( ph -> K <_ ( |^ ` K ) )
79 max1 
 |-  ( ( ( |^ ` K ) e. RR /\ M e. RR ) -> ( |^ ` K ) <_ if ( ( |^ ` K ) <_ M , M , ( |^ ` K ) ) )
80 22 23 79 syl2anc 
 |-  ( ph -> ( |^ ` K ) <_ if ( ( |^ ` K ) <_ M , M , ( |^ ` K ) ) )
81 80 26 breqtrd 
 |-  ( ph -> ( |^ ` K ) <_ N )
82 7 22 75 78 81 letrd 
 |-  ( ph -> K <_ N )
83 82 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ -. j <_ N ) -> K <_ N )
84 simpr 
 |-  ( ( ( ph /\ j e. Z ) /\ -. j <_ N ) -> -. j <_ N )
85 76 74 ltnled 
 |-  ( ( ( ph /\ j e. Z ) /\ -. j <_ N ) -> ( N < j <-> -. j <_ N ) )
86 84 85 mpbird 
 |-  ( ( ( ph /\ j e. Z ) /\ -. j <_ N ) -> N < j )
87 70 76 74 83 86 lelttrd 
 |-  ( ( ( ph /\ j e. Z ) /\ -. j <_ N ) -> K < j )
88 70 74 87 ltled 
 |-  ( ( ( ph /\ j e. Z ) /\ -. j <_ N ) -> K <_ j )
89 45 adantr 
 |-  ( ( ( ph /\ j e. Z ) /\ K <_ j ) -> ( F ` j ) e. RR )
90 6 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ K <_ j ) -> Y e. RR )
91 44 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ K <_ j ) -> X e. RR )
92 simpr 
 |-  ( ( ( ph /\ j e. Z ) /\ K <_ j ) -> K <_ j )
93 8 r19.21bi 
 |-  ( ( ph /\ j e. Z ) -> ( K <_ j -> ( F ` j ) <_ Y ) )
94 93 adantr 
 |-  ( ( ( ph /\ j e. Z ) /\ K <_ j ) -> ( K <_ j -> ( F ` j ) <_ Y ) )
95 92 94 mpd 
 |-  ( ( ( ph /\ j e. Z ) /\ K <_ j ) -> ( F ` j ) <_ Y )
96 max2 
 |-  ( ( W e. RR /\ Y e. RR ) -> Y <_ if ( W <_ Y , Y , W ) )
97 42 6 96 syl2anc 
 |-  ( ph -> Y <_ if ( W <_ Y , Y , W ) )
98 97 11 breqtrrdi 
 |-  ( ph -> Y <_ X )
99 98 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ K <_ j ) -> Y <_ X )
100 89 90 91 95 99 letrd 
 |-  ( ( ( ph /\ j e. Z ) /\ K <_ j ) -> ( F ` j ) <_ X )
101 88 100 syldan 
 |-  ( ( ( ph /\ j e. Z ) /\ -. j <_ N ) -> ( F ` j ) <_ X )
102 69 101 pm2.61dan 
 |-  ( ( ph /\ j e. Z ) -> ( F ` j ) <_ X )
103 102 ex 
 |-  ( ph -> ( j e. Z -> ( F ` j ) <_ X ) )
104 1 103 ralrimi 
 |-  ( ph -> A. j e. Z ( F ` j ) <_ X )
105 nfv 
 |-  F/ x A. j e. Z ( F ` j ) <_ X
106 nfcv 
 |-  F/_ j x
107 106 2 nfeq 
 |-  F/ j x = X
108 breq2 
 |-  ( x = X -> ( ( F ` j ) <_ x <-> ( F ` j ) <_ X ) )
109 107 108 ralbid 
 |-  ( x = X -> ( A. j e. Z ( F ` j ) <_ x <-> A. j e. Z ( F ` j ) <_ X ) )
110 105 109 rspce 
 |-  ( ( X e. RR /\ A. j e. Z ( F ` j ) <_ X ) -> E. x e. RR A. j e. Z ( F ` j ) <_ x )
111 44 104 110 syl2anc 
 |-  ( ph -> E. x e. RR A. j e. Z ( F ` j ) <_ x )