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 ⊢ 𝑅 = ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) )
climreeq.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climreeq.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climreeq.4 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
Assertion climreeq ( 𝜑 → ( 𝐹 𝑅 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 climreeq.1 ⊢ 𝑅 = ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) )
2 climreeq.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 climreeq.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 climreeq.4 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
5 1 breqi ⊢ ( 𝐹 𝑅 𝐴 ↔ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 )
6 ax-resscn ⊢ ℝ ⊆ ℂ
7 6 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
8 4 7 fssd ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℂ )
9 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
10 9 2 lmclimf ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℂ ) → ( 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )
11 3 8 10 syl2anc ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )
12 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
13 reex ⊢ ℝ ∈ V
14 13 a1i ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → ℝ ∈ V )
15 9 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
16 15 a1i ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → ( TopOpen ‘ ℂfld ) ∈ Top )
17 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝐴 ∈ ℝ )
18 3 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝑀 ∈ ℤ )
19 4 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝐹 : 𝑍 ⟶ ℝ )
20 12 2 14 16 17 18 19 lmss ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → ( 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ↔ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) )
21 20 pm5.32da ⊢ ( 𝜑 → ( ( 𝐴 ∈ ℝ ∧ 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ) ↔ ( 𝐴 ∈ ℝ ∧ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) ) )
22 simpr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ) → 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 )
23 3 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ) → 𝑀 ∈ ℤ )
24 11 biimpa ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ) → 𝐹 ⇝ 𝐴 )
25 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
26 25 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
27 2 23 24 26 climrecl ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ) → 𝐴 ∈ ℝ )
28 27 ex ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 → 𝐴 ∈ ℝ ) )
29 28 ancrd ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 → ( 𝐴 ∈ ℝ ∧ 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ) ) )
30 22 29 impbid2 ⊢ ( 𝜑 → ( ( 𝐴 ∈ ℝ ∧ 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ) ↔ 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ) )
31 simpr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) → 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 )
32 retopon ⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
33 32 a1i ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) → ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) )
34 simpr ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) → 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 )
35 lmcl ⊢ ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) → 𝐴 ∈ ℝ )
36 33 34 35 syl2anc ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) → 𝐴 ∈ ℝ )
37 36 ex ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 → 𝐴 ∈ ℝ ) )
38 37 ancrd ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 → ( 𝐴 ∈ ℝ ∧ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) ) )
39 31 38 impbid2 ⊢ ( 𝜑 → ( ( 𝐴 ∈ ℝ ∧ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) ↔ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) )
40 21 30 39 3bitr3d ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ↔ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) )
41 11 40 bitr3d ⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) )
42 5 41 bitr4id ⊢ ( 𝜑 → ( 𝐹 𝑅 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )