Theorem climreeq

Description: If F is a real function, then F converges to A with respect to the standard topology on the reals if and only if it converges to A with respect to the standard topology on complex numbers. In the theorem, R is defined to be convergence w.r.t. the standard topology on the reals and then F R A represents the statement " F converges to A , with respect to the standard topology on the reals". Notice that there is no need for the hypothesis that A is a real number. (Contributed by Glauco Siliprandi, 2-Jul-2017)

	Ref	Expression
Hypotheses	climreeq.1	|- R = ( ~~>t ` ( topGen ` ran (,) ) )
	climreeq.2	|- Z = ( ZZ>= ` M )
	climreeq.3	|- ( ph -> M e. ZZ )
	climreeq.4	|- ( ph -> F : Z --> RR )
Assertion	climreeq	|- ( ph -> ( F R A <-> F ~~> A ) )

Proof

Step	Hyp	Ref	Expression
1		climreeq.1	|- R = ( ~~>t ` ( topGen ` ran (,) ) )
2		climreeq.2	|- Z = ( ZZ>= ` M )
3		climreeq.3	|- ( ph -> M e. ZZ )
4		climreeq.4	|- ( ph -> F : Z --> RR )
5	1	breqi	|- ( F R A <-> F ( ~~>t ` ( topGen ` ran (,) ) ) A )
6		ax-resscn	|- RR C_ CC
7	6	a1i	|- ( ph -> RR C_ CC )
8	4 7	fssd	|- ( ph -> F : Z --> CC )
9		eqid	|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
10	9 2	lmclimf	|- ( ( M e. ZZ /\ F : Z --> CC ) -> ( F ( ~~>t ` ( TopOpen ` CCfld ) ) A <-> F ~~> A ) )
11	3 8 10	syl2anc	|- ( ph -> ( F ( ~~>t ` ( TopOpen ` CCfld ) ) A <-> F ~~> A ) )
12		tgioo4	|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
13		reex	|- RR e. _V
14	13	a1i	|- ( ( ph /\ A e. RR ) -> RR e. _V )
15	9	cnfldtop	|- ( TopOpen ` CCfld ) e. Top
16	15	a1i	|- ( ( ph /\ A e. RR ) -> ( TopOpen ` CCfld ) e. Top )
17		simpr	|- ( ( ph /\ A e. RR ) -> A e. RR )
18	3	adantr	|- ( ( ph /\ A e. RR ) -> M e. ZZ )
19	4	adantr	|- ( ( ph /\ A e. RR ) -> F : Z --> RR )
20	12 2 14 16 17 18 19	lmss	|- ( ( ph /\ A e. RR ) -> ( F ( ~~>t ` ( TopOpen ` CCfld ) ) A <-> F ( ~~>t ` ( topGen ` ran (,) ) ) A ) )
21	20	pm5.32da	|- ( ph -> ( ( A e. RR /\ F ( ~~>t ` ( TopOpen ` CCfld ) ) A ) <-> ( A e. RR /\ F ( ~~>t ` ( topGen ` ran (,) ) ) A ) ) )
22		simpr	|- ( ( A e. RR /\ F ( ~~>t ` ( TopOpen ` CCfld ) ) A ) -> F ( ~~>t ` ( TopOpen ` CCfld ) ) A )
23	3	adantr	|- ( ( ph /\ F ( ~~>t ` ( TopOpen ` CCfld ) ) A ) -> M e. ZZ )
24	11	biimpa	|- ( ( ph /\ F ( ~~>t ` ( TopOpen ` CCfld ) ) A ) -> F ~~> A )
25	4	ffvelcdmda	|- ( ( ph /\ n e. Z ) -> ( F ` n ) e. RR )
26	25	adantlr	|- ( ( ( ph /\ F ( ~~>t ` ( TopOpen ` CCfld ) ) A ) /\ n e. Z ) -> ( F ` n ) e. RR )
27	2 23 24 26	climrecl	|- ( ( ph /\ F ( ~~>t ` ( TopOpen ` CCfld ) ) A ) -> A e. RR )
28	27	ex	|- ( ph -> ( F ( ~~>t ` ( TopOpen ` CCfld ) ) A -> A e. RR ) )
29	28	ancrd	|- ( ph -> ( F ( ~~>t ` ( TopOpen ` CCfld ) ) A -> ( A e. RR /\ F ( ~~>t ` ( TopOpen ` CCfld ) ) A ) ) )
30	22 29	impbid2	|- ( ph -> ( ( A e. RR /\ F ( ~~>t ` ( TopOpen ` CCfld ) ) A ) <-> F ( ~~>t ` ( TopOpen ` CCfld ) ) A ) )
31		simpr	|- ( ( A e. RR /\ F ( ~~>t ` ( topGen ` ran (,) ) ) A ) -> F ( ~~>t ` ( topGen ` ran (,) ) ) A )
32		retopon	|- ( topGen ` ran (,) ) e. ( TopOn ` RR )
33	32	a1i	|- ( ( ph /\ F ( ~~>t ` ( topGen ` ran (,) ) ) A ) -> ( topGen ` ran (,) ) e. ( TopOn ` RR ) )
34		simpr	|- ( ( ph /\ F ( ~~>t ` ( topGen ` ran (,) ) ) A ) -> F ( ~~>t ` ( topGen ` ran (,) ) ) A )
35		lmcl	|- ( ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ F ( ~~>t ` ( topGen ` ran (,) ) ) A ) -> A e. RR )
36	33 34 35	syl2anc	|- ( ( ph /\ F ( ~~>t ` ( topGen ` ran (,) ) ) A ) -> A e. RR )
37	36	ex	|- ( ph -> ( F ( ~~>t ` ( topGen ` ran (,) ) ) A -> A e. RR ) )
38	37	ancrd	|- ( ph -> ( F ( ~~>t ` ( topGen ` ran (,) ) ) A -> ( A e. RR /\ F ( ~~>t ` ( topGen ` ran (,) ) ) A ) ) )
39	31 38	impbid2	|- ( ph -> ( ( A e. RR /\ F ( ~~>t ` ( topGen ` ran (,) ) ) A ) <-> F ( ~~>t ` ( topGen ` ran (,) ) ) A ) )
40	21 30 39	3bitr3d	|- ( ph -> ( F ( ~~>t ` ( TopOpen ` CCfld ) ) A <-> F ( ~~>t ` ( topGen ` ran (,) ) ) A ) )
41	11 40	bitr3d	|- ( ph -> ( F ~~> A <-> F ( ~~>t ` ( topGen ` ran (,) ) ) A ) )
42	5 41	bitr4id	|- ( ph -> ( F R A <-> F ~~> A ) )