limsuppnflem

Description: If the restriction of a function to every upper interval is unbounded above, its limsup is +oo . (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsuppnflem.j	$⊢ \underline{Ⅎ} j F$
	limsuppnflem.a	$⊢ φ \to A \subseteq ℝ$
	limsuppnflem.f	$⊢ φ \to F : A ⟶ ℝ^{*}$
Assertion	limsuppnflem	$⊢ φ \to (lim sup (F) = +∞ \leftrightarrow \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j)))$

Proof

Step	Hyp	Ref	Expression
1		limsuppnflem.j	$⊢ \underline{Ⅎ} j F$
2		limsuppnflem.a	$⊢ φ \to A \subseteq ℝ$
3		limsuppnflem.f	$⊢ φ \to F : A ⟶ ℝ^{*}$
4		id	$⊢ φ \to φ$
5		imnan	$⊢ (k \leq j \to \neg x \leq F (j)) \leftrightarrow \neg (k \leq j \land x \leq F (j))$
6	5	ralbii	$⊢ \forall j \in A (k \leq j \to \neg x \leq F (j)) \leftrightarrow \forall j \in A \neg (k \leq j \land x \leq F (j))$
7		ralnex	$⊢ \forall j \in A \neg (k \leq j \land x \leq F (j)) \leftrightarrow \neg \exists j \in A (k \leq j \land x \leq F (j))$
8	6 7	bitri	$⊢ \forall j \in A (k \leq j \to \neg x \leq F (j)) \leftrightarrow \neg \exists j \in A (k \leq j \land x \leq F (j))$
9	8	rexbii	$⊢ \exists k \in ℝ \forall j \in A (k \leq j \to \neg x \leq F (j)) \leftrightarrow \exists k \in ℝ \neg \exists j \in A (k \leq j \land x \leq F (j))$
10		rexnal	$⊢ \exists k \in ℝ \neg \exists j \in A (k \leq j \land x \leq F (j)) \leftrightarrow \neg \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))$
11	9 10	bitri	$⊢ \exists k \in ℝ \forall j \in A (k \leq j \to \neg x \leq F (j)) \leftrightarrow \neg \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))$
12	11	rexbii	$⊢ \exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to \neg x \leq F (j)) \leftrightarrow \exists x \in ℝ \neg \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))$
13		rexnal	$⊢ \exists x \in ℝ \neg \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j)) \leftrightarrow \neg \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))$
14	12 13	bitri	$⊢ \exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to \neg x \leq F (j)) \leftrightarrow \neg \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))$
15	14	biimpri	$⊢ \neg \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j)) \to \exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to \neg x \leq F (j))$
16		simp1	$⊢ ((((φ \land x \in ℝ) \land k \in ℝ) \land j \in A) \land (k \leq j \to \neg x \leq F (j)) \land k \leq j) \to (((φ \land x \in ℝ) \land k \in ℝ) \land j \in A)$
17		id	$⊢ (k \leq j \to \neg x \leq F (j)) \to (k \leq j \to \neg x \leq F (j))$
18	17	imp	$⊢ ((k \leq j \to \neg x \leq F (j)) \land k \leq j) \to \neg x \leq F (j)$
19	18	3adant1	$⊢ ((((φ \land x \in ℝ) \land k \in ℝ) \land j \in A) \land (k \leq j \to \neg x \leq F (j)) \land k \leq j) \to \neg x \leq F (j)$
20	3	ffvelcdmda	$⊢ (φ \land j \in A) \to F (j) \in ℝ^{*}$
21	20	ad4ant14	$⊢ (((φ \land x \in ℝ) \land k \in ℝ) \land j \in A) \to F (j) \in ℝ^{*}$
22	21	adantr	$⊢ ((((φ \land x \in ℝ) \land k \in ℝ) \land j \in A) \land \neg x \leq F (j)) \to F (j) \in ℝ^{*}$
23		simpllr	$⊢ (((φ \land x \in ℝ) \land k \in ℝ) \land j \in A) \to x \in ℝ$
24		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
25	23 24	syl	$⊢ (((φ \land x \in ℝ) \land k \in ℝ) \land j \in A) \to x \in ℝ^{*}$
26	25	adantr	$⊢ ((((φ \land x \in ℝ) \land k \in ℝ) \land j \in A) \land \neg x \leq F (j)) \to x \in ℝ^{*}$
27		simpr	$⊢ (((φ \land x \in ℝ) \land j \in A) \land \neg x \leq F (j)) \to \neg x \leq F (j)$
28	20	ad4ant13	$⊢ (((φ \land x \in ℝ) \land j \in A) \land \neg x \leq F (j)) \to F (j) \in ℝ^{*}$
29	24	ad3antlr	$⊢ (((φ \land x \in ℝ) \land j \in A) \land \neg x \leq F (j)) \to x \in ℝ^{*}$
30	28 29	xrltnled	$⊢ (((φ \land x \in ℝ) \land j \in A) \land \neg x \leq F (j)) \to (F (j) < x \leftrightarrow \neg x \leq F (j))$
31	27 30	mpbird	$⊢ (((φ \land x \in ℝ) \land j \in A) \land \neg x \leq F (j)) \to F (j) < x$
32	31	adantllr	$⊢ ((((φ \land x \in ℝ) \land k \in ℝ) \land j \in A) \land \neg x \leq F (j)) \to F (j) < x$
33	22 26 32	xrltled	$⊢ ((((φ \land x \in ℝ) \land k \in ℝ) \land j \in A) \land \neg x \leq F (j)) \to F (j) \leq x$
34	16 19 33	syl2anc	$⊢ ((((φ \land x \in ℝ) \land k \in ℝ) \land j \in A) \land (k \leq j \to \neg x \leq F (j)) \land k \leq j) \to F (j) \leq x$
35	34	3exp	$⊢ (((φ \land x \in ℝ) \land k \in ℝ) \land j \in A) \to ((k \leq j \to \neg x \leq F (j)) \to (k \leq j \to F (j) \leq x))$
36	35	ralimdva	$⊢ ((φ \land x \in ℝ) \land k \in ℝ) \to (\forall j \in A (k \leq j \to \neg x \leq F (j)) \to \forall j \in A (k \leq j \to F (j) \leq x))$
37	36	reximdva	$⊢ (φ \land x \in ℝ) \to (\exists k \in ℝ \forall j \in A (k \leq j \to \neg x \leq F (j)) \to \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x))$
38	37	reximdva	$⊢ φ \to (\exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to \neg x \leq F (j)) \to \exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x))$
39	38	imp	$⊢ (φ \land \exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to \neg x \leq F (j))) \to \exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x)$
40	4 15 39	syl2an	$⊢ (φ \land \neg \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))) \to \exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x)$
41		reex	$⊢ ℝ \in V$
42	41	a1i	$⊢ φ \to ℝ \in V$
43	42 2	ssexd	$⊢ φ \to A \in V$
44	3 43	fexd	$⊢ φ \to F \in V$
45	44	limsupcld	$⊢ φ \to lim sup (F) \in ℝ^{*}$
46	45	ad2antrr	$⊢ ((φ \land x \in ℝ) \land \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x)) \to lim sup (F) \in ℝ^{*}$
47	24	ad2antlr	$⊢ ((φ \land x \in ℝ) \land \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x)) \to x \in ℝ^{*}$
48		pnfxr	$⊢ +∞ \in ℝ^{*}$
49	48	a1i	$⊢ ((φ \land x \in ℝ) \land \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x)) \to +∞ \in ℝ^{*}$
50	2	ad2antrr	$⊢ ((φ \land x \in ℝ) \land \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x)) \to A \subseteq ℝ$
51	3	ad2antrr	$⊢ ((φ \land x \in ℝ) \land \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x)) \to F : A ⟶ ℝ^{*}$
52		simpr	$⊢ ((φ \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) \leq x)$
53	1 50 51 47 52	limsupbnd1f	$⊢ ((φ \land x \in ℝ) \land \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x)) \to lim sup (F) \leq x$
54		ltpnf	$⊢ x \in ℝ \to x < +∞$
55	54	ad2antlr	$⊢ ((φ \land x \in ℝ) \land \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x)) \to x < +∞$
56	46 47 49 53 55	xrlelttrd	$⊢ ((φ \land x \in ℝ) \land \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x)) \to lim sup (F) < +∞$
57	56	rexlimdva2	$⊢ φ \to (\exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x) \to lim sup (F) < +∞)$
58	57	imp	$⊢ (φ \land \exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x)) \to lim sup (F) < +∞$
59	40 58	syldan	$⊢ (φ \land \neg \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))) \to lim sup (F) < +∞$
60	59	adantlr	$⊢ ((φ \land lim sup (F) = +∞) \land \neg \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))) \to lim sup (F) < +∞$
61		id	$⊢ lim sup (F) = +∞ \to lim sup (F) = +∞$
62	48	a1i	$⊢ lim sup (F) = +∞ \to +∞ \in ℝ^{*}$
63	61 62	eqeltrd	$⊢ lim sup (F) = +∞ \to lim sup (F) \in ℝ^{*}$
64	63 61	xreqnltd	$⊢ lim sup (F) = +∞ \to \neg lim sup (F) < +∞$
65	64	adantl	$⊢ (φ \land lim sup (F) = +∞) \to \neg lim sup (F) < +∞$
66	65	adantr	$⊢ ((φ \land lim sup (F) = +∞) \land \neg \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))) \to \neg lim sup (F) < +∞$
67	60 66	condan	$⊢ (φ \land lim sup (F) = +∞) \to \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))$
68	67	ex	$⊢ φ \to (lim sup (F) = +∞ \to \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j)))$
69	2	adantr	$⊢ (φ \land \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))) \to A \subseteq ℝ$
70	3	adantr	$⊢ (φ \land \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))) \to F : A ⟶ ℝ^{*}$
71		simpr	$⊢ (φ \land \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))) \to \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))$
72	1 69 70 71	limsuppnfd	$⊢ (φ \land \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))) \to lim sup (F) = +∞$
73	72	ex	$⊢ φ \to (\forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j)) \to lim sup (F) = +∞)$
74	68 73	impbid	$⊢ φ \to (lim sup (F) = +∞ \leftrightarrow \forall x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j)))$

Metamath Proof Explorer

Theorem limsuppnflem

Proof