Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 limsupresre.1 ⊢ φ → F ∈ V
2 id ⊢ k ∈ ℝ → k ∈ ℝ
3 pnfxr ⊢ +∞ ∈ ℝ *
4 3 a1i ⊢ k ∈ ℝ → +∞ ∈ ℝ *
5 icossre ⊢ k ∈ ℝ ∧ +∞ ∈ ℝ * → k +∞ ⊆ ℝ
6 2 4 5 syl2anc ⊢ k ∈ ℝ → k +∞ ⊆ ℝ
7 resima2 ⊢ k +∞ ⊆ ℝ → F ↾ ℝ k +∞ = F k +∞
8 6 7 syl ⊢ k ∈ ℝ → F ↾ ℝ k +∞ = F k +∞
9 8 ineq1d ⊢ k ∈ ℝ → F ↾ ℝ k +∞ ∩ ℝ * = F k +∞ ∩ ℝ *
10 9 supeq1d ⊢ k ∈ ℝ → sup F ↾ ℝ k +∞ ∩ ℝ * ℝ * < = sup F k +∞ ∩ ℝ * ℝ * <
11 10 mpteq2ia ⊢ k ∈ ℝ ⟼ sup F ↾ ℝ k +∞ ∩ ℝ * ℝ * < = k ∈ ℝ ⟼ sup F k +∞ ∩ ℝ * ℝ * <
12 11 a1i ⊢ φ → k ∈ ℝ ⟼ sup F ↾ ℝ k +∞ ∩ ℝ * ℝ * < = k ∈ ℝ ⟼ sup F k +∞ ∩ ℝ * ℝ * <
13 12 rneqd ⊢ φ → ran ⁡ k ∈ ℝ ⟼ sup F ↾ ℝ k +∞ ∩ ℝ * ℝ * < = ran ⁡ k ∈ ℝ ⟼ sup F k +∞ ∩ ℝ * ℝ * <
14 13 infeq1d ⊢ φ → inf ran ⁡ k ∈ ℝ ⟼ sup F ↾ ℝ k +∞ ∩ ℝ * ℝ * < ℝ * < = inf ran ⁡ k ∈ ℝ ⟼ sup F k +∞ ∩ ℝ * ℝ * < ℝ * <
15 1 resexd ⊢ φ → F ↾ ℝ ∈ V
16 eqid ⊢ k ∈ ℝ ⟼ sup F ↾ ℝ k +∞ ∩ ℝ * ℝ * < = k ∈ ℝ ⟼ sup F ↾ ℝ k +∞ ∩ ℝ * ℝ * <
17 16 limsupval ⊢ F ↾ ℝ ∈ V → lim sup ⁡ F ↾ ℝ = inf ran ⁡ k ∈ ℝ ⟼ sup F ↾ ℝ k +∞ ∩ ℝ * ℝ * < ℝ * <
18 15 17 syl ⊢ φ → lim sup ⁡ F ↾ ℝ = inf ran ⁡ k ∈ ℝ ⟼ sup F ↾ ℝ k +∞ ∩ ℝ * ℝ * < ℝ * <
19 eqid ⊢ k ∈ ℝ ⟼ sup F k +∞ ∩ ℝ * ℝ * < = k ∈ ℝ ⟼ sup F k +∞ ∩ ℝ * ℝ * <
20 19 limsupval ⊢ F ∈ V → lim sup ⁡ F = inf ran ⁡ k ∈ ℝ ⟼ sup F k +∞ ∩ ℝ * ℝ * < ℝ * <
21 1 20 syl ⊢ φ → lim sup ⁡ F = inf ran ⁡ k ∈ ℝ ⟼ sup F k +∞ ∩ ℝ * ℝ * < ℝ * <
22 14 18 21 3eqtr4d ⊢ φ → lim sup ⁡ F ↾ ℝ = lim sup ⁡ F