Step |
Hyp |
Ref |
Expression |
1 |
|
liminfgelimsupuz.1 |
|- ( ph -> M e. ZZ ) |
2 |
|
liminfgelimsupuz.2 |
|- Z = ( ZZ>= ` M ) |
3 |
|
liminfgelimsupuz.3 |
|- ( ph -> F : Z --> RR* ) |
4 |
2
|
fvexi |
|- Z e. _V |
5 |
4
|
a1i |
|- ( ph -> Z e. _V ) |
6 |
3 5
|
fexd |
|- ( ph -> F e. _V ) |
7 |
6
|
liminfcld |
|- ( ph -> ( liminf ` F ) e. RR* ) |
8 |
7
|
adantr |
|- ( ( ph /\ ( limsup ` F ) <_ ( liminf ` F ) ) -> ( liminf ` F ) e. RR* ) |
9 |
6
|
limsupcld |
|- ( ph -> ( limsup ` F ) e. RR* ) |
10 |
9
|
adantr |
|- ( ( ph /\ ( limsup ` F ) <_ ( liminf ` F ) ) -> ( limsup ` F ) e. RR* ) |
11 |
1 2 3
|
liminflelimsupuz |
|- ( ph -> ( liminf ` F ) <_ ( limsup ` F ) ) |
12 |
11
|
adantr |
|- ( ( ph /\ ( limsup ` F ) <_ ( liminf ` F ) ) -> ( liminf ` F ) <_ ( limsup ` F ) ) |
13 |
|
simpr |
|- ( ( ph /\ ( limsup ` F ) <_ ( liminf ` F ) ) -> ( limsup ` F ) <_ ( liminf ` F ) ) |
14 |
8 10 12 13
|
xrletrid |
|- ( ( ph /\ ( limsup ` F ) <_ ( liminf ` F ) ) -> ( liminf ` F ) = ( limsup ` F ) ) |
15 |
9
|
adantr |
|- ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) -> ( limsup ` F ) e. RR* ) |
16 |
|
id |
|- ( ( liminf ` F ) = ( limsup ` F ) -> ( liminf ` F ) = ( limsup ` F ) ) |
17 |
16
|
eqcomd |
|- ( ( liminf ` F ) = ( limsup ` F ) -> ( limsup ` F ) = ( liminf ` F ) ) |
18 |
17
|
adantl |
|- ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) -> ( limsup ` F ) = ( liminf ` F ) ) |
19 |
15 18
|
xreqled |
|- ( ( ph /\ ( liminf ` F ) = ( limsup ` F ) ) -> ( limsup ` F ) <_ ( liminf ` F ) ) |
20 |
14 19
|
impbida |
|- ( ph -> ( ( limsup ` F ) <_ ( liminf ` F ) <-> ( liminf ` F ) = ( limsup ` F ) ) ) |