limsupresre

Description: The supremum limit of a function only depends on the real part of its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021)

		Ref	Expression
	Hypothesis	limsupresre.1	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	Assertion	limsupresre	⊢ ( 𝜑 → ( lim sup ‘ ( 𝐹 ↾ ℝ ) ) = ( lim sup ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		limsupresre.1	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2		id	⊢ ( 𝑘 ∈ ℝ → 𝑘 ∈ ℝ )
3		pnfxr	⊢ +∞ ∈ ℝ^*
4	3	a1i	⊢ ( 𝑘 ∈ ℝ → +∞ ∈ ℝ^* )
5		icossre	⊢ ( ( 𝑘 ∈ ℝ ∧ +∞ ∈ ℝ^* ) → ( 𝑘 [,) +∞ ) ⊆ ℝ )
6	2 4 5	syl2anc	⊢ ( 𝑘 ∈ ℝ → ( 𝑘 [,) +∞ ) ⊆ ℝ )
7		resima2	⊢ ( ( 𝑘 [,) +∞ ) ⊆ ℝ → ( ( 𝐹 ↾ ℝ ) “ ( 𝑘 [,) +∞ ) ) = ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
8	6 7	syl	⊢ ( 𝑘 ∈ ℝ → ( ( 𝐹 ↾ ℝ ) “ ( 𝑘 [,) +∞ ) ) = ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
9	8	ineq1d	⊢ ( 𝑘 ∈ ℝ → ( ( ( 𝐹 ↾ ℝ ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) = ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) )
10	9	supeq1d	⊢ ( 𝑘 ∈ ℝ → sup ( ( ( ( 𝐹 ↾ ℝ ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) = sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
11	10	mpteq2ia	⊢ ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝐹 ↾ ℝ ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
12	11	a1i	⊢ ( 𝜑 → ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝐹 ↾ ℝ ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) )
13	12	rneqd	⊢ ( 𝜑 → ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝐹 ↾ ℝ ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) = ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) )
14	13	infeq1d	⊢ ( 𝜑 → inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝐹 ↾ ℝ ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) , ℝ^* , < ) = inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) , ℝ^* , < ) )
15	1	resexd	⊢ ( 𝜑 → ( 𝐹 ↾ ℝ ) ∈ V )
16		eqid	⊢ ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝐹 ↾ ℝ ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) = ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝐹 ↾ ℝ ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
17	16	limsupval	⊢ ( ( 𝐹 ↾ ℝ ) ∈ V → ( lim sup ‘ ( 𝐹 ↾ ℝ ) ) = inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝐹 ↾ ℝ ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) , ℝ^* , < ) )
18	15 17	syl	⊢ ( 𝜑 → ( lim sup ‘ ( 𝐹 ↾ ℝ ) ) = inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝐹 ↾ ℝ ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) , ℝ^* , < ) )
19		eqid	⊢ ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
20	19	limsupval	⊢ ( 𝐹 ∈ 𝑉 → ( lim sup ‘ 𝐹 ) = inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) , ℝ^* , < ) )
21	1 20	syl	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) , ℝ^* , < ) )
22	14 18 21	3eqtr4d	⊢ ( 𝜑 → ( lim sup ‘ ( 𝐹 ↾ ℝ ) ) = ( lim sup ‘ 𝐹 ) )

Metamath Proof Explorer

Theorem limsupresre

Proof