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 = ℤ ≥ M
climreeq.3 ⊢ φ → M ∈ ℤ
climreeq.4 ⊢ φ → F : Z ⟶ ℝ
Assertion climreeq ⊢ φ → F R A ↔ F ⇝ A

Proof

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