climxlim2

Description: A sequence of extended reals, converging w.r.t. the standard topology on the complex numbers is a converging sequence w.r.t. the standard topology on the extended reals. This is non-trivial, because +oo and -oo could, in principle, be complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022)

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

Proof

Step	Hyp	Ref	Expression
1		climxlim2.m	\|- ( ph -> M e. ZZ )
2		climxlim2.z	\|- Z = ( ZZ>= ` M )
3		climxlim2.f	\|- ( ph -> F : Z --> RR* )
4		climxlim2.a	\|- ( ph -> F ~~> A )
5	2	eluzelz2	\|- ( j e. Z -> j e. ZZ )
6	5	ad2antlr	\|- ( ( ( ph /\ j e. Z ) /\ ( F \|` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> CC ) -> j e. ZZ )
7		eqid	\|- ( ZZ>= ` j ) = ( ZZ>= ` j )
8	3	adantr	\|- ( ( ph /\ j e. Z ) -> F : Z --> RR* )
9	2	uzssd3	\|- ( j e. Z -> ( ZZ>= ` j ) C_ Z )
10	9	adantl	\|- ( ( ph /\ j e. Z ) -> ( ZZ>= ` j ) C_ Z )
11	8 10	fssresd	\|- ( ( ph /\ j e. Z ) -> ( F \|` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR* )
12	11	adantr	\|- ( ( ( ph /\ j e. Z ) /\ ( F \|` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> CC ) -> ( F \|` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR* )
13		simpr	\|- ( ( ( ph /\ j e. Z ) /\ ( F \|` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> CC ) -> ( F \|` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> CC )
14	4	adantr	\|- ( ( ph /\ j e. Z ) -> F ~~> A )
15	2	fvexi	\|- Z e. _V
16	15	a1i	\|- ( ph -> Z e. _V )
17	3 16	fexd	\|- ( ph -> F e. _V )
18		climres	\|- ( ( j e. ZZ /\ F e. _V ) -> ( ( F \|` ( ZZ>= ` j ) ) ~~> A <-> F ~~> A ) )
19	5 17 18	syl2anr	\|- ( ( ph /\ j e. Z ) -> ( ( F \|` ( ZZ>= ` j ) ) ~~> A <-> F ~~> A ) )
20	14 19	mpbird	\|- ( ( ph /\ j e. Z ) -> ( F \|` ( ZZ>= ` j ) ) ~~> A )
21	20	adantr	\|- ( ( ( ph /\ j e. Z ) /\ ( F \|` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> CC ) -> ( F \|` ( ZZ>= ` j ) ) ~~> A )
22	6 7 12 13 21	climxlim2lem	\|- ( ( ( ph /\ j e. Z ) /\ ( F \|` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> CC ) -> ( F \|` ( ZZ>= ` j ) ) ~~>* A )
23	2 3	fuzxrpmcn	\|- ( ph -> F e. ( RR* ^pm CC ) )
24	23	adantr	\|- ( ( ph /\ j e. Z ) -> F e. ( RR* ^pm CC ) )
25	5	adantl	\|- ( ( ph /\ j e. Z ) -> j e. ZZ )
26	24 25	xlimres	\|- ( ( ph /\ j e. Z ) -> ( F ~~>* A <-> ( F \|` ( ZZ>= ` j ) ) ~~>* A ) )
27	26	adantr	\|- ( ( ( ph /\ j e. Z ) /\ ( F \|` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> CC ) -> ( F ~~>* A <-> ( F \|` ( ZZ>= ` j ) ) ~~>* A ) )
28	22 27	mpbird	\|- ( ( ( ph /\ j e. Z ) /\ ( F \|` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> CC ) -> F ~~>* A )
29	3	ffnd	\|- ( ph -> F Fn Z )
30		climcl	\|- ( F ~~> A -> A e. CC )
31	4 30	syl	\|- ( ph -> A e. CC )
32		breldmg	\|- ( ( F e. _V /\ A e. CC /\ F ~~> A ) -> F e. dom ~~> )
33	17 31 4 32	syl3anc	\|- ( ph -> F e. dom ~~> )
34	1 2 29 33	climrescn	\|- ( ph -> E. j e. Z ( F \|` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> CC )
35	28 34	r19.29a	\|- ( ph -> F ~~>* A )

Metamath Proof Explorer

Theorem climxlim2

Proof