Theorem liminfvaluz4

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	liminfvaluz4.1	|- F/ k ph
	liminfvaluz4.2	|- F/_ k F
	liminfvaluz4.3	|- ( ph -> M e. ZZ )
	liminfvaluz4.4	|- Z = ( ZZ>= ` M )
	liminfvaluz4.5	|- ( ph -> F : Z --> RR )
Assertion	liminfvaluz4	|- ( ph -> ( liminf ` F ) = -e ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		liminfvaluz4.1	|- F/ k ph
2		liminfvaluz4.2	|- F/_ k F
3		liminfvaluz4.3	|- ( ph -> M e. ZZ )
4		liminfvaluz4.4	|- Z = ( ZZ>= ` M )
5		liminfvaluz4.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	ffvelrnda	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
10	1 3 4 9	liminfvaluz2	|- ( ph -> ( liminf ` ( k e. Z |-> ( F ` k ) ) ) = -e ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) )
11	8 10	eqtrd	|- ( ph -> ( liminf ` F ) = -e ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) )