Metamath Proof Explorer

Theorem liminflbuz2

Description: A sequence with values in the extended reals, and with liminf that is not -oo , is eventually greater than -oo . (Contributed by Glauco Siliprandi, 23-Apr-2023)

Ref Expression
Hypotheses liminflbuz2.1 
|- F/ j ph
liminflbuz2.2 
|- F/_ j F
liminflbuz2.3 
|- ( ph -> M e. ZZ )
liminflbuz2.4 
|- Z = ( ZZ>= ` M )
liminflbuz2.5 
|- ( ph -> F : Z --> RR* )
liminflbuz2.6 
|- ( ph -> ( liminf ` F ) =/= -oo )
Assertion liminflbuz2 
|- ( ph -> E. k e. Z A. j e. ( ZZ>= ` k ) -oo < ( F ` j ) )

Proof

Step Hyp Ref Expression
1 liminflbuz2.1 
 |-  F/ j ph
2 liminflbuz2.2 
 |-  F/_ j F
3 liminflbuz2.3 
 |-  ( ph -> M e. ZZ )
4 liminflbuz2.4 
 |-  Z = ( ZZ>= ` M )
5 liminflbuz2.5 
 |-  ( ph -> F : Z --> RR* )
6 liminflbuz2.6 
 |-  ( ph -> ( liminf ` F ) =/= -oo )
7 nfv 
 |-  F/ j k e. Z
8 1 7 nfan 
 |-  F/ j ( ph /\ k e. Z )
9 simpll 
 |-  ( ( ( ph /\ k e. Z ) /\ j e. ( ZZ>= ` k ) ) -> ph )
10 4 uztrn2 
 |-  ( ( k e. Z /\ j e. ( ZZ>= ` k ) ) -> j e. Z )
11 10 adantll 
 |-  ( ( ( ph /\ k e. Z ) /\ j e. ( ZZ>= ` k ) ) -> j e. Z )
12 5 ffvelrnda 
 |-  ( ( ph /\ j e. Z ) -> ( F ` j ) e. RR* )
13 12 adantr 
 |-  ( ( ( ph /\ j e. Z ) /\ -. -oo < ( F ` j ) ) -> ( F ` j ) e. RR* )
14 mnfxr 
 |-  -oo e. RR*
15 14 a1i 
 |-  ( ( ( ph /\ j e. Z ) /\ -. -oo < ( F ` j ) ) -> -oo e. RR* )
16 simpr 
 |-  ( ( ( ph /\ j e. Z ) /\ -. -oo < ( F ` j ) ) -> -. -oo < ( F ` j ) )
17 13 15 16 xrnltled 
 |-  ( ( ( ph /\ j e. Z ) /\ -. -oo < ( F ` j ) ) -> ( F ` j ) <_ -oo )
18 xlemnf 
 |-  ( ( F ` j ) e. RR* -> ( ( F ` j ) <_ -oo <-> ( F ` j ) = -oo ) )
19 13 18 syl 
 |-  ( ( ( ph /\ j e. Z ) /\ -. -oo < ( F ` j ) ) -> ( ( F ` j ) <_ -oo <-> ( F ` j ) = -oo ) )
20 17 19 mpbid 
 |-  ( ( ( ph /\ j e. Z ) /\ -. -oo < ( F ` j ) ) -> ( F ` j ) = -oo )
21 xnegeq 
 |-  ( ( F ` j ) = -oo -> -e ( F ` j ) = -e -oo )
22 xnegmnf 
 |-  -e -oo = +oo
23 21 22 eqtrdi 
 |-  ( ( F ` j ) = -oo -> -e ( F ` j ) = +oo )
24 20 23 syl 
 |-  ( ( ( ph /\ j e. Z ) /\ -. -oo < ( F ` j ) ) -> -e ( F ` j ) = +oo )
25 24 adantlr 
 |-  ( ( ( ( ph /\ j e. Z ) /\ -e ( F ` j ) =/= +oo ) /\ -. -oo < ( F ` j ) ) -> -e ( F ` j ) = +oo )
26 neneq 
 |-  ( -e ( F ` j ) =/= +oo -> -. -e ( F ` j ) = +oo )
27 26 ad2antlr 
 |-  ( ( ( ( ph /\ j e. Z ) /\ -e ( F ` j ) =/= +oo ) /\ -. -oo < ( F ` j ) ) -> -. -e ( F ` j ) = +oo )
28 25 27 condan 
 |-  ( ( ( ph /\ j e. Z ) /\ -e ( F ` j ) =/= +oo ) -> -oo < ( F ` j ) )
29 28 ex 
 |-  ( ( ph /\ j e. Z ) -> ( -e ( F ` j ) =/= +oo -> -oo < ( F ` j ) ) )
30 9 11 29 syl2anc 
 |-  ( ( ( ph /\ k e. Z ) /\ j e. ( ZZ>= ` k ) ) -> ( -e ( F ` j ) =/= +oo -> -oo < ( F ` j ) ) )
31 8 30 ralimdaa 
 |-  ( ( ph /\ k e. Z ) -> ( A. j e. ( ZZ>= ` k ) -e ( F ` j ) =/= +oo -> A. j e. ( ZZ>= ` k ) -oo < ( F ` j ) ) )
32 31 imp 
 |-  ( ( ( ph /\ k e. Z ) /\ A. j e. ( ZZ>= ` k ) -e ( F ` j ) =/= +oo ) -> A. j e. ( ZZ>= ` k ) -oo < ( F ` j ) )
33 12 xnegcld 
 |-  ( ( ph /\ j e. Z ) -> -e ( F ` j ) e. RR* )
34 33 adantr 
 |-  ( ( ( ph /\ j e. Z ) /\ ( ( j e. Z |-> -e ( F ` j ) ) ` j ) < +oo ) -> -e ( F ` j ) e. RR* )
35 pnfxr 
 |-  +oo e. RR*
36 35 a1i 
 |-  ( ( ( ph /\ j e. Z ) /\ ( ( j e. Z |-> -e ( F ` j ) ) ` j ) < +oo ) -> +oo e. RR* )
37 eqidd 
 |-  ( ph -> ( j e. Z |-> -e ( F ` j ) ) = ( j e. Z |-> -e ( F ` j ) ) )
38 37 33 fvmpt2d 
 |-  ( ( ph /\ j e. Z ) -> ( ( j e. Z |-> -e ( F ` j ) ) ` j ) = -e ( F ` j ) )
39 38 adantr 
 |-  ( ( ( ph /\ j e. Z ) /\ ( ( j e. Z |-> -e ( F ` j ) ) ` j ) < +oo ) -> ( ( j e. Z |-> -e ( F ` j ) ) ` j ) = -e ( F ` j ) )
40 simpr 
 |-  ( ( ( ph /\ j e. Z ) /\ ( ( j e. Z |-> -e ( F ` j ) ) ` j ) < +oo ) -> ( ( j e. Z |-> -e ( F ` j ) ) ` j ) < +oo )
41 39 40 eqbrtrrd 
 |-  ( ( ( ph /\ j e. Z ) /\ ( ( j e. Z |-> -e ( F ` j ) ) ` j ) < +oo ) -> -e ( F ` j ) < +oo )
42 34 36 41 xrltned 
 |-  ( ( ( ph /\ j e. Z ) /\ ( ( j e. Z |-> -e ( F ` j ) ) ` j ) < +oo ) -> -e ( F ` j ) =/= +oo )
43 42 ex 
 |-  ( ( ph /\ j e. Z ) -> ( ( ( j e. Z |-> -e ( F ` j ) ) ` j ) < +oo -> -e ( F ` j ) =/= +oo ) )
44 9 11 43 syl2anc 
 |-  ( ( ( ph /\ k e. Z ) /\ j e. ( ZZ>= ` k ) ) -> ( ( ( j e. Z |-> -e ( F ` j ) ) ` j ) < +oo -> -e ( F ` j ) =/= +oo ) )
45 8 44 ralimdaa 
 |-  ( ( ph /\ k e. Z ) -> ( A. j e. ( ZZ>= ` k ) ( ( j e. Z |-> -e ( F ` j ) ) ` j ) < +oo -> A. j e. ( ZZ>= ` k ) -e ( F ` j ) =/= +oo ) )
46 45 imp 
 |-  ( ( ( ph /\ k e. Z ) /\ A. j e. ( ZZ>= ` k ) ( ( j e. Z |-> -e ( F ` j ) ) ` j ) < +oo ) -> A. j e. ( ZZ>= ` k ) -e ( F ` j ) =/= +oo )
47 nfmpt1 
 |-  F/_ j ( j e. Z |-> -e ( F ` j ) )
48 1 33 fmptd2f 
 |-  ( ph -> ( j e. Z |-> -e ( F ` j ) ) : Z --> RR* )
49 4 fvexi 
 |-  Z e. _V
50 49 a1i 
 |-  ( ph -> Z e. _V )
51 5 50 fexd 
 |-  ( ph -> F e. _V )
52 51 liminfcld 
 |-  ( ph -> ( liminf ` F ) e. RR* )
53 52 xnegnegd 
 |-  ( ph -> -e -e ( liminf ` F ) = ( liminf ` F ) )
54 1 2 3 4 5 liminfvaluz3 
 |-  ( ph -> ( liminf ` F ) = -e ( limsup ` ( j e. Z |-> -e ( F ` j ) ) ) )
55 53 54 eqtr2d 
 |-  ( ph -> -e ( limsup ` ( j e. Z |-> -e ( F ` j ) ) ) = -e -e ( liminf ` F ) )
56 50 mptexd 
 |-  ( ph -> ( j e. Z |-> -e ( F ` j ) ) e. _V )
57 56 limsupcld 
 |-  ( ph -> ( limsup ` ( j e. Z |-> -e ( F ` j ) ) ) e. RR* )
58 52 xnegcld 
 |-  ( ph -> -e ( liminf ` F ) e. RR* )
59 xneg11 
 |-  ( ( ( limsup ` ( j e. Z |-> -e ( F ` j ) ) ) e. RR* /\ -e ( liminf ` F ) e. RR* ) -> ( -e ( limsup ` ( j e. Z |-> -e ( F ` j ) ) ) = -e -e ( liminf ` F ) <-> ( limsup ` ( j e. Z |-> -e ( F ` j ) ) ) = -e ( liminf ` F ) ) )
60 57 58 59 syl2anc 
 |-  ( ph -> ( -e ( limsup ` ( j e. Z |-> -e ( F ` j ) ) ) = -e -e ( liminf ` F ) <-> ( limsup ` ( j e. Z |-> -e ( F ` j ) ) ) = -e ( liminf ` F ) ) )
61 55 60 mpbid 
 |-  ( ph -> ( limsup ` ( j e. Z |-> -e ( F ` j ) ) ) = -e ( liminf ` F ) )
62 nne 
 |-  ( -. -e ( liminf ` F ) =/= +oo <-> -e ( liminf ` F ) = +oo )
63 53 eqcomd 
 |-  ( ph -> ( liminf ` F ) = -e -e ( liminf ` F ) )
64 63 adantr 
 |-  ( ( ph /\ -e ( liminf ` F ) = +oo ) -> ( liminf ` F ) = -e -e ( liminf ` F ) )
65 xnegeq 
 |-  ( -e ( liminf ` F ) = +oo -> -e -e ( liminf ` F ) = -e +oo )
66 65 adantl 
 |-  ( ( ph /\ -e ( liminf ` F ) = +oo ) -> -e -e ( liminf ` F ) = -e +oo )
67 xnegpnf 
 |-  -e +oo = -oo
68 67 a1i 
 |-  ( ( ph /\ -e ( liminf ` F ) = +oo ) -> -e +oo = -oo )
69 64 66 68 3eqtrd 
 |-  ( ( ph /\ -e ( liminf ` F ) = +oo ) -> ( liminf ` F ) = -oo )
70 62 69 sylan2b 
 |-  ( ( ph /\ -. -e ( liminf ` F ) =/= +oo ) -> ( liminf ` F ) = -oo )
71 6 neneqd 
 |-  ( ph -> -. ( liminf ` F ) = -oo )
72 71 adantr 
 |-  ( ( ph /\ -. -e ( liminf ` F ) =/= +oo ) -> -. ( liminf ` F ) = -oo )
73 70 72 condan 
 |-  ( ph -> -e ( liminf ` F ) =/= +oo )
74 61 73 eqnetrd 
 |-  ( ph -> ( limsup ` ( j e. Z |-> -e ( F ` j ) ) ) =/= +oo )
75 1 47 3 4 48 74 limsupubuz2 
 |-  ( ph -> E. k e. Z A. j e. ( ZZ>= ` k ) ( ( j e. Z |-> -e ( F ` j ) ) ` j ) < +oo )
76 46 75 reximddv3 
 |-  ( ph -> E. k e. Z A. j e. ( ZZ>= ` k ) -e ( F ` j ) =/= +oo )
77 32 76 reximddv3 
 |-  ( ph -> E. k e. Z A. j e. ( ZZ>= ` k ) -oo < ( F ` j ) )