Theorem liminfresre

Description: The inferior limit of a function only depends on the real part of its domain. (Contributed by Glauco Siliprandi, 2-Jan-2022)

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

Proof

Step	Hyp	Ref	Expression
1		liminfresre.1	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
3	2	resabs1i	⊢ ( ( 𝐹 ↾ ℝ ) ↾ ( 0 [,) +∞ ) ) = ( 𝐹 ↾ ( 0 [,) +∞ ) )
4	3	fveq2i	⊢ ( lim inf ‘ ( ( 𝐹 ↾ ℝ ) ↾ ( 0 [,) +∞ ) ) ) = ( lim inf ‘ ( 𝐹 ↾ ( 0 [,) +∞ ) ) )
5	4	a1i	⊢ ( 𝜑 → ( lim inf ‘ ( ( 𝐹 ↾ ℝ ) ↾ ( 0 [,) +∞ ) ) ) = ( lim inf ‘ ( 𝐹 ↾ ( 0 [,) +∞ ) ) ) )
6		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
7		eqid	⊢ ( 0 [,) +∞ ) = ( 0 [,) +∞ )
8	1	resexd	⊢ ( 𝜑 → ( 𝐹 ↾ ℝ ) ∈ V )
9	6 7 8	liminfresico	⊢ ( 𝜑 → ( lim inf ‘ ( ( 𝐹 ↾ ℝ ) ↾ ( 0 [,) +∞ ) ) ) = ( lim inf ‘ ( 𝐹 ↾ ℝ ) ) )
10	6 7 1	liminfresico	⊢ ( 𝜑 → ( lim inf ‘ ( 𝐹 ↾ ( 0 [,) +∞ ) ) ) = ( lim inf ‘ 𝐹 ) )
11	5 9 10	3eqtr3d	⊢ ( 𝜑 → ( lim inf ‘ ( 𝐹 ↾ ℝ ) ) = ( lim inf ‘ 𝐹 ) )