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	ffvelrnd	$⊢ ((φ \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	40 41	syl	$⊢ i \in Z \to ℤ_{\geq (i + 1)} \subseteq ℤ_{\geq i}$
43		ssres2	$⊢ ℤ_{\geq (i + 1)} \subseteq ℤ_{\geq i} \to {F ↾}_{ℤ_{\geq (i + 1)}} \subseteq {F ↾}_{ℤ_{\geq i}}$
44	42 43	syl	$⊢ i \in Z \to {F ↾}_{ℤ_{\geq (i + 1)}} \subseteq {F ↾}_{ℤ_{\geq i}}$
45		rnss	$⊢ {F ↾}_{ℤ_{\geq (i + 1)}} \subseteq {F ↾}_{ℤ_{\geq i}} \to ran ({F ↾}_{ℤ_{\geq (i + 1)}}) \subseteq ran ({F ↾}_{ℤ_{\geq i}})$
46	44 45	syl	$⊢ i \in Z \to ran ({F ↾}_{ℤ_{\geq (i + 1)}}) \subseteq ran ({F ↾}_{ℤ_{\geq i}})$
47	46	adantl	$⊢ (φ \land i \in Z) \to ran ({F ↾}_{ℤ_{\geq (i + 1)}}) \subseteq ran ({F ↾}_{ℤ_{\geq i}})$
48		rnresss	$⊢ ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ran F$
49	48	a1i	$⊢ (φ \land i \in Z) \to ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ran F$
50	3	frnd	$⊢ φ \to ran F \subseteq ℝ$
51	50	adantr	$⊢ (φ \land i \in Z) \to ran F \subseteq ℝ$
52	49 51	sstrd	$⊢ (φ \land i \in Z) \to ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ℝ$
53		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
54	53	a1i	$⊢ (φ \land i \in Z) \to ℝ \subseteq ℝ^{*}$
55	52 54	sstrd	$⊢ (φ \land i \in Z) \to ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ℝ^{*}$
56		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}}) ℝ^{*} <)$
57	47 55 56	syl2anc	$⊢ (φ \land i \in Z) \to sup (ran ({F ↾}_{ℤ_{\geq (i + 1)}}) ℝ^{} <) \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <)$
58		eqidd	$⊢ i \in Z \to (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) = (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <))$
59		fveq2	$⊢ n = i + 1 \to ℤ_{\geq n} = ℤ_{\geq (i + 1)}$
60	59	reseq2d	$⊢ n = i + 1 \to {F ↾}_{ℤ_{\geq n}} = {F ↾}_{ℤ_{\geq (i + 1)}}$
61	60	rneqd	$⊢ n = i + 1 \to ran ({F ↾}_{ℤ_{\geq n}}) = ran ({F ↾}_{ℤ_{\geq (i + 1)}})$
62	61	supeq1d	$⊢ n = i + 1 \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq (i + 1)}}) ℝ^{} <)$
63	62	adantl	$⊢ (i \in Z \land n = i + 1) \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq (i + 1)}}) ℝ^{} <)$
64	2	peano2uzs	$⊢ i \in Z \to i + 1 \in Z$
65		xrltso	$⊢ < Or ℝ^{*}$
66	65	supex	$⊢ sup (ran ({F ↾}_{ℤ_{\geq (i + 1)}}) ℝ^{*} <) \in V$
67	66	a1i	$⊢ i \in Z \to sup (ran ({F ↾}_{ℤ_{\geq (i + 1)}}) ℝ^{*} <) \in V$
68	58 63 64 67	fvmptd	$⊢ i \in Z \to (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) (i + 1) = sup (ran ({F ↾}_{ℤ_{\geq (i + 1)}}) ℝ^{} <)$
69	68	adantl	$⊢ (φ \land i \in Z) \to (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) (i + 1) = sup (ran ({F ↾}_{ℤ_{\geq (i + 1)}}) ℝ^{} <)$
70		fveq2	$⊢ n = i \to ℤ_{\geq n} = ℤ_{\geq i}$
71	70	reseq2d	$⊢ n = i \to {F ↾}_{ℤ_{\geq n}} = {F ↾}_{ℤ_{\geq i}}$
72	71	rneqd	$⊢ n = i \to ran ({F ↾}_{ℤ_{\geq n}}) = ran ({F ↾}_{ℤ_{\geq i}})$
73	72	supeq1d	$⊢ n = i \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <)$
74	73	adantl	$⊢ (i \in Z \land n = i) \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <)$
75		id	$⊢ i \in Z \to i \in Z$
76	65	supex	$⊢ sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <) \in V$
77	76	a1i	$⊢ i \in Z \to sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <) \in V$
78	58 74 75 77	fvmptd	$⊢ i \in Z \to (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) (i) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <)$
79	78	adantl	$⊢ (φ \land i \in Z) \to (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) (i) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <)$
80	69 79	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}}) ℝ^{} <))$
81	57 80	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)$
82		nfcv	$⊢ \underline{Ⅎ} j F$
83	3	frexr	$⊢ φ \to F : Z ⟶ ℝ^{*}$
84	82 1 2 83	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))$
85	4 84	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)$
86	85	simpld	$⊢ φ \to \exists x \in ℝ \forall i \in Z \exists j \in ℤ_{\geq i} x \leq F (j)$
87		simp-4r	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to x \in ℝ$
88	87	rexrd	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to x \in ℝ^{*}$
89	83	3ad2ant1	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F : Z ⟶ ℝ^{*}$
90	2	uztrn2	$⊢ (i \in Z \land j \in ℤ_{\geq i}) \to j \in Z$
91	90	3adant1	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to j \in Z$
92	89 91	ffvelrnd	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F (j) \in ℝ^{*}$
93	92	ad5ant134	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to F (j) \in ℝ^{*}$
94	55	supxrcld	$⊢ (φ \land i \in Z) \to sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) \in ℝ^{}$
95	94	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 ℝ^{}$
96		simpr	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to x \leq F (j)$
97	55	3adant3	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ℝ^{*}$
98		fvres	$⊢ j \in ℤ_{\geq i} \to ({F ↾}_{ℤ_{\geq i}}) (j) = F (j)$
99	98	eqcomd	$⊢ j \in ℤ_{\geq i} \to F (j) = ({F ↾}_{ℤ_{\geq i}}) (j)$
100	99	3ad2ant3	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F (j) = ({F ↾}_{ℤ_{\geq i}}) (j)$
101	3	ffnd	$⊢ φ \to F Fn Z$
102	101	adantr	$⊢ (φ \land i \in Z) \to F Fn Z$
103	2 75	uzssd2	$⊢ i \in Z \to ℤ_{\geq i} \subseteq Z$
104	103	adantl	$⊢ (φ \land i \in Z) \to ℤ_{\geq i} \subseteq Z$
105		fnssres	$⊢ (F Fn Z \land ℤ_{\geq i} \subseteq Z) \to ({F ↾}_{ℤ_{\geq i}}) Fn ℤ_{\geq i}$
106	102 104 105	syl2anc	$⊢ (φ \land i \in Z) \to ({F ↾}_{ℤ_{\geq i}}) Fn ℤ_{\geq i}$
107	106	3adant3	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to ({F ↾}_{ℤ_{\geq i}}) Fn ℤ_{\geq i}$
108		simp3	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to j \in ℤ_{\geq i}$
109		fnfvelrn	$⊢ (({F ↾}_{ℤ_{\geq i}}) Fn ℤ_{\geq i} \land j \in ℤ_{\geq i}) \to ({F ↾}_{ℤ_{\geq i}}) (j) \in ran ({F ↾}_{ℤ_{\geq i}})$
110	107 108 109	syl2anc	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to ({F ↾}_{ℤ_{\geq i}}) (j) \in ran ({F ↾}_{ℤ_{\geq i}})$
111	100 110	eqeltrd	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F (j) \in ran ({F ↾}_{ℤ_{\geq i}})$
112		eqid	$⊢ sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <)$
113	97 111 112	supxrubd	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F (j) \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <)$
114	113	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}}) ℝ^{*} <)$
115	88 93 95 96 114	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}}) ℝ^{*} <)$
116	115	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}}) ℝ^{*} <))$
117	116	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}}) ℝ^{*} <))$
118	117	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}}) ℝ^{*} <))$
119	86 118	mpd	$⊢ φ \to \exists x \in ℝ \forall i \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <)$
120		simpl	$⊢ (y = x \land i \in Z) \to y = x$
121	78	adantl	$⊢ (y = x \land i \in Z) \to (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) (i) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <)$
122	120 121	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}}) ℝ^{} <))$
123	122	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}}) ℝ^{} <))$
124	123	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}}) ℝ^{} <)$
125	119 124	sylibr	$⊢ φ \to \exists y \in ℝ \forall i \in Z y \leq (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <)) (i)$
126	2 1 33 81 125	climinf	$⊢ φ \to (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) ⇝ sup (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) ℝ <)$
127		fveq2	$⊢ n = k \to ℤ_{\geq n} = ℤ_{\geq k}$
128	127	reseq2d	$⊢ n = k \to {F ↾}_{ℤ_{\geq n}} = {F ↾}_{ℤ_{\geq k}}$
129	128	rneqd	$⊢ n = k \to ran ({F ↾}_{ℤ_{\geq n}}) = ran ({F ↾}_{ℤ_{\geq k}})$
130	129	supeq1d	$⊢ n = k \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{} <)$
131	130	cbvmptv	$⊢ (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) = (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{} <))$
132	131	a1i	$⊢ φ \to (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) = (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{} <))$
133	1 2 3 4	limsupvaluz2	$⊢ φ \to lim sup (F) = sup (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <)) ℝ <)$
134	133	eqcomd	$⊢ φ \to sup (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <)) ℝ <) = lim sup (F)$
135	132 134	breq12d	$⊢ φ \to ((n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) ⇝ sup (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) ℝ <) \leftrightarrow (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{*} <)) ⇝ lim sup (F))$
136	126 135	mpbid	$⊢ φ \to (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{*} <)) ⇝ lim sup (F)$

Metamath Proof Explorer

Theorem supcnvlimsup

Proof