Theorem 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	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	limsupvaluz.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	limsupvaluz.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
Assertion	limsupvaluz	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) ) , ℝ* , < ) )

Proof

Step	Hyp	Ref	Expression
1		limsupvaluz.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		limsupvaluz.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		limsupvaluz.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
4		eqid	⊢ ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
5	2	fvexi	⊢ 𝑍 ∈ V
6	5	a1i	⊢ ( 𝜑 → 𝑍 ∈ V )
7	3 6	fexd	⊢ ( 𝜑 → 𝐹 ∈ V )
8	7	elexd	⊢ ( 𝜑 → 𝐹 ∈ V )
9		uzssre	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℝ
10	2 9	eqsstri	⊢ 𝑍 ⊆ ℝ
11	10	a1i	⊢ ( 𝜑 → 𝑍 ⊆ ℝ )
12	2	uzsup	⊢ ( 𝑀 ∈ ℤ → sup ( 𝑍 , ℝ* , < ) = +∞ )
13	1 12	syl	⊢ ( 𝜑 → sup ( 𝑍 , ℝ* , < ) = +∞ )
14	4 8 11 13	limsupval2	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ( ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) “ 𝑍 ) , ℝ* , < ) )
15	11	mptima2	⊢ ( 𝜑 → ( ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) “ 𝑍 ) = ran ( 𝑖 ∈ 𝑍 ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
16		oveq1	⊢ ( 𝑖 = 𝑛 → ( 𝑖 [,) +∞ ) = ( 𝑛 [,) +∞ ) )
17	16	imaeq2d	⊢ ( 𝑖 = 𝑛 → ( 𝐹 “ ( 𝑖 [,) +∞ ) ) = ( 𝐹 “ ( 𝑛 [,) +∞ ) ) )
18	17	ineq1d	⊢ ( 𝑖 = 𝑛 → ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) = ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) )
19	18	supeq1d	⊢ ( 𝑖 = 𝑛 → sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) = sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
20	19	cbvmptv	⊢ ( 𝑖 ∈ 𝑍 ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑛 ∈ 𝑍 ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
21	20	a1i	⊢ ( 𝜑 → ( 𝑖 ∈ 𝑍 ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑛 ∈ 𝑍 ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
22		fimass	⊢ ( 𝐹 : 𝑍 ⟶ ℝ* → ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ⊆ ℝ* )
23	3 22	syl	⊢ ( 𝜑 → ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ⊆ ℝ* )
24		df-ss	⊢ ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ⊆ ℝ* ↔ ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) = ( 𝐹 “ ( 𝑛 [,) +∞ ) ) )
25	24	biimpi	⊢ ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ⊆ ℝ* → ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) = ( 𝐹 “ ( 𝑛 [,) +∞ ) ) )
26	23 25	syl	⊢ ( 𝜑 → ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) = ( 𝐹 “ ( 𝑛 [,) +∞ ) ) )
27	26	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) = ( 𝐹 “ ( 𝑛 [,) +∞ ) ) )
28		df-ima	⊢ ( 𝐹 “ ( 𝑛 [,) +∞ ) ) = ran ( 𝐹 ↾ ( 𝑛 [,) +∞ ) )
29	28	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 “ ( 𝑛 [,) +∞ ) ) = ran ( 𝐹 ↾ ( 𝑛 [,) +∞ ) ) )
30	3	freld	⊢ ( 𝜑 → Rel 𝐹 )
31		resindm	⊢ ( Rel 𝐹 → ( 𝐹 ↾ ( ( 𝑛 [,) +∞ ) ∩ dom 𝐹 ) ) = ( 𝐹 ↾ ( 𝑛 [,) +∞ ) ) )
32	30 31	syl	⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝑛 [,) +∞ ) ∩ dom 𝐹 ) ) = ( 𝐹 ↾ ( 𝑛 [,) +∞ ) ) )
33	32	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ↾ ( ( 𝑛 [,) +∞ ) ∩ dom 𝐹 ) ) = ( 𝐹 ↾ ( 𝑛 [,) +∞ ) ) )
34		incom	⊢ ( ( 𝑛 [,) +∞ ) ∩ 𝑍 ) = ( 𝑍 ∩ ( 𝑛 [,) +∞ ) )
35	2	ineq1i	⊢ ( 𝑍 ∩ ( 𝑛 [,) +∞ ) ) = ( ( ℤ≥ ‘ 𝑀 ) ∩ ( 𝑛 [,) +∞ ) )
36	34 35	eqtri	⊢ ( ( 𝑛 [,) +∞ ) ∩ 𝑍 ) = ( ( ℤ≥ ‘ 𝑀 ) ∩ ( 𝑛 [,) +∞ ) )
37	36	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑛 [,) +∞ ) ∩ 𝑍 ) = ( ( ℤ≥ ‘ 𝑀 ) ∩ ( 𝑛 [,) +∞ ) ) )
38	3	fdmd	⊢ ( 𝜑 → dom 𝐹 = 𝑍 )
39	38	ineq2d	⊢ ( 𝜑 → ( ( 𝑛 [,) +∞ ) ∩ dom 𝐹 ) = ( ( 𝑛 [,) +∞ ) ∩ 𝑍 ) )
40	39	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑛 [,) +∞ ) ∩ dom 𝐹 ) = ( ( 𝑛 [,) +∞ ) ∩ 𝑍 ) )
41	2	eleq2i	⊢ ( 𝑛 ∈ 𝑍 ↔ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
42	41	biimpi	⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
43	42	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
44	43	uzinico2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ℤ≥ ‘ 𝑛 ) = ( ( ℤ≥ ‘ 𝑀 ) ∩ ( 𝑛 [,) +∞ ) ) )
45	37 40 44	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑛 [,) +∞ ) ∩ dom 𝐹 ) = ( ℤ≥ ‘ 𝑛 ) )
46	45	reseq2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ↾ ( ( 𝑛 [,) +∞ ) ∩ dom 𝐹 ) ) = ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) )
47	33 46	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ↾ ( 𝑛 [,) +∞ ) ) = ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) )
48	47	rneqd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ran ( 𝐹 ↾ ( 𝑛 [,) +∞ ) ) = ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) )
49	27 29 48	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) = ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) )
50	49	supeq1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) )
51	50	mpteq2dva	⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) )
52	21 51	eqtrd	⊢ ( 𝜑 → ( 𝑖 ∈ 𝑍 ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) )
53	52	rneqd	⊢ ( 𝜑 → ran ( 𝑖 ∈ 𝑍 ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) )
54	15 53	eqtrd	⊢ ( 𝜑 → ( ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) “ 𝑍 ) = ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) )
55	54	infeq1d	⊢ ( 𝜑 → inf ( ( ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) “ 𝑍 ) , ℝ* , < ) = inf ( ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) , ℝ* , < ) )
56		fveq2	⊢ ( 𝑛 = 𝑘 → ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑘 ) )
57	56	reseq2d	⊢ ( 𝑛 = 𝑘 → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) = ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) )
58	57	rneqd	⊢ ( 𝑛 = 𝑘 → ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) = ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) )
59	58	supeq1d	⊢ ( 𝑛 = 𝑘 → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) )
60	59	cbvmptv	⊢ ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) = ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) )
61	60	rneqi	⊢ ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) = ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) )
62	61	infeq1i	⊢ inf ( ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) , ℝ* , < ) = inf ( ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) ) , ℝ* , < )
63	62	a1i	⊢ ( 𝜑 → inf ( ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) , ℝ* , < ) = inf ( ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) ) , ℝ* , < ) )
64	14 55 63	3eqtrd	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) ) , ℝ* , < ) )