Metamath Proof Explorer

Theorem liminfpnfuz

Description: The inferior limit of a function is +oo if and only if every real number is the lower bound of the restriction of the function to a set of upper integers. (Contributed by Glauco Siliprandi, 23-Apr-2023)

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

Proof

Step Hyp Ref Expression
1 liminfpnfuz.1 
 |-  F/_ j F
2 liminfpnfuz.2 
 |-  ( ph -> M e. ZZ )
3 liminfpnfuz.3 
 |-  Z = ( ZZ>= ` M )
4 liminfpnfuz.4 
 |-  ( ph -> F : Z --> RR* )
5 nfv 
 |-  F/ l ph
6 nfcv 
 |-  F/_ l F
7 5 6 2 3 4 liminfvaluz3 
 |-  ( ph -> ( liminf ` F ) = -e ( limsup ` ( l e. Z |-> -e ( F ` l ) ) ) )
8 nfcv 
 |-  F/_ j l
9 1 8 nffv 
 |-  F/_ j ( F ` l )
10 9 nfxneg 
 |-  F/_ j -e ( F ` l )
11 nfcv 
 |-  F/_ l -e ( F ` j )
12 fveq2 
 |-  ( l = j -> ( F ` l ) = ( F ` j ) )
13 12 xnegeqd 
 |-  ( l = j -> -e ( F ` l ) = -e ( F ` j ) )
14 10 11 13 cbvmpt 
 |-  ( l e. Z |-> -e ( F ` l ) ) = ( j e. Z |-> -e ( F ` j ) )
15 14 fveq2i 
 |-  ( limsup ` ( l e. Z |-> -e ( F ` l ) ) ) = ( limsup ` ( j e. Z |-> -e ( F ` j ) ) )
16 15 xnegeqi 
 |-  -e ( limsup ` ( l e. Z |-> -e ( F ` l ) ) ) = -e ( limsup ` ( j e. Z |-> -e ( F ` j ) ) )
17 7 16 eqtrdi 
 |-  ( ph -> ( liminf ` F ) = -e ( limsup ` ( j e. Z |-> -e ( F ` j ) ) ) )
18 17 eqeq1d 
 |-  ( ph -> ( ( liminf ` F ) = +oo <-> -e ( limsup ` ( j e. Z |-> -e ( F ` j ) ) ) = +oo ) )
19 xnegmnf 
 |-  -e -oo = +oo
20 19 eqcomi 
 |-  +oo = -e -oo
21 20 a1i 
 |-  ( ph -> +oo = -e -oo )
22 21 eqeq2d 
 |-  ( ph -> ( -e ( limsup ` ( j e. Z |-> -e ( F ` j ) ) ) = +oo <-> -e ( limsup ` ( j e. Z |-> -e ( F ` j ) ) ) = -e -oo ) )
23 3 fvexi 
 |-  Z e. _V
24 23 mptex 
 |-  ( j e. Z |-> -e ( F ` j ) ) e. _V
25 24 a1i 
 |-  ( ph -> ( j e. Z |-> -e ( F ` j ) ) e. _V )
26 25 limsupcld 
 |-  ( ph -> ( limsup ` ( j e. Z |-> -e ( F ` j ) ) ) e. RR* )
27 mnfxr 
 |-  -oo e. RR*
28 xneg11 
 |-  ( ( ( limsup ` ( j e. Z |-> -e ( F ` j ) ) ) e. RR* /\ -oo e. RR* ) -> ( -e ( limsup ` ( j e. Z |-> -e ( F ` j ) ) ) = -e -oo <-> ( limsup ` ( j e. Z |-> -e ( F ` j ) ) ) = -oo ) )
29 26 27 28 sylancl 
 |-  ( ph -> ( -e ( limsup ` ( j e. Z |-> -e ( F ` j ) ) ) = -e -oo <-> ( limsup ` ( j e. Z |-> -e ( F ` j ) ) ) = -oo ) )
30 22 29 bitrd 
 |-  ( ph -> ( -e ( limsup ` ( j e. Z |-> -e ( F ` j ) ) ) = +oo <-> ( limsup ` ( j e. Z |-> -e ( F ` j ) ) ) = -oo ) )
31 3 uztrn2 
 |-  ( ( k e. Z /\ j e. ( ZZ>= ` k ) ) -> j e. Z )
32 xnegex 
 |-  -e ( F ` j ) e. _V
33 fvmpt4 
 |-  ( ( j e. Z /\ -e ( F ` j ) e. _V ) -> ( ( j e. Z |-> -e ( F ` j ) ) ` j ) = -e ( F ` j ) )
34 31 32 33 sylancl 
 |-  ( ( k e. Z /\ j e. ( ZZ>= ` k ) ) -> ( ( j e. Z |-> -e ( F ` j ) ) ` j ) = -e ( F ` j ) )
35 34 breq1d 
 |-  ( ( k e. Z /\ j e. ( ZZ>= ` k ) ) -> ( ( ( j e. Z |-> -e ( F ` j ) ) ` j ) <_ x <-> -e ( F ` j ) <_ x ) )
36 35 ralbidva 
 |-  ( k e. Z -> ( A. j e. ( ZZ>= ` k ) ( ( j e. Z |-> -e ( F ` j ) ) ` j ) <_ x <-> A. j e. ( ZZ>= ` k ) -e ( F ` j ) <_ x ) )
37 36 rexbiia 
 |-  ( E. k e. Z A. j e. ( ZZ>= ` k ) ( ( j e. Z |-> -e ( F ` j ) ) ` j ) <_ x <-> E. k e. Z A. j e. ( ZZ>= ` k ) -e ( F ` j ) <_ x )
38 37 ralbii 
 |-  ( A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( ( j e. Z |-> -e ( F ` j ) ) ` j ) <_ x <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) -e ( F ` j ) <_ x )
39 38 a1i 
 |-  ( ph -> ( A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( ( j e. Z |-> -e ( F ` j ) ) ` j ) <_ x <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) -e ( F ` j ) <_ x ) )
40 nfmpt1 
 |-  F/_ j ( j e. Z |-> -e ( F ` j ) )
41 4 ffvelcdmda 
 |-  ( ( ph /\ l e. Z ) -> ( F ` l ) e. RR* )
42 41 xnegcld 
 |-  ( ( ph /\ l e. Z ) -> -e ( F ` l ) e. RR* )
43 14 eqcomi 
 |-  ( j e. Z |-> -e ( F ` j ) ) = ( l e. Z |-> -e ( F ` l ) )
44 42 43 fmptd 
 |-  ( ph -> ( j e. Z |-> -e ( F ` j ) ) : Z --> RR* )
45 40 2 3 44 limsupmnfuz 
 |-  ( ph -> ( ( limsup ` ( j e. Z |-> -e ( F ` j ) ) ) = -oo <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( ( j e. Z |-> -e ( F ` j ) ) ` j ) <_ x ) )
46 1 3 4 xlimpnfxnegmnf 
 |-  ( ph -> ( A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) x <_ ( F ` j ) <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) -e ( F ` j ) <_ x ) )
47 39 45 46 3bitr4d 
 |-  ( ph -> ( ( limsup ` ( j e. Z |-> -e ( F ` j ) ) ) = -oo <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) )
48 18 30 47 3bitrd 
 |-  ( ph -> ( ( liminf ` F ) = +oo <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) )