Theorem limsupre2

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 smaller than the function, at some point, in any upper part of the reals; 2. there is a real number that is eventually larger than the function. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupre2.1	$$⊢\underset{\_}{Ⅎ}jF$$
	limsupre2.2	$$⊢\phi \to A\subseteq ℝ$$
	limsupre2.3	$$⊢\phi \to F:A⟶{ℝ}^{*}$$
Assertion	limsupre2	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)\in ℝ\leftrightarrow \left(\exists x\in ℝ\forall k\in ℝ\exists j\in A\left(k\le j\wedge x<F\left(j\right)\right)\wedge \exists x\in ℝ\exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)<x\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		limsupre2.1	$$⊢\underset{\_}{Ⅎ}jF$$
2		limsupre2.2	$$⊢\phi \to A\subseteq ℝ$$
3		limsupre2.3	$$⊢\phi \to F:A⟶{ℝ}^{*}$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}lF$$
5	4 2 3	limsupre2lem	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)\in ℝ\leftrightarrow \left(\exists y\in ℝ\forall i\in ℝ\exists l\in A\left(i\le l\wedge y<F\left(l\right)\right)\wedge \exists y\in ℝ\exists i\in ℝ\forall l\in A\left(i\le l\to F\left(l\right)<y\right)\right)\right)$$
6		breq1	$$⊢y=x\to \left(y<F\left(l\right)\leftrightarrow x<F\left(l\right)\right)$$
7	6	anbi2d	$$⊢y=x\to \left(\left(i\le l\wedge y<F\left(l\right)\right)\leftrightarrow \left(i\le l\wedge x<F\left(l\right)\right)\right)$$
8	7	rexbidv	$$⊢y=x\to \left(\exists l\in A\left(i\le l\wedge y<F\left(l\right)\right)\leftrightarrow \exists l\in A\left(i\le l\wedge x<F\left(l\right)\right)\right)$$
9	8	ralbidv	$$⊢y=x\to \left(\forall i\in ℝ\exists l\in A\left(i\le l\wedge y<F\left(l\right)\right)\leftrightarrow \forall i\in ℝ\exists l\in A\left(i\le l\wedge x<F\left(l\right)\right)\right)$$
10		breq1	$$⊢i=k\to \left(i\le l\leftrightarrow k\le l\right)$$
11	10	anbi1d	$$⊢i=k\to \left(\left(i\le l\wedge x<F\left(l\right)\right)\leftrightarrow \left(k\le l\wedge x<F\left(l\right)\right)\right)$$
12	11	rexbidv	$$⊢i=k\to \left(\exists l\in A\left(i\le l\wedge x<F\left(l\right)\right)\leftrightarrow \exists l\in A\left(k\le l\wedge x<F\left(l\right)\right)\right)$$
13		nfv	$$⊢Ⅎjk\le l$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}jx$$
15		nfcv	$$⊢\underset{\_}{Ⅎ}j<$$
16		nfcv	$$⊢\underset{\_}{Ⅎ}jl$$
17	1 16	nffv	$$⊢\underset{\_}{Ⅎ}jF\left(l\right)$$
18	14 15 17	nfbr	$$⊢Ⅎjx<F\left(l\right)$$
19	13 18	nfan	$$⊢Ⅎj\left(k\le l\wedge x<F\left(l\right)\right)$$
20		nfv	$$⊢Ⅎl\left(k\le j\wedge x<F\left(j\right)\right)$$
21		breq2	$$⊢l=j\to \left(k\le l\leftrightarrow k\le j\right)$$
22		fveq2	$$⊢l=j\to F\left(l\right)=F\left(j\right)$$
23	22	breq2d	$$⊢l=j\to \left(x<F\left(l\right)\leftrightarrow x<F\left(j\right)\right)$$
24	21 23	anbi12d	$$⊢l=j\to \left(\left(k\le l\wedge x<F\left(l\right)\right)\leftrightarrow \left(k\le j\wedge x<F\left(j\right)\right)\right)$$
25	19 20 24	cbvrexw	$$⊢\exists l\in A\left(k\le l\wedge x<F\left(l\right)\right)\leftrightarrow \exists j\in A\left(k\le j\wedge x<F\left(j\right)\right)$$
26	25	a1i	$$⊢i=k\to \left(\exists l\in A\left(k\le l\wedge x<F\left(l\right)\right)\leftrightarrow \exists j\in A\left(k\le j\wedge x<F\left(j\right)\right)\right)$$
27	12 26	bitrd	$$⊢i=k\to \left(\exists l\in A\left(i\le l\wedge x<F\left(l\right)\right)\leftrightarrow \exists j\in A\left(k\le j\wedge x<F\left(j\right)\right)\right)$$
28	27	cbvralvw	$$⊢\forall i\in ℝ\exists l\in A\left(i\le l\wedge x<F\left(l\right)\right)\leftrightarrow \forall k\in ℝ\exists j\in A\left(k\le j\wedge x<F\left(j\right)\right)$$
29	28	a1i	$$⊢y=x\to \left(\forall i\in ℝ\exists l\in A\left(i\le l\wedge x<F\left(l\right)\right)\leftrightarrow \forall k\in ℝ\exists j\in A\left(k\le j\wedge x<F\left(j\right)\right)\right)$$
30	9 29	bitrd	$$⊢y=x\to \left(\forall i\in ℝ\exists l\in A\left(i\le l\wedge y<F\left(l\right)\right)\leftrightarrow \forall k\in ℝ\exists j\in A\left(k\le j\wedge x<F\left(j\right)\right)\right)$$
31	30	cbvrexvw	$$⊢\exists y\in ℝ\forall i\in ℝ\exists l\in A\left(i\le l\wedge y<F\left(l\right)\right)\leftrightarrow \exists x\in ℝ\forall k\in ℝ\exists j\in A\left(k\le j\wedge x<F\left(j\right)\right)$$
32	31	a1i	$$⊢\phi \to \left(\exists y\in ℝ\forall i\in ℝ\exists l\in A\left(i\le l\wedge y<F\left(l\right)\right)\leftrightarrow \exists x\in ℝ\forall k\in ℝ\exists j\in A\left(k\le j\wedge x<F\left(j\right)\right)\right)$$
33		breq2	$$⊢y=x\to \left(F\left(l\right)<y\leftrightarrow F\left(l\right)<x\right)$$
34	33	imbi2d	$$⊢y=x\to \left(\left(i\le l\to F\left(l\right)<y\right)\leftrightarrow \left(i\le l\to F\left(l\right)<x\right)\right)$$
35	34	ralbidv	$$⊢y=x\to \left(\forall l\in A\left(i\le l\to F\left(l\right)<y\right)\leftrightarrow \forall l\in A\left(i\le l\to F\left(l\right)<x\right)\right)$$
36	35	rexbidv	$$⊢y=x\to \left(\exists i\in ℝ\forall l\in A\left(i\le l\to F\left(l\right)<y\right)\leftrightarrow \exists i\in ℝ\forall l\in A\left(i\le l\to F\left(l\right)<x\right)\right)$$
37	10	imbi1d	$$⊢i=k\to \left(\left(i\le l\to F\left(l\right)<x\right)\leftrightarrow \left(k\le l\to F\left(l\right)<x\right)\right)$$
38	37	ralbidv	$$⊢i=k\to \left(\forall l\in A\left(i\le l\to F\left(l\right)<x\right)\leftrightarrow \forall l\in A\left(k\le l\to F\left(l\right)<x\right)\right)$$
39	17 15 14	nfbr	$$⊢ℲjF\left(l\right)<x$$
40	13 39	nfim	$$⊢Ⅎj\left(k\le l\to F\left(l\right)<x\right)$$
41		nfv	$$⊢Ⅎl\left(k\le j\to F\left(j\right)<x\right)$$
42	22	breq1d	$$⊢l=j\to \left(F\left(l\right)<x\leftrightarrow F\left(j\right)<x\right)$$
43	21 42	imbi12d	$$⊢l=j\to \left(\left(k\le l\to F\left(l\right)<x\right)\leftrightarrow \left(k\le j\to F\left(j\right)<x\right)\right)$$
44	40 41 43	cbvralw	$$⊢\forall l\in A\left(k\le l\to F\left(l\right)<x\right)\leftrightarrow \forall j\in A\left(k\le j\to F\left(j\right)<x\right)$$
45	44	a1i	$$⊢i=k\to \left(\forall l\in A\left(k\le l\to F\left(l\right)<x\right)\leftrightarrow \forall j\in A\left(k\le j\to F\left(j\right)<x\right)\right)$$
46	38 45	bitrd	$$⊢i=k\to \left(\forall l\in A\left(i\le l\to F\left(l\right)<x\right)\leftrightarrow \forall j\in A\left(k\le j\to F\left(j\right)<x\right)\right)$$
47	46	cbvrexvw	$$⊢\exists i\in ℝ\forall l\in A\left(i\le l\to F\left(l\right)<x\right)\leftrightarrow \exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)<x\right)$$
48	47	a1i	$$⊢y=x\to \left(\exists i\in ℝ\forall l\in A\left(i\le l\to F\left(l\right)<x\right)\leftrightarrow \exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)<x\right)\right)$$
49	36 48	bitrd	$$⊢y=x\to \left(\exists i\in ℝ\forall l\in A\left(i\le l\to F\left(l\right)<y\right)\leftrightarrow \exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)<x\right)\right)$$
50	49	cbvrexvw	$$⊢\exists y\in ℝ\exists i\in ℝ\forall l\in A\left(i\le l\to F\left(l\right)<y\right)\leftrightarrow \exists x\in ℝ\exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)<x\right)$$
51	50	a1i	$$⊢\phi \to \left(\exists y\in ℝ\exists i\in ℝ\forall l\in A\left(i\le l\to F\left(l\right)<y\right)\leftrightarrow \exists x\in ℝ\exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)<x\right)\right)$$
52	32 51	anbi12d	$$⊢\phi \to \left(\left(\exists y\in ℝ\forall i\in ℝ\exists l\in A\left(i\le l\wedge y<F\left(l\right)\right)\wedge \exists y\in ℝ\exists i\in ℝ\forall l\in A\left(i\le l\to F\left(l\right)<y\right)\right)\leftrightarrow \left(\exists x\in ℝ\forall k\in ℝ\exists j\in A\left(k\le j\wedge x<F\left(j\right)\right)\wedge \exists x\in ℝ\exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)<x\right)\right)\right)$$
53	5 52	bitrd	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)\in ℝ\leftrightarrow \left(\exists x\in ℝ\forall k\in ℝ\exists j\in A\left(k\le j\wedge x<F\left(j\right)\right)\wedge \exists x\in ℝ\exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)<x\right)\right)\right)$$