limsupvaluz

Description: The superior limit, when the domain of the function is a set of upper integers (the first condition is needed, otherwise the l.h.s. would be -oo and the r.h.s. would be +oo ). (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		limsupvaluz.m	$⊢ φ \to M \in ℤ$
2		limsupvaluz.z	$⊢ Z = ℤ_{\geq M}$
3		limsupvaluz.f	$⊢ φ \to F : Z ⟶ ℝ^{*}$
4		eqid	$⊢ (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) = (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <))$
5	2	fvexi	$⊢ Z \in V$
6	5	a1i	$⊢ φ \to Z \in V$
7	3 6	fexd	$⊢ φ \to F \in V$
8		uzssre	$⊢ ℤ_{\geq M} \subseteq ℝ$
9	2 8	eqsstri	$⊢ Z \subseteq ℝ$
10	9	a1i	$⊢ φ \to Z \subseteq ℝ$
11	2	uzsup	$⊢ M \in ℤ \to sup (Z ℝ^{*} <) = +∞$
12	1 11	syl	$⊢ φ \to sup (Z ℝ^{*} <) = +∞$
13	4 7 10 12	limsupval2	$⊢ φ \to lim sup (F) = inf ((i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) [Z] ℝ^{*} <)$
14	10	mptimass	$⊢ φ \to (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) [Z] = ran (i \in Z ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <))$
15		oveq1	$⊢ i = n \to [i, +∞) = [n, +∞)$
16	15	imaeq2d	$⊢ i = n \to F [[i, +∞)] = F [[n, +∞)]$
17	16	ineq1d	$⊢ i = n \to F [[i, +∞)] \cap ℝ^{} = F [[n, +∞)] \cap ℝ^{}$
18	17	supeq1d	$⊢ i = n \to sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) = sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)$
19	18	cbvmptv	$⊢ (i \in Z ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) = (n \in Z ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <))$
20	19	a1i	$⊢ φ \to (i \in Z ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) = (n \in Z ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <))$
21		fimass	$⊢ F : Z ⟶ ℝ^{} \to F [[n, +∞)] \subseteq ℝ^{}$
22	3 21	syl	$⊢ φ \to F [[n, +∞)] \subseteq ℝ^{*}$
23		dfss2	$⊢ F [[n, +∞)] \subseteq ℝ^{} \leftrightarrow F [[n, +∞)] \cap ℝ^{} = F [[n, +∞)]$
24	23	biimpi	$⊢ F [[n, +∞)] \subseteq ℝ^{} \to F [[n, +∞)] \cap ℝ^{} = F [[n, +∞)]$
25	22 24	syl	$⊢ φ \to F [[n, +∞)] \cap ℝ^{*} = F [[n, +∞)]$
26	25	adantr	$⊢ (φ \land n \in Z) \to F [[n, +∞)] \cap ℝ^{*} = F [[n, +∞)]$
27		df-ima	$⊢ F [[n, +∞)] = ran ({F ↾}_{[n, +∞)})$
28	27	a1i	$⊢ (φ \land n \in Z) \to F [[n, +∞)] = ran ({F ↾}_{[n, +∞)})$
29	3	freld	$⊢ φ \to Rel F$
30		resindm	$⊢ Rel F \to {F ↾}_{([n, +∞) \cap dom F)} = {F ↾}_{[n, +∞)}$
31	29 30	syl	$⊢ φ \to {F ↾}_{([n, +∞) \cap dom F)} = {F ↾}_{[n, +∞)}$
32	31	adantr	$⊢ (φ \land n \in Z) \to {F ↾}_{([n, +∞) \cap dom F)} = {F ↾}_{[n, +∞)}$
33		incom	$⊢ [n, +∞) \cap Z = Z \cap [n, +∞)$
34	2	ineq1i	$⊢ Z \cap [n, +∞) = ℤ_{\geq M} \cap [n, +∞)$
35	33 34	eqtri	$⊢ [n, +∞) \cap Z = ℤ_{\geq M} \cap [n, +∞)$
36	35	a1i	$⊢ (φ \land n \in Z) \to [n, +∞) \cap Z = ℤ_{\geq M} \cap [n, +∞)$
37	3	fdmd	$⊢ φ \to dom F = Z$
38	37	ineq2d	$⊢ φ \to [n, +∞) \cap dom F = [n, +∞) \cap Z$
39	38	adantr	$⊢ (φ \land n \in Z) \to [n, +∞) \cap dom F = [n, +∞) \cap Z$
40	2	eleq2i	$⊢ n \in Z \leftrightarrow n \in ℤ_{\geq M}$
41	40	biimpi	$⊢ n \in Z \to n \in ℤ_{\geq M}$
42	41	adantl	$⊢ (φ \land n \in Z) \to n \in ℤ_{\geq M}$
43	42	uzinico2	$⊢ (φ \land n \in Z) \to ℤ_{\geq n} = ℤ_{\geq M} \cap [n, +∞)$
44	36 39 43	3eqtr4d	$⊢ (φ \land n \in Z) \to [n, +∞) \cap dom F = ℤ_{\geq n}$
45	44	reseq2d	$⊢ (φ \land n \in Z) \to {F ↾}_{([n, +∞) \cap dom F)} = {F ↾}_{ℤ_{\geq n}}$
46	32 45	eqtr3d	$⊢ (φ \land n \in Z) \to {F ↾}_{[n, +∞)} = {F ↾}_{ℤ_{\geq n}}$
47	46	rneqd	$⊢ (φ \land n \in Z) \to ran ({F ↾}_{[n, +∞)}) = ran ({F ↾}_{ℤ_{\geq n}})$
48	26 28 47	3eqtrd	$⊢ (φ \land n \in Z) \to F [[n, +∞)] \cap ℝ^{*} = ran ({F ↾}_{ℤ_{\geq n}})$
49	48	supeq1d	$⊢ (φ \land n \in Z) \to sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <)$
50	49	mpteq2dva	$⊢ φ \to (n \in Z ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) = (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <))$
51	20 50	eqtrd	$⊢ φ \to (i \in Z ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) = (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <))$
52	51	rneqd	$⊢ φ \to ran (i \in Z ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) = ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <))$
53	14 52	eqtrd	$⊢ φ \to (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) [Z] = ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <))$
54	53	infeq1d	$⊢ φ \to inf ((i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) [Z] ℝ^{} <) = inf (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) ℝ^{*} <)$
55		fveq2	$⊢ n = k \to ℤ_{\geq n} = ℤ_{\geq k}$
56	55	reseq2d	$⊢ n = k \to {F ↾}_{ℤ_{\geq n}} = {F ↾}_{ℤ_{\geq k}}$
57	56	rneqd	$⊢ n = k \to ran ({F ↾}_{ℤ_{\geq n}}) = ran ({F ↾}_{ℤ_{\geq k}})$
58	57	supeq1d	$⊢ n = k \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{} <)$
59	58	cbvmptv	$⊢ (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) = (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{} <))$
60	59	rneqi	$⊢ ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) = ran (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{} <))$
61	60	infeq1i	$⊢ inf (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) ℝ^{} <) = inf (ran (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{} <)) ℝ^{} <)$
62	61	a1i	$⊢ φ \to inf (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) ℝ^{} <) = inf (ran (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{} <)) ℝ^{} <)$
63	13 54 62	3eqtrd	$⊢ φ \to lim sup (F) = inf (ran (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{} <)) ℝ^{} <)$

Metamath Proof Explorer

Theorem limsupvaluz

Proof