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	$⊢ Ⅎ j φ$
	limsupub.e	$⊢ \underline{Ⅎ} j F$
	limsupub.a	$⊢ φ \to A \subseteq ℝ$
	limsupub.f	$⊢ φ \to F : A ⟶ ℝ^{*}$
	limsupub.n	$⊢ φ \to lim sup (F) \neq +∞$
Assertion	limsupub	$⊢ φ \to \exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x)$

Proof

Step	Hyp	Ref	Expression
1		limsupub.j	$⊢ Ⅎ j φ$
2		limsupub.e	$⊢ \underline{Ⅎ} j F$
3		limsupub.a	$⊢ φ \to A \subseteq ℝ$
4		limsupub.f	$⊢ φ \to F : A ⟶ ℝ^{*}$
5		limsupub.n	$⊢ φ \to lim sup (F) \neq +∞$
6	3	adantr	$⊢ (φ \land \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x < F (j))) \to A \subseteq ℝ$
7	4	adantr	$⊢ (φ \land \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x < F (j))) \to F : A ⟶ ℝ^{*}$
8		nfv	$⊢ Ⅎ j x \in ℝ$
9	1 8	nfan	$⊢ Ⅎ j (φ \land x \in ℝ)$
10		simprl	$⊢ (((φ \land x \in ℝ) \land j \in A) \land (k \leq j \land x < F (j))) \to k \leq j$
11		simpllr	$⊢ (((φ \land x \in ℝ) \land j \in A) \land x < F (j)) \to x \in ℝ$
12		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
13	11 12	syl	$⊢ (((φ \land x \in ℝ) \land j \in A) \land x < F (j)) \to x \in ℝ^{*}$
14	4	ffvelcdmda	$⊢ (φ \land j \in A) \to F (j) \in ℝ^{*}$
15	14	ad4ant13	$⊢ (((φ \land x \in ℝ) \land j \in A) \land x < F (j)) \to F (j) \in ℝ^{*}$
16		simpr	$⊢ (((φ \land x \in ℝ) \land j \in A) \land x < F (j)) \to x < F (j)$
17	13 15 16	xrltled	$⊢ (((φ \land x \in ℝ) \land j \in A) \land x < F (j)) \to x \leq F (j)$
18	17	adantrl	$⊢ (((φ \land x \in ℝ) \land j \in A) \land (k \leq j \land x < F (j))) \to x \leq F (j)$
19	10 18	jca	$⊢ (((φ \land x \in ℝ) \land j \in A) \land (k \leq j \land x < F (j))) \to (k \leq j \land x \leq F (j))$
20	19	ex	$⊢ ((φ \land x \in ℝ) \land j \in A) \to ((k \leq j \land x < F (j)) \to (k \leq j \land x \leq F (j)))$
21	20	ex	$⊢ (φ \land x \in ℝ) \to (j \in A \to ((k \leq j \land x < F (j)) \to (k \leq j \land x \leq F (j))))$
22	9 21	reximdai	$⊢ (φ \land x \in ℝ) \to (\exists j \in A (k \leq j \land x < F (j)) \to \exists j \in A (k \leq j \land x \leq F (j)))$
23	22	ralimdv	$⊢ (φ \land x \in ℝ) \to (\forall k \in ℝ \exists j \in A (k \leq j \land x < F (j)) \to \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j)))$
24	23	ralimdva	$⊢ φ \to (\forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x < F (j)) \to \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j)))$
25	24	imp	$⊢ (φ \land \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x < F (j))) \to \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))$
26	2 6 7 25	limsuppnfd	$⊢ (φ \land \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x < F (j))) \to lim sup (F) = +∞$
27	5	neneqd	$⊢ φ \to \neg lim sup (F) = +∞$
28	27	adantr	$⊢ (φ \land \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x < F (j))) \to \neg lim sup (F) = +∞$
29	26 28	pm2.65da	$⊢ φ \to \neg \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x < F (j))$
30		imnan	$⊢ (k \leq j \to \neg x < F (j)) \leftrightarrow \neg (k \leq j \land x < F (j))$
31	30	ralbii	$⊢ \forall j \in A (k \leq j \to \neg x < F (j)) \leftrightarrow \forall j \in A \neg (k \leq j \land x < F (j))$
32		ralnex	$⊢ \forall j \in A \neg (k \leq j \land x < F (j)) \leftrightarrow \neg \exists j \in A (k \leq j \land x < F (j))$
33	31 32	bitri	$⊢ \forall j \in A (k \leq j \to \neg x < F (j)) \leftrightarrow \neg \exists j \in A (k \leq j \land x < F (j))$
34	33	rexbii	$⊢ \exists k \in ℝ \forall j \in A (k \leq j \to \neg x < F (j)) \leftrightarrow \exists k \in ℝ \neg \exists j \in A (k \leq j \land x < F (j))$
35		rexnal	$⊢ \exists k \in ℝ \neg \exists j \in A (k \leq j \land x < F (j)) \leftrightarrow \neg \forall k \in ℝ \exists j \in A (k \leq j \land x < F (j))$
36	34 35	bitri	$⊢ \exists k \in ℝ \forall j \in A (k \leq j \to \neg x < F (j)) \leftrightarrow \neg \forall k \in ℝ \exists j \in A (k \leq j \land x < F (j))$
37	36	rexbii	$⊢ \exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to \neg x < F (j)) \leftrightarrow \exists x \in ℝ \neg \forall k \in ℝ \exists j \in A (k \leq j \land x < F (j))$
38		rexnal	$⊢ \exists x \in ℝ \neg \forall k \in ℝ \exists j \in A (k \leq j \land x < F (j)) \leftrightarrow \neg \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x < F (j))$
39	37 38	bitri	$⊢ \exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to \neg x < F (j)) \leftrightarrow \neg \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x < F (j))$
40	29 39	sylibr	$⊢ φ \to \exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to \neg x < F (j))$
41		nfv	$⊢ Ⅎ j k \in ℝ$
42	9 41	nfan	$⊢ Ⅎ j ((φ \land x \in ℝ) \land k \in ℝ)$
43	14	ad4ant14	$⊢ (((φ \land x \in ℝ) \land k \in ℝ) \land j \in A) \to F (j) \in ℝ^{*}$
44		simpllr	$⊢ (((φ \land x \in ℝ) \land k \in ℝ) \land j \in A) \to x \in ℝ$
45	44	rexrd	$⊢ (((φ \land x \in ℝ) \land k \in ℝ) \land j \in A) \to x \in ℝ^{*}$
46	43 45	xrlenltd	$⊢ (((φ \land x \in ℝ) \land k \in ℝ) \land j \in A) \to (F (j) \leq x \leftrightarrow \neg x < F (j))$
47	46	imbi2d	$⊢ (((φ \land x \in ℝ) \land k \in ℝ) \land j \in A) \to ((k \leq j \to F (j) \leq x) \leftrightarrow (k \leq j \to \neg x < F (j)))$
48	42 47	ralbida	$⊢ ((φ \land x \in ℝ) \land k \in ℝ) \to (\forall j \in A (k \leq j \to F (j) \leq x) \leftrightarrow \forall j \in A (k \leq j \to \neg x < F (j)))$
49	48	rexbidva	$⊢ (φ \land x \in ℝ) \to (\exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x) \leftrightarrow \exists k \in ℝ \forall j \in A (k \leq j \to \neg x < F (j)))$
50	49	rexbidva	$⊢ φ \to (\exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x) \leftrightarrow \exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to \neg x < F (j)))$
51	40 50	mpbird	$⊢ φ \to \exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x)$

Metamath Proof Explorer

Theorem limsupub

Proof