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	$⊢ \underline{Ⅎ} j F$
	limsupre3uzlem.2	$⊢ φ \to M \in ℤ$
	limsupre3uzlem.3	$⊢ Z = ℤ_{\geq M}$
	limsupre3uzlem.4	$⊢ φ \to F : Z ⟶ ℝ^{*}$
Assertion	limsupre3uzlem	$⊢ φ \to (lim sup (F) \in ℝ \leftrightarrow (\exists x \in ℝ \forall k \in Z \exists j \in ℤ_{\geq k} x \leq F (j) \land \exists x \in ℝ \exists k \in Z \forall j \in ℤ_{\geq k} F (j) \leq x))$

Proof

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

Metamath Proof Explorer

Theorem limsupre3uzlem

Proof