Theorem liminf0

Description: The inferior limit of the empty set. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Assertion	liminf0	|- ( liminf ` (/) ) = +oo

Proof

Step	Hyp	Ref	Expression
1		nftru	|- F/ x T.
2		0ex	|- (/) e. _V
3	2	a1i	|- ( T. -> (/) e. _V )
4		0red	|- ( T. -> 0 e. RR )
5		noel	|- -. x e. (/)
6		elinel1	|- ( x e. ( (/) i^i ( 0 [,) +oo ) ) -> x e. (/) )
7	6	con3i	|- ( -. x e. (/) -> -. x e. ( (/) i^i ( 0 [,) +oo ) ) )
8	5 7	ax-mp	|- -. x e. ( (/) i^i ( 0 [,) +oo ) )
9		pm2.21	|- ( -. x e. ( (/) i^i ( 0 [,) +oo ) ) -> ( x e. ( (/) i^i ( 0 [,) +oo ) ) -> ( (/) ` x ) e. RR* ) )
10	8 9	ax-mp	|- ( x e. ( (/) i^i ( 0 [,) +oo ) ) -> ( (/) ` x ) e. RR* )
11	10	adantl	|- ( ( T. /\ x e. ( (/) i^i ( 0 [,) +oo ) ) ) -> ( (/) ` x ) e. RR* )
12	1 3 4 11	liminfval3	|- ( T. -> ( liminf ` ( x e. (/) |-> ( (/) ` x ) ) ) = -e ( limsup ` ( x e. (/) |-> -e ( (/) ` x ) ) ) )
13	12	mptru	|- ( liminf ` ( x e. (/) |-> ( (/) ` x ) ) ) = -e ( limsup ` ( x e. (/) |-> -e ( (/) ` x ) ) )
14		mpt0	|- ( x e. (/) |-> ( (/) ` x ) ) = (/)
15	14	fveq2i	|- ( liminf ` ( x e. (/) |-> ( (/) ` x ) ) ) = ( liminf ` (/) )
16		mpt0	|- ( x e. (/) |-> -e ( (/) ` x ) ) = (/)
17	16	fveq2i	|- ( limsup ` ( x e. (/) |-> -e ( (/) ` x ) ) ) = ( limsup ` (/) )
18		limsup0	|- ( limsup ` (/) ) = -oo
19	17 18	eqtri	|- ( limsup ` ( x e. (/) |-> -e ( (/) ` x ) ) ) = -oo
20	19	xnegeqi	|- -e ( limsup ` ( x e. (/) |-> -e ( (/) ` x ) ) ) = -e -oo
21		xnegmnf	|- -e -oo = +oo
22	20 21	eqtri	|- -e ( limsup ` ( x e. (/) |-> -e ( (/) ` x ) ) ) = +oo
23	13 15 22	3eqtr3i	|- ( liminf ` (/) ) = +oo