limsupre3lem

Description: Given a function on the extended reals, its supremum limit is real if and only if two condition holds: 1. there is a real number that is less than or equal to the function, at some point, in any upper part of the reals; 2. there is a real number that is eventually greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupre3lem.1	$⊢ \underline{Ⅎ} j F$
	limsupre3lem.2	$⊢ φ \to A \subseteq ℝ$
	limsupre3lem.3	$⊢ φ \to F : A ⟶ ℝ^{*}$
Assertion	limsupre3lem	$⊢ φ \to (lim sup (F) \in ℝ \leftrightarrow (\exists x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j)) \land \exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x)))$

Proof

Step	Hyp	Ref	Expression
1		limsupre3lem.1	$⊢ \underline{Ⅎ} j F$
2		limsupre3lem.2	$⊢ φ \to A \subseteq ℝ$
3		limsupre3lem.3	$⊢ φ \to F : A ⟶ ℝ^{*}$
4	1 2 3	limsupre2	$⊢ φ \to (lim sup (F) \in ℝ \leftrightarrow (\exists y \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land y < F (j)) \land \exists y \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) < y)))$
5		simp2	$⊢ (φ \land y \in ℝ \land \forall k \in ℝ \exists j \in A (k \leq j \land y < F (j))) \to y \in ℝ$
6		nfv	$⊢ Ⅎ j (φ \land y \in ℝ)$
7		simp3l	$⊢ ((φ \land y \in ℝ) \land j \in A \land (k \leq j \land y < F (j))) \to k \leq j$
8		simp1r	$⊢ ((φ \land y \in ℝ) \land j \in A \land y < F (j)) \to y \in ℝ$
9	8	rexrd	$⊢ ((φ \land y \in ℝ) \land j \in A \land y < F (j)) \to y \in ℝ^{*}$
10	3	ffvelcdmda	$⊢ (φ \land j \in A) \to F (j) \in ℝ^{*}$
11	10	adantlr	$⊢ ((φ \land y \in ℝ) \land j \in A) \to F (j) \in ℝ^{*}$
12	11	3adant3	$⊢ ((φ \land y \in ℝ) \land j \in A \land y < F (j)) \to F (j) \in ℝ^{*}$
13		simp3	$⊢ ((φ \land y \in ℝ) \land j \in A \land y < F (j)) \to y < F (j)$
14	9 12 13	xrltled	$⊢ ((φ \land y \in ℝ) \land j \in A \land y < F (j)) \to y \leq F (j)$
15	14	3adant3l	$⊢ ((φ \land y \in ℝ) \land j \in A \land (k \leq j \land y < F (j))) \to y \leq F (j)$
16	7 15	jca	$⊢ ((φ \land y \in ℝ) \land j \in A \land (k \leq j \land y < F (j))) \to (k \leq j \land y \leq F (j))$
17	16	3exp	$⊢ (φ \land y \in ℝ) \to (j \in A \to ((k \leq j \land y < F (j)) \to (k \leq j \land y \leq F (j))))$
18	6 17	reximdai	$⊢ (φ \land y \in ℝ) \to (\exists j \in A (k \leq j \land y < F (j)) \to \exists j \in A (k \leq j \land y \leq F (j)))$
19	18	ralimdv	$⊢ (φ \land y \in ℝ) \to (\forall k \in ℝ \exists j \in A (k \leq j \land y < F (j)) \to \forall k \in ℝ \exists j \in A (k \leq j \land y \leq F (j)))$
20	19	3impia	$⊢ (φ \land y \in ℝ \land \forall k \in ℝ \exists j \in A (k \leq j \land y < F (j))) \to \forall k \in ℝ \exists j \in A (k \leq j \land y \leq F (j))$
21		breq1	$⊢ x = y \to (x \leq F (j) \leftrightarrow y \leq F (j))$
22	21	anbi2d	$⊢ x = y \to ((k \leq j \land x \leq F (j)) \leftrightarrow (k \leq j \land y \leq F (j)))$
23	22	rexbidv	$⊢ x = y \to (\exists j \in A (k \leq j \land x \leq F (j)) \leftrightarrow \exists j \in A (k \leq j \land y \leq F (j)))$
24	23	ralbidv	$⊢ x = y \to (\forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j)) \leftrightarrow \forall k \in ℝ \exists j \in A (k \leq j \land y \leq F (j)))$
25	24	rspcev	$⊢ (y \in ℝ \land \forall k \in ℝ \exists j \in A (k \leq j \land y \leq F (j))) \to \exists x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))$
26	5 20 25	syl2anc	$⊢ (φ \land y \in ℝ \land \forall k \in ℝ \exists j \in A (k \leq j \land y < F (j))) \to \exists x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))$
27	26	3exp	$⊢ φ \to (y \in ℝ \to (\forall k \in ℝ \exists j \in A (k \leq j \land y < F (j)) \to \exists x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))))$
28	27	rexlimdv	$⊢ φ \to (\exists y \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land y < F (j)) \to \exists x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j)))$
29		peano2rem	$⊢ x \in ℝ \to x - 1 \in ℝ$
30	29	ad2antlr	$⊢ ((φ \land x \in ℝ) \land \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))) \to x - 1 \in ℝ$
31		nfv	$⊢ Ⅎ j (φ \land x \in ℝ)$
32		simp3l	$⊢ ((φ \land x \in ℝ) \land j \in A \land (k \leq j \land x \leq F (j))) \to k \leq j$
33		simp1r	$⊢ ((φ \land x \in ℝ) \land j \in A \land (k \leq j \land x \leq F (j))) \to x \in ℝ$
34	29	rexrd	$⊢ x \in ℝ \to x - 1 \in ℝ^{*}$
35	33 34	syl	$⊢ ((φ \land x \in ℝ) \land j \in A \land (k \leq j \land x \leq F (j))) \to x - 1 \in ℝ^{*}$
36	33	rexrd	$⊢ ((φ \land x \in ℝ) \land j \in A \land (k \leq j \land x \leq F (j))) \to x \in ℝ^{*}$
37	10	adantlr	$⊢ ((φ \land x \in ℝ) \land j \in A) \to F (j) \in ℝ^{*}$
38	37	3adant3	$⊢ ((φ \land x \in ℝ) \land j \in A \land (k \leq j \land x \leq F (j))) \to F (j) \in ℝ^{*}$
39	33	ltm1d	$⊢ ((φ \land x \in ℝ) \land j \in A \land (k \leq j \land x \leq F (j))) \to x - 1 < x$
40		simp3r	$⊢ ((φ \land x \in ℝ) \land j \in A \land (k \leq j \land x \leq F (j))) \to x \leq F (j)$
41	35 36 38 39 40	xrltletrd	$⊢ ((φ \land x \in ℝ) \land j \in A \land (k \leq j \land x \leq F (j))) \to x - 1 < F (j)$
42	32 41	jca	$⊢ ((φ \land x \in ℝ) \land j \in A \land (k \leq j \land x \leq F (j))) \to (k \leq j \land x - 1 < F (j))$
43	42	3exp	$⊢ (φ \land x \in ℝ) \to (j \in A \to ((k \leq j \land x \leq F (j)) \to (k \leq j \land x - 1 < F (j))))$
44	31 43	reximdai	$⊢ (φ \land x \in ℝ) \to (\exists j \in A (k \leq j \land x \leq F (j)) \to \exists j \in A (k \leq j \land x - 1 < F (j)))$
45	44	ralimdv	$⊢ (φ \land x \in ℝ) \to (\forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j)) \to \forall k \in ℝ \exists j \in A (k \leq j \land x - 1 < F (j)))$
46	45	imp	$⊢ ((φ \land x \in ℝ) \land \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))) \to \forall k \in ℝ \exists j \in A (k \leq j \land x - 1 < F (j))$
47		breq1	$⊢ y = x - 1 \to (y < F (j) \leftrightarrow x - 1 < F (j))$
48	47	anbi2d	$⊢ y = x - 1 \to ((k \leq j \land y < F (j)) \leftrightarrow (k \leq j \land x - 1 < F (j)))$
49	48	rexbidv	$⊢ y = x - 1 \to (\exists j \in A (k \leq j \land y < F (j)) \leftrightarrow \exists j \in A (k \leq j \land x - 1 < F (j)))$
50	49	ralbidv	$⊢ y = x - 1 \to (\forall k \in ℝ \exists j \in A (k \leq j \land y < F (j)) \leftrightarrow \forall k \in ℝ \exists j \in A (k \leq j \land x - 1 < F (j)))$
51	50	rspcev	$⊢ (x - 1 \in ℝ \land \forall k \in ℝ \exists j \in A (k \leq j \land x - 1 < F (j))) \to \exists y \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land y < F (j))$
52	30 46 51	syl2anc	$⊢ ((φ \land x \in ℝ) \land \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j))) \to \exists y \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land y < F (j))$
53	52	rexlimdva2	$⊢ φ \to (\exists x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j)) \to \exists y \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land y < F (j)))$
54	28 53	impbid	$⊢ φ \to (\exists y \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land y < F (j)) \leftrightarrow \exists x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j)))$
55		simplr	$⊢ ((φ \land y \in ℝ) \land \exists k \in ℝ \forall j \in A (k \leq j \to F (j) < y)) \to y \in ℝ$
56	11	adantr	$⊢ (((φ \land y \in ℝ) \land j \in A) \land F (j) < y) \to F (j) \in ℝ^{*}$
57		rexr	$⊢ y \in ℝ \to y \in ℝ^{*}$
58	57	ad3antlr	$⊢ (((φ \land y \in ℝ) \land j \in A) \land F (j) < y) \to y \in ℝ^{*}$
59		simpr	$⊢ (((φ \land y \in ℝ) \land j \in A) \land F (j) < y) \to F (j) < y$
60	56 58 59	xrltled	$⊢ (((φ \land y \in ℝ) \land j \in A) \land F (j) < y) \to F (j) \leq y$
61	60	ex	$⊢ ((φ \land y \in ℝ) \land j \in A) \to (F (j) < y \to F (j) \leq y)$
62	61	imim2d	$⊢ ((φ \land y \in ℝ) \land j \in A) \to ((k \leq j \to F (j) < y) \to (k \leq j \to F (j) \leq y))$
63	62	ralimdva	$⊢ (φ \land y \in ℝ) \to (\forall j \in A (k \leq j \to F (j) < y) \to \forall j \in A (k \leq j \to F (j) \leq y))$
64	63	reximdv	$⊢ (φ \land y \in ℝ) \to (\exists k \in ℝ \forall j \in A (k \leq j \to F (j) < y) \to \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq y))$
65	64	imp	$⊢ ((φ \land y \in ℝ) \land \exists k \in ℝ \forall j \in A (k \leq j \to F (j) < y)) \to \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq y)$
66		breq2	$⊢ x = y \to (F (j) \leq x \leftrightarrow F (j) \leq y)$
67	66	imbi2d	$⊢ x = y \to ((k \leq j \to F (j) \leq x) \leftrightarrow (k \leq j \to F (j) \leq y))$
68	67	ralbidv	$⊢ x = y \to (\forall j \in A (k \leq j \to F (j) \leq x) \leftrightarrow \forall j \in A (k \leq j \to F (j) \leq y))$
69	68	rexbidv	$⊢ x = y \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 F (j) \leq y))$
70	69	rspcev	$⊢ (y \in ℝ \land \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq y)) \to \exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x)$
71	55 65 70	syl2anc	$⊢ ((φ \land y \in ℝ) \land \exists k \in ℝ \forall j \in A (k \leq j \to F (j) < y)) \to \exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x)$
72	71	rexlimdva2	$⊢ φ \to (\exists y \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) < y) \to \exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x))$
73		peano2re	$⊢ x \in ℝ \to x + 1 \in ℝ$
74	73	ad2antlr	$⊢ ((φ \land x \in ℝ) \land \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x)) \to x + 1 \in ℝ$
75	37	adantr	$⊢ (((φ \land x \in ℝ) \land j \in A) \land F (j) \leq x) \to F (j) \in ℝ^{*}$
76		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
77	76	ad3antlr	$⊢ (((φ \land x \in ℝ) \land j \in A) \land F (j) \leq x) \to x \in ℝ^{*}$
78	73	rexrd	$⊢ x \in ℝ \to x + 1 \in ℝ^{*}$
79	78	ad3antlr	$⊢ (((φ \land x \in ℝ) \land j \in A) \land F (j) \leq x) \to x + 1 \in ℝ^{*}$
80		simpr	$⊢ (((φ \land x \in ℝ) \land j \in A) \land F (j) \leq x) \to F (j) \leq x$
81		ltp1	$⊢ x \in ℝ \to x < x + 1$
82	81	ad3antlr	$⊢ (((φ \land x \in ℝ) \land j \in A) \land F (j) \leq x) \to x < x + 1$
83	75 77 79 80 82	xrlelttrd	$⊢ (((φ \land x \in ℝ) \land j \in A) \land F (j) \leq x) \to F (j) < x + 1$
84	83	ex	$⊢ ((φ \land x \in ℝ) \land j \in A) \to (F (j) \leq x \to F (j) < x + 1)$
85	84	imim2d	$⊢ ((φ \land x \in ℝ) \land j \in A) \to ((k \leq j \to F (j) \leq x) \to (k \leq j \to F (j) < x + 1))$
86	85	ralimdva	$⊢ (φ \land x \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) < x + 1))$
87	86	reximdv	$⊢ (φ \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) < x + 1))$
88	87	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) < x + 1)$
89		breq2	$⊢ y = x + 1 \to (F (j) < y \leftrightarrow F (j) < x + 1)$
90	89	imbi2d	$⊢ y = x + 1 \to ((k \leq j \to F (j) < y) \leftrightarrow (k \leq j \to F (j) < x + 1))$
91	90	ralbidv	$⊢ y = x + 1 \to (\forall j \in A (k \leq j \to F (j) < y) \leftrightarrow \forall j \in A (k \leq j \to F (j) < x + 1))$
92	91	rexbidv	$⊢ y = x + 1 \to (\exists k \in ℝ \forall j \in A (k \leq j \to F (j) < y) \leftrightarrow \exists k \in ℝ \forall j \in A (k \leq j \to F (j) < x + 1))$
93	92	rspcev	$⊢ (x + 1 \in ℝ \land \exists k \in ℝ \forall j \in A (k \leq j \to F (j) < x + 1)) \to \exists y \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) < y)$
94	74 88 93	syl2anc	$⊢ ((φ \land x \in ℝ) \land \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x)) \to \exists y \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) < y)$
95	94	rexlimdva2	$⊢ φ \to (\exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x) \to \exists y \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) < y))$
96	72 95	impbid	$⊢ φ \to (\exists y \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) < y) \leftrightarrow \exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x))$
97	54 96	anbi12d	$⊢ φ \to ((\exists y \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land y < F (j)) \land \exists y \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) < y)) \leftrightarrow (\exists x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j)) \land \exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x)))$
98	4 97	bitrd	$⊢ φ \to (lim sup (F) \in ℝ \leftrightarrow (\exists x \in ℝ \forall k \in ℝ \exists j \in A (k \leq j \land x \leq F (j)) \land \exists x \in ℝ \exists k \in ℝ \forall j \in A (k \leq j \to F (j) \leq x)))$

Metamath Proof Explorer

Theorem limsupre3lem

Proof