Theorem liminfvaluz

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

Proof

Step	Hyp	Ref	Expression
1		liminfvaluz.k	|- F/ k ph
2		liminfvaluz.m	|- ( ph -> M e. ZZ )
3		liminfvaluz.z	|- Z = ( ZZ>= ` M )
4		liminfvaluz.b	|- ( ( ph /\ k e. Z ) -> B e. RR* )
5	3	fvexi	|- Z e. _V
6	5	a1i	|- ( ph -> Z e. _V )
7	2	zred	|- ( ph -> M e. RR )
8		simpr	|- ( ( ph /\ k e. ( Z i^i ( M [,) +oo ) ) ) -> k e. ( Z i^i ( M [,) +oo ) ) )
9	2 3	uzinico3	|- ( ph -> Z = ( Z i^i ( M [,) +oo ) ) )
10	9	eqcomd	|- ( ph -> ( Z i^i ( M [,) +oo ) ) = Z )
11	10	adantr	|- ( ( ph /\ k e. ( Z i^i ( M [,) +oo ) ) ) -> ( Z i^i ( M [,) +oo ) ) = Z )
12	8 11	eleqtrd	|- ( ( ph /\ k e. ( Z i^i ( M [,) +oo ) ) ) -> k e. Z )
13	12 4	syldan	|- ( ( ph /\ k e. ( Z i^i ( M [,) +oo ) ) ) -> B e. RR* )
14	1 6 7 13	liminfval3	|- ( ph -> ( liminf ` ( k e. Z |-> B ) ) = -e ( limsup ` ( k e. Z |-> -e B ) ) )