This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐹 ) )