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

Metamath Proof Explorer

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 ) ) )