Theorem xlimclim2

Description: Given a sequence of extended reals, it converges to a real number A w.r.t. the standard topology on the reals (see climreeq ), if and only if it converges to A w.r.t. to the standard topology on the extended reals. In order for the first part of the statement to even make sense, the sequence will of course eventually become (and stay) real: showing this, is the key step of the proof. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	xlimclim2.m	|- ( ph -> M e. ZZ )
	xlimclim2.z	|- Z = ( ZZ>= ` M )
	xlimclim2.f	|- ( ph -> F : Z --> RR* )
	xlimclim2.a	|- ( ph -> A e. RR )
Assertion	xlimclim2	|- ( ph -> ( F ~~>* A <-> F ~~> A ) )

Proof

Step	Hyp	Ref	Expression
1		xlimclim2.m	|- ( ph -> M e. ZZ )
2		xlimclim2.z	|- Z = ( ZZ>= ` M )
3		xlimclim2.f	|- ( ph -> F : Z --> RR* )
4		xlimclim2.a	|- ( ph -> A e. RR )
5		simpr	|- ( ( ph /\ F ~~>* A ) -> F ~~>* A )
6	3	adantr	|- ( ( ph /\ F ~~>* A ) -> F : Z --> RR* )
7	4	adantr	|- ( ( ph /\ F ~~>* A ) -> A e. RR )
8	1	adantr	|- ( ( ph /\ F ~~>* A ) -> M e. ZZ )
9	8 2 6 7 5	xlimxrre	|- ( ( ph /\ F ~~>* A ) -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )
10	2 6 7 9	xlimclim2lem	|- ( ( ph /\ F ~~>* A ) -> ( F ~~>* A <-> F ~~> A ) )
11	5 10	mpbid	|- ( ( ph /\ F ~~>* A ) -> F ~~> A )
12		simpr	|- ( ( ph /\ F ~~> A ) -> F ~~> A )
13	3	adantr	|- ( ( ph /\ F ~~> A ) -> F : Z --> RR* )
14	4	adantr	|- ( ( ph /\ F ~~> A ) -> A e. RR )
15	1	adantr	|- ( ( ph /\ F ~~> A ) -> M e. ZZ )
16	15 2 13 14 12	climxrre	|- ( ( ph /\ F ~~> A ) -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )
17	2 13 14 16	xlimclim2lem	|- ( ( ph /\ F ~~> A ) -> ( F ~~>* A <-> F ~~> A ) )
18	12 17	mpbird	|- ( ( ph /\ F ~~> A ) -> F ~~>* A )
19	11 18	impbida	|- ( ph -> ( F ~~>* A <-> F ~~> A ) )