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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ^* )
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	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )

Metamath Proof Explorer

Theorem limsupub

Proof