This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem climliminflimsupd

Description: If a sequence of real numbers converges, its inferior limit and its superior limit are equal. (Contributed by Glauco Siliprandi, 2-Jan-2022)

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

Proof

Step Hyp Ref Expression
1 climliminflimsupd.1 
 |-  ( ph -> M e. ZZ )
2 climliminflimsupd.2 
 |-  Z = ( ZZ>= ` M )
3 climliminflimsupd.3 
 |-  ( ph -> F : Z --> RR )
4 climliminflimsupd.4 
 |-  ( ph -> F e. dom ~~> )
5 3 feqmptd 
 |-  ( ph -> F = ( k e. Z |-> ( F ` k ) ) )
6 5 fveq2d 
 |-  ( ph -> ( liminf ` F ) = ( liminf ` ( k e. Z |-> ( F ` k ) ) ) )
7 2 fvexi 
 |-  Z e. _V
8 7 mptex 
 |-  ( k e. Z |-> ( F ` k ) ) e. _V
9 liminfcl 
 |-  ( ( k e. Z |-> ( F ` k ) ) e. _V -> ( liminf ` ( k e. Z |-> ( F ` k ) ) ) e. RR* )
10 8 9 ax-mp 
 |-  ( liminf ` ( k e. Z |-> ( F ` k ) ) ) e. RR*
11 10 a1i 
 |-  ( ph -> ( liminf ` ( k e. Z |-> ( F ` k ) ) ) e. RR* )
12 6 11 eqeltrd 
 |-  ( ph -> ( liminf ` F ) e. RR* )
13 nfv 
 |-  F/ k ph
14 3 ffvelcdmda 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
15 14 renegcld 
 |-  ( ( ph /\ k e. Z ) -> -u ( F ` k ) e. RR )
16 13 1 2 15 limsupvaluz4 
 |-  ( ph -> ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) = -e ( liminf ` ( k e. Z |-> -u -u ( F ` k ) ) ) )
17 climrel 
 |-  Rel ~~>
18 17 a1i 
 |-  ( ph -> Rel ~~> )
19 nfcv 
 |-  F/_ k F
20 1 2 3 climlimsup 
 |-  ( ph -> ( F e. dom ~~> <-> F ~~> ( limsup ` F ) ) )
21 4 20 mpbid 
 |-  ( ph -> F ~~> ( limsup ` F ) )
22 14 recnd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
23 13 19 2 1 21 22 climneg 
 |-  ( ph -> ( k e. Z |-> -u ( F ` k ) ) ~~> -u ( limsup ` F ) )
24 releldm 
 |-  ( ( Rel ~~> /\ ( k e. Z |-> -u ( F ` k ) ) ~~> -u ( limsup ` F ) ) -> ( k e. Z |-> -u ( F ` k ) ) e. dom ~~> )
25 18 23 24 syl2anc 
 |-  ( ph -> ( k e. Z |-> -u ( F ` k ) ) e. dom ~~> )
26 15 fmpttd 
 |-  ( ph -> ( k e. Z |-> -u ( F ` k ) ) : Z --> RR )
27 1 2 26 climlimsup 
 |-  ( ph -> ( ( k e. Z |-> -u ( F ` k ) ) e. dom ~~> <-> ( k e. Z |-> -u ( F ` k ) ) ~~> ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) ) )
28 25 27 mpbid 
 |-  ( ph -> ( k e. Z |-> -u ( F ` k ) ) ~~> ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) )
29 climuni 
 |-  ( ( ( k e. Z |-> -u ( F ` k ) ) ~~> ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) /\ ( k e. Z |-> -u ( F ` k ) ) ~~> -u ( limsup ` F ) ) -> ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) = -u ( limsup ` F ) )
30 28 23 29 syl2anc 
 |-  ( ph -> ( limsup ` ( k e. Z |-> -u ( F ` k ) ) ) = -u ( limsup ` F ) )
31 22 negnegd 
 |-  ( ( ph /\ k e. Z ) -> -u -u ( F ` k ) = ( F ` k ) )
32 31 mpteq2dva 
 |-  ( ph -> ( k e. Z |-> -u -u ( F ` k ) ) = ( k e. Z |-> ( F ` k ) ) )
33 32 5 eqtr4d 
 |-  ( ph -> ( k e. Z |-> -u -u ( F ` k ) ) = F )
34 33 fveq2d 
 |-  ( ph -> ( liminf ` ( k e. Z |-> -u -u ( F ` k ) ) ) = ( liminf ` F ) )
35 34 xnegeqd 
 |-  ( ph -> -e ( liminf ` ( k e. Z |-> -u -u ( F ` k ) ) ) = -e ( liminf ` F ) )
36 16 30 35 3eqtr3d 
 |-  ( ph -> -u ( limsup ` F ) = -e ( liminf ` F ) )
37 2 1 21 14 climrecl 
 |-  ( ph -> ( limsup ` F ) e. RR )
38 37 renegcld 
 |-  ( ph -> -u ( limsup ` F ) e. RR )
39 36 38 eqeltrrd 
 |-  ( ph -> -e ( liminf ` F ) e. RR )
40 xnegrecl2 
 |-  ( ( ( liminf ` F ) e. RR* /\ -e ( liminf ` F ) e. RR ) -> ( liminf ` F ) e. RR )
41 12 39 40 syl2anc 
 |-  ( ph -> ( liminf ` F ) e. RR )
42 41 recnd 
 |-  ( ph -> ( liminf ` F ) e. CC )
43 37 recnd 
 |-  ( ph -> ( limsup ` F ) e. CC )
44 41 rexnegd 
 |-  ( ph -> -e ( liminf ` F ) = -u ( liminf ` F ) )
45 36 44 eqtr2d 
 |-  ( ph -> -u ( liminf ` F ) = -u ( limsup ` F ) )
46 42 43 45 neg11d 
 |-  ( ph -> ( liminf ` F ) = ( limsup ` F ) )