Theorem limsupreuzmpt

Description: Given a function on the reals, defined on a set of upper integers, 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	limsupreuzmpt.j	$$⊢Ⅎj\phi$$
	limsupreuzmpt.m	$$⊢\phi \to M\in \mathbb{Z}$$
	limsupreuzmpt.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	limsupreuzmpt.b	$$⊢\left(\phi \wedge j\in Z\right)\to B\in ℝ$$
Assertion	limsupreuzmpt	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(\left(j\in Z⟼B\right)\right)\in ℝ\leftrightarrow \left(\exists x\in ℝ\forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le B\wedge \exists x\in ℝ\forall j\in ZB\le x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		limsupreuzmpt.j	$$⊢Ⅎj\phi$$
2		limsupreuzmpt.m	$$⊢\phi \to M\in \mathbb{Z}$$
3		limsupreuzmpt.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
4		limsupreuzmpt.b	$$⊢\left(\phi \wedge j\in Z\right)\to B\in ℝ$$
5		nfmpt1	$$⊢\underset{\_}{Ⅎ}j\left(j\in Z⟼B\right)$$
6	1 4	fmptd2f	$$⊢\phi \to \left(j\in Z⟼B\right):Z⟶ℝ$$
7	5 2 3 6	limsupreuz	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(\left(j\in Z⟼B\right)\right)\in ℝ\leftrightarrow \left(\exists y\in ℝ\forall i\in Z\exists j\in {\mathbb{Z}}_{\ge i}y\le \left(j\in Z⟼B\right)\left(j\right)\wedge \exists y\in ℝ\forall j\in Z\left(j\in Z⟼B\right)\left(j\right)\le y\right)\right)$$
8		nfv	$$⊢Ⅎji\in Z$$
9	1 8	nfan	$$⊢Ⅎj\left(\phi \wedge i\in Z\right)$$
10		simpll	$$⊢\left(\left(\phi \wedge i\in Z\right)\wedge j\in {\mathbb{Z}}_{\ge i}\right)\to \phi$$
11	3	uztrn2	$$⊢\left(i\in Z\wedge j\in {\mathbb{Z}}_{\ge i}\right)\to j\in Z$$
12	11	adantll	$$⊢\left(\left(\phi \wedge i\in Z\right)\wedge j\in {\mathbb{Z}}_{\ge i}\right)\to j\in Z$$
13		eqid	$$⊢\left(j\in Z⟼B\right)=\left(j\in Z⟼B\right)$$
14	13	a1i	$$⊢\phi \to \left(j\in Z⟼B\right)=\left(j\in Z⟼B\right)$$
15	14 4	fvmpt2d	$$⊢\left(\phi \wedge j\in Z\right)\to \left(j\in Z⟼B\right)\left(j\right)=B$$
16	10 12 15	syl2anc	$$⊢\left(\left(\phi \wedge i\in Z\right)\wedge j\in {\mathbb{Z}}_{\ge i}\right)\to \left(j\in Z⟼B\right)\left(j\right)=B$$
17	16	breq2d	$$⊢\left(\left(\phi \wedge i\in Z\right)\wedge j\in {\mathbb{Z}}_{\ge i}\right)\to \left(y\le \left(j\in Z⟼B\right)\left(j\right)\leftrightarrow y\le B\right)$$
18	9 17	rexbida	$$⊢\left(\phi \wedge i\in Z\right)\to \left(\exists j\in {\mathbb{Z}}_{\ge i}y\le \left(j\in Z⟼B\right)\left(j\right)\leftrightarrow \exists j\in {\mathbb{Z}}_{\ge i}y\le B\right)$$
19	18	ralbidva	$$⊢\phi \to \left(\forall i\in Z\exists j\in {\mathbb{Z}}_{\ge i}y\le \left(j\in Z⟼B\right)\left(j\right)\leftrightarrow \forall i\in Z\exists j\in {\mathbb{Z}}_{\ge i}y\le B\right)$$
20	19	rexbidv	$$⊢\phi \to \left(\exists y\in ℝ\forall i\in Z\exists j\in {\mathbb{Z}}_{\ge i}y\le \left(j\in Z⟼B\right)\left(j\right)\leftrightarrow \exists y\in ℝ\forall i\in Z\exists j\in {\mathbb{Z}}_{\ge i}y\le B\right)$$
21		breq1	$$⊢y=x\to \left(y\le B\leftrightarrow x\le B\right)$$
22	21	rexbidv	$$⊢y=x\to \left(\exists j\in {\mathbb{Z}}_{\ge i}y\le B\leftrightarrow \exists j\in {\mathbb{Z}}_{\ge i}x\le B\right)$$
23	22	ralbidv	$$⊢y=x\to \left(\forall i\in Z\exists j\in {\mathbb{Z}}_{\ge i}y\le B\leftrightarrow \forall i\in Z\exists j\in {\mathbb{Z}}_{\ge i}x\le B\right)$$
24		fveq2	$$⊢i=k\to {\mathbb{Z}}_{\ge i}={\mathbb{Z}}_{\ge k}$$
25	24	rexeqdv	$$⊢i=k\to \left(\exists j\in {\mathbb{Z}}_{\ge i}x\le B\leftrightarrow \exists j\in {\mathbb{Z}}_{\ge k}x\le B\right)$$
26	25	cbvralvw	$$⊢\forall i\in Z\exists j\in {\mathbb{Z}}_{\ge i}x\le B\leftrightarrow \forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le B$$
27	26	a1i	$$⊢y=x\to \left(\forall i\in Z\exists j\in {\mathbb{Z}}_{\ge i}x\le B\leftrightarrow \forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le B\right)$$
28	23 27	bitrd	$$⊢y=x\to \left(\forall i\in Z\exists j\in {\mathbb{Z}}_{\ge i}y\le B\leftrightarrow \forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le B\right)$$
29	28	cbvrexvw	$$⊢\exists y\in ℝ\forall i\in Z\exists j\in {\mathbb{Z}}_{\ge i}y\le B\leftrightarrow \exists x\in ℝ\forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le B$$
30	29	a1i	$$⊢\phi \to \left(\exists y\in ℝ\forall i\in Z\exists j\in {\mathbb{Z}}_{\ge i}y\le B\leftrightarrow \exists x\in ℝ\forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le B\right)$$
31	20 30	bitrd	$$⊢\phi \to \left(\exists y\in ℝ\forall i\in Z\exists j\in {\mathbb{Z}}_{\ge i}y\le \left(j\in Z⟼B\right)\left(j\right)\leftrightarrow \exists x\in ℝ\forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le B\right)$$
32	15	breq1d	$$⊢\left(\phi \wedge j\in Z\right)\to \left(\left(j\in Z⟼B\right)\left(j\right)\le y\leftrightarrow B\le y\right)$$
33	1 32	ralbida	$$⊢\phi \to \left(\forall j\in Z\left(j\in Z⟼B\right)\left(j\right)\le y\leftrightarrow \forall j\in ZB\le y\right)$$
34	33	rexbidv	$$⊢\phi \to \left(\exists y\in ℝ\forall j\in Z\left(j\in Z⟼B\right)\left(j\right)\le y\leftrightarrow \exists y\in ℝ\forall j\in ZB\le y\right)$$
35		breq2	$$⊢y=x\to \left(B\le y\leftrightarrow B\le x\right)$$
36	35	ralbidv	$$⊢y=x\to \left(\forall j\in ZB\le y\leftrightarrow \forall j\in ZB\le x\right)$$
37	36	cbvrexvw	$$⊢\exists y\in ℝ\forall j\in ZB\le y\leftrightarrow \exists x\in ℝ\forall j\in ZB\le x$$
38	37	a1i	$$⊢\phi \to \left(\exists y\in ℝ\forall j\in ZB\le y\leftrightarrow \exists x\in ℝ\forall j\in ZB\le x\right)$$
39	34 38	bitrd	$$⊢\phi \to \left(\exists y\in ℝ\forall j\in Z\left(j\in Z⟼B\right)\left(j\right)\le y\leftrightarrow \exists x\in ℝ\forall j\in ZB\le x\right)$$
40	31 39	anbi12d	$$⊢\phi \to \left(\left(\exists y\in ℝ\forall i\in Z\exists j\in {\mathbb{Z}}_{\ge i}y\le \left(j\in Z⟼B\right)\left(j\right)\wedge \exists y\in ℝ\forall j\in Z\left(j\in Z⟼B\right)\left(j\right)\le y\right)\leftrightarrow \left(\exists x\in ℝ\forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le B\wedge \exists x\in ℝ\forall j\in ZB\le x\right)\right)$$
41	7 40	bitrd	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(\left(j\in Z⟼B\right)\right)\in ℝ\leftrightarrow \left(\exists x\in ℝ\forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le B\wedge \exists x\in ℝ\forall j\in ZB\le x\right)\right)$$