supcnvlimsup

Description: If a function on a set of upper integers has a real superior limit, the supremum of the rightmost parts of the function, converges to that superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	supcnvlimsup.m	$⊢ φ \to M \in ℤ$
	supcnvlimsup.z	$⊢ Z = ℤ_{\geq M}$
	supcnvlimsup.f	$⊢ φ \to F : Z ⟶ ℝ$
	supcnvlimsup.r	$⊢ φ \to lim sup (F) \in ℝ$
Assertion	supcnvlimsup	$⊢ φ \to (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{*} <)) ⇝ lim sup (F)$

Proof

Step	Hyp	Ref	Expression
1		supcnvlimsup.m	$⊢ φ \to M \in ℤ$
2		supcnvlimsup.z	$⊢ Z = ℤ_{\geq M}$
3		supcnvlimsup.f	$⊢ φ \to F : Z ⟶ ℝ$
4		supcnvlimsup.r	$⊢ φ \to lim sup (F) \in ℝ$
5	3	adantr	$⊢ (φ \land n \in Z) \to F : Z ⟶ ℝ$
6		id	$⊢ n \in Z \to n \in Z$
7	2 6	uzssd2	$⊢ n \in Z \to ℤ_{\geq n} \subseteq Z$
8	7	adantl	$⊢ (φ \land n \in Z) \to ℤ_{\geq n} \subseteq Z$
9	5 8	feqresmpt	$⊢ (φ \land n \in Z) \to {F ↾}_{ℤ_{\geq n}} = (m \in ℤ_{\geq n} ⟼ F (m))$
10	9	rneqd	$⊢ (φ \land n \in Z) \to ran ({F ↾}_{ℤ_{\geq n}}) = ran (m \in ℤ_{\geq n} ⟼ F (m))$
11	10	supeq1d	$⊢ (φ \land n \in Z) \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran (m \in ℤ_{\geq n} ⟼ F (m)) ℝ^{} <)$
12		nfcv	$⊢ \underline{Ⅎ} m F$
13	4	renepnfd	$⊢ φ \to lim sup (F) \neq +∞$
14	12 2 3 13	limsupubuz	$⊢ φ \to \exists x \in ℝ \forall m \in Z F (m) \leq x$
15	14	adantr	$⊢ (φ \land n \in Z) \to \exists x \in ℝ \forall m \in Z F (m) \leq x$
16		ssralv	$⊢ ℤ_{\geq n} \subseteq Z \to (\forall m \in Z F (m) \leq x \to \forall m \in ℤ_{\geq n} F (m) \leq x)$
17	7 16	syl	$⊢ n \in Z \to (\forall m \in Z F (m) \leq x \to \forall m \in ℤ_{\geq n} F (m) \leq x)$
18	17	adantl	$⊢ (φ \land n \in Z) \to (\forall m \in Z F (m) \leq x \to \forall m \in ℤ_{\geq n} F (m) \leq x)$
19	18	reximdv	$⊢ (φ \land n \in Z) \to (\exists x \in ℝ \forall m \in Z F (m) \leq x \to \exists x \in ℝ \forall m \in ℤ_{\geq n} F (m) \leq x)$
20	15 19	mpd	$⊢ (φ \land n \in Z) \to \exists x \in ℝ \forall m \in ℤ_{\geq n} F (m) \leq x$
21		nfv	$⊢ Ⅎ m (φ \land n \in Z)$
22	2	eluzelz2	$⊢ n \in Z \to n \in ℤ$
23		uzid	$⊢ n \in ℤ \to n \in ℤ_{\geq n}$
24		ne0i	$⊢ n \in ℤ_{\geq n} \to ℤ_{\geq n} \neq \emptyset$
25	22 23 24	3syl	$⊢ n \in Z \to ℤ_{\geq n} \neq \emptyset$
26	25	adantl	$⊢ (φ \land n \in Z) \to ℤ_{\geq n} \neq \emptyset$
27	5	adantr	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to F : Z ⟶ ℝ$
28	8	sselda	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to m \in Z$
29	27 28	ffvelcdmd	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to F (m) \in ℝ$
30	21 26 29	supxrre3rnmpt	$⊢ (φ \land n \in Z) \to (sup (ran (m \in ℤ_{\geq n} ⟼ F (m)) ℝ^{*} <) \in ℝ \leftrightarrow \exists x \in ℝ \forall m \in ℤ_{\geq n} F (m) \leq x)$
31	20 30	mpbird	$⊢ (φ \land n \in Z) \to sup (ran (m \in ℤ_{\geq n} ⟼ F (m)) ℝ^{*} <) \in ℝ$
32	11 31	eqeltrd	$⊢ (φ \land n \in Z) \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <) \in ℝ$
33	32	fmpttd	$⊢ φ \to (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <)) : Z ⟶ ℝ$
34		eqid	$⊢ ℤ_{\geq i} = ℤ_{\geq i}$
35	2	eluzelz2	$⊢ i \in Z \to i \in ℤ$
36	35	peano2zd	$⊢ i \in Z \to i + 1 \in ℤ$
37	35	zred	$⊢ i \in Z \to i \in ℝ$
38		lep1	$⊢ i \in ℝ \to i \leq i + 1$
39	37 38	syl	$⊢ i \in Z \to i \leq i + 1$
40	34 35 36 39	eluzd	$⊢ i \in Z \to i + 1 \in ℤ_{\geq i}$
41		uzss	$⊢ i + 1 \in ℤ_{\geq i} \to ℤ_{\geq (i + 1)} \subseteq ℤ_{\geq i}$
42		ssres2	$⊢ ℤ_{\geq (i + 1)} \subseteq ℤ_{\geq i} \to {F ↾}_{ℤ_{\geq (i + 1)}} \subseteq {F ↾}_{ℤ_{\geq i}}$
43		rnss	$⊢ {F ↾}_{ℤ_{\geq (i + 1)}} \subseteq {F ↾}_{ℤ_{\geq i}} \to ran ({F ↾}_{ℤ_{\geq (i + 1)}}) \subseteq ran ({F ↾}_{ℤ_{\geq i}})$
44	40 41 42 43	4syl	$⊢ i \in Z \to ran ({F ↾}_{ℤ_{\geq (i + 1)}}) \subseteq ran ({F ↾}_{ℤ_{\geq i}})$
45	44	adantl	$⊢ (φ \land i \in Z) \to ran ({F ↾}_{ℤ_{\geq (i + 1)}}) \subseteq ran ({F ↾}_{ℤ_{\geq i}})$
46		rnresss	$⊢ ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ran F$
47	46	a1i	$⊢ (φ \land i \in Z) \to ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ran F$
48	3	frnd	$⊢ φ \to ran F \subseteq ℝ$
49	48	adantr	$⊢ (φ \land i \in Z) \to ran F \subseteq ℝ$
50	47 49	sstrd	$⊢ (φ \land i \in Z) \to ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ℝ$
51		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
52	51	a1i	$⊢ (φ \land i \in Z) \to ℝ \subseteq ℝ^{*}$
53	50 52	sstrd	$⊢ (φ \land i \in Z) \to ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ℝ^{*}$
54		supxrss	$⊢ (ran ({F ↾}_{ℤ_{\geq (i + 1)}}) \subseteq ran ({F ↾}_{ℤ_{\geq i}}) \land ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ℝ^{}) \to sup (ran ({F ↾}_{ℤ_{\geq (i + 1)}}) ℝ^{} <) \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <)$
55	45 53 54	syl2anc	$⊢ (φ \land i \in Z) \to sup (ran ({F ↾}_{ℤ_{\geq (i + 1)}}) ℝ^{} <) \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <)$
56		eqidd	$⊢ i \in Z \to (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) = (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <))$
57		fveq2	$⊢ n = i + 1 \to ℤ_{\geq n} = ℤ_{\geq (i + 1)}$
58	57	reseq2d	$⊢ n = i + 1 \to {F ↾}_{ℤ_{\geq n}} = {F ↾}_{ℤ_{\geq (i + 1)}}$
59	58	rneqd	$⊢ n = i + 1 \to ran ({F ↾}_{ℤ_{\geq n}}) = ran ({F ↾}_{ℤ_{\geq (i + 1)}})$
60	59	supeq1d	$⊢ n = i + 1 \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq (i + 1)}}) ℝ^{} <)$
61	60	adantl	$⊢ (i \in Z \land n = i + 1) \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq (i + 1)}}) ℝ^{} <)$
62	2	peano2uzs	$⊢ i \in Z \to i + 1 \in Z$
63		xrltso	$⊢ < Or ℝ^{*}$
64	63	supex	$⊢ sup (ran ({F ↾}_{ℤ_{\geq (i + 1)}}) ℝ^{*} <) \in V$
65	64	a1i	$⊢ i \in Z \to sup (ran ({F ↾}_{ℤ_{\geq (i + 1)}}) ℝ^{*} <) \in V$
66	56 61 62 65	fvmptd	$⊢ i \in Z \to (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) (i + 1) = sup (ran ({F ↾}_{ℤ_{\geq (i + 1)}}) ℝ^{} <)$
67	66	adantl	$⊢ (φ \land i \in Z) \to (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) (i + 1) = sup (ran ({F ↾}_{ℤ_{\geq (i + 1)}}) ℝ^{} <)$
68		fveq2	$⊢ n = i \to ℤ_{\geq n} = ℤ_{\geq i}$
69	68	reseq2d	$⊢ n = i \to {F ↾}_{ℤ_{\geq n}} = {F ↾}_{ℤ_{\geq i}}$
70	69	rneqd	$⊢ n = i \to ran ({F ↾}_{ℤ_{\geq n}}) = ran ({F ↾}_{ℤ_{\geq i}})$
71	70	supeq1d	$⊢ n = i \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <)$
72	71	adantl	$⊢ (i \in Z \land n = i) \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <)$
73		id	$⊢ i \in Z \to i \in Z$
74	63	supex	$⊢ sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <) \in V$
75	74	a1i	$⊢ i \in Z \to sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <) \in V$
76	56 72 73 75	fvmptd	$⊢ i \in Z \to (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) (i) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <)$
77	76	adantl	$⊢ (φ \land i \in Z) \to (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) (i) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <)$
78	67 77	breq12d	$⊢ (φ \land i \in Z) \to ((n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) (i + 1) \leq (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) (i) \leftrightarrow sup (ran ({F ↾}_{ℤ_{\geq (i + 1)}}) ℝ^{} <) \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <))$
79	55 78	mpbird	$⊢ (φ \land i \in Z) \to (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) (i + 1) \leq (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) (i)$
80		nfcv	$⊢ \underline{Ⅎ} j F$
81	3	frexr	$⊢ φ \to F : Z ⟶ ℝ^{*}$
82	80 1 2 81	limsupre3uz	$⊢ φ \to (lim sup (F) \in ℝ \leftrightarrow (\exists x \in ℝ \forall i \in Z \exists j \in ℤ_{\geq i} x \leq F (j) \land \exists x \in ℝ \exists i \in Z \forall j \in ℤ_{\geq i} F (j) \leq x))$
83	4 82	mpbid	$⊢ φ \to (\exists x \in ℝ \forall i \in Z \exists j \in ℤ_{\geq i} x \leq F (j) \land \exists x \in ℝ \exists i \in Z \forall j \in ℤ_{\geq i} F (j) \leq x)$
84	83	simpld	$⊢ φ \to \exists x \in ℝ \forall i \in Z \exists j \in ℤ_{\geq i} x \leq F (j)$
85		simp-4r	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to x \in ℝ$
86	85	rexrd	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to x \in ℝ^{*}$
87	81	3ad2ant1	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F : Z ⟶ ℝ^{*}$
88	2	uztrn2	$⊢ (i \in Z \land j \in ℤ_{\geq i}) \to j \in Z$
89	88	3adant1	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to j \in Z$
90	87 89	ffvelcdmd	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F (j) \in ℝ^{*}$
91	90	ad5ant134	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to F (j) \in ℝ^{*}$
92	53	supxrcld	$⊢ (φ \land i \in Z) \to sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) \in ℝ^{}$
93	92	ad5ant13	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) \in ℝ^{}$
94		simpr	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to x \leq F (j)$
95	53	3adant3	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ℝ^{*}$
96		fvres	$⊢ j \in ℤ_{\geq i} \to ({F ↾}_{ℤ_{\geq i}}) (j) = F (j)$
97	96	eqcomd	$⊢ j \in ℤ_{\geq i} \to F (j) = ({F ↾}_{ℤ_{\geq i}}) (j)$
98	97	3ad2ant3	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F (j) = ({F ↾}_{ℤ_{\geq i}}) (j)$
99	3	ffnd	$⊢ φ \to F Fn Z$
100	99	adantr	$⊢ (φ \land i \in Z) \to F Fn Z$
101	2 73	uzssd2	$⊢ i \in Z \to ℤ_{\geq i} \subseteq Z$
102	101	adantl	$⊢ (φ \land i \in Z) \to ℤ_{\geq i} \subseteq Z$
103		fnssres	$⊢ (F Fn Z \land ℤ_{\geq i} \subseteq Z) \to ({F ↾}_{ℤ_{\geq i}}) Fn ℤ_{\geq i}$
104	100 102 103	syl2anc	$⊢ (φ \land i \in Z) \to ({F ↾}_{ℤ_{\geq i}}) Fn ℤ_{\geq i}$
105	104	3adant3	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to ({F ↾}_{ℤ_{\geq i}}) Fn ℤ_{\geq i}$
106		simp3	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to j \in ℤ_{\geq i}$
107		fnfvelrn	$⊢ (({F ↾}_{ℤ_{\geq i}}) Fn ℤ_{\geq i} \land j \in ℤ_{\geq i}) \to ({F ↾}_{ℤ_{\geq i}}) (j) \in ran ({F ↾}_{ℤ_{\geq i}})$
108	105 106 107	syl2anc	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to ({F ↾}_{ℤ_{\geq i}}) (j) \in ran ({F ↾}_{ℤ_{\geq i}})$
109	98 108	eqeltrd	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F (j) \in ran ({F ↾}_{ℤ_{\geq i}})$
110		eqid	$⊢ sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <)$
111	95 109 110	supxrubd	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F (j) \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <)$
112	111	ad5ant134	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to F (j) \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <)$
113	86 91 93 94 112	xrletrd	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <)$
114	113	rexlimdva2	$⊢ ((φ \land x \in ℝ) \land i \in Z) \to (\exists j \in ℤ_{\geq i} x \leq F (j) \to x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <))$
115	114	ralimdva	$⊢ (φ \land x \in ℝ) \to (\forall i \in Z \exists j \in ℤ_{\geq i} x \leq F (j) \to \forall i \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <))$
116	115	reximdva	$⊢ φ \to (\exists x \in ℝ \forall i \in Z \exists j \in ℤ_{\geq i} x \leq F (j) \to \exists x \in ℝ \forall i \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <))$
117	84 116	mpd	$⊢ φ \to \exists x \in ℝ \forall i \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <)$
118		simpl	$⊢ (y = x \land i \in Z) \to y = x$
119	76	adantl	$⊢ (y = x \land i \in Z) \to (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) (i) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <)$
120	118 119	breq12d	$⊢ (y = x \land i \in Z) \to (y \leq (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) (i) \leftrightarrow x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <))$
121	120	ralbidva	$⊢ y = x \to (\forall i \in Z y \leq (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) (i) \leftrightarrow \forall i \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <))$
122	121	cbvrexvw	$⊢ \exists y \in ℝ \forall i \in Z y \leq (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) (i) \leftrightarrow \exists x \in ℝ \forall i \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <)$
123	117 122	sylibr	$⊢ φ \to \exists y \in ℝ \forall i \in Z y \leq (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <)) (i)$
124	2 1 33 79 123	climinf	$⊢ φ \to (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) ⇝ inf (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) ℝ <)$
125		fveq2	$⊢ n = k \to ℤ_{\geq n} = ℤ_{\geq k}$
126	125	reseq2d	$⊢ n = k \to {F ↾}_{ℤ_{\geq n}} = {F ↾}_{ℤ_{\geq k}}$
127	126	rneqd	$⊢ n = k \to ran ({F ↾}_{ℤ_{\geq n}}) = ran ({F ↾}_{ℤ_{\geq k}})$
128	127	supeq1d	$⊢ n = k \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{} <)$
129	128	cbvmptv	$⊢ (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) = (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{} <))$
130	129	a1i	$⊢ φ \to (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) = (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{} <))$
131	1 2 3 4	limsupvaluz2	$⊢ φ \to lim sup (F) = inf (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <)) ℝ <)$
132	131	eqcomd	$⊢ φ \to inf (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <)) ℝ <) = lim sup (F)$
133	130 132	breq12d	$⊢ φ \to ((n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) ⇝ inf (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) ℝ <) \leftrightarrow (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{*} <)) ⇝ lim sup (F))$
134	124 133	mpbid	$⊢ φ \to (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{*} <)) ⇝ lim sup (F)$

Metamath Proof Explorer

Theorem supcnvlimsup

Proof