Theorem limsupreuz

Description: Given a function on the 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, infinitely often; 2. there is a real number that is greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupreuz.1	$$⊢\underset{\_}{Ⅎ}jF$$
	limsupreuz.2	$$⊢\phi \to M\in \mathbb{Z}$$
	limsupreuz.3	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	limsupreuz.4	$$⊢\phi \to F:Z⟶ℝ$$
Assertion	limsupreuz	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)\in ℝ\leftrightarrow \left(\exists x\in ℝ\forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\wedge \exists x\in ℝ\forall j\in ZF\left(j\right)\le x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		limsupreuz.1	$$⊢\underset{\_}{Ⅎ}jF$$
2		limsupreuz.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		limsupreuz.3	$$⊢Z={\mathbb{Z}}_{\ge M}$$
4		limsupreuz.4	$$⊢\phi \to F:Z⟶ℝ$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}lF$$
6	4	frexr	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
7	5 2 3 6	limsupre3uzlem	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)\in ℝ\leftrightarrow \left(\exists y\in ℝ\forall i\in Z\exists l\in {\mathbb{Z}}_{\ge i}y\le F\left(l\right)\wedge \exists y\in ℝ\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\right)\right)$$
8		breq1	$$⊢y=x\to \left(y\le F\left(l\right)\leftrightarrow x\le F\left(l\right)\right)$$
9	8	rexbidv	$$⊢y=x\to \left(\exists l\in {\mathbb{Z}}_{\ge i}y\le F\left(l\right)\leftrightarrow \exists l\in {\mathbb{Z}}_{\ge i}x\le F\left(l\right)\right)$$
10	9	ralbidv	$$⊢y=x\to \left(\forall i\in Z\exists l\in {\mathbb{Z}}_{\ge i}y\le F\left(l\right)\leftrightarrow \forall i\in Z\exists l\in {\mathbb{Z}}_{\ge i}x\le F\left(l\right)\right)$$
11		fveq2	$$⊢i=k\to {\mathbb{Z}}_{\ge i}={\mathbb{Z}}_{\ge k}$$
12	11	rexeqdv	$$⊢i=k\to \left(\exists l\in {\mathbb{Z}}_{\ge i}x\le F\left(l\right)\leftrightarrow \exists l\in {\mathbb{Z}}_{\ge k}x\le F\left(l\right)\right)$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}jx$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}j\le$$
15		nfcv	$$⊢\underset{\_}{Ⅎ}jl$$
16	1 15	nffv	$$⊢\underset{\_}{Ⅎ}jF\left(l\right)$$
17	13 14 16	nfbr	$$⊢Ⅎjx\le F\left(l\right)$$
18		nfv	$$⊢Ⅎlx\le F\left(j\right)$$
19		fveq2	$$⊢l=j\to F\left(l\right)=F\left(j\right)$$
20	19	breq2d	$$⊢l=j\to \left(x\le F\left(l\right)\leftrightarrow x\le F\left(j\right)\right)$$
21	17 18 20	cbvrexw	$$⊢\exists l\in {\mathbb{Z}}_{\ge k}x\le F\left(l\right)\leftrightarrow \exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)$$
22	21	a1i	$$⊢i=k\to \left(\exists l\in {\mathbb{Z}}_{\ge k}x\le F\left(l\right)\leftrightarrow \exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)$$
23	12 22	bitrd	$$⊢i=k\to \left(\exists l\in {\mathbb{Z}}_{\ge i}x\le F\left(l\right)\leftrightarrow \exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)$$
24	23	cbvralvw	$$⊢\forall i\in Z\exists l\in {\mathbb{Z}}_{\ge i}x\le F\left(l\right)\leftrightarrow \forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)$$
25	24	a1i	$$⊢y=x\to \left(\forall i\in Z\exists l\in {\mathbb{Z}}_{\ge i}x\le F\left(l\right)\leftrightarrow \forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)$$
26	10 25	bitrd	$$⊢y=x\to \left(\forall i\in Z\exists l\in {\mathbb{Z}}_{\ge i}y\le F\left(l\right)\leftrightarrow \forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)$$
27	26	cbvrexvw	$$⊢\exists y\in ℝ\forall i\in Z\exists l\in {\mathbb{Z}}_{\ge i}y\le F\left(l\right)\leftrightarrow \exists x\in ℝ\forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)$$
28		breq2	$$⊢y=x\to \left(F\left(l\right)\le y\leftrightarrow F\left(l\right)\le x\right)$$
29	28	ralbidv	$$⊢y=x\to \left(\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\leftrightarrow \forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le x\right)$$
30	29	rexbidv	$$⊢y=x\to \left(\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\leftrightarrow \exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le x\right)$$
31	11	raleqdv	$$⊢i=k\to \left(\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le x\leftrightarrow \forall l\in {\mathbb{Z}}_{\ge k}F\left(l\right)\le x\right)$$
32	16 14 13	nfbr	$$⊢ℲjF\left(l\right)\le x$$
33		nfv	$$⊢ℲlF\left(j\right)\le x$$
34	19	breq1d	$$⊢l=j\to \left(F\left(l\right)\le x\leftrightarrow F\left(j\right)\le x\right)$$
35	32 33 34	cbvralw	$$⊢\forall l\in {\mathbb{Z}}_{\ge k}F\left(l\right)\le x\leftrightarrow \forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x$$
36	35	a1i	$$⊢i=k\to \left(\forall l\in {\mathbb{Z}}_{\ge k}F\left(l\right)\le x\leftrightarrow \forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)$$
37	31 36	bitrd	$$⊢i=k\to \left(\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le x\leftrightarrow \forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)$$
38	37	cbvrexvw	$$⊢\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le x\leftrightarrow \exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x$$
39	38	a1i	$$⊢y=x\to \left(\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le x\leftrightarrow \exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)$$
40	30 39	bitrd	$$⊢y=x\to \left(\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\leftrightarrow \exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)$$
41	40	cbvrexvw	$$⊢\exists y\in ℝ\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\leftrightarrow \exists x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x$$
42	27 41	anbi12i	$$⊢\left(\exists y\in ℝ\forall i\in Z\exists l\in {\mathbb{Z}}_{\ge i}y\le F\left(l\right)\wedge \exists y\in ℝ\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\right)\leftrightarrow \left(\exists x\in ℝ\forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\wedge \exists x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)$$
43	42	a1i	$$⊢\phi \to \left(\left(\exists y\in ℝ\forall i\in Z\exists l\in {\mathbb{Z}}_{\ge i}y\le F\left(l\right)\wedge \exists y\in ℝ\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\right)\leftrightarrow \left(\exists x\in ℝ\forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\wedge \exists x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)\right)$$
44	7 43	bitrd	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)\in ℝ\leftrightarrow \left(\exists x\in ℝ\forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\wedge \exists x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)\right)$$
45		nfv	$$⊢ℲiF\left(j\right)\le x$$
46		nfcv	$$⊢\underset{\_}{Ⅎ}ji$$
47	1 46	nffv	$$⊢\underset{\_}{Ⅎ}jF\left(i\right)$$
48	47 14 13	nfbr	$$⊢ℲjF\left(i\right)\le x$$
49		fveq2	$$⊢j=i\to F\left(j\right)=F\left(i\right)$$
50	49	breq1d	$$⊢j=i\to \left(F\left(j\right)\le x\leftrightarrow F\left(i\right)\le x\right)$$
51	45 48 50	cbvralw	$$⊢\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\leftrightarrow \forall i\in {\mathbb{Z}}_{\ge k}F\left(i\right)\le x$$
52	51	rexbii	$$⊢\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\leftrightarrow \exists k\in Z\forall i\in {\mathbb{Z}}_{\ge k}F\left(i\right)\le x$$
53	52	rexbii	$$⊢\exists x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\leftrightarrow \exists x\in ℝ\exists k\in Z\forall i\in {\mathbb{Z}}_{\ge k}F\left(i\right)\le x$$
54	53	a1i	$$⊢\phi \to \left(\exists x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\leftrightarrow \exists x\in ℝ\exists k\in Z\forall i\in {\mathbb{Z}}_{\ge k}F\left(i\right)\le x\right)$$
55		nfv	$$⊢Ⅎi\phi$$
56	4	adantr	$$⊢\left(\phi \wedge i\in Z\right)\to F:Z⟶ℝ$$
57		simpr	$$⊢\left(\phi \wedge i\in Z\right)\to i\in Z$$
58	56 57	ffvelrnd	$$⊢\left(\phi \wedge i\in Z\right)\to F\left(i\right)\in ℝ$$
59	55 2 3 58	uzub	$$⊢\phi \to \left(\exists x\in ℝ\exists k\in Z\forall i\in {\mathbb{Z}}_{\ge k}F\left(i\right)\le x\leftrightarrow \exists x\in ℝ\forall i\in ZF\left(i\right)\le x\right)$$
60		eqcom	$$⊢j=i\leftrightarrow i=j$$
61	60	imbi1i	$$⊢\left(j=i\to \left(F\left(j\right)\le x\leftrightarrow F\left(i\right)\le x\right)\right)\leftrightarrow \left(i=j\to \left(F\left(j\right)\le x\leftrightarrow F\left(i\right)\le x\right)\right)$$
62		bicom	$$⊢\left(F\left(j\right)\le x\leftrightarrow F\left(i\right)\le x\right)\leftrightarrow \left(F\left(i\right)\le x\leftrightarrow F\left(j\right)\le x\right)$$
63	62	imbi2i	$$⊢\left(i=j\to \left(F\left(j\right)\le x\leftrightarrow F\left(i\right)\le x\right)\right)\leftrightarrow \left(i=j\to \left(F\left(i\right)\le x\leftrightarrow F\left(j\right)\le x\right)\right)$$
64	61 63	bitri	$$⊢\left(j=i\to \left(F\left(j\right)\le x\leftrightarrow F\left(i\right)\le x\right)\right)\leftrightarrow \left(i=j\to \left(F\left(i\right)\le x\leftrightarrow F\left(j\right)\le x\right)\right)$$
65	50 64	mpbi	$$⊢i=j\to \left(F\left(i\right)\le x\leftrightarrow F\left(j\right)\le x\right)$$
66	48 45 65	cbvralw	$$⊢\forall i\in ZF\left(i\right)\le x\leftrightarrow \forall j\in ZF\left(j\right)\le x$$
67	66	rexbii	$$⊢\exists x\in ℝ\forall i\in ZF\left(i\right)\le x\leftrightarrow \exists x\in ℝ\forall j\in ZF\left(j\right)\le x$$
68	67	a1i	$$⊢\phi \to \left(\exists x\in ℝ\forall i\in ZF\left(i\right)\le x\leftrightarrow \exists x\in ℝ\forall j\in ZF\left(j\right)\le x\right)$$
69	54 59 68	3bitrd	$$⊢\phi \to \left(\exists x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\leftrightarrow \exists x\in ℝ\forall j\in ZF\left(j\right)\le x\right)$$
70	69	anbi2d	$$⊢\phi \to \left(\left(\exists x\in ℝ\forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\wedge \exists x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)\leftrightarrow \left(\exists x\in ℝ\forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\wedge \exists x\in ℝ\forall j\in ZF\left(j\right)\le x\right)\right)$$
71	44 70	bitrd	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)\in ℝ\leftrightarrow \left(\exists x\in ℝ\forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\wedge \exists x\in ℝ\forall j\in ZF\left(j\right)\le x\right)\right)$$