Metamath Proof Explorer

Theorem limsupub

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

Ref Expression
Hypotheses limsupub.j ⊢ Ⅎ 𝑗 𝜑
limsupub.e ⊢ Ⅎ 𝑗 𝐹
limsupub.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
limsupub.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
limsupub.n ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ≠ +∞ )
Assertion limsupub ( 𝜑 → ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 limsupub.j ⊢ Ⅎ 𝑗 𝜑
2 limsupub.e ⊢ Ⅎ 𝑗 𝐹
3 limsupub.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
4 limsupub.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
5 limsupub.n ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ≠ +∞ )
6 3 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) → 𝐴 ⊆ ℝ )
7 4 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) → 𝐹 : 𝐴 ⟶ ℝ* )
8 nfv ⊢ Ⅎ 𝑗 𝑥 ∈ ℝ
9 1 8 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑥 ∈ ℝ )
10 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) → 𝑘 ≤ 𝑗 )
11 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) → 𝑥 ∈ ℝ )
12 rexr ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
13 11 12 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) → 𝑥 ∈ ℝ* )
14 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
15 14 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
16 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) → 𝑥 < ( 𝐹 ‘ 𝑗 ) )
17 13 15 16 xrltled ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) → 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
18 17 adantrl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) → 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
19 10 18 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) → ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
20 19 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) → ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
21 20 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑗 ∈ 𝐴 → ( ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) → ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) ) )
22 9 21 reximdai ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) → ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
23 22 ralimdv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) → ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
24 23 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) → ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
25 24 imp ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) → ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
26 2 6 7 25 limsuppnfd ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) → ( lim sup ‘ 𝐹 ) = +∞ )
27 5 neneqd ⊢ ( 𝜑 → ¬ ( lim sup ‘ 𝐹 ) = +∞ )
28 27 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) → ¬ ( lim sup ‘ 𝐹 ) = +∞ )
29 26 28 pm2.65da ⊢ ( 𝜑 → ¬ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) )
30 imnan ⊢ ( ( 𝑘 ≤ 𝑗 → ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) )
31 30 ralbii ⊢ ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ↔ ∀ 𝑗 ∈ 𝐴 ¬ ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) )
32 ralnex ⊢ ( ∀ 𝑗 ∈ 𝐴 ¬ ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) )
33 31 32 bitri ⊢ ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) )
34 33 rexbii ⊢ ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑘 ∈ ℝ ¬ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) )
35 rexnal ⊢ ( ∃ 𝑘 ∈ ℝ ¬ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) )
36 34 35 bitri ⊢ ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) )
37 36 rexbii ⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑥 ∈ ℝ ¬ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) )
38 rexnal ⊢ ( ∃ 𝑥 ∈ ℝ ¬ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) )
39 37 38 bitri ⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) )
40 29 39 sylibr ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) )
41 nfv ⊢ Ⅎ 𝑗 𝑘 ∈ ℝ
42 9 41 nfan ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ )
43 14 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
44 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
45 44 rexrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → 𝑥 ∈ ℝ* )
46 43 45 xrlenltd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) )
47 46 imbi2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ( 𝑘 ≤ 𝑗 → ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) )
48 42 47 ralbida ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) → ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) )
49 48 rexbidva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) )
50 49 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) )
51 40 50 mpbird ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )