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 ⊢ Ⅎ 𝑗 𝜑
limsupubuzlem.e ⊢ Ⅎ 𝑗 𝑋
limsupubuzlem.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
limsupubuzlem.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
limsupubuzlem.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
limsupubuzlem.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
limsupubuzlem.k ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
limsupubuzlem.b ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝑍 ( 𝐾 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑌 ) )
limsupubuzlem.n ⊢ 𝑁 = if ( ( ⌈ ‘ 𝐾 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝐾 ) )
limsupubuzlem.w ⊢ 𝑊 = sup ( ran ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐹 ‘ 𝑗 ) ) , ℝ , < )
limsupubuzlem.x ⊢ 𝑋 = if ( 𝑊 ≤ 𝑌 , 𝑌 , 𝑊 )
Assertion limsupubuzlem ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )

Proof

Step Hyp Ref Expression
1 limsupubuzlem.j ⊢ Ⅎ 𝑗 𝜑
2 limsupubuzlem.e ⊢ Ⅎ 𝑗 𝑋
3 limsupubuzlem.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 limsupubuzlem.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5 limsupubuzlem.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
6 limsupubuzlem.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
7 limsupubuzlem.k ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
8 limsupubuzlem.b ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝑍 ( 𝐾 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑌 ) )
9 limsupubuzlem.n ⊢ 𝑁 = if ( ( ⌈ ‘ 𝐾 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝐾 ) )
10 limsupubuzlem.w ⊢ 𝑊 = sup ( ran ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐹 ‘ 𝑗 ) ) , ℝ , < )
11 limsupubuzlem.x ⊢ 𝑋 = if ( 𝑊 ≤ 𝑌 , 𝑌 , 𝑊 )
12 10 a1i ⊢ ( 𝜑 → 𝑊 = sup ( ran ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐹 ‘ 𝑗 ) ) , ℝ , < ) )
13 ltso ⊢ < Or ℝ
14 13 a1i ⊢ ( 𝜑 → < Or ℝ )
15 fzfid ⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) ∈ Fin )
16 eqid ⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 )
17 9 a1i ⊢ ( 𝜑 → 𝑁 = if ( ( ⌈ ‘ 𝐾 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝐾 ) ) )
18 ceilcl ⊢ ( 𝐾 ∈ ℝ → ( ⌈ ‘ 𝐾 ) ∈ ℤ )
19 7 18 syl ⊢ ( 𝜑 → ( ⌈ ‘ 𝐾 ) ∈ ℤ )
20 3 19 ifcld ⊢ ( 𝜑 → if ( ( ⌈ ‘ 𝐾 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝐾 ) ) ∈ ℤ )
21 17 20 eqeltrd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
22 19 zred ⊢ ( 𝜑 → ( ⌈ ‘ 𝐾 ) ∈ ℝ )
23 3 zred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
24 max2 ⊢ ( ( ( ⌈ ‘ 𝐾 ) ∈ ℝ ∧ 𝑀 ∈ ℝ ) → 𝑀 ≤ if ( ( ⌈ ‘ 𝐾 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝐾 ) ) )
25 22 23 24 syl2anc ⊢ ( 𝜑 → 𝑀 ≤ if ( ( ⌈ ‘ 𝐾 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝐾 ) ) )
26 17 eqcomd ⊢ ( 𝜑 → if ( ( ⌈ ‘ 𝐾 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝐾 ) ) = 𝑁 )
27 25 26 breqtrd ⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
28 16 3 21 27 eluzd ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
29 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
30 28 29 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
31 30 ne0d ⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) ≠ ∅ )
32 5 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐹 : 𝑍 ⟶ ℝ )
33 3 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ∈ ℤ )
34 elfzelz ⊢ ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) → 𝑗 ∈ ℤ )
35 34 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑗 ∈ ℤ )
36 elfzle1 ⊢ ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) → 𝑀 ≤ 𝑗 )
37 36 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ≤ 𝑗 )
38 16 33 35 37 eluzd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
39 38 4 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑗 ∈ 𝑍 )
40 32 39 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
41 1 14 15 31 40 fisupclrnmpt ⊢ ( 𝜑 → sup ( ran ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐹 ‘ 𝑗 ) ) , ℝ , < ) ∈ ℝ )
42 12 41 eqeltrd ⊢ ( 𝜑 → 𝑊 ∈ ℝ )
43 6 42 ifcld ⊢ ( 𝜑 → if ( 𝑊 ≤ 𝑌 , 𝑌 , 𝑊 ) ∈ ℝ )
44 11 43 eqeltrid ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
45 5 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
46 45 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑗 ≤ 𝑁 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
47 42 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑗 ≤ 𝑁 ) → 𝑊 ∈ ℝ )
48 44 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑗 ≤ 𝑁 ) → 𝑋 ∈ ℝ )
49 simpll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑗 ≤ 𝑁 ) → 𝜑 )
50 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑗 ≤ 𝑁 ) → 𝑀 ∈ ℤ )
51 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑗 ≤ 𝑁 ) → 𝑁 ∈ ℤ )
52 4 eluzelz2 ⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ )
53 52 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑗 ≤ 𝑁 ) → 𝑗 ∈ ℤ )
54 4 eleq2i ⊢ ( 𝑗 ∈ 𝑍 ↔ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
55 54 biimpi ⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
56 eluzle ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ 𝑗 )
57 55 56 syl ⊢ ( 𝑗 ∈ 𝑍 → 𝑀 ≤ 𝑗 )
58 57 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑗 ≤ 𝑁 ) → 𝑀 ≤ 𝑗 )
59 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑗 ≤ 𝑁 ) → 𝑗 ≤ 𝑁 )
60 50 51 53 58 59 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑗 ≤ 𝑁 ) → 𝑗 ∈ ( 𝑀 ... 𝑁 ) )
61 1 15 40 fimaxre4 ⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ ∀ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑏 )
62 1 40 61 suprubrnmpt ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑗 ) ≤ sup ( ran ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐹 ‘ 𝑗 ) ) , ℝ , < ) )
63 62 10 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑊 )
64 49 60 63 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑗 ≤ 𝑁 ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑊 )
65 max1 ⊢ ( ( 𝑊 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → 𝑊 ≤ if ( 𝑊 ≤ 𝑌 , 𝑌 , 𝑊 ) )
66 42 6 65 syl2anc ⊢ ( 𝜑 → 𝑊 ≤ if ( 𝑊 ≤ 𝑌 , 𝑌 , 𝑊 ) )
67 66 11 breqtrrdi ⊢ ( 𝜑 → 𝑊 ≤ 𝑋 )
68 67 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑗 ≤ 𝑁 ) → 𝑊 ≤ 𝑋 )
69 46 47 48 64 68 letrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑗 ≤ 𝑁 ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑋 )
70 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ¬ 𝑗 ≤ 𝑁 ) → 𝐾 ∈ ℝ )
71 uzssre ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℝ
72 4 71 eqsstri ⊢ 𝑍 ⊆ ℝ
73 72 sseli ⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ℝ )
74 73 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ¬ 𝑗 ≤ 𝑁 ) → 𝑗 ∈ ℝ )
75 71 28 sseldi ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
76 75 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ¬ 𝑗 ≤ 𝑁 ) → 𝑁 ∈ ℝ )
77 ceilge ⊢ ( 𝐾 ∈ ℝ → 𝐾 ≤ ( ⌈ ‘ 𝐾 ) )
78 7 77 syl ⊢ ( 𝜑 → 𝐾 ≤ ( ⌈ ‘ 𝐾 ) )
79 max1 ⊢ ( ( ( ⌈ ‘ 𝐾 ) ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( ⌈ ‘ 𝐾 ) ≤ if ( ( ⌈ ‘ 𝐾 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝐾 ) ) )
80 22 23 79 syl2anc ⊢ ( 𝜑 → ( ⌈ ‘ 𝐾 ) ≤ if ( ( ⌈ ‘ 𝐾 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝐾 ) ) )
81 80 26 breqtrd ⊢ ( 𝜑 → ( ⌈ ‘ 𝐾 ) ≤ 𝑁 )
82 7 22 75 78 81 letrd ⊢ ( 𝜑 → 𝐾 ≤ 𝑁 )
83 82 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ¬ 𝑗 ≤ 𝑁 ) → 𝐾 ≤ 𝑁 )
84 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ¬ 𝑗 ≤ 𝑁 ) → ¬ 𝑗 ≤ 𝑁 )
85 76 74 ltnled ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ¬ 𝑗 ≤ 𝑁 ) → ( 𝑁 < 𝑗 ↔ ¬ 𝑗 ≤ 𝑁 ) )
86 84 85 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ¬ 𝑗 ≤ 𝑁 ) → 𝑁 < 𝑗 )
87 70 76 74 83 86 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ¬ 𝑗 ≤ 𝑁 ) → 𝐾 < 𝑗 )
88 70 74 87 ltled ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ¬ 𝑗 ≤ 𝑁 ) → 𝐾 ≤ 𝑗 )
89 45 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝐾 ≤ 𝑗 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
90 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝐾 ≤ 𝑗 ) → 𝑌 ∈ ℝ )
91 44 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝐾 ≤ 𝑗 ) → 𝑋 ∈ ℝ )
92 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝐾 ≤ 𝑗 ) → 𝐾 ≤ 𝑗 )
93 8 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐾 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑌 ) )
94 93 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝐾 ≤ 𝑗 ) → ( 𝐾 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑌 ) )
95 92 94 mpd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝐾 ≤ 𝑗 ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑌 )
96 max2 ⊢ ( ( 𝑊 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → 𝑌 ≤ if ( 𝑊 ≤ 𝑌 , 𝑌 , 𝑊 ) )
97 42 6 96 syl2anc ⊢ ( 𝜑 → 𝑌 ≤ if ( 𝑊 ≤ 𝑌 , 𝑌 , 𝑊 ) )
98 97 11 breqtrrdi ⊢ ( 𝜑 → 𝑌 ≤ 𝑋 )
99 98 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝐾 ≤ 𝑗 ) → 𝑌 ≤ 𝑋 )
100 89 90 91 95 99 letrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝐾 ≤ 𝑗 ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑋 )
101 88 100 syldan ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ¬ 𝑗 ≤ 𝑁 ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑋 )
102 69 101 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝑋 )
103 102 ex ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑍 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑋 ) )
104 1 103 ralrimi ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑋 )
105 nfv ⊢ Ⅎ 𝑥 ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑋
106 nfcv ⊢ Ⅎ 𝑗 𝑥
107 106 2 nfeq ⊢ Ⅎ 𝑗 𝑥 = 𝑋
108 breq2 ⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑗 ) ≤ 𝑋 ) )
109 107 108 ralbid ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑋 ) )
110 105 109 rspce ⊢ ( ( 𝑋 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑋 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
111 44 104 110 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )