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	2	uzssre2	⊢ 𝑍 ⊆ ℝ
9	8	a1i	⊢ ( 𝜑 → 𝑍 ⊆ ℝ )
10	2	uzsup	⊢ ( 𝑀 ∈ ℤ → sup ( 𝑍 , ℝ* , < ) = +∞ )
11	1 10	syl	⊢ ( 𝜑 → sup ( 𝑍 , ℝ* , < ) = +∞ )
12	4 7 9 11	limsupval2	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ( ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) “ 𝑍 ) , ℝ* , < ) )
13	9	mptimass	⊢ ( 𝜑 → ( ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) “ 𝑍 ) = ran ( 𝑖 ∈ 𝑍 ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
14		oveq1	⊢ ( 𝑖 = 𝑛 → ( 𝑖 [,) +∞ ) = ( 𝑛 [,) +∞ ) )
15	14	imaeq2d	⊢ ( 𝑖 = 𝑛 → ( 𝐹 “ ( 𝑖 [,) +∞ ) ) = ( 𝐹 “ ( 𝑛 [,) +∞ ) ) )
16	15	ineq1d	⊢ ( 𝑖 = 𝑛 → ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) = ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) )
17	16	supeq1d	⊢ ( 𝑖 = 𝑛 → sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) = sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
18	17	cbvmptv	⊢ ( 𝑖 ∈ 𝑍 ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑛 ∈ 𝑍 ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
19	3	fimassd	⊢ ( 𝜑 → ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ⊆ ℝ* )
20		dfss2	⊢ ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ⊆ ℝ* ↔ ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) = ( 𝐹 “ ( 𝑛 [,) +∞ ) ) )
21	19 20	sylib	⊢ ( 𝜑 → ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) = ( 𝐹 “ ( 𝑛 [,) +∞ ) ) )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) = ( 𝐹 “ ( 𝑛 [,) +∞ ) ) )
23		df-ima	⊢ ( 𝐹 “ ( 𝑛 [,) +∞ ) ) = ran ( 𝐹 ↾ ( 𝑛 [,) +∞ ) )
24	23	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 “ ( 𝑛 [,) +∞ ) ) = ran ( 𝐹 ↾ ( 𝑛 [,) +∞ ) ) )
25		resindm	⊢ ( 𝐹 ↾ ( ( 𝑛 [,) +∞ ) ∩ dom 𝐹 ) ) = ( 𝐹 ↾ ( 𝑛 [,) +∞ ) )
26	2	ineq1i	⊢ ( 𝑍 ∩ ( 𝑛 [,) +∞ ) ) = ( ( ℤ≥ ‘ 𝑀 ) ∩ ( 𝑛 [,) +∞ ) )
27	26	ineqcomi	⊢ ( ( 𝑛 [,) +∞ ) ∩ 𝑍 ) = ( ( ℤ≥ ‘ 𝑀 ) ∩ ( 𝑛 [,) +∞ ) )
28	3	fdmd	⊢ ( 𝜑 → dom 𝐹 = 𝑍 )
29	28	ineq2d	⊢ ( 𝜑 → ( ( 𝑛 [,) +∞ ) ∩ dom 𝐹 ) = ( ( 𝑛 [,) +∞ ) ∩ 𝑍 ) )
30	29	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑛 [,) +∞ ) ∩ dom 𝐹 ) = ( ( 𝑛 [,) +∞ ) ∩ 𝑍 ) )
31	2	eleq2i	⊢ ( 𝑛 ∈ 𝑍 ↔ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
32	31	bilani	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
33	32	uzinico2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ℤ≥ ‘ 𝑛 ) = ( ( ℤ≥ ‘ 𝑀 ) ∩ ( 𝑛 [,) +∞ ) ) )
34	27 30 33	3eqtr4a	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑛 [,) +∞ ) ∩ dom 𝐹 ) = ( ℤ≥ ‘ 𝑛 ) )
35	34	reseq2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ↾ ( ( 𝑛 [,) +∞ ) ∩ dom 𝐹 ) ) = ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) )
36	25 35	eqtr3id	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ↾ ( 𝑛 [,) +∞ ) ) = ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) )
37	36	rneqd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ran ( 𝐹 ↾ ( 𝑛 [,) +∞ ) ) = ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) )
38	22 24 37	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) = ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) )
39	38	supeq1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) )
40	39	mpteq2dva	⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) )
41	18 40	eqtrid	⊢ ( 𝜑 → ( 𝑖 ∈ 𝑍 ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) )
42	41	rneqd	⊢ ( 𝜑 → ran ( 𝑖 ∈ 𝑍 ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) )
43	13 42	eqtrd	⊢ ( 𝜑 → ( ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) “ 𝑍 ) = ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) )
44	43	infeq1d	⊢ ( 𝜑 → inf ( ( ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) “ 𝑍 ) , ℝ* , < ) = inf ( ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) , ℝ* , < ) )
45		fveq2	⊢ ( 𝑛 = 𝑘 → ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑘 ) )
46	45	reseq2d	⊢ ( 𝑛 = 𝑘 → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) = ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) )
47	46	rneqd	⊢ ( 𝑛 = 𝑘 → ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) = ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) )
48	47	supeq1d	⊢ ( 𝑛 = 𝑘 → sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) )
49	48	cbvmptv	⊢ ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) = ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) )
50	49	rneqi	⊢ ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) = ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) )
51	50	infeq1i	⊢ inf ( ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) , ℝ* , < ) = inf ( ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) ) , ℝ* , < )
52	51	a1i	⊢ ( 𝜑 → inf ( ran ( 𝑛 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑛 ) ) , ℝ* , < ) ) , ℝ* , < ) = inf ( ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) ) , ℝ* , < ) )
53	12 44 52	3eqtrd	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) ) , ℝ* , < ) )