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 ) ) )