Theorem liminfvaluz3

Description: Alternate definition of liminf for an extended real-valued function, defined on a set of upper integers. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	liminfvaluz3.1	|- F/ k ph
	liminfvaluz3.2	|- F/_ k F
	liminfvaluz3.3	|- ( ph -> M e. ZZ )
	liminfvaluz3.4	|- Z = ( ZZ>= ` M )
	liminfvaluz3.5	|- ( ph -> F : Z --> RR* )
Assertion	liminfvaluz3	|- ( ph -> ( liminf ` F ) = -e ( limsup ` ( k e. Z |-> -e ( F ` k ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		liminfvaluz3.1	|- F/ k ph
2		liminfvaluz3.2	|- F/_ k F
3		liminfvaluz3.3	|- ( ph -> M e. ZZ )
4		liminfvaluz3.4	|- Z = ( ZZ>= ` M )
5		liminfvaluz3.5	|- ( ph -> F : Z --> RR* )
6		nfcv	|- F/_ k Z
7	6 2 5	feqmptdf	|- ( ph -> F = ( k e. Z |-> ( F ` k ) ) )
8	7	fveq2d	|- ( ph -> ( liminf ` F ) = ( liminf ` ( k e. Z |-> ( F ` k ) ) ) )
9	5	ffvelcdmda	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR* )
10	1 3 4 9	liminfvaluz	|- ( ph -> ( liminf ` ( k e. Z |-> ( F ` k ) ) ) = -e ( limsup ` ( k e. Z |-> -e ( F ` k ) ) ) )
11	8 10	eqtrd	|- ( ph -> ( liminf ` F ) = -e ( limsup ` ( k e. Z |-> -e ( F ` k ) ) ) )