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