Metamath Proof Explorer

Theorem lmclimf

Description: Relate a limit on the metric space of complex numbers to our complex number limit notation. (Contributed by NM, 24-Jul-2007) (Revised by Mario Carneiro, 1-May-2014)

Ref Expression
Hypotheses lmclim.2 ⊢ J = TopOpen ⁡ ℂ fld
lmclim.3 ⊢ Z = ℤ ≥ M
Assertion lmclimf ⊢ M ∈ ℤ ∧ F : Z ⟶ ℂ → F ⇝t ⁡ J P ↔ F ⇝ P

Proof

Step Hyp Ref Expression
1 lmclim.2 ⊢ J = TopOpen ⁡ ℂ fld
2 lmclim.3 ⊢ Z = ℤ ≥ M
3 simpr ⊢ M ∈ ℤ ∧ F : Z ⟶ ℂ → F : Z ⟶ ℂ
4 uzssz ⊢ ℤ ≥ M ⊆ ℤ
5 zsscn ⊢ ℤ ⊆ ℂ
6 4 5 sstri ⊢ ℤ ≥ M ⊆ ℂ
7 2 6 eqsstri ⊢ Z ⊆ ℂ
8 cnex ⊢ ℂ ∈ V
9 elpm2r ⊢ ℂ ∈ V ∧ ℂ ∈ V ∧ F : Z ⟶ ℂ ∧ Z ⊆ ℂ → F ∈ ℂ ↑ 𝑝𝑚 ℂ
10 8 8 9 mpanl12 ⊢ F : Z ⟶ ℂ ∧ Z ⊆ ℂ → F ∈ ℂ ↑ 𝑝𝑚 ℂ
11 3 7 10 sylancl ⊢ M ∈ ℤ ∧ F : Z ⟶ ℂ → F ∈ ℂ ↑ 𝑝𝑚 ℂ
12 fdm ⊢ F : Z ⟶ ℂ → dom ⁡ F = Z
13 eqimss2 ⊢ dom ⁡ F = Z → Z ⊆ dom ⁡ F
14 3 12 13 3syl ⊢ M ∈ ℤ ∧ F : Z ⟶ ℂ → Z ⊆ dom ⁡ F
15 1 2 lmclim ⊢ M ∈ ℤ ∧ Z ⊆ dom ⁡ F → F ⇝t ⁡ J P ↔ F ∈ ℂ ↑ 𝑝𝑚 ℂ ∧ F ⇝ P
16 14 15 syldan ⊢ M ∈ ℤ ∧ F : Z ⟶ ℂ → F ⇝t ⁡ J P ↔ F ∈ ℂ ↑ 𝑝𝑚 ℂ ∧ F ⇝ P
17 11 16 mpbirand ⊢ M ∈ ℤ ∧ F : Z ⟶ ℂ → F ⇝t ⁡ J P ↔ F ⇝ P