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

Metamath Proof Explorer

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