Theorem liminfval3

Description: Alternate definition of liminf when the given function is eventually extended real-valued. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	liminfval3.x	|- F/ x ph
	liminfval3.a	|- ( ph -> A e. V )
	liminfval3.m	|- ( ph -> M e. RR )
	liminfval3.b	|- ( ( ph /\ x e. ( A i^i ( M [,) +oo ) ) ) -> B e. RR* )
Assertion	liminfval3	|- ( ph -> ( liminf ` ( x e. A |-> B ) ) = -e ( limsup ` ( x e. A |-> -e B ) ) )

Proof

Step	Hyp	Ref	Expression
1		liminfval3.x	|- F/ x ph
2		liminfval3.a	|- ( ph -> A e. V )
3		liminfval3.m	|- ( ph -> M e. RR )
4		liminfval3.b	|- ( ( ph /\ x e. ( A i^i ( M [,) +oo ) ) ) -> B e. RR* )
5		inss1	|- ( A i^i ( M [,) +oo ) ) C_ A
6	5	a1i	|- ( ph -> ( A i^i ( M [,) +oo ) ) C_ A )
7	2 6	ssexd	|- ( ph -> ( A i^i ( M [,) +oo ) ) e. _V )
8	1 7 4	liminfvalxrmpt	|- ( ph -> ( liminf ` ( x e. ( A i^i ( M [,) +oo ) ) |-> B ) ) = -e ( limsup ` ( x e. ( A i^i ( M [,) +oo ) ) |-> -e B ) ) )
9		eqid	|- ( M [,) +oo ) = ( M [,) +oo )
10	3 9 2	liminfresicompt	|- ( ph -> ( liminf ` ( x e. ( A i^i ( M [,) +oo ) ) |-> B ) ) = ( liminf ` ( x e. A |-> B ) ) )
11	10	eqcomd	|- ( ph -> ( liminf ` ( x e. A |-> B ) ) = ( liminf ` ( x e. ( A i^i ( M [,) +oo ) ) |-> B ) ) )
12	2 3 9	limsupresicompt	|- ( ph -> ( limsup ` ( x e. A |-> -e B ) ) = ( limsup ` ( x e. ( A i^i ( M [,) +oo ) ) |-> -e B ) ) )
13	12	xnegeqd	|- ( ph -> -e ( limsup ` ( x e. A |-> -e B ) ) = -e ( limsup ` ( x e. ( A i^i ( M [,) +oo ) ) |-> -e B ) ) )
14	8 11 13	3eqtr4d	|- ( ph -> ( liminf ` ( x e. A |-> B ) ) = -e ( limsup ` ( x e. A |-> -e B ) ) )