Metamath Proof Explorer

Theorem xlimliminflimsup

Description: A sequence of extended reals converges if and only if its inferior limit and its superior limit are equal. (Contributed by Glauco Siliprandi, 23-Apr-2023)

Ref Expression
Hypotheses xlimliminflimsup.m 
|- ( ph -> M e. ZZ )
xlimliminflimsup.z 
|- Z = ( ZZ>= ` M )
xlimliminflimsup.f 
|- ( ph -> F : Z --> RR* )
Assertion xlimliminflimsup 
|- ( ph -> ( F e. dom ~~>* <-> ( liminf ` F ) = ( limsup ` F ) ) )

Proof

Step Hyp Ref Expression
1 xlimliminflimsup.m 
 |-  ( ph -> M e. ZZ )
2 xlimliminflimsup.z 
 |-  Z = ( ZZ>= ` M )
3 xlimliminflimsup.f 
 |-  ( ph -> F : Z --> RR* )
4 1 ad2antrr 
 |-  ( ( ( ph /\ F e. dom ~~>* ) /\ ( ~~>* ` F ) e. RR ) -> M e. ZZ )
5 3 ad2antrr 
 |-  ( ( ( ph /\ F e. dom ~~>* ) /\ ( ~~>* ` F ) e. RR ) -> F : Z --> RR* )
6 simpr 
 |-  ( ( ( ph /\ F e. dom ~~>* ) /\ ( ~~>* ` F ) e. RR ) -> ( ~~>* ` F ) e. RR )
7 xlimdm 
 |-  ( F e. dom ~~>* <-> F ~~>* ( ~~>* ` F ) )
8 7 biimpi 
 |-  ( F e. dom ~~>* -> F ~~>* ( ~~>* ` F ) )
9 8 ad2antlr 
 |-  ( ( ( ph /\ F e. dom ~~>* ) /\ ( ~~>* ` F ) e. RR ) -> F ~~>* ( ~~>* ` F ) )
10 4 2 5 6 9 xlimxrre 
 |-  ( ( ( ph /\ F e. dom ~~>* ) /\ ( ~~>* ` F ) e. RR ) -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )
11 2 eluzelz2 
 |-  ( j e. Z -> j e. ZZ )
12 11 ad2antlr 
 |-  ( ( ( ( ( ph /\ F e. dom ~~>* ) /\ ( ~~>* ` F ) e. RR ) /\ j e. Z ) /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR ) -> j e. ZZ )
13 eqid 
 |-  ( ZZ>= ` j ) = ( ZZ>= ` j )
14 simpr 
 |-  ( ( ( ( ( ph /\ F e. dom ~~>* ) /\ ( ~~>* ` F ) e. RR ) /\ j e. Z ) /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR ) -> ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )
15 14 frexr 
 |-  ( ( ( ( ( ph /\ F e. dom ~~>* ) /\ ( ~~>* ` F ) e. RR ) /\ j e. Z ) /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR ) -> ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR* )
16 9 adantr 
 |-  ( ( ( ( ph /\ F e. dom ~~>* ) /\ ( ~~>* ` F ) e. RR ) /\ j e. Z ) -> F ~~>* ( ~~>* ` F ) )
17 2 3 fuzxrpmcn 
 |-  ( ph -> F e. ( RR* ^pm CC ) )
18 17 ad3antrrr 
 |-  ( ( ( ( ph /\ F e. dom ~~>* ) /\ ( ~~>* ` F ) e. RR ) /\ j e. Z ) -> F e. ( RR* ^pm CC ) )
19 11 adantl 
 |-  ( ( ( ( ph /\ F e. dom ~~>* ) /\ ( ~~>* ` F ) e. RR ) /\ j e. Z ) -> j e. ZZ )
20 18 19 xlimres 
 |-  ( ( ( ( ph /\ F e. dom ~~>* ) /\ ( ~~>* ` F ) e. RR ) /\ j e. Z ) -> ( F ~~>* ( ~~>* ` F ) <-> ( F |` ( ZZ>= ` j ) ) ~~>* ( ~~>* ` F ) ) )
21 16 20 mpbid 
 |-  ( ( ( ( ph /\ F e. dom ~~>* ) /\ ( ~~>* ` F ) e. RR ) /\ j e. Z ) -> ( F |` ( ZZ>= ` j ) ) ~~>* ( ~~>* ` F ) )
22 21 adantr 
 |-  ( ( ( ( ( ph /\ F e. dom ~~>* ) /\ ( ~~>* ` F ) e. RR ) /\ j e. Z ) /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR ) -> ( F |` ( ZZ>= ` j ) ) ~~>* ( ~~>* ` F ) )
23 simpllr 
 |-  ( ( ( ( ( ph /\ F e. dom ~~>* ) /\ ( ~~>* ` F ) e. RR ) /\ j e. Z ) /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR ) -> ( ~~>* ` F ) e. RR )
24 12 13 15 22 23 xlimclimdm 
 |-  ( ( ( ( ( ph /\ F e. dom ~~>* ) /\ ( ~~>* ` F ) e. RR ) /\ j e. Z ) /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR ) -> ( F |` ( ZZ>= ` j ) ) e. dom ~~> )
25 12 13 14 24 climliminflimsupd 
 |-  ( ( ( ( ( ph /\ F e. dom ~~>* ) /\ ( ~~>* ` F ) e. RR ) /\ j e. Z ) /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR ) -> ( liminf ` ( F |` ( ZZ>= ` j ) ) ) = ( limsup ` ( F |` ( ZZ>= ` j ) ) ) )
26 11 adantl 
 |-  ( ( ph /\ j e. Z ) -> j e. ZZ )
27 17 elexd 
 |-  ( ph -> F e. _V )
28 27 adantr 
 |-  ( ( ph /\ j e. Z ) -> F e. _V )
29 3 fdmd 
 |-  ( ph -> dom F = Z )
30 26 ssd 
 |-  ( ph -> Z C_ ZZ )
31 29 30 eqsstrd 
 |-  ( ph -> dom F C_ ZZ )
32 31 adantr 
 |-  ( ( ph /\ j e. Z ) -> dom F C_ ZZ )
33 26 13 28 32 liminfresuz2 
 |-  ( ( ph /\ j e. Z ) -> ( liminf ` ( F |` ( ZZ>= ` j ) ) ) = ( liminf ` F ) )
34 33 eqcomd 
 |-  ( ( ph /\ j e. Z ) -> ( liminf ` F ) = ( liminf ` ( F |` ( ZZ>= ` j ) ) ) )
35 34 ad5ant14 
 |-  ( ( ( ( ( ph /\ F e. dom ~~>* ) /\ ( ~~>* ` F ) e. RR ) /\ j e. Z ) /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR ) -> ( liminf ` F ) = ( liminf ` ( F |` ( ZZ>= ` j ) ) ) )
36 26 13 28 32 limsupresuz2 
 |-  ( ( ph /\ j e. Z ) -> ( limsup ` ( F |` ( ZZ>= ` j ) ) ) = ( limsup ` F ) )
37 36 eqcomd 
 |-  ( ( ph /\ j e. Z ) -> ( limsup ` F ) = ( limsup ` ( F |` ( ZZ>= ` j ) ) ) )
38 37 ad5ant14 
 |-  ( ( ( ( ( ph /\ F e. dom ~~>* ) /\ ( ~~>* ` F ) e. RR ) /\ j e. Z ) /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR ) -> ( limsup ` F ) = ( limsup ` ( F |` ( ZZ>= ` j ) ) ) )
39 25 35 38 3eqtr4d 
 |-  ( ( ( ( ( ph /\ F e. dom ~~>* ) /\ ( ~~>* ` F ) e. RR ) /\ j e. Z ) /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR ) -> ( liminf ` F ) = ( limsup ` F ) )
40 10 39 rexlimddv2 
 |-  ( ( ( ph /\ F e. dom ~~>* ) /\ ( ~~>* ` F ) e. RR ) -> ( liminf ` F ) = ( limsup ` F ) )
41 simpll 
 |-  ( ( ( ph /\ F e. dom ~~>* ) /\ ( ~~>* ` F ) = +oo ) -> ph )
42 8 adantr 
 |-  ( ( F e. dom ~~>* /\ ( ~~>* ` F ) = +oo ) -> F ~~>* ( ~~>* ` F ) )
43 simpr 
 |-  ( ( F e. dom ~~>* /\ ( ~~>* ` F ) = +oo ) -> ( ~~>* ` F ) = +oo )
44 42 43 breqtrd 
 |-  ( ( F e. dom ~~>* /\ ( ~~>* ` F ) = +oo ) -> F ~~>* +oo )
45 44 adantll 
 |-  ( ( ( ph /\ F e. dom ~~>* ) /\ ( ~~>* ` F ) = +oo ) -> F ~~>* +oo )
46 17 liminfcld 
 |-  ( ph -> ( liminf ` F ) e. RR* )
47 46 adantr 
 |-  ( ( ph /\ F ~~>* +oo ) -> ( liminf ` F ) e. RR* )
48 17 limsupcld 
 |-  ( ph -> ( limsup ` F ) e. RR* )
49 48 adantr 
 |-  ( ( ph /\ F ~~>* +oo ) -> ( limsup ` F ) e. RR* )
50 1 2 3 liminflelimsupuz 
 |-  ( ph -> ( liminf ` F ) <_ ( limsup ` F ) )
51 50 adantr 
 |-  ( ( ph /\ F ~~>* +oo ) -> ( liminf ` F ) <_ ( limsup ` F ) )
52 49 pnfged 
 |-  ( ( ph /\ F ~~>* +oo ) -> ( limsup ` F ) <_ +oo )
53 1 adantr 
 |-  ( ( ph /\ F ~~>* +oo ) -> M e. ZZ )
54 3 adantr 
 |-  ( ( ph /\ F ~~>* +oo ) -> F : Z --> RR* )
55 simpr 
 |-  ( ( ph /\ F ~~>* +oo ) -> F ~~>* +oo )
56 53 2 54 55 xlimpnfliminf 
 |-  ( ( ph /\ F ~~>* +oo ) -> ( liminf ` F ) = +oo )
57 52 56 breqtrrd 
 |-  ( ( ph /\ F ~~>* +oo ) -> ( limsup ` F ) <_ ( liminf ` F ) )
58 47 49 51 57 xrletrid 
 |-  ( ( ph /\ F ~~>* +oo ) -> ( liminf ` F ) = ( limsup ` F ) )
59 41 45 58 syl2anc 
 |-  ( ( ( ph /\ F e. dom ~~>* ) /\ ( ~~>* ` F ) = +oo ) -> ( liminf ` F ) = ( limsup ` F ) )
60 59 adantlr 
 |-  ( ( ( ( ph /\ F e. dom ~~>* ) /\ -. ( ~~>* ` F ) e. RR ) /\ ( ~~>* ` F ) = +oo ) -> ( liminf ` F ) = ( limsup ` F ) )
61 simplll 
 |-  ( ( ( ( ph /\ F e. dom ~~>* ) /\ -. ( ~~>* ` F ) e. RR ) /\ -. ( ~~>* ` F ) = +oo ) -> ph )
62 8 ad2antrr 
 |-  ( ( ( F e. dom ~~>* /\ -. ( ~~>* ` F ) e. RR ) /\ -. ( ~~>* ` F ) = +oo ) -> F ~~>* ( ~~>* ` F ) )
63 xlimcl 
 |-  ( F ~~>* ( ~~>* ` F ) -> ( ~~>* ` F ) e. RR* )
64 8 63 syl 
 |-  ( F e. dom ~~>* -> ( ~~>* ` F ) e. RR* )
65 64 ad2antrr 
 |-  ( ( ( F e. dom ~~>* /\ -. ( ~~>* ` F ) e. RR ) /\ -. ( ~~>* ` F ) = +oo ) -> ( ~~>* ` F ) e. RR* )
66 simplr 
 |-  ( ( ( F e. dom ~~>* /\ -. ( ~~>* ` F ) e. RR ) /\ -. ( ~~>* ` F ) = +oo ) -> -. ( ~~>* ` F ) e. RR )
67 neqne 
 |-  ( -. ( ~~>* ` F ) = +oo -> ( ~~>* ` F ) =/= +oo )
68 67 adantl 
 |-  ( ( ( F e. dom ~~>* /\ -. ( ~~>* ` F ) e. RR ) /\ -. ( ~~>* ` F ) = +oo ) -> ( ~~>* ` F ) =/= +oo )
69 65 66 68 xrnpnfmnf 
 |-  ( ( ( F e. dom ~~>* /\ -. ( ~~>* ` F ) e. RR ) /\ -. ( ~~>* ` F ) = +oo ) -> ( ~~>* ` F ) = -oo )
70 62 69 breqtrd 
 |-  ( ( ( F e. dom ~~>* /\ -. ( ~~>* ` F ) e. RR ) /\ -. ( ~~>* ` F ) = +oo ) -> F ~~>* -oo )
71 70 adantlll 
 |-  ( ( ( ( ph /\ F e. dom ~~>* ) /\ -. ( ~~>* ` F ) e. RR ) /\ -. ( ~~>* ` F ) = +oo ) -> F ~~>* -oo )
72 46 adantr 
 |-  ( ( ph /\ F ~~>* -oo ) -> ( liminf ` F ) e. RR* )
73 48 adantr 
 |-  ( ( ph /\ F ~~>* -oo ) -> ( limsup ` F ) e. RR* )
74 50 adantr 
 |-  ( ( ph /\ F ~~>* -oo ) -> ( liminf ` F ) <_ ( limsup ` F ) )
75 1 adantr 
 |-  ( ( ph /\ F ~~>* -oo ) -> M e. ZZ )
76 3 adantr 
 |-  ( ( ph /\ F ~~>* -oo ) -> F : Z --> RR* )
77 simpr 
 |-  ( ( ph /\ F ~~>* -oo ) -> F ~~>* -oo )
78 75 2 76 77 xlimmnflimsup 
 |-  ( ( ph /\ F ~~>* -oo ) -> ( limsup ` F ) = -oo )
79 72 mnfled 
 |-  ( ( ph /\ F ~~>* -oo ) -> -oo <_ ( liminf ` F ) )
80 78 79 eqbrtrd 
 |-  ( ( ph /\ F ~~>* -oo ) -> ( limsup ` F ) <_ ( liminf ` F ) )
81 72 73 74 80 xrletrid 
 |-  ( ( ph /\ F ~~>* -oo ) -> ( liminf ` F ) = ( limsup ` F ) )
82 61 71 81 syl2anc 
 |-  ( ( ( ( ph /\ F e. dom ~~>* ) /\ -. ( ~~>* ` F ) e. RR ) /\ -. ( ~~>* ` F ) = +oo ) -> ( liminf ` F ) = ( limsup ` F ) )
83 60 82 pm2.61dan 
 |-  ( ( ( ph /\ F e. dom ~~>* ) /\ -. ( ~~>* ` F ) e. RR ) -> ( liminf ` F ) = ( limsup ` F ) )
84 40 83 pm2.61dan 
 |-  ( ( ph /\ F e. dom ~~>* ) -> ( liminf ` F ) = ( limsup ` F ) )
85 27 adantr 
 |-  ( ( ph /\ ( limsup ` F ) = -oo ) -> F e. _V )
86 mnfxr 
 |-  -oo e. RR*
87 86 a1i 
 |-  ( ( ph /\ ( limsup ` F ) = -oo ) -> -oo e. RR* )
88 simpr 
 |-  ( ( ph /\ ( limsup ` F ) = -oo ) -> ( limsup ` F ) = -oo )
89 1 adantr 
 |-  ( ( ph /\ ( limsup ` F ) = -oo ) -> M e. ZZ )
90 3 adantr 
 |-  ( ( ph /\ ( limsup ` F ) = -oo ) -> F : Z --> RR* )
91 89 2 90 xlimmnflimsup2 
 |-  ( ( ph /\ ( limsup ` F ) = -oo ) -> ( F ~~>* -oo <-> ( limsup ` F ) = -oo ) )
92 88 91 mpbird 
 |-  ( ( ph /\ ( limsup ` F ) = -oo ) -> F ~~>* -oo )
93 85 87 92 breldmd 
 |-  ( ( ph /\ ( limsup ` F ) = -oo ) -> F e. dom ~~>* )
94 93 adantlr 
 |-  ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) = -oo ) -> F e. dom ~~>* )
95 1 ad2antrr 
 |-  ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) e. RR ) -> M e. ZZ )
96 3 ad2antrr 
 |-  ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) e. RR ) -> F : Z --> RR* )
97 simpr 
 |-  ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) e. RR ) -> ( limsup ` F ) e. RR )
98 97 renepnfd 
 |-  ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) e. RR ) -> ( limsup ` F ) =/= +oo )
99 simplr 
 |-  ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) e. RR ) -> ( liminf ` F ) = ( limsup ` F ) )
100 99 97 eqeltrd 
 |-  ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) e. RR ) -> ( liminf ` F ) e. RR )
101 100 renemnfd 
 |-  ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) e. RR ) -> ( liminf ` F ) =/= -oo )
102 95 2 96 98 101 liminflimsupxrre 
 |-  ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) e. RR ) -> E. m e. Z ( F |` ( ZZ>= ` m ) ) : ( ZZ>= ` m ) --> RR )
103 2 eluzelz2 
 |-  ( m e. Z -> m e. ZZ )
104 103 ad2antlr 
 |-  ( ( ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) e. RR ) /\ m e. Z ) /\ ( F |` ( ZZ>= ` m ) ) : ( ZZ>= ` m ) --> RR ) -> m e. ZZ )
105 eqid 
 |-  ( ZZ>= ` m ) = ( ZZ>= ` m )
106 simpr 
 |-  ( ( ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) e. RR ) /\ m e. Z ) /\ ( F |` ( ZZ>= ` m ) ) : ( ZZ>= ` m ) --> RR ) -> ( F |` ( ZZ>= ` m ) ) : ( ZZ>= ` m ) --> RR )
107 simplll 
 |-  ( ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) e. RR ) /\ m e. Z ) -> ph )
108 simpl 
 |-  ( ( ( liminf ` F ) = ( limsup ` F ) /\ ( limsup ` F ) e. RR ) -> ( liminf ` F ) = ( limsup ` F ) )
109 simpr 
 |-  ( ( ( liminf ` F ) = ( limsup ` F ) /\ ( limsup ` F ) e. RR ) -> ( limsup ` F ) e. RR )
110 108 109 eqeltrd 
 |-  ( ( ( liminf ` F ) = ( limsup ` F ) /\ ( limsup ` F ) e. RR ) -> ( liminf ` F ) e. RR )
111 110 ad4ant23 
 |-  ( ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) e. RR ) /\ m e. Z ) -> ( liminf ` F ) e. RR )
112 simpr 
 |-  ( ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) e. RR ) /\ m e. Z ) -> m e. Z )
113 103 3ad2ant3 
 |-  ( ( ph /\ ( liminf ` F ) e. RR /\ m e. Z ) -> m e. ZZ )
114 27 3ad2ant1 
 |-  ( ( ph /\ ( liminf ` F ) e. RR /\ m e. Z ) -> F e. _V )
115 31 3ad2ant1 
 |-  ( ( ph /\ ( liminf ` F ) e. RR /\ m e. Z ) -> dom F C_ ZZ )
116 113 105 114 115 liminfresuz2 
 |-  ( ( ph /\ ( liminf ` F ) e. RR /\ m e. Z ) -> ( liminf ` ( F |` ( ZZ>= ` m ) ) ) = ( liminf ` F ) )
117 simp2 
 |-  ( ( ph /\ ( liminf ` F ) e. RR /\ m e. Z ) -> ( liminf ` F ) e. RR )
118 116 117 eqeltrd 
 |-  ( ( ph /\ ( liminf ` F ) e. RR /\ m e. Z ) -> ( liminf ` ( F |` ( ZZ>= ` m ) ) ) e. RR )
119 107 111 112 118 syl3anc 
 |-  ( ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) e. RR ) /\ m e. Z ) -> ( liminf ` ( F |` ( ZZ>= ` m ) ) ) e. RR )
120 119 adantr 
 |-  ( ( ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) e. RR ) /\ m e. Z ) /\ ( F |` ( ZZ>= ` m ) ) : ( ZZ>= ` m ) --> RR ) -> ( liminf ` ( F |` ( ZZ>= ` m ) ) ) e. RR )
121 simp2 
 |-  ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) /\ m e. Z ) -> ( liminf ` F ) = ( limsup ` F ) )
122 103 adantl 
 |-  ( ( ph /\ m e. Z ) -> m e. ZZ )
123 27 adantr 
 |-  ( ( ph /\ m e. Z ) -> F e. _V )
124 31 adantr 
 |-  ( ( ph /\ m e. Z ) -> dom F C_ ZZ )
125 122 105 123 124 liminfresuz2 
 |-  ( ( ph /\ m e. Z ) -> ( liminf ` ( F |` ( ZZ>= ` m ) ) ) = ( liminf ` F ) )
126 125 3adant2 
 |-  ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) /\ m e. Z ) -> ( liminf ` ( F |` ( ZZ>= ` m ) ) ) = ( liminf ` F ) )
127 122 105 123 124 limsupresuz2 
 |-  ( ( ph /\ m e. Z ) -> ( limsup ` ( F |` ( ZZ>= ` m ) ) ) = ( limsup ` F ) )
128 127 3adant2 
 |-  ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) /\ m e. Z ) -> ( limsup ` ( F |` ( ZZ>= ` m ) ) ) = ( limsup ` F ) )
129 121 126 128 3eqtr4d 
 |-  ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) /\ m e. Z ) -> ( liminf ` ( F |` ( ZZ>= ` m ) ) ) = ( limsup ` ( F |` ( ZZ>= ` m ) ) ) )
130 129 ad5ant124 
 |-  ( ( ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) e. RR ) /\ m e. Z ) /\ ( F |` ( ZZ>= ` m ) ) : ( ZZ>= ` m ) --> RR ) -> ( liminf ` ( F |` ( ZZ>= ` m ) ) ) = ( limsup ` ( F |` ( ZZ>= ` m ) ) ) )
131 104 105 106 climliminflimsup3 
 |-  ( ( ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) e. RR ) /\ m e. Z ) /\ ( F |` ( ZZ>= ` m ) ) : ( ZZ>= ` m ) --> RR ) -> ( ( F |` ( ZZ>= ` m ) ) e. dom ~~> <-> ( ( liminf ` ( F |` ( ZZ>= ` m ) ) ) e. RR /\ ( liminf ` ( F |` ( ZZ>= ` m ) ) ) = ( limsup ` ( F |` ( ZZ>= ` m ) ) ) ) ) )
132 120 130 131 mpbir2and 
 |-  ( ( ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) e. RR ) /\ m e. Z ) /\ ( F |` ( ZZ>= ` m ) ) : ( ZZ>= ` m ) --> RR ) -> ( F |` ( ZZ>= ` m ) ) e. dom ~~> )
133 104 105 106 132 dmclimxlim 
 |-  ( ( ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) e. RR ) /\ m e. Z ) /\ ( F |` ( ZZ>= ` m ) ) : ( ZZ>= ` m ) --> RR ) -> ( F |` ( ZZ>= ` m ) ) e. dom ~~>* )
134 17 ad4antr 
 |-  ( ( ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) e. RR ) /\ m e. Z ) /\ ( F |` ( ZZ>= ` m ) ) : ( ZZ>= ` m ) --> RR ) -> F e. ( RR* ^pm CC ) )
135 134 104 xlimresdm 
 |-  ( ( ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) e. RR ) /\ m e. Z ) /\ ( F |` ( ZZ>= ` m ) ) : ( ZZ>= ` m ) --> RR ) -> ( F e. dom ~~>* <-> ( F |` ( ZZ>= ` m ) ) e. dom ~~>* ) )
136 133 135 mpbird 
 |-  ( ( ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) e. RR ) /\ m e. Z ) /\ ( F |` ( ZZ>= ` m ) ) : ( ZZ>= ` m ) --> RR ) -> F e. dom ~~>* )
137 102 136 rexlimddv2 
 |-  ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) e. RR ) -> F e. dom ~~>* )
138 137 adantlr 
 |-  ( ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) =/= -oo ) /\ ( limsup ` F ) e. RR ) -> F e. dom ~~>* )
139 simpll 
 |-  ( ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) =/= -oo ) /\ -. ( limsup ` F ) e. RR ) -> ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) )
140 simpllr 
 |-  ( ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) =/= -oo ) /\ -. ( limsup ` F ) e. RR ) -> ( liminf ` F ) = ( limsup ` F ) )
141 48 ad2antrr 
 |-  ( ( ( ph /\ ( limsup ` F ) =/= -oo ) /\ -. ( limsup ` F ) e. RR ) -> ( limsup ` F ) e. RR* )
142 simpr 
 |-  ( ( ( ph /\ ( limsup ` F ) =/= -oo ) /\ -. ( limsup ` F ) e. RR ) -> -. ( limsup ` F ) e. RR )
143 simplr 
 |-  ( ( ( ph /\ ( limsup ` F ) =/= -oo ) /\ -. ( limsup ` F ) e. RR ) -> ( limsup ` F ) =/= -oo )
144 141 142 143 xrnmnfpnf 
 |-  ( ( ( ph /\ ( limsup ` F ) =/= -oo ) /\ -. ( limsup ` F ) e. RR ) -> ( limsup ` F ) = +oo )
145 144 adantllr 
 |-  ( ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) =/= -oo ) /\ -. ( limsup ` F ) e. RR ) -> ( limsup ` F ) = +oo )
146 140 145 eqtrd 
 |-  ( ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) =/= -oo ) /\ -. ( limsup ` F ) e. RR ) -> ( liminf ` F ) = +oo )
147 27 adantr 
 |-  ( ( ph /\ ( liminf ` F ) = +oo ) -> F e. _V )
148 pnfxr 
 |-  +oo e. RR*
149 148 a1i 
 |-  ( ( ph /\ ( liminf ` F ) = +oo ) -> +oo e. RR* )
150 1 2 3 xlimpnfliminf2 
 |-  ( ph -> ( F ~~>* +oo <-> ( liminf ` F ) = +oo ) )
151 150 biimpar 
 |-  ( ( ph /\ ( liminf ` F ) = +oo ) -> F ~~>* +oo )
152 147 149 151 breldmd 
 |-  ( ( ph /\ ( liminf ` F ) = +oo ) -> F e. dom ~~>* )
153 152 adantlr 
 |-  ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( liminf ` F ) = +oo ) -> F e. dom ~~>* )
154 139 146 153 syl2anc 
 |-  ( ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) =/= -oo ) /\ -. ( limsup ` F ) e. RR ) -> F e. dom ~~>* )
155 138 154 pm2.61dan 
 |-  ( ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) /\ ( limsup ` F ) =/= -oo ) -> F e. dom ~~>* )
156 94 155 pm2.61dane 
 |-  ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) -> F e. dom ~~>* )
157 84 156 impbida 
 |-  ( ph -> ( F e. dom ~~>* <-> ( liminf ` F ) = ( limsup ` F ) ) )