Theorem limsupre3

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	limsupre3.1	$$⊢\underset{\_}{Ⅎ}jF$$
	limsupre3.2	$$⊢\phi \to A\subseteq ℝ$$
	limsupre3.3	$$⊢\phi \to F:A⟶{ℝ}^{*}$$
Assertion	limsupre3	$$⊢\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\le 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)\le x\right)\right)\right)$$

Proof

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