Theorem limsupre3uzlem

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, infinitely often; 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	limsupre3uzlem.1	$$⊢\underset{\_}{Ⅎ}jF$$
	limsupre3uzlem.2	$$⊢\phi \to M\in \mathbb{Z}$$
	limsupre3uzlem.3	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	limsupre3uzlem.4	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
Assertion	limsupre3uzlem	$$⊢\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)$$

Proof

Step	Hyp	Ref	Expression
1		limsupre3uzlem.1	$$⊢\underset{\_}{Ⅎ}jF$$
2		limsupre3uzlem.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		limsupre3uzlem.3	$$⊢Z={\mathbb{Z}}_{\ge M}$$
4		limsupre3uzlem.4	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
5		uzssre	$$⊢{\mathbb{Z}}_{\ge M}\subseteq ℝ$$
6	3 5	eqsstri	$$⊢Z\subseteq ℝ$$
7	6	a1i	$$⊢\phi \to Z\subseteq ℝ$$
8	1 7 4	limsupre3	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)\in ℝ\leftrightarrow \left(\exists x\in ℝ\forall y\in ℝ\exists j\in Z\left(y\le j\wedge x\le F\left(j\right)\right)\wedge \exists x\in ℝ\exists y\in ℝ\forall j\in Z\left(y\le j\to F\left(j\right)\le x\right)\right)\right)$$
9		breq1	$$⊢y=k\to \left(y\le j\leftrightarrow k\le j\right)$$
10	9	anbi1d	$$⊢y=k\to \left(\left(y\le j\wedge x\le F\left(j\right)\right)\leftrightarrow \left(k\le j\wedge x\le F\left(j\right)\right)\right)$$
11	10	rexbidv	$$⊢y=k\to \left(\exists j\in Z\left(y\le j\wedge x\le F\left(j\right)\right)\leftrightarrow \exists j\in Z\left(k\le j\wedge x\le F\left(j\right)\right)\right)$$
12	11	cbvralvw	$$⊢\forall y\in ℝ\exists j\in Z\left(y\le j\wedge x\le F\left(j\right)\right)\leftrightarrow \forall k\in ℝ\exists j\in Z\left(k\le j\wedge x\le F\left(j\right)\right)$$
13	12	biimpi	$$⊢\forall y\in ℝ\exists j\in Z\left(y\le j\wedge x\le F\left(j\right)\right)\to \forall k\in ℝ\exists j\in Z\left(k\le j\wedge x\le F\left(j\right)\right)$$
14		nfra1	$$⊢Ⅎk\forall k\in ℝ\exists j\in Z\left(k\le j\wedge x\le F\left(j\right)\right)$$
15		simpr	$$⊢\left(\forall k\in ℝ\exists j\in Z\left(k\le j\wedge x\le F\left(j\right)\right)\wedge k\in Z\right)\to k\in Z$$
16	6 15	sselid	$$⊢\left(\forall k\in ℝ\exists j\in Z\left(k\le j\wedge x\le F\left(j\right)\right)\wedge k\in Z\right)\to k\in ℝ$$
17		rspa	$$⊢\left(\forall k\in ℝ\exists j\in Z\left(k\le j\wedge x\le F\left(j\right)\right)\wedge k\in ℝ\right)\to \exists j\in Z\left(k\le j\wedge x\le F\left(j\right)\right)$$
18	16 17	syldan	$$⊢\left(\forall k\in ℝ\exists j\in Z\left(k\le j\wedge x\le F\left(j\right)\right)\wedge k\in Z\right)\to \exists j\in Z\left(k\le j\wedge x\le F\left(j\right)\right)$$
19		nfv	$$⊢Ⅎjk\in Z$$
20		nfre1	$$⊢Ⅎj\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)$$
21		eqid	$$⊢{\mathbb{Z}}_{\ge k}={\mathbb{Z}}_{\ge k}$$
22	3	eluzelz2	$$⊢k\in Z\to k\in \mathbb{Z}$$
23	22	3ad2ant1	$$⊢\left(k\in Z\wedge j\in Z\wedge k\le j\right)\to k\in \mathbb{Z}$$
24	3	eluzelz2	$$⊢j\in Z\to j\in \mathbb{Z}$$
25	24	3ad2ant2	$$⊢\left(k\in Z\wedge j\in Z\wedge k\le j\right)\to j\in \mathbb{Z}$$
26		simp3	$$⊢\left(k\in Z\wedge j\in Z\wedge k\le j\right)\to k\le j$$
27	21 23 25 26	eluzd	$$⊢\left(k\in Z\wedge j\in Z\wedge k\le j\right)\to j\in {\mathbb{Z}}_{\ge k}$$
28	27	3adant3r	$$⊢\left(k\in Z\wedge j\in Z\wedge \left(k\le j\wedge x\le F\left(j\right)\right)\right)\to j\in {\mathbb{Z}}_{\ge k}$$
29		simp3r	$$⊢\left(k\in Z\wedge j\in Z\wedge \left(k\le j\wedge x\le F\left(j\right)\right)\right)\to x\le F\left(j\right)$$
30		rspe	$$⊢\left(j\in {\mathbb{Z}}_{\ge k}\wedge x\le F\left(j\right)\right)\to \exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)$$
31	28 29 30	syl2anc	$$⊢\left(k\in Z\wedge j\in Z\wedge \left(k\le j\wedge x\le F\left(j\right)\right)\right)\to \exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)$$
32	31	3exp	$$⊢k\in Z\to \left(j\in Z\to \left(\left(k\le j\wedge x\le F\left(j\right)\right)\to \exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)\right)$$
33	19 20 32	rexlimd	$$⊢k\in Z\to \left(\exists j\in Z\left(k\le j\wedge x\le F\left(j\right)\right)\to \exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)$$
34	33	imp	$$⊢\left(k\in Z\wedge \exists j\in Z\left(k\le j\wedge x\le F\left(j\right)\right)\right)\to \exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)$$
35	15 18 34	syl2anc	$$⊢\left(\forall k\in ℝ\exists j\in Z\left(k\le j\wedge x\le F\left(j\right)\right)\wedge k\in Z\right)\to \exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)$$
36	14 35	ralrimia	$$⊢\forall k\in ℝ\exists j\in Z\left(k\le j\wedge x\le F\left(j\right)\right)\to \forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)$$
37	13 36	syl	$$⊢\forall y\in ℝ\exists j\in Z\left(y\le j\wedge x\le F\left(j\right)\right)\to \forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)$$
38	37	a1i	$$⊢\phi \to \left(\forall y\in ℝ\exists j\in Z\left(y\le j\wedge x\le F\left(j\right)\right)\to \forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)$$
39		iftrue	$$⊢M\le ⌈y⌉\to if\left(M\le ⌈y⌉,⌈y⌉,M\right)=⌈y⌉$$
40	39	adantl	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge M\le ⌈y⌉\right)\to if\left(M\le ⌈y⌉,⌈y⌉,M\right)=⌈y⌉$$
41	2	ad2antrr	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge M\le ⌈y⌉\right)\to M\in \mathbb{Z}$$
42		ceilcl	$$⊢y\in ℝ\to ⌈y⌉\in \mathbb{Z}$$
43	42	ad2antlr	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge M\le ⌈y⌉\right)\to ⌈y⌉\in \mathbb{Z}$$
44		simpr	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge M\le ⌈y⌉\right)\to M\le ⌈y⌉$$
45	3 41 43 44	eluzd	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge M\le ⌈y⌉\right)\to ⌈y⌉\in Z$$
46	40 45	eqeltrd	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge M\le ⌈y⌉\right)\to if\left(M\le ⌈y⌉,⌈y⌉,M\right)\in Z$$
47		iffalse	$$⊢\neg M\le ⌈y⌉\to if\left(M\le ⌈y⌉,⌈y⌉,M\right)=M$$
48	47	adantl	$$⊢\left(\phi \wedge \neg M\le ⌈y⌉\right)\to if\left(M\le ⌈y⌉,⌈y⌉,M\right)=M$$
49	2 3	uzidd2	$$⊢\phi \to M\in Z$$
50	49	adantr	$$⊢\left(\phi \wedge \neg M\le ⌈y⌉\right)\to M\in Z$$
51	48 50	eqeltrd	$$⊢\left(\phi \wedge \neg M\le ⌈y⌉\right)\to if\left(M\le ⌈y⌉,⌈y⌉,M\right)\in Z$$
52	51	adantlr	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge \neg M\le ⌈y⌉\right)\to if\left(M\le ⌈y⌉,⌈y⌉,M\right)\in Z$$
53	46 52	pm2.61dan	$$⊢\left(\phi \wedge y\in ℝ\right)\to if\left(M\le ⌈y⌉,⌈y⌉,M\right)\in Z$$
54	53	adantlr	$$⊢\left(\left(\phi \wedge \forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)\wedge y\in ℝ\right)\to if\left(M\le ⌈y⌉,⌈y⌉,M\right)\in Z$$
55		simplr	$$⊢\left(\left(\phi \wedge \forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)\wedge y\in ℝ\right)\to \forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)$$
56		fveq2	$$⊢k=if\left(M\le ⌈y⌉,⌈y⌉,M\right)\to {\mathbb{Z}}_{\ge k}={\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}$$
57	56	rexeqdv	$$⊢k=if\left(M\le ⌈y⌉,⌈y⌉,M\right)\to \left(\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\leftrightarrow \exists j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}x\le F\left(j\right)\right)$$
58	57	rspcva	$$⊢\left(if\left(M\le ⌈y⌉,⌈y⌉,M\right)\in Z\wedge \forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)\to \exists j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}x\le F\left(j\right)$$
59	54 55 58	syl2anc	$$⊢\left(\left(\phi \wedge \forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)\wedge y\in ℝ\right)\to \exists j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}x\le F\left(j\right)$$
60		nfv	$$⊢Ⅎj\phi$$
61	19	nfci	$$⊢\underset{\_}{Ⅎ}jZ$$
62	61 20	nfralw	$$⊢Ⅎj\forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)$$
63	60 62	nfan	$$⊢Ⅎj\left(\phi \wedge \forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)$$
64		nfv	$$⊢Ⅎjy\in ℝ$$
65	63 64	nfan	$$⊢Ⅎj\left(\left(\phi \wedge \forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)\wedge y\in ℝ\right)$$
66		nfre1	$$⊢Ⅎj\exists j\in Z\left(y\le j\wedge x\le F\left(j\right)\right)$$
67	2	ad2antrr	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\right)\to M\in \mathbb{Z}$$
68		eluzelz	$$⊢j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\to j\in \mathbb{Z}$$
69	68	adantl	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\right)\to j\in \mathbb{Z}$$
70	67	zred	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\right)\to M\in ℝ$$
71	6 53	sselid	$$⊢\left(\phi \wedge y\in ℝ\right)\to if\left(M\le ⌈y⌉,⌈y⌉,M\right)\in ℝ$$
72	71	adantr	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\right)\to if\left(M\le ⌈y⌉,⌈y⌉,M\right)\in ℝ$$
73	69	zred	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\right)\to j\in ℝ$$
74	6 49	sselid	$$⊢\phi \to M\in ℝ$$
75	74	adantr	$$⊢\left(\phi \wedge y\in ℝ\right)\to M\in ℝ$$
76	42	zred	$$⊢y\in ℝ\to ⌈y⌉\in ℝ$$
77	76	adantl	$$⊢\left(\phi \wedge y\in ℝ\right)\to ⌈y⌉\in ℝ$$
78		max1	$$⊢\left(M\in ℝ\wedge ⌈y⌉\in ℝ\right)\to M\le if\left(M\le ⌈y⌉,⌈y⌉,M\right)$$
79	75 77 78	syl2anc	$$⊢\left(\phi \wedge y\in ℝ\right)\to M\le if\left(M\le ⌈y⌉,⌈y⌉,M\right)$$
80	79	adantr	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\right)\to M\le if\left(M\le ⌈y⌉,⌈y⌉,M\right)$$
81		eluzle	$$⊢j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\to if\left(M\le ⌈y⌉,⌈y⌉,M\right)\le j$$
82	81	adantl	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\right)\to if\left(M\le ⌈y⌉,⌈y⌉,M\right)\le j$$
83	70 72 73 80 82	letrd	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\right)\to M\le j$$
84	3 67 69 83	eluzd	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\right)\to j\in Z$$
85	84	3adant3	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\wedge x\le F\left(j\right)\right)\to j\in Z$$
86		simplr	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\right)\to y\in ℝ$$
87		simpr	$$⊢\left(\phi \wedge y\in ℝ\right)\to y\in ℝ$$
88		ceilge	$$⊢y\in ℝ\to y\le ⌈y⌉$$
89	88	adantl	$$⊢\left(\phi \wedge y\in ℝ\right)\to y\le ⌈y⌉$$
90		max2	$$⊢\left(M\in ℝ\wedge ⌈y⌉\in ℝ\right)\to ⌈y⌉\le if\left(M\le ⌈y⌉,⌈y⌉,M\right)$$
91	75 77 90	syl2anc	$$⊢\left(\phi \wedge y\in ℝ\right)\to ⌈y⌉\le if\left(M\le ⌈y⌉,⌈y⌉,M\right)$$
92	87 77 71 89 91	letrd	$$⊢\left(\phi \wedge y\in ℝ\right)\to y\le if\left(M\le ⌈y⌉,⌈y⌉,M\right)$$
93	92	adantr	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\right)\to y\le if\left(M\le ⌈y⌉,⌈y⌉,M\right)$$
94	86 72 73 93 82	letrd	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\right)\to y\le j$$
95	94	3adant3	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\wedge x\le F\left(j\right)\right)\to y\le j$$
96		simp3	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\wedge x\le F\left(j\right)\right)\to x\le F\left(j\right)$$
97	95 96	jca	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\wedge x\le F\left(j\right)\right)\to \left(y\le j\wedge x\le F\left(j\right)\right)$$
98		rspe	$$⊢\left(j\in Z\wedge \left(y\le j\wedge x\le F\left(j\right)\right)\right)\to \exists j\in Z\left(y\le j\wedge x\le F\left(j\right)\right)$$
99	85 97 98	syl2anc	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\wedge x\le F\left(j\right)\right)\to \exists j\in Z\left(y\le j\wedge x\le F\left(j\right)\right)$$
100	99	3exp	$$⊢\left(\phi \wedge y\in ℝ\right)\to \left(j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\to \left(x\le F\left(j\right)\to \exists j\in Z\left(y\le j\wedge x\le F\left(j\right)\right)\right)\right)$$
101	100	adantlr	$$⊢\left(\left(\phi \wedge \forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)\wedge y\in ℝ\right)\to \left(j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\to \left(x\le F\left(j\right)\to \exists j\in Z\left(y\le j\wedge x\le F\left(j\right)\right)\right)\right)$$
102	65 66 101	rexlimd	$$⊢\left(\left(\phi \wedge \forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)\wedge y\in ℝ\right)\to \left(\exists j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}x\le F\left(j\right)\to \exists j\in Z\left(y\le j\wedge x\le F\left(j\right)\right)\right)$$
103	59 102	mpd	$$⊢\left(\left(\phi \wedge \forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)\wedge y\in ℝ\right)\to \exists j\in Z\left(y\le j\wedge x\le F\left(j\right)\right)$$
104	103	ralrimiva	$$⊢\left(\phi \wedge \forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)\to \forall y\in ℝ\exists j\in Z\left(y\le j\wedge x\le F\left(j\right)\right)$$
105	104	ex	$$⊢\phi \to \left(\forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\to \forall y\in ℝ\exists j\in Z\left(y\le j\wedge x\le F\left(j\right)\right)\right)$$
106	38 105	impbid	$$⊢\phi \to \left(\forall y\in ℝ\exists j\in Z\left(y\le j\wedge x\le F\left(j\right)\right)\leftrightarrow \forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)$$
107	106	rexbidv	$$⊢\phi \to \left(\exists x\in ℝ\forall y\in ℝ\exists j\in Z\left(y\le j\wedge x\le F\left(j\right)\right)\leftrightarrow \exists x\in ℝ\forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)$$
108	53	adantr	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge \forall j\in Z\left(y\le j\to F\left(j\right)\le x\right)\right)\to if\left(M\le ⌈y⌉,⌈y⌉,M\right)\in Z$$
109	60 64	nfan	$$⊢Ⅎj\left(\phi \wedge y\in ℝ\right)$$
110		nfra1	$$⊢Ⅎj\forall j\in Z\left(y\le j\to F\left(j\right)\le x\right)$$
111	109 110	nfan	$$⊢Ⅎj\left(\left(\phi \wedge y\in ℝ\right)\wedge \forall j\in Z\left(y\le j\to F\left(j\right)\le x\right)\right)$$
112	94	adantlr	$$⊢\left(\left(\left(\phi \wedge y\in ℝ\right)\wedge \forall j\in Z\left(y\le j\to F\left(j\right)\le x\right)\right)\wedge j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\right)\to y\le j$$
113		simplr	$$⊢\left(\left(\left(\phi \wedge y\in ℝ\right)\wedge \forall j\in Z\left(y\le j\to F\left(j\right)\le x\right)\right)\wedge j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\right)\to \forall j\in Z\left(y\le j\to F\left(j\right)\le x\right)$$
114	84	adantlr	$$⊢\left(\left(\left(\phi \wedge y\in ℝ\right)\wedge \forall j\in Z\left(y\le j\to F\left(j\right)\le x\right)\right)\wedge j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\right)\to j\in Z$$
115		rspa	$$⊢\left(\forall j\in Z\left(y\le j\to F\left(j\right)\le x\right)\wedge j\in Z\right)\to \left(y\le j\to F\left(j\right)\le x\right)$$
116	113 114 115	syl2anc	$$⊢\left(\left(\left(\phi \wedge y\in ℝ\right)\wedge \forall j\in Z\left(y\le j\to F\left(j\right)\le x\right)\right)\wedge j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\right)\to \left(y\le j\to F\left(j\right)\le x\right)$$
117	112 116	mpd	$$⊢\left(\left(\left(\phi \wedge y\in ℝ\right)\wedge \forall j\in Z\left(y\le j\to F\left(j\right)\le x\right)\right)\wedge j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\right)\to F\left(j\right)\le x$$
118	117	ex	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge \forall j\in Z\left(y\le j\to F\left(j\right)\le x\right)\right)\to \left(j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}\to F\left(j\right)\le x\right)$$
119	111 118	ralrimi	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge \forall j\in Z\left(y\le j\to F\left(j\right)\le x\right)\right)\to \forall j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}F\left(j\right)\le x$$
120	56	raleqdv	$$⊢k=if\left(M\le ⌈y⌉,⌈y⌉,M\right)\to \left(\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\leftrightarrow \forall j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}F\left(j\right)\le x\right)$$
121	120	rspcev	$$⊢\left(if\left(M\le ⌈y⌉,⌈y⌉,M\right)\in Z\wedge \forall j\in {\mathbb{Z}}_{\ge if\left(M\le ⌈y⌉,⌈y⌉,M\right)}F\left(j\right)\le x\right)\to \exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x$$
122	108 119 121	syl2anc	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge \forall j\in Z\left(y\le j\to F\left(j\right)\le x\right)\right)\to \exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x$$
123	122	rexlimdva2	$$⊢\phi \to \left(\exists y\in ℝ\forall j\in Z\left(y\le j\to F\left(j\right)\le x\right)\to \exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)$$
124	6	sseli	$$⊢k\in Z\to k\in ℝ$$
125	124	ad2antlr	$$⊢\left(\left(\phi \wedge k\in Z\right)\wedge \forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)\to k\in ℝ$$
126		nfra1	$$⊢Ⅎj\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x$$
127	19 126	nfan	$$⊢Ⅎj\left(k\in Z\wedge \forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)$$
128		simp1r	$$⊢\left(\left(k\in Z\wedge \forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)\wedge j\in Z\wedge k\le j\right)\to \forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x$$
129	27	3adant1r	$$⊢\left(\left(k\in Z\wedge \forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)\wedge j\in Z\wedge k\le j\right)\to j\in {\mathbb{Z}}_{\ge k}$$
130		rspa	$$⊢\left(\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\wedge j\in {\mathbb{Z}}_{\ge k}\right)\to F\left(j\right)\le x$$
131	128 129 130	syl2anc	$$⊢\left(\left(k\in Z\wedge \forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)\wedge j\in Z\wedge k\le j\right)\to F\left(j\right)\le x$$
132	131	3exp	$$⊢\left(k\in Z\wedge \forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)\to \left(j\in Z\to \left(k\le j\to F\left(j\right)\le x\right)\right)$$
133	127 132	ralrimi	$$⊢\left(k\in Z\wedge \forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)\to \forall j\in Z\left(k\le j\to F\left(j\right)\le x\right)$$
134	133	adantll	$$⊢\left(\left(\phi \wedge k\in Z\right)\wedge \forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)\to \forall j\in Z\left(k\le j\to F\left(j\right)\le x\right)$$
135	9	rspceaimv	$$⊢\left(k\in ℝ\wedge \forall j\in Z\left(k\le j\to F\left(j\right)\le x\right)\right)\to \exists y\in ℝ\forall j\in Z\left(y\le j\to F\left(j\right)\le x\right)$$
136	125 134 135	syl2anc	$$⊢\left(\left(\phi \wedge k\in Z\right)\wedge \forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)\to \exists y\in ℝ\forall j\in Z\left(y\le j\to F\left(j\right)\le x\right)$$
137	136	rexlimdva2	$$⊢\phi \to \left(\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\to \exists y\in ℝ\forall j\in Z\left(y\le j\to F\left(j\right)\le x\right)\right)$$
138	123 137	impbid	$$⊢\phi \to \left(\exists y\in ℝ\forall j\in Z\left(y\le j\to F\left(j\right)\le x\right)\leftrightarrow \exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)$$
139	138	rexbidv	$$⊢\phi \to \left(\exists x\in ℝ\exists y\in ℝ\forall j\in Z\left(y\le j\to F\left(j\right)\le x\right)\leftrightarrow \exists x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)$$
140	107 139	anbi12d	$$⊢\phi \to \left(\left(\exists x\in ℝ\forall y\in ℝ\exists j\in Z\left(y\le j\wedge x\le F\left(j\right)\right)\wedge \exists x\in ℝ\exists y\in ℝ\forall j\in Z\left(y\le j\to F\left(j\right)\le x\right)\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)$$
141	8 140	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)$$