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	|- F/ x ph
	liminfvalxrmpt.2	|- ( ph -> A e. V )
	liminfvalxrmpt.3	|- ( ( ph /\ x e. A ) -> B e. RR* )
Assertion	liminfvalxrmpt	|- ( ph -> ( liminf ` ( x e. A |-> B ) ) = -e ( limsup ` ( x e. A |-> -e B ) ) )

Proof

Step	Hyp	Ref	Expression
1		liminfvalxrmpt.1	|- F/ x ph
2		liminfvalxrmpt.2	|- ( ph -> A e. V )
3		liminfvalxrmpt.3	|- ( ( ph /\ x e. A ) -> B e. RR* )
4		nfmpt1	|- F/_ x ( x e. A |-> B )
5	1 3	fmptd2f	|- ( ph -> ( x e. A |-> B ) : A --> RR* )
6	4 2 5	liminfvalxr	|- ( ph -> ( liminf ` ( x e. A |-> B ) ) = -e ( limsup ` ( x e. A |-> -e ( ( x e. A |-> B ) ` x ) ) ) )
7		eqidd	|- ( ph -> ( x e. A |-> B ) = ( x e. A |-> B ) )
8	7 3	fvmpt2d	|- ( ( ph /\ x e. A ) -> ( ( x e. A |-> B ) ` x ) = B )
9	8	xnegeqd	|- ( ( ph /\ x e. A ) -> -e ( ( x e. A |-> B ) ` x ) = -e B )
10	1 9	mpteq2da	|- ( ph -> ( x e. A |-> -e ( ( x e. A |-> B ) ` x ) ) = ( x e. A |-> -e B ) )
11	10	fveq2d	|- ( ph -> ( limsup ` ( x e. A |-> -e ( ( x e. A |-> B ) ` x ) ) ) = ( limsup ` ( x e. A |-> -e B ) ) )
12	11	xnegeqd	|- ( ph -> -e ( limsup ` ( x e. A |-> -e ( ( x e. A |-> B ) ` x ) ) ) = -e ( limsup ` ( x e. A |-> -e B ) ) )
13	6 12	eqtrd	|- ( ph -> ( liminf ` ( x e. A |-> B ) ) = -e ( limsup ` ( x e. A |-> -e B ) ) )