Metamath Proof Explorer

Theorem limsupval4

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

Ref Expression
Hypotheses limsupval4.x 
|- F/ x ph
limsupval4.a 
|- ( ph -> A e. V )
limsupval4.m 
|- ( ph -> M e. RR )
limsupval4.b 
|- ( ( ph /\ x e. ( A i^i ( M [,) +oo ) ) ) -> B e. RR* )
Assertion limsupval4 
|- ( ph -> ( limsup ` ( x e. A |-> B ) ) = -e ( liminf ` ( x e. A |-> -e B ) ) )

Proof

Step Hyp Ref Expression
1 limsupval4.x 
 |-  F/ x ph
2 limsupval4.a 
 |-  ( ph -> A e. V )
3 limsupval4.m 
 |-  ( ph -> M e. RR )
4 limsupval4.b 
 |-  ( ( ph /\ x e. ( A i^i ( M [,) +oo ) ) ) -> B e. RR* )
5 ovex 
 |-  ( M [,) +oo ) e. _V
6 5 inex2 
 |-  ( A i^i ( M [,) +oo ) ) e. _V
7 6 mptex 
 |-  ( x e. ( A i^i ( M [,) +oo ) ) |-> B ) e. _V
8 limsupcl 
 |-  ( ( x e. ( A i^i ( M [,) +oo ) ) |-> B ) e. _V -> ( limsup ` ( x e. ( A i^i ( M [,) +oo ) ) |-> B ) ) e. RR* )
9 7 8 ax-mp 
 |-  ( limsup ` ( x e. ( A i^i ( M [,) +oo ) ) |-> B ) ) e. RR*
10 9 a1i 
 |-  ( ph -> ( limsup ` ( x e. ( A i^i ( M [,) +oo ) ) |-> B ) ) e. RR* )
11 10 xnegnegd 
 |-  ( ph -> -e -e ( limsup ` ( x e. ( A i^i ( M [,) +oo ) ) |-> B ) ) = ( limsup ` ( x e. ( A i^i ( M [,) +oo ) ) |-> B ) ) )
12 11 eqcomd 
 |-  ( ph -> ( limsup ` ( x e. ( A i^i ( M [,) +oo ) ) |-> B ) ) = -e -e ( limsup ` ( x e. ( A i^i ( M [,) +oo ) ) |-> B ) ) )
13 eqid 
 |-  ( M [,) +oo ) = ( M [,) +oo )
14 2 3 13 limsupresicompt 
 |-  ( ph -> ( limsup ` ( x e. A |-> B ) ) = ( limsup ` ( x e. ( A i^i ( M [,) +oo ) ) |-> B ) ) )
15 4 xnegcld 
 |-  ( ( ph /\ x e. ( A i^i ( M [,) +oo ) ) ) -> -e B e. RR* )
16 1 2 3 15 liminfval3 
 |-  ( ph -> ( liminf ` ( x e. A |-> -e B ) ) = -e ( limsup ` ( x e. A |-> -e -e B ) ) )
17 2 3 13 limsupresicompt 
 |-  ( ph -> ( limsup ` ( x e. A |-> -e -e B ) ) = ( limsup ` ( x e. ( A i^i ( M [,) +oo ) ) |-> -e -e B ) ) )
18 4 xnegnegd 
 |-  ( ( ph /\ x e. ( A i^i ( M [,) +oo ) ) ) -> -e -e B = B )
19 1 18 mpteq2da 
 |-  ( ph -> ( x e. ( A i^i ( M [,) +oo ) ) |-> -e -e B ) = ( x e. ( A i^i ( M [,) +oo ) ) |-> B ) )
20 19 fveq2d 
 |-  ( ph -> ( limsup ` ( x e. ( A i^i ( M [,) +oo ) ) |-> -e -e B ) ) = ( limsup ` ( x e. ( A i^i ( M [,) +oo ) ) |-> B ) ) )
21 17 20 eqtrd 
 |-  ( ph -> ( limsup ` ( x e. A |-> -e -e B ) ) = ( limsup ` ( x e. ( A i^i ( M [,) +oo ) ) |-> B ) ) )
22 21 xnegeqd 
 |-  ( ph -> -e ( limsup ` ( x e. A |-> -e -e B ) ) = -e ( limsup ` ( x e. ( A i^i ( M [,) +oo ) ) |-> B ) ) )
23 16 22 eqtrd 
 |-  ( ph -> ( liminf ` ( x e. A |-> -e B ) ) = -e ( limsup ` ( x e. ( A i^i ( M [,) +oo ) ) |-> B ) ) )
24 23 xnegeqd 
 |-  ( ph -> -e ( liminf ` ( x e. A |-> -e B ) ) = -e -e ( limsup ` ( x e. ( A i^i ( M [,) +oo ) ) |-> B ) ) )
25 12 14 24 3eqtr4d 
 |-  ( ph -> ( limsup ` ( x e. A |-> B ) ) = -e ( liminf ` ( x e. A |-> -e B ) ) )