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 ⊢ Ⅎ 𝑗 𝐹
limsupubuz.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
limsupubuz.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
limsupubuz.n ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ≠ +∞ )
Assertion limsupubuz ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )

Proof

Step Hyp Ref Expression
1 limsupubuz.j ⊢ Ⅎ 𝑗 𝐹
2 limsupubuz.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 limsupubuz.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
4 limsupubuz.n ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ≠ +∞ )
5 nfv ⊢ Ⅎ 𝑙 𝜑
6 nfcv ⊢ Ⅎ 𝑙 𝐹
7 uzssre ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℝ
8 2 7 eqsstri ⊢ 𝑍 ⊆ ℝ
9 8 a1i ⊢ ( 𝜑 → 𝑍 ⊆ ℝ )
10 3 frexr ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
11 5 6 9 10 4 limsupub ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) )
13 nfv ⊢ Ⅎ 𝑙 𝑀 ∈ ℤ
14 5 13 nfan ⊢ Ⅎ 𝑙 ( 𝜑 ∧ 𝑀 ∈ ℤ )
15 nfv ⊢ Ⅎ 𝑙 𝑦 ∈ ℝ
16 14 15 nfan ⊢ Ⅎ 𝑙 ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ )
17 nfv ⊢ Ⅎ 𝑙 𝑘 ∈ ℝ
18 16 17 nfan ⊢ Ⅎ 𝑙 ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ )
19 nfra1 ⊢ Ⅎ 𝑙 ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 )
20 18 19 nfan ⊢ Ⅎ 𝑙 ( ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) )
21 nfmpt1 ⊢ Ⅎ 𝑙 ( 𝑙 ∈ ( 𝑀 ... if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) ) ↦ ( 𝐹 ‘ 𝑙 ) )
22 21 nfrn ⊢ Ⅎ 𝑙 ran ( 𝑙 ∈ ( 𝑀 ... if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) ) ↦ ( 𝐹 ‘ 𝑙 ) )
23 nfcv ⊢ Ⅎ 𝑙 ℝ
24 nfcv ⊢ Ⅎ 𝑙 <
25 22 23 24 nfsup ⊢ Ⅎ 𝑙 sup ( ran ( 𝑙 ∈ ( 𝑀 ... if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) ) ↦ ( 𝐹 ‘ 𝑙 ) ) , ℝ , < )
26 nfcv ⊢ Ⅎ 𝑙 ≤
27 nfcv ⊢ Ⅎ 𝑙 𝑦
28 25 26 27 nfbr ⊢ Ⅎ 𝑙 sup ( ran ( 𝑙 ∈ ( 𝑀 ... if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) ) ↦ ( 𝐹 ‘ 𝑙 ) ) , ℝ , < ) ≤ 𝑦
29 28 27 25 nfif ⊢ Ⅎ 𝑙 if ( sup ( ran ( 𝑙 ∈ ( 𝑀 ... if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) ) ↦ ( 𝐹 ‘ 𝑙 ) ) , ℝ , < ) ≤ 𝑦 , 𝑦 , sup ( ran ( 𝑙 ∈ ( 𝑀 ... if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) ) ↦ ( 𝐹 ‘ 𝑙 ) ) , ℝ , < ) )
30 breq2 ⊢ ( 𝑙 = 𝑖 → ( 𝑘 ≤ 𝑙 ↔ 𝑘 ≤ 𝑖 ) )
31 fveq2 ⊢ ( 𝑙 = 𝑖 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑖 ) )
32 31 breq1d ⊢ ( 𝑙 = 𝑖 → ( ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ( 𝐹 ‘ 𝑖 ) ≤ 𝑦 ) )
33 30 32 imbi12d ⊢ ( 𝑙 = 𝑖 → ( ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ( 𝑘 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ 𝑦 ) ) )
34 33 cbvralvw ⊢ ( ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ∀ 𝑖 ∈ 𝑍 ( 𝑘 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ 𝑦 ) )
35 34 biimpi ⊢ ( ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) → ∀ 𝑖 ∈ 𝑍 ( 𝑘 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ 𝑦 ) )
36 35 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ) → ∀ 𝑖 ∈ 𝑍 ( 𝑘 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ 𝑦 ) )
37 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑖 ∈ 𝑍 ( 𝑘 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ 𝑦 ) ) → 𝑀 ∈ ℤ )
38 36 37 syldan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ) → 𝑀 ∈ ℤ )
39 3 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑖 ∈ 𝑍 ( 𝑘 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ 𝑦 ) ) → 𝐹 : 𝑍 ⟶ ℝ )
40 36 39 syldan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ) → 𝐹 : 𝑍 ⟶ ℝ )
41 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑖 ∈ 𝑍 ( 𝑘 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ 𝑦 ) ) → 𝑦 ∈ ℝ )
42 36 41 syldan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ) → 𝑦 ∈ ℝ )
43 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑖 ∈ 𝑍 ( 𝑘 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ 𝑦 ) ) → 𝑘 ∈ ℝ )
44 36 43 syldan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ) → 𝑘 ∈ ℝ )
45 34 biimpri ⊢ ( ∀ 𝑖 ∈ 𝑍 ( 𝑘 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ 𝑦 ) → ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) )
46 36 45 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ) → ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) )
47 eqid ⊢ if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) = if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) )
48 eqid ⊢ sup ( ran ( 𝑙 ∈ ( 𝑀 ... if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) ) ↦ ( 𝐹 ‘ 𝑙 ) ) , ℝ , < ) = sup ( ran ( 𝑙 ∈ ( 𝑀 ... if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) ) ↦ ( 𝐹 ‘ 𝑙 ) ) , ℝ , < )
49 eqid ⊢ if ( sup ( ran ( 𝑙 ∈ ( 𝑀 ... if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) ) ↦ ( 𝐹 ‘ 𝑙 ) ) , ℝ , < ) ≤ 𝑦 , 𝑦 , sup ( ran ( 𝑙 ∈ ( 𝑀 ... if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) ) ↦ ( 𝐹 ‘ 𝑙 ) ) , ℝ , < ) ) = if ( sup ( ran ( 𝑙 ∈ ( 𝑀 ... if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) ) ↦ ( 𝐹 ‘ 𝑙 ) ) , ℝ , < ) ≤ 𝑦 , 𝑦 , sup ( ran ( 𝑙 ∈ ( 𝑀 ... if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) ) ↦ ( 𝐹 ‘ 𝑙 ) ) , ℝ , < ) )
50 20 29 38 2 40 42 44 46 47 48 49 limsupubuzlem ⊢ ( ( ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 )
51 50 rexlimdva2 ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑘 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
52 51 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ( ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
53 12 52 mpd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 )
54 2 a1i ⊢ ( ¬ 𝑀 ∈ ℤ → 𝑍 = ( ℤ≥ ‘ 𝑀 ) )
55 uz0 ⊢ ( ¬ 𝑀 ∈ ℤ → ( ℤ≥ ‘ 𝑀 ) = ∅ )
56 54 55 eqtrd ⊢ ( ¬ 𝑀 ∈ ℤ → 𝑍 = ∅ )
57 0red ⊢ ( 𝑍 = ∅ → 0 ∈ ℝ )
58 rzal ⊢ ( 𝑍 = ∅ → ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 0 )
59 brralrspcev ⊢ ( ( 0 ∈ ℝ ∧ ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 0 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 )
60 57 58 59 syl2anc ⊢ ( 𝑍 = ∅ → ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 )
61 56 60 syl ⊢ ( ¬ 𝑀 ∈ ℤ → ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 )
62 61 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝑀 ∈ ℤ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 )
63 53 62 pm2.61dan ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 )
64 nfcv ⊢ Ⅎ 𝑗 𝑙
65 1 64 nffv ⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 )
66 nfcv ⊢ Ⅎ 𝑗 ≤
67 nfcv ⊢ Ⅎ 𝑗 𝑥
68 65 66 67 nfbr ⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥
69 nfv ⊢ Ⅎ 𝑙 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥
70 fveq2 ⊢ ( 𝑙 = 𝑗 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑗 ) )
71 70 breq1d ⊢ ( 𝑙 = 𝑗 → ( ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
72 68 69 71 cbvralw ⊢ ( ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
73 72 rexbii ⊢ ( ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
74 63 73 sylib ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )