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

Metamath Proof Explorer

Theorem limsupvaluz4

Description: Alternate definition of liminf for a real-valued function, defined on a set of upper integers. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses limsupvaluz4.k ⊢ Ⅎ 𝑘 𝜑
limsupvaluz4.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
limsupvaluz4.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
limsupvaluz4.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
Assertion limsupvaluz4 ( 𝜑 → ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ) = -𝑒 ( lim inf ‘ ( 𝑘 ∈ 𝑍 ↦ - 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 limsupvaluz4.k ⊢ Ⅎ 𝑘 𝜑
2 limsupvaluz4.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 limsupvaluz4.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4 limsupvaluz4.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
5 4 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℝ* )
6 1 2 3 5 limsupvaluz3 ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ) = -𝑒 ( lim inf ‘ ( 𝑘 ∈ 𝑍 ↦ -𝑒 𝐵 ) ) )
7 4 rexnegd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → -𝑒 𝐵 = - 𝐵 )
8 1 7 mpteq2da ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ -𝑒 𝐵 ) = ( 𝑘 ∈ 𝑍 ↦ - 𝐵 ) )
9 8 fveq2d ⊢ ( 𝜑 → ( lim inf ‘ ( 𝑘 ∈ 𝑍 ↦ -𝑒 𝐵 ) ) = ( lim inf ‘ ( 𝑘 ∈ 𝑍 ↦ - 𝐵 ) ) )
10 9 xnegeqd ⊢ ( 𝜑 → -𝑒 ( lim inf ‘ ( 𝑘 ∈ 𝑍 ↦ -𝑒 𝐵 ) ) = -𝑒 ( lim inf ‘ ( 𝑘 ∈ 𝑍 ↦ - 𝐵 ) ) )
11 6 10 eqtrd ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ 𝐵 ) ) = -𝑒 ( lim inf ‘ ( 𝑘 ∈ 𝑍 ↦ - 𝐵 ) ) )