Theorem liminfvalxrmpt

Description: Alternate definition of liminf when F is an extended real-valued function. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	liminfvalxrmpt.1	⊢ Ⅎ 𝑥 𝜑
	liminfvalxrmpt.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	liminfvalxrmpt.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
Assertion	liminfvalxrmpt	⊢ ( 𝜑 → ( lim inf ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		liminfvalxrmpt.1	⊢ Ⅎ 𝑥 𝜑
2		liminfvalxrmpt.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		liminfvalxrmpt.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
4		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5	1 3	fmptd2f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℝ* )
6	4 2 5	liminfvalxr	⊢ ( 𝜑 → ( lim inf ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ) )
7		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
8	7 3	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
9	8	xnegeqd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → -𝑒 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = -𝑒 𝐵 )
10	1 9	mpteq2da	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ -𝑒 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) )
11	10	fveq2d	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ) = ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) )
12	11	xnegeqd	⊢ ( 𝜑 → -𝑒 ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) )
13	6 12	eqtrd	⊢ ( 𝜑 → ( lim inf ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) )