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

Metamath Proof Explorer

Theorem limsupvaluz

Proof