Metamath Proof Explorer

Theorem liminflimsupclim

Description: A sequence of real numbers converges if its inferior limit is real, and it is greater than or equal to the superior limit (in such a case, they are actually equal, see liminflelimsupuz ). (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses liminflimsupclim.1 
|- ( ph -> M e. ZZ )
liminflimsupclim.2 
|- Z = ( ZZ>= ` M )
liminflimsupclim.3 
|- ( ph -> F : Z --> RR )
liminflimsupclim.4 
|- ( ph -> ( liminf ` F ) e. RR )
liminflimsupclim.5 
|- ( ph -> ( limsup ` F ) <_ ( liminf ` F ) )
Assertion liminflimsupclim 
|- ( ph -> F e. dom ~~> )

Proof

Step Hyp Ref Expression
1 liminflimsupclim.1 
 |-  ( ph -> M e. ZZ )
2 liminflimsupclim.2 
 |-  Z = ( ZZ>= ` M )
3 liminflimsupclim.3 
 |-  ( ph -> F : Z --> RR )
4 liminflimsupclim.4 
 |-  ( ph -> ( liminf ` F ) e. RR )
5 liminflimsupclim.5 
 |-  ( ph -> ( limsup ` F ) <_ ( liminf ` F ) )
6 climrel 
 |-  Rel ~~>
7 6 a1i 
 |-  ( ph -> Rel ~~> )
8 2 fvexi 
 |-  Z e. _V
9 8 a1i 
 |-  ( ph -> Z e. _V )
10 3 9 fexd 
 |-  ( ph -> F e. _V )
11 10 limsupcld 
 |-  ( ph -> ( limsup ` F ) e. RR* )
12 4 rexrd 
 |-  ( ph -> ( liminf ` F ) e. RR* )
13 3 frexr 
 |-  ( ph -> F : Z --> RR* )
14 1 2 13 liminflelimsupuz 
 |-  ( ph -> ( liminf ` F ) <_ ( limsup ` F ) )
15 11 12 5 14 xrletrid 
 |-  ( ph -> ( limsup ` F ) = ( liminf ` F ) )
16 15 4 eqeltrd 
 |-  ( ph -> ( limsup ` F ) e. RR )
17 16 recnd 
 |-  ( ph -> ( limsup ` F ) e. CC )
18 nfcv 
 |-  F/_ k F
19 1 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> M e. ZZ )
20 3 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> F : Z --> RR )
21 4 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> ( liminf ` F ) e. RR )
22 simpr 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR+ )
23 18 19 2 20 21 22 liminflt 
 |-  ( ( ph /\ x e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( liminf ` F ) < ( ( F ` k ) + x ) )
24 21 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( liminf ` F ) e. RR )
25 3 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> F : Z --> RR )
26 2 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
27 26 adantll 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
28 25 27 ffvelcdmd 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. RR )
29 28 adantllr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. RR )
30 22 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> x e. RR+ )
31 rpre 
 |-  ( x e. RR+ -> x e. RR )
32 30 31 syl 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> x e. RR )
33 24 29 32 ltsubadd2d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( liminf ` F ) - ( F ` k ) ) < x <-> ( liminf ` F ) < ( ( F ` k ) + x ) ) )
34 33 bicomd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( liminf ` F ) < ( ( F ` k ) + x ) <-> ( ( liminf ` F ) - ( F ` k ) ) < x ) )
35 28 recnd 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. CC )
36 15 eqcomd 
 |-  ( ph -> ( liminf ` F ) = ( limsup ` F ) )
37 36 17 eqeltrd 
 |-  ( ph -> ( liminf ` F ) e. CC )
38 37 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( liminf ` F ) e. CC )
39 35 38 negsubdi2d 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> -u ( ( F ` k ) - ( liminf ` F ) ) = ( ( liminf ` F ) - ( F ` k ) ) )
40 39 breq1d 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( -u ( ( F ` k ) - ( liminf ` F ) ) < x <-> ( ( liminf ` F ) - ( F ` k ) ) < x ) )
41 40 adantllr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( -u ( ( F ` k ) - ( liminf ` F ) ) < x <-> ( ( liminf ` F ) - ( F ` k ) ) < x ) )
42 41 bicomd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( liminf ` F ) - ( F ` k ) ) < x <-> -u ( ( F ` k ) - ( liminf ` F ) ) < x ) )
43 29 24 resubcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` k ) - ( liminf ` F ) ) e. RR )
44 ltnegcon1 
 |-  ( ( ( ( F ` k ) - ( liminf ` F ) ) e. RR /\ x e. RR ) -> ( -u ( ( F ` k ) - ( liminf ` F ) ) < x <-> -u x < ( ( F ` k ) - ( liminf ` F ) ) ) )
45 43 32 44 syl2anc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( -u ( ( F ` k ) - ( liminf ` F ) ) < x <-> -u x < ( ( F ` k ) - ( liminf ` F ) ) ) )
46 42 45 bitrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( liminf ` F ) - ( F ` k ) ) < x <-> -u x < ( ( F ` k ) - ( liminf ` F ) ) ) )
47 36 oveq2d 
 |-  ( ph -> ( ( F ` k ) - ( liminf ` F ) ) = ( ( F ` k ) - ( limsup ` F ) ) )
48 47 breq2d 
 |-  ( ph -> ( -u x < ( ( F ` k ) - ( liminf ` F ) ) <-> -u x < ( ( F ` k ) - ( limsup ` F ) ) ) )
49 48 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( -u x < ( ( F ` k ) - ( liminf ` F ) ) <-> -u x < ( ( F ` k ) - ( limsup ` F ) ) ) )
50 34 46 49 3bitrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( liminf ` F ) < ( ( F ` k ) + x ) <-> -u x < ( ( F ` k ) - ( limsup ` F ) ) ) )
51 50 ralbidva 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( liminf ` F ) < ( ( F ` k ) + x ) <-> A. k e. ( ZZ>= ` j ) -u x < ( ( F ` k ) - ( limsup ` F ) ) ) )
52 51 rexbidva 
 |-  ( ( ph /\ x e. RR+ ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( liminf ` F ) < ( ( F ` k ) + x ) <-> E. j e. Z A. k e. ( ZZ>= ` j ) -u x < ( ( F ` k ) - ( limsup ` F ) ) ) )
53 23 52 mpbid 
 |-  ( ( ph /\ x e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) -u x < ( ( F ` k ) - ( limsup ` F ) ) )
54 16 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> ( limsup ` F ) e. RR )
55 18 19 2 20 54 22 limsupgt 
 |-  ( ( ph /\ x e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) - x ) < ( limsup ` F ) )
56 54 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( limsup ` F ) e. RR )
57 ltsub23 
 |-  ( ( ( F ` k ) e. RR /\ x e. RR /\ ( limsup ` F ) e. RR ) -> ( ( ( F ` k ) - x ) < ( limsup ` F ) <-> ( ( F ` k ) - ( limsup ` F ) ) < x ) )
58 29 32 56 57 syl3anc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) - x ) < ( limsup ` F ) <-> ( ( F ` k ) - ( limsup ` F ) ) < x ) )
59 58 ralbidva 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) - x ) < ( limsup ` F ) <-> A. k e. ( ZZ>= ` j ) ( ( F ` k ) - ( limsup ` F ) ) < x ) )
60 59 rexbidva 
 |-  ( ( ph /\ x e. RR+ ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) - x ) < ( limsup ` F ) <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) - ( limsup ` F ) ) < x ) )
61 55 60 mpbid 
 |-  ( ( ph /\ x e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) - ( limsup ` F ) ) < x )
62 53 61 jca 
 |-  ( ( ph /\ x e. RR+ ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) -u x < ( ( F ` k ) - ( limsup ` F ) ) /\ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) - ( limsup ` F ) ) < x ) )
63 2 rexanuz2 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( -u x < ( ( F ` k ) - ( limsup ` F ) ) /\ ( ( F ` k ) - ( limsup ` F ) ) < x ) <-> ( E. j e. Z A. k e. ( ZZ>= ` j ) -u x < ( ( F ` k ) - ( limsup ` F ) ) /\ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) - ( limsup ` F ) ) < x ) )
64 62 63 sylibr 
 |-  ( ( ph /\ x e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( -u x < ( ( F ` k ) - ( limsup ` F ) ) /\ ( ( F ` k ) - ( limsup ` F ) ) < x ) )
65 simplll 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ph )
66 simpllr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> x e. RR+ )
67 26 adantll 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
68 simpr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ k e. Z ) /\ ( -u x < ( ( F ` k ) - ( limsup ` F ) ) /\ ( ( F ` k ) - ( limsup ` F ) ) < x ) ) -> ( -u x < ( ( F ` k ) - ( limsup ` F ) ) /\ ( ( F ` k ) - ( limsup ` F ) ) < x ) )
69 3 ffvelcdmda 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
70 16 adantr 
 |-  ( ( ph /\ k e. Z ) -> ( limsup ` F ) e. RR )
71 69 70 resubcld 
 |-  ( ( ph /\ k e. Z ) -> ( ( F ` k ) - ( limsup ` F ) ) e. RR )
72 71 adantlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. Z ) -> ( ( F ` k ) - ( limsup ` F ) ) e. RR )
73 31 ad2antlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. Z ) -> x e. RR )
74 abslt 
 |-  ( ( ( ( F ` k ) - ( limsup ` F ) ) e. RR /\ x e. RR ) -> ( ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < x <-> ( -u x < ( ( F ` k ) - ( limsup ` F ) ) /\ ( ( F ` k ) - ( limsup ` F ) ) < x ) ) )
75 72 73 74 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. Z ) -> ( ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < x <-> ( -u x < ( ( F ` k ) - ( limsup ` F ) ) /\ ( ( F ` k ) - ( limsup ` F ) ) < x ) ) )
76 75 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ k e. Z ) /\ ( -u x < ( ( F ` k ) - ( limsup ` F ) ) /\ ( ( F ` k ) - ( limsup ` F ) ) < x ) ) -> ( ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < x <-> ( -u x < ( ( F ` k ) - ( limsup ` F ) ) /\ ( ( F ` k ) - ( limsup ` F ) ) < x ) ) )
77 68 76 mpbird 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ k e. Z ) /\ ( -u x < ( ( F ` k ) - ( limsup ` F ) ) /\ ( ( F ` k ) - ( limsup ` F ) ) < x ) ) -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < x )
78 77 ex 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. Z ) -> ( ( -u x < ( ( F ` k ) - ( limsup ` F ) ) /\ ( ( F ` k ) - ( limsup ` F ) ) < x ) -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < x ) )
79 65 66 67 78 syl21anc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( -u x < ( ( F ` k ) - ( limsup ` F ) ) /\ ( ( F ` k ) - ( limsup ` F ) ) < x ) -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < x ) )
80 79 ralimdva 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( -u x < ( ( F ` k ) - ( limsup ` F ) ) /\ ( ( F ` k ) - ( limsup ` F ) ) < x ) -> A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < x ) )
81 80 reximdva 
 |-  ( ( ph /\ x e. RR+ ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( -u x < ( ( F ` k ) - ( limsup ` F ) ) /\ ( ( F ` k ) - ( limsup ` F ) ) < x ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < x ) )
82 64 81 mpd 
 |-  ( ( ph /\ x e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < x )
83 82 ralrimiva 
 |-  ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < x )
84 17 83 jca 
 |-  ( ph -> ( ( limsup ` F ) e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < x ) )
85 ax-resscn 
 |-  RR C_ CC
86 85 a1i 
 |-  ( ph -> RR C_ CC )
87 3 86 fssd 
 |-  ( ph -> F : Z --> CC )
88 18 1 2 87 climuz 
 |-  ( ph -> ( F ~~> ( limsup ` F ) <-> ( ( limsup ` F ) e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < x ) ) )
89 84 88 mpbird 
 |-  ( ph -> F ~~> ( limsup ` F ) )
90 releldm 
 |-  ( ( Rel ~~> /\ F ~~> ( limsup ` F ) ) -> F e. dom ~~> )
91 7 89 90 syl2anc 
 |-  ( ph -> F e. dom ~~> )