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

Metamath Proof Explorer

Theorem climliminf

Description: A sequence of real numbers converges if and only if it converges to its inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022)

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

Proof

Step Hyp Ref Expression
1 climliminf.1 
 |-  ( ph -> M e. ZZ )
2 climliminf.2 
 |-  Z = ( ZZ>= ` M )
3 climliminf.3 
 |-  ( ph -> F : Z --> RR )
4 1 2 3 climlimsup 
 |-  ( ph -> ( F e. dom ~~> <-> F ~~> ( limsup ` F ) ) )
5 4 biimpd 
 |-  ( ph -> ( F e. dom ~~> -> F ~~> ( limsup ` F ) ) )
6 5 imp 
 |-  ( ( ph /\ F e. dom ~~> ) -> F ~~> ( limsup ` F ) )
7 1 adantr 
 |-  ( ( ph /\ F e. dom ~~> ) -> M e. ZZ )
8 3 adantr 
 |-  ( ( ph /\ F e. dom ~~> ) -> F : Z --> RR )
9 simpr 
 |-  ( ( ph /\ F e. dom ~~> ) -> F e. dom ~~> )
10 7 2 8 9 climliminflimsupd 
 |-  ( ( ph /\ F e. dom ~~> ) -> ( liminf ` F ) = ( limsup ` F ) )
11 6 10 breqtrrd 
 |-  ( ( ph /\ F e. dom ~~> ) -> F ~~> ( liminf ` F ) )
12 climrel 
 |-  Rel ~~>
13 12 releldmi 
 |-  ( F ~~> ( liminf ` F ) -> F e. dom ~~> )
14 13 adantl 
 |-  ( ( ph /\ F ~~> ( liminf ` F ) ) -> F e. dom ~~> )
15 11 14 impbida 
 |-  ( ph -> ( F e. dom ~~> <-> F ~~> ( liminf ` F ) ) )