Metamath Proof Explorer

Theorem liminfltlem

Description: Given a sequence of real numbers, there exists an upper part of the sequence that's approximated from above by the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses liminfltlem.m 
|- ( ph -> M e. ZZ )
liminfltlem.z 
|- Z = ( ZZ>= ` M )
liminfltlem.f 
|- ( ph -> F : Z --> RR )
liminfltlem.r 
|- ( ph -> ( liminf ` F ) e. RR )
liminfltlem.x 
|- ( ph -> X e. RR+ )
Assertion liminfltlem 
|- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( liminf ` F ) < ( ( F ` k ) + X ) )

Proof

Step Hyp Ref Expression
1 liminfltlem.m 
 |-  ( ph -> M e. ZZ )
2 liminfltlem.z 
 |-  Z = ( ZZ>= ` M )
3 liminfltlem.f 
 |-  ( ph -> F : Z --> RR )
4 liminfltlem.r 
 |-  ( ph -> ( liminf ` F ) e. RR )
5 liminfltlem.x 
 |-  ( ph -> X e. RR+ )
6 nfmpt1 
 |-  F/_ k ( k e. Z |-> -u ( F ` k ) )
7 3 ffvelrnda 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
8 7 renegcld 
 |-  ( ( ph /\ k e. Z ) -> -u ( F ` k ) e. RR )
9 8 fmpttd 
 |-  ( ph -> ( k e. Z |-> -u ( F ` k ) ) : Z --> RR )
10 2 fvexi 
 |-  Z e. _V
11 10 mptex 
 |-  ( k e. Z |-> -u ( F ` k ) ) e. _V
12 11 limsupcli 
 |-  ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) e. RR*
13 12 a1i 
 |-  ( ph -> ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) e. RR* )
14 nfv 
 |-  F/ k ph
15 nfcv 
 |-  F/_ k F
16 14 15 1 2 3 liminfvaluz4 
 |-  ( ph -> ( liminf ` F ) = -e ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) )
17 16 4 eqeltrrd 
 |-  ( ph -> -e ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) e. RR )
18 13 17 xnegrecl2d 
 |-  ( ph -> ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) e. RR )
19 6 1 2 9 18 5 limsupgt 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( ( k e. Z |-> -u ( F ` k ) ) ` k ) - X ) < ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) )
20 simpll 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ph )
21 2 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
22 21 adantll 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
23 negex 
 |-  -u ( F ` k ) e. _V
24 fvmpt4 
 |-  ( ( k e. Z /\ -u ( F ` k ) e. _V ) -> ( ( k e. Z |-> -u ( F ` k ) ) ` k ) = -u ( F ` k ) )
25 23 24 mpan2 
 |-  ( k e. Z -> ( ( k e. Z |-> -u ( F ` k ) ) ` k ) = -u ( F ` k ) )
26 25 adantl 
 |-  ( ( ph /\ k e. Z ) -> ( ( k e. Z |-> -u ( F ` k ) ) ` k ) = -u ( F ` k ) )
27 26 oveq1d 
 |-  ( ( ph /\ k e. Z ) -> ( ( ( k e. Z |-> -u ( F ` k ) ) ` k ) - X ) = ( -u ( F ` k ) - X ) )
28 7 recnd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
29 5 rpred 
 |-  ( ph -> X e. RR )
30 29 adantr 
 |-  ( ( ph /\ k e. Z ) -> X e. RR )
31 30 recnd 
 |-  ( ( ph /\ k e. Z ) -> X e. CC )
32 28 31 negdi2d 
 |-  ( ( ph /\ k e. Z ) -> -u ( ( F ` k ) + X ) = ( -u ( F ` k ) - X ) )
33 27 32 eqtr4d 
 |-  ( ( ph /\ k e. Z ) -> ( ( ( k e. Z |-> -u ( F ` k ) ) ` k ) - X ) = -u ( ( F ` k ) + X ) )
34 18 recnd 
 |-  ( ph -> ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) e. CC )
35 18 rexnegd 
 |-  ( ph -> -e ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) = -u ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) )
36 16 35 eqtr2d 
 |-  ( ph -> -u ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) = ( liminf ` F ) )
37 34 36 negcon1ad 
 |-  ( ph -> -u ( liminf ` F ) = ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) )
38 37 eqcomd 
 |-  ( ph -> ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) = -u ( liminf ` F ) )
39 38 adantr 
 |-  ( ( ph /\ k e. Z ) -> ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) = -u ( liminf ` F ) )
40 33 39 breq12d 
 |-  ( ( ph /\ k e. Z ) -> ( ( ( ( k e. Z |-> -u ( F ` k ) ) ` k ) - X ) < ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) <-> -u ( ( F ` k ) + X ) < -u ( liminf ` F ) ) )
41 4 adantr 
 |-  ( ( ph /\ k e. Z ) -> ( liminf ` F ) e. RR )
42 7 30 readdcld 
 |-  ( ( ph /\ k e. Z ) -> ( ( F ` k ) + X ) e. RR )
43 41 42 ltnegd 
 |-  ( ( ph /\ k e. Z ) -> ( ( liminf ` F ) < ( ( F ` k ) + X ) <-> -u ( ( F ` k ) + X ) < -u ( liminf ` F ) ) )
44 40 43 bitr4d 
 |-  ( ( ph /\ k e. Z ) -> ( ( ( ( k e. Z |-> -u ( F ` k ) ) ` k ) - X ) < ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) <-> ( liminf ` F ) < ( ( F ` k ) + X ) ) )
45 20 22 44 syl2anc 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( ( k e. Z |-> -u ( F ` k ) ) ` k ) - X ) < ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) <-> ( liminf ` F ) < ( ( F ` k ) + X ) ) )
46 45 ralbidva 
 |-  ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( ( ( k e. Z |-> -u ( F ` k ) ) ` k ) - X ) < ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) <-> A. k e. ( ZZ>= ` j ) ( liminf ` F ) < ( ( F ` k ) + X ) ) )
47 46 rexbidva 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( ( k e. Z |-> -u ( F ` k ) ) ` k ) - X ) < ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( liminf ` F ) < ( ( F ` k ) + X ) ) )
48 19 47 mpbid 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( liminf ` F ) < ( ( F ` k ) + X ) )