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 
|- F/ k ph
limsupvaluz4.m 
|- ( ph -> M e. ZZ )
limsupvaluz4.z 
|- Z = ( ZZ>= ` M )
limsupvaluz4.b 
|- ( ( ph /\ k e. Z ) -> B e. RR )
Assertion limsupvaluz4 
|- ( ph -> ( limsup ` ( k e. Z |-> B ) ) = -e ( liminf ` ( k e. Z |-> -u B ) ) )

Proof

Step Hyp Ref Expression
1 limsupvaluz4.k 
 |-  F/ k ph
2 limsupvaluz4.m 
 |-  ( ph -> M e. ZZ )
3 limsupvaluz4.z 
 |-  Z = ( ZZ>= ` M )
4 limsupvaluz4.b 
 |-  ( ( ph /\ k e. Z ) -> B e. RR )
5 4 rexrd 
 |-  ( ( ph /\ k e. Z ) -> B e. RR* )
6 1 2 3 5 limsupvaluz3 
 |-  ( ph -> ( limsup ` ( k e. Z |-> B ) ) = -e ( liminf ` ( k e. Z |-> -e B ) ) )
7 4 rexnegd 
 |-  ( ( ph /\ k e. Z ) -> -e B = -u B )
8 1 7 mpteq2da 
 |-  ( ph -> ( k e. Z |-> -e B ) = ( k e. Z |-> -u B ) )
9 8 fveq2d 
 |-  ( ph -> ( liminf ` ( k e. Z |-> -e B ) ) = ( liminf ` ( k e. Z |-> -u B ) ) )
10 9 xnegeqd 
 |-  ( ph -> -e ( liminf ` ( k e. Z |-> -e B ) ) = -e ( liminf ` ( k e. Z |-> -u B ) ) )
11 6 10 eqtrd 
 |-  ( ph -> ( limsup ` ( k e. Z |-> B ) ) = -e ( liminf ` ( k e. Z |-> -u B ) ) )