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