limsupub2

Description: A extended real valued function, with limsup that is not +oo , is eventually less than +oo . (Contributed by Glauco Siliprandi, 23-Apr-2023)

	Ref	Expression
Hypotheses	limsupub2.1	$⊢ Ⅎ j φ$
	limsupub2.2	$⊢ \underline{Ⅎ} j F$
	limsupub2.3	$⊢ φ \to A \subseteq ℝ$
	limsupub2.4	$⊢ φ \to F : A ⟶ ℝ^{*}$
	limsupub2.5	$⊢ φ \to lim sup (F) \neq +∞$
Assertion	limsupub2	$⊢ φ \to \exists k \in ℝ \forall j \in A (k \leq j \to F (j) < +∞)$

Proof

Step	Hyp	Ref	Expression
1		limsupub2.1	$⊢ Ⅎ j φ$
2		limsupub2.2	$⊢ \underline{Ⅎ} j F$
3		limsupub2.3	$⊢ φ \to A \subseteq ℝ$
4		limsupub2.4	$⊢ φ \to F : A ⟶ ℝ^{*}$
5		limsupub2.5	$⊢ φ \to lim sup (F) \neq +∞$
6		nfv	$⊢ Ⅎ j x \in ℝ$
7	1 6	nfan	$⊢ Ⅎ j (φ \land x \in ℝ)$
8		nfv	$⊢ Ⅎ j k \in ℝ$
9	7 8	nfan	$⊢ Ⅎ j ((φ \land x \in ℝ) \land k \in ℝ)$
10	4	ffvelcdmda	$⊢ (φ \land j \in A) \to F (j) \in ℝ^{*}$
11	10	ad5ant14	$⊢ ((((φ \land x \in ℝ) \land k \in ℝ) \land j \in A) \land F (j) \leq x) \to F (j) \in ℝ^{*}$
12		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
13	12	ad4antlr	$⊢ ((((φ \land x \in ℝ) \land k \in ℝ) \land j \in A) \land F (j) \leq x) \to x \in ℝ^{*}$
14		pnfxr	$⊢ +∞ \in ℝ^{*}$
15	14	a1i	$⊢ ((((φ \land x \in ℝ) \land k \in ℝ) \land j \in A) \land F (j) \leq x) \to +∞ \in ℝ^{*}$
16		simpr	$⊢ ((((φ \land x \in ℝ) \land k \in ℝ) \land j \in A) \land F (j) \leq x) \to F (j) \leq x$
17		ltpnf	$⊢ x \in ℝ \to x < +∞$
18	17	ad4antlr	$⊢ ((((φ \land x \in ℝ) \land k \in ℝ) \land j \in A) \land F (j) \leq x) \to x < +∞$
19	11 13 15 16 18	xrlelttrd	$⊢ ((((φ \land x \in ℝ) \land k \in ℝ) \land j \in A) \land F (j) \leq x) \to F (j) < +∞$
20	19	ex	$⊢ (((φ \land x \in ℝ) \land k \in ℝ) \land j \in A) \to (F (j) \leq x \to F (j) < +∞)$
21	20	imim2d	$⊢ (((φ \land x \in ℝ) \land k \in ℝ) \land j \in A) \to ((k \leq j \to F (j) \leq x) \to (k \leq j \to F (j) < +∞))$
22	9 21	ralimdaa	$⊢ ((φ \land x \in ℝ) \land k \in ℝ) \to (\forall j \in A (k \leq j \to F (j) \leq x) \to \forall j \in A (k \leq j \to F (j) < +∞))$
23	22	reximdva	$⊢ (φ \land x \in ℝ) \to (\exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x) \to \exists k \in ℝ \forall j \in A (k \leq j \to F (j) < +∞))$
24	23	imp	$⊢ ((φ \land x \in ℝ) \land \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x)) \to \exists k \in ℝ \forall j \in A (k \leq j \to F (j) < +∞)$
25	1 2 3 4 5	limsupub	$⊢ φ \to \exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x)$
26	24 25	r19.29a	$⊢ φ \to \exists k \in ℝ \forall j \in A (k \leq j \to F (j) < +∞)$

Metamath Proof Explorer

Theorem limsupub2

Proof