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 ( 𝜑 → ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗𝐴 ( 𝑘𝑗 → ( 𝐹𝑗 ) ≤ 𝑥 ) )