Theorem limsupre2lem

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	limsupre2lem.1	$$⊢\underset{\_}{Ⅎ}jF$$
	limsupre2lem.2	$$⊢\phi \to A\subseteq ℝ$$
	limsupre2lem.3	$$⊢\phi \to F:A⟶{ℝ}^{*}$$
Assertion	limsupre2lem	$$⊢\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		limsupre2lem.1	$$⊢\underset{\_}{Ⅎ}jF$$
2		limsupre2lem.2	$$⊢\phi \to A\subseteq ℝ$$
3		limsupre2lem.3	$$⊢\phi \to F:A⟶{ℝ}^{*}$$
4		reex	$$⊢ℝ\in \mathrm{V}$$
5	4	a1i	$$⊢\phi \to ℝ\in \mathrm{V}$$
6	5 2	ssexd	$$⊢\phi \to A\in \mathrm{V}$$
7	3 6	fexd	$$⊢\phi \to F\in \mathrm{V}$$
8	7	limsupcld	$$⊢\phi \to \mathrm{lim\; sup}\left(F\right)\in {ℝ}^{*}$$
9		xrre4	$$⊢\mathrm{lim\; sup}\left(F\right)\in {ℝ}^{*}\to \left(\mathrm{lim\; sup}\left(F\right)\in ℝ\leftrightarrow \left(\mathrm{lim\; sup}\left(F\right)\ne \mathrm{-\infty }\wedge \mathrm{lim\; sup}\left(F\right)\ne \mathrm{+\infty }\right)\right)$$
10	8 9	syl	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)\in ℝ\leftrightarrow \left(\mathrm{lim\; sup}\left(F\right)\ne \mathrm{-\infty }\wedge \mathrm{lim\; sup}\left(F\right)\ne \mathrm{+\infty }\right)\right)$$
11		df-ne	$$⊢\mathrm{lim\; sup}\left(F\right)\ne \mathrm{-\infty }\leftrightarrow \neg \mathrm{lim\; sup}\left(F\right)=\mathrm{-\infty }$$
12	11	a1i	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)\ne \mathrm{-\infty }\leftrightarrow \neg \mathrm{lim\; sup}\left(F\right)=\mathrm{-\infty }\right)$$
13	1 2 3	limsupmnf	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)=\mathrm{-\infty }\leftrightarrow \forall x\in ℝ\exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)\le x\right)\right)$$
14	13	notbid	$$⊢\phi \to \left(\neg \mathrm{lim\; sup}\left(F\right)=\mathrm{-\infty }\leftrightarrow \neg \forall x\in ℝ\exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)\le x\right)\right)$$
15		annim	$$⊢\left(k\le j\wedge \neg F\left(j\right)\le x\right)\leftrightarrow \neg \left(k\le j\to F\left(j\right)\le x\right)$$
16	15	rexbii	$$⊢\exists j\in A\left(k\le j\wedge \neg F\left(j\right)\le x\right)\leftrightarrow \exists j\in A\neg \left(k\le j\to F\left(j\right)\le x\right)$$
17		rexnal	$$⊢\exists j\in A\neg \left(k\le j\to F\left(j\right)\le x\right)\leftrightarrow \neg \forall j\in A\left(k\le j\to F\left(j\right)\le x\right)$$
18	16 17	bitri	$$⊢\exists j\in A\left(k\le j\wedge \neg F\left(j\right)\le x\right)\leftrightarrow \neg \forall j\in A\left(k\le j\to F\left(j\right)\le x\right)$$
19	18	ralbii	$$⊢\forall k\in ℝ\exists j\in A\left(k\le j\wedge \neg F\left(j\right)\le x\right)\leftrightarrow \forall k\in ℝ\neg \forall j\in A\left(k\le j\to F\left(j\right)\le x\right)$$
20		ralnex	$$⊢\forall k\in ℝ\neg \forall j\in A\left(k\le j\to F\left(j\right)\le x\right)\leftrightarrow \neg \exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)\le x\right)$$
21	19 20	bitri	$$⊢\forall k\in ℝ\exists j\in A\left(k\le j\wedge \neg F\left(j\right)\le x\right)\leftrightarrow \neg \exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)\le x\right)$$
22	21	rexbii	$$⊢\exists x\in ℝ\forall k\in ℝ\exists j\in A\left(k\le j\wedge \neg F\left(j\right)\le x\right)\leftrightarrow \exists x\in ℝ\neg \exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)\le x\right)$$
23		rexnal	$$⊢\exists x\in ℝ\neg \exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)\le x\right)\leftrightarrow \neg \forall x\in ℝ\exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)\le x\right)$$
24	22 23	bitr2i	$$⊢\neg \forall x\in ℝ\exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)\le x\right)\leftrightarrow \exists x\in ℝ\forall k\in ℝ\exists j\in A\left(k\le j\wedge \neg F\left(j\right)\le x\right)$$
25	24	a1i	$$⊢\phi \to \left(\neg \forall x\in ℝ\exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)\le x\right)\leftrightarrow \exists x\in ℝ\forall k\in ℝ\exists j\in A\left(k\le j\wedge \neg F\left(j\right)\le x\right)\right)$$
26		simplr	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge j\in A\right)\to x\in ℝ$$
27	26	rexrd	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge j\in A\right)\to x\in {ℝ}^{*}$$
28	3	adantr	$$⊢\left(\phi \wedge x\in ℝ\right)\to F:A⟶{ℝ}^{*}$$
29	28	ffvelcdmda	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge j\in A\right)\to F\left(j\right)\in {ℝ}^{*}$$
30	27 29	xrltnled	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge j\in A\right)\to \left(x<F\left(j\right)\leftrightarrow \neg F\left(j\right)\le x\right)$$
31	30	bicomd	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge j\in A\right)\to \left(\neg F\left(j\right)\le x\leftrightarrow x<F\left(j\right)\right)$$
32	31	anbi2d	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge j\in A\right)\to \left(\left(k\le j\wedge \neg F\left(j\right)\le x\right)\leftrightarrow \left(k\le j\wedge x<F\left(j\right)\right)\right)$$
33	32	rexbidva	$$⊢\left(\phi \wedge x\in ℝ\right)\to \left(\exists j\in A\left(k\le j\wedge \neg F\left(j\right)\le x\right)\leftrightarrow \exists j\in A\left(k\le j\wedge x<F\left(j\right)\right)\right)$$
34	33	ralbidv	$$⊢\left(\phi \wedge x\in ℝ\right)\to \left(\forall k\in ℝ\exists j\in A\left(k\le j\wedge \neg F\left(j\right)\le x\right)\leftrightarrow \forall k\in ℝ\exists j\in A\left(k\le j\wedge x<F\left(j\right)\right)\right)$$
35	34	rexbidva	$$⊢\phi \to \left(\exists x\in ℝ\forall k\in ℝ\exists j\in A\left(k\le j\wedge \neg F\left(j\right)\le x\right)\leftrightarrow \exists x\in ℝ\forall k\in ℝ\exists j\in A\left(k\le j\wedge x<F\left(j\right)\right)\right)$$
36	25 35	bitrd	$$⊢\phi \to \left(\neg \forall x\in ℝ\exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)\le x\right)\leftrightarrow \exists x\in ℝ\forall k\in ℝ\exists j\in A\left(k\le j\wedge x<F\left(j\right)\right)\right)$$
37	12 14 36	3bitrd	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)\ne \mathrm{-\infty }\leftrightarrow \exists x\in ℝ\forall k\in ℝ\exists j\in A\left(k\le j\wedge x<F\left(j\right)\right)\right)$$
38		df-ne	$$⊢\mathrm{lim\; sup}\left(F\right)\ne \mathrm{+\infty }\leftrightarrow \neg \mathrm{lim\; sup}\left(F\right)=\mathrm{+\infty }$$
39	38	a1i	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)\ne \mathrm{+\infty }\leftrightarrow \neg \mathrm{lim\; sup}\left(F\right)=\mathrm{+\infty }\right)$$
40	1 2 3	limsuppnf	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)=\mathrm{+\infty }\leftrightarrow \forall x\in ℝ\forall k\in ℝ\exists j\in A\left(k\le j\wedge x\le F\left(j\right)\right)\right)$$
41	40	notbid	$$⊢\phi \to \left(\neg \mathrm{lim\; sup}\left(F\right)=\mathrm{+\infty }\leftrightarrow \neg \forall x\in ℝ\forall k\in ℝ\exists j\in A\left(k\le j\wedge x\le F\left(j\right)\right)\right)$$
42	29 27	xrltnled	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge j\in A\right)\to \left(F\left(j\right)<x\leftrightarrow \neg x\le F\left(j\right)\right)$$
43	42	imbi2d	$$⊢\left(\left(\phi \wedge x\in ℝ\right)\wedge j\in A\right)\to \left(\left(k\le j\to F\left(j\right)<x\right)\leftrightarrow \left(k\le j\to \neg x\le F\left(j\right)\right)\right)$$
44	43	ralbidva	$$⊢\left(\phi \wedge x\in ℝ\right)\to \left(\forall j\in A\left(k\le j\to F\left(j\right)<x\right)\leftrightarrow \forall j\in A\left(k\le j\to \neg x\le F\left(j\right)\right)\right)$$
45	44	rexbidv	$$⊢\left(\phi \wedge x\in ℝ\right)\to \left(\exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)<x\right)\leftrightarrow \exists k\in ℝ\forall j\in A\left(k\le j\to \neg x\le F\left(j\right)\right)\right)$$
46	45	rexbidva	$$⊢\phi \to \left(\exists x\in ℝ\exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)<x\right)\leftrightarrow \exists x\in ℝ\exists k\in ℝ\forall j\in A\left(k\le j\to \neg x\le F\left(j\right)\right)\right)$$
47		imnan	$$⊢\left(k\le j\to \neg x\le F\left(j\right)\right)\leftrightarrow \neg \left(k\le j\wedge x\le F\left(j\right)\right)$$
48	47	ralbii	$$⊢\forall j\in A\left(k\le j\to \neg x\le F\left(j\right)\right)\leftrightarrow \forall j\in A\neg \left(k\le j\wedge x\le F\left(j\right)\right)$$
49		ralnex	$$⊢\forall j\in A\neg \left(k\le j\wedge x\le F\left(j\right)\right)\leftrightarrow \neg \exists j\in A\left(k\le j\wedge x\le F\left(j\right)\right)$$
50	48 49	bitri	$$⊢\forall j\in A\left(k\le j\to \neg x\le F\left(j\right)\right)\leftrightarrow \neg \exists j\in A\left(k\le j\wedge x\le F\left(j\right)\right)$$
51	50	rexbii	$$⊢\exists k\in ℝ\forall j\in A\left(k\le j\to \neg x\le F\left(j\right)\right)\leftrightarrow \exists k\in ℝ\neg \exists j\in A\left(k\le j\wedge x\le F\left(j\right)\right)$$
52		rexnal	$$⊢\exists k\in ℝ\neg \exists j\in A\left(k\le j\wedge x\le F\left(j\right)\right)\leftrightarrow \neg \forall k\in ℝ\exists j\in A\left(k\le j\wedge x\le F\left(j\right)\right)$$
53	51 52	bitri	$$⊢\exists k\in ℝ\forall j\in A\left(k\le j\to \neg x\le F\left(j\right)\right)\leftrightarrow \neg \forall k\in ℝ\exists j\in A\left(k\le j\wedge x\le F\left(j\right)\right)$$
54	53	rexbii	$$⊢\exists x\in ℝ\exists k\in ℝ\forall j\in A\left(k\le j\to \neg x\le F\left(j\right)\right)\leftrightarrow \exists x\in ℝ\neg \forall k\in ℝ\exists j\in A\left(k\le j\wedge x\le F\left(j\right)\right)$$
55		rexnal	$$⊢\exists x\in ℝ\neg \forall k\in ℝ\exists j\in A\left(k\le j\wedge x\le F\left(j\right)\right)\leftrightarrow \neg \forall x\in ℝ\forall k\in ℝ\exists j\in A\left(k\le j\wedge x\le F\left(j\right)\right)$$
56	54 55	bitri	$$⊢\exists x\in ℝ\exists k\in ℝ\forall j\in A\left(k\le j\to \neg x\le F\left(j\right)\right)\leftrightarrow \neg \forall x\in ℝ\forall k\in ℝ\exists j\in A\left(k\le j\wedge x\le F\left(j\right)\right)$$
57	56	a1i	$$⊢\phi \to \left(\exists x\in ℝ\exists k\in ℝ\forall j\in A\left(k\le j\to \neg x\le F\left(j\right)\right)\leftrightarrow \neg \forall x\in ℝ\forall k\in ℝ\exists j\in A\left(k\le j\wedge x\le F\left(j\right)\right)\right)$$
58	46 57	bitr2d	$$⊢\phi \to \left(\neg \forall x\in ℝ\forall k\in ℝ\exists j\in A\left(k\le j\wedge x\le F\left(j\right)\right)\leftrightarrow \exists x\in ℝ\exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)<x\right)\right)$$
59	39 41 58	3bitrd	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)\ne \mathrm{+\infty }\leftrightarrow \exists x\in ℝ\exists k\in ℝ\forall j\in A\left(k\le j\to F\left(j\right)<x\right)\right)$$
60	37 59	anbi12d	$$⊢\phi \to \left(\left(\mathrm{lim\; sup}\left(F\right)\ne \mathrm{-\infty }\wedge \mathrm{lim\; sup}\left(F\right)\ne \mathrm{+\infty }\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)$$
61	10 60	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)$$