This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	ffvelcdmda	\|- ( ( 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 ) ) ) )