Metamath Proof Explorer

Theorem liminfreuzlem

Description: Given a function on the reals, its inferior limit is real if and only if two condition holds: 1. there is a real number that is greater than or equal to the function, infinitely often; 2. there is a real number that is smaller than or equal to the function. (Contributed by Glauco Siliprandi, 2-Jan-2022)

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

Proof

Step Hyp Ref Expression
1 liminfreuzlem.1 
 |-  F/_ j F
2 liminfreuzlem.2 
 |-  ( ph -> M e. ZZ )
3 liminfreuzlem.3 
 |-  Z = ( ZZ>= ` M )
4 liminfreuzlem.4 
 |-  ( ph -> F : Z --> RR )
5 nfv 
 |-  F/ j ph
6 5 1 2 3 4 liminfvaluz4 
 |-  ( ph -> ( liminf ` F ) = -e ( limsup ` ( j e. Z |-> -u ( F ` j ) ) ) )
7 6 eleq1d 
 |-  ( ph -> ( ( liminf ` F ) e. RR <-> -e ( limsup ` ( j e. Z |-> -u ( F ` j ) ) ) e. RR ) )
8 3 fvexi 
 |-  Z e. _V
9 8 mptex 
 |-  ( j e. Z |-> -u ( F ` j ) ) e. _V
10 limsupcl 
 |-  ( ( j e. Z |-> -u ( F ` j ) ) e. _V -> ( limsup ` ( j e. Z |-> -u ( F ` j ) ) ) e. RR* )
11 9 10 ax-mp 
 |-  ( limsup ` ( j e. Z |-> -u ( F ` j ) ) ) e. RR*
12 11 a1i 
 |-  ( ph -> ( limsup ` ( j e. Z |-> -u ( F ` j ) ) ) e. RR* )
13 12 xnegred 
 |-  ( ph -> ( ( limsup ` ( j e. Z |-> -u ( F ` j ) ) ) e. RR <-> -e ( limsup ` ( j e. Z |-> -u ( F ` j ) ) ) e. RR ) )
14 7 13 bitr4d 
 |-  ( ph -> ( ( liminf ` F ) e. RR <-> ( limsup ` ( j e. Z |-> -u ( F ` j ) ) ) e. RR ) )
15 4 ffvelrnda 
 |-  ( ( ph /\ j e. Z ) -> ( F ` j ) e. RR )
16 15 renegcld 
 |-  ( ( ph /\ j e. Z ) -> -u ( F ` j ) e. RR )
17 5 2 3 16 limsupreuzmpt 
 |-  ( ph -> ( ( limsup ` ( j e. Z |-> -u ( F ` j ) ) ) e. RR <-> ( E. y e. RR A. k e. Z E. j e. ( ZZ>= ` k ) y <_ -u ( F ` j ) /\ E. y e. RR A. j e. Z -u ( F ` j ) <_ y ) ) )
18 renegcl 
 |-  ( y e. RR -> -u y e. RR )
19 18 ad2antlr 
 |-  ( ( ( ph /\ y e. RR ) /\ A. k e. Z E. j e. ( ZZ>= ` k ) y <_ -u ( F ` j ) ) -> -u y e. RR )
20 simpllr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ k e. Z ) /\ j e. ( ZZ>= ` k ) ) -> y e. RR )
21 4 ad2antrr 
 |-  ( ( ( ph /\ k e. Z ) /\ j e. ( ZZ>= ` k ) ) -> F : Z --> RR )
22 3 uztrn2 
 |-  ( ( k e. Z /\ j e. ( ZZ>= ` k ) ) -> j e. Z )
23 22 adantll 
 |-  ( ( ( ph /\ k e. Z ) /\ j e. ( ZZ>= ` k ) ) -> j e. Z )
24 21 23 ffvelrnd 
 |-  ( ( ( ph /\ k e. Z ) /\ j e. ( ZZ>= ` k ) ) -> ( F ` j ) e. RR )
25 24 adantllr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ k e. Z ) /\ j e. ( ZZ>= ` k ) ) -> ( F ` j ) e. RR )
26 20 25 leneg2d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ k e. Z ) /\ j e. ( ZZ>= ` k ) ) -> ( y <_ -u ( F ` j ) <-> ( F ` j ) <_ -u y ) )
27 26 rexbidva 
 |-  ( ( ( ph /\ y e. RR ) /\ k e. Z ) -> ( E. j e. ( ZZ>= ` k ) y <_ -u ( F ` j ) <-> E. j e. ( ZZ>= ` k ) ( F ` j ) <_ -u y ) )
28 27 ralbidva 
 |-  ( ( ph /\ y e. RR ) -> ( A. k e. Z E. j e. ( ZZ>= ` k ) y <_ -u ( F ` j ) <-> A. k e. Z E. j e. ( ZZ>= ` k ) ( F ` j ) <_ -u y ) )
29 28 biimpd 
 |-  ( ( ph /\ y e. RR ) -> ( A. k e. Z E. j e. ( ZZ>= ` k ) y <_ -u ( F ` j ) -> A. k e. Z E. j e. ( ZZ>= ` k ) ( F ` j ) <_ -u y ) )
30 29 imp 
 |-  ( ( ( ph /\ y e. RR ) /\ A. k e. Z E. j e. ( ZZ>= ` k ) y <_ -u ( F ` j ) ) -> A. k e. Z E. j e. ( ZZ>= ` k ) ( F ` j ) <_ -u y )
31 breq2 
 |-  ( x = -u y -> ( ( F ` j ) <_ x <-> ( F ` j ) <_ -u y ) )
32 31 rexbidv 
 |-  ( x = -u y -> ( E. j e. ( ZZ>= ` k ) ( F ` j ) <_ x <-> E. j e. ( ZZ>= ` k ) ( F ` j ) <_ -u y ) )
33 32 ralbidv 
 |-  ( x = -u y -> ( A. k e. Z E. j e. ( ZZ>= ` k ) ( F ` j ) <_ x <-> A. k e. Z E. j e. ( ZZ>= ` k ) ( F ` j ) <_ -u y ) )
34 33 rspcev 
 |-  ( ( -u y e. RR /\ A. k e. Z E. j e. ( ZZ>= ` k ) ( F ` j ) <_ -u y ) -> E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) ( F ` j ) <_ x )
35 19 30 34 syl2anc 
 |-  ( ( ( ph /\ y e. RR ) /\ A. k e. Z E. j e. ( ZZ>= ` k ) y <_ -u ( F ` j ) ) -> E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) ( F ` j ) <_ x )
36 35 rexlimdva2 
 |-  ( ph -> ( E. y e. RR A. k e. Z E. j e. ( ZZ>= ` k ) y <_ -u ( F ` j ) -> E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
37 renegcl 
 |-  ( x e. RR -> -u x e. RR )
38 37 ad2antlr 
 |-  ( ( ( ph /\ x e. RR ) /\ A. k e. Z E. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) -> -u x e. RR )
39 24 adantllr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. Z ) /\ j e. ( ZZ>= ` k ) ) -> ( F ` j ) e. RR )
40 simpllr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. Z ) /\ j e. ( ZZ>= ` k ) ) -> x e. RR )
41 39 40 lenegd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. Z ) /\ j e. ( ZZ>= ` k ) ) -> ( ( F ` j ) <_ x <-> -u x <_ -u ( F ` j ) ) )
42 41 rexbidva 
 |-  ( ( ( ph /\ x e. RR ) /\ k e. Z ) -> ( E. j e. ( ZZ>= ` k ) ( F ` j ) <_ x <-> E. j e. ( ZZ>= ` k ) -u x <_ -u ( F ` j ) ) )
43 42 ralbidva 
 |-  ( ( ph /\ x e. RR ) -> ( A. k e. Z E. j e. ( ZZ>= ` k ) ( F ` j ) <_ x <-> A. k e. Z E. j e. ( ZZ>= ` k ) -u x <_ -u ( F ` j ) ) )
44 43 biimpd 
 |-  ( ( ph /\ x e. RR ) -> ( A. k e. Z E. j e. ( ZZ>= ` k ) ( F ` j ) <_ x -> A. k e. Z E. j e. ( ZZ>= ` k ) -u x <_ -u ( F ` j ) ) )
45 44 imp 
 |-  ( ( ( ph /\ x e. RR ) /\ A. k e. Z E. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) -> A. k e. Z E. j e. ( ZZ>= ` k ) -u x <_ -u ( F ` j ) )
46 breq1 
 |-  ( y = -u x -> ( y <_ -u ( F ` j ) <-> -u x <_ -u ( F ` j ) ) )
47 46 rexbidv 
 |-  ( y = -u x -> ( E. j e. ( ZZ>= ` k ) y <_ -u ( F ` j ) <-> E. j e. ( ZZ>= ` k ) -u x <_ -u ( F ` j ) ) )
48 47 ralbidv 
 |-  ( y = -u x -> ( A. k e. Z E. j e. ( ZZ>= ` k ) y <_ -u ( F ` j ) <-> A. k e. Z E. j e. ( ZZ>= ` k ) -u x <_ -u ( F ` j ) ) )
49 48 rspcev 
 |-  ( ( -u x e. RR /\ A. k e. Z E. j e. ( ZZ>= ` k ) -u x <_ -u ( F ` j ) ) -> E. y e. RR A. k e. Z E. j e. ( ZZ>= ` k ) y <_ -u ( F ` j ) )
50 38 45 49 syl2anc 
 |-  ( ( ( ph /\ x e. RR ) /\ A. k e. Z E. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) -> E. y e. RR A. k e. Z E. j e. ( ZZ>= ` k ) y <_ -u ( F ` j ) )
51 50 rexlimdva2 
 |-  ( ph -> ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) ( F ` j ) <_ x -> E. y e. RR A. k e. Z E. j e. ( ZZ>= ` k ) y <_ -u ( F ` j ) ) )
52 36 51 impbid 
 |-  ( ph -> ( E. y e. RR A. k e. Z E. j e. ( ZZ>= ` k ) y <_ -u ( F ` j ) <-> E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
53 18 ad2antlr 
 |-  ( ( ( ph /\ y e. RR ) /\ A. j e. Z -u ( F ` j ) <_ y ) -> -u y e. RR )
54 15 adantlr 
 |-  ( ( ( ph /\ y e. RR ) /\ j e. Z ) -> ( F ` j ) e. RR )
55 simplr 
 |-  ( ( ( ph /\ y e. RR ) /\ j e. Z ) -> y e. RR )
56 54 55 leneg3d 
 |-  ( ( ( ph /\ y e. RR ) /\ j e. Z ) -> ( -u ( F ` j ) <_ y <-> -u y <_ ( F ` j ) ) )
57 56 ralbidva 
 |-  ( ( ph /\ y e. RR ) -> ( A. j e. Z -u ( F ` j ) <_ y <-> A. j e. Z -u y <_ ( F ` j ) ) )
58 57 biimpd 
 |-  ( ( ph /\ y e. RR ) -> ( A. j e. Z -u ( F ` j ) <_ y -> A. j e. Z -u y <_ ( F ` j ) ) )
59 58 imp 
 |-  ( ( ( ph /\ y e. RR ) /\ A. j e. Z -u ( F ` j ) <_ y ) -> A. j e. Z -u y <_ ( F ` j ) )
60 breq1 
 |-  ( x = -u y -> ( x <_ ( F ` j ) <-> -u y <_ ( F ` j ) ) )
61 60 ralbidv 
 |-  ( x = -u y -> ( A. j e. Z x <_ ( F ` j ) <-> A. j e. Z -u y <_ ( F ` j ) ) )
62 61 rspcev 
 |-  ( ( -u y e. RR /\ A. j e. Z -u y <_ ( F ` j ) ) -> E. x e. RR A. j e. Z x <_ ( F ` j ) )
63 53 59 62 syl2anc 
 |-  ( ( ( ph /\ y e. RR ) /\ A. j e. Z -u ( F ` j ) <_ y ) -> E. x e. RR A. j e. Z x <_ ( F ` j ) )
64 63 rexlimdva2 
 |-  ( ph -> ( E. y e. RR A. j e. Z -u ( F ` j ) <_ y -> E. x e. RR A. j e. Z x <_ ( F ` j ) ) )
65 37 ad2antlr 
 |-  ( ( ( ph /\ x e. RR ) /\ A. j e. Z x <_ ( F ` j ) ) -> -u x e. RR )
66 simplr 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. Z ) -> x e. RR )
67 15 adantlr 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. Z ) -> ( F ` j ) e. RR )
68 66 67 lenegd 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. Z ) -> ( x <_ ( F ` j ) <-> -u ( F ` j ) <_ -u x ) )
69 68 ralbidva 
 |-  ( ( ph /\ x e. RR ) -> ( A. j e. Z x <_ ( F ` j ) <-> A. j e. Z -u ( F ` j ) <_ -u x ) )
70 69 biimpd 
 |-  ( ( ph /\ x e. RR ) -> ( A. j e. Z x <_ ( F ` j ) -> A. j e. Z -u ( F ` j ) <_ -u x ) )
71 70 imp 
 |-  ( ( ( ph /\ x e. RR ) /\ A. j e. Z x <_ ( F ` j ) ) -> A. j e. Z -u ( F ` j ) <_ -u x )
72 brralrspcev 
 |-  ( ( -u x e. RR /\ A. j e. Z -u ( F ` j ) <_ -u x ) -> E. y e. RR A. j e. Z -u ( F ` j ) <_ y )
73 65 71 72 syl2anc 
 |-  ( ( ( ph /\ x e. RR ) /\ A. j e. Z x <_ ( F ` j ) ) -> E. y e. RR A. j e. Z -u ( F ` j ) <_ y )
74 73 rexlimdva2 
 |-  ( ph -> ( E. x e. RR A. j e. Z x <_ ( F ` j ) -> E. y e. RR A. j e. Z -u ( F ` j ) <_ y ) )
75 64 74 impbid 
 |-  ( ph -> ( E. y e. RR A. j e. Z -u ( F ` j ) <_ y <-> E. x e. RR A. j e. Z x <_ ( F ` j ) ) )
76 52 75 anbi12d 
 |-  ( ph -> ( ( E. y e. RR A. k e. Z E. j e. ( ZZ>= ` k ) y <_ -u ( F ` j ) /\ E. y e. RR A. j e. Z -u ( F ` j ) <_ y ) <-> ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) ( F ` j ) <_ x /\ E. x e. RR A. j e. Z x <_ ( F ` j ) ) ) )
77 17 76 bitrd 
 |-  ( ph -> ( ( limsup ` ( j e. Z |-> -u ( F ` j ) ) ) e. RR <-> ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) ( F ` j ) <_ x /\ E. x e. RR A. j e. Z x <_ ( F ` j ) ) ) )
78 14 77 bitrd 
 |-  ( ph -> ( ( liminf ` F ) e. RR <-> ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) ( F ` j ) <_ x /\ E. x e. RR A. j e. Z x <_ ( F ` j ) ) ) )