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 ⊢ φ → F ∈ V
Assertion liminfresre ⊢ φ → lim inf ⁡ F ↾ ℝ = lim inf ⁡ F

Proof

Step Hyp Ref Expression
1 liminfresre.1 ⊢ φ → F ∈ V
2 rge0ssre ⊢ 0 +∞ ⊆ ℝ
3 2 resabs1i ⊢ F ↾ ℝ ↾ 0 +∞ = F ↾ 0 +∞
4 3 fveq2i ⊢ lim inf ⁡ F ↾ ℝ ↾ 0 +∞ = lim inf ⁡ F ↾ 0 +∞
5 4 a1i ⊢ φ → lim inf ⁡ F ↾ ℝ ↾ 0 +∞ = lim inf ⁡ F ↾ 0 +∞
6 0red ⊢ φ → 0 ∈ ℝ
7 eqid ⊢ 0 +∞ = 0 +∞
8 1 resexd ⊢ φ → F ↾ ℝ ∈ V
9 6 7 8 liminfresico ⊢ φ → lim inf ⁡ F ↾ ℝ ↾ 0 +∞ = lim inf ⁡ F ↾ ℝ
10 6 7 1 liminfresico ⊢ φ → lim inf ⁡ F ↾ 0 +∞ = lim inf ⁡ F
11 5 9 10 3eqtr3d ⊢ φ → lim inf ⁡ F ↾ ℝ = lim inf ⁡ F