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

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 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
lmclim.3 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion lmclimf ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℂ ) → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ 𝐹 ⇝ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 lmclim.2 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2 lmclim.3 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 simpr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℂ ) → 𝐹 : 𝑍 ⟶ ℂ )
4 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
5 zsscn ⊢ ℤ ⊆ ℂ
6 4 5 sstri ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℂ
7 2 6 eqsstri ⊢ 𝑍 ⊆ ℂ
8 cnex ⊢ ℂ ∈ V
9 elpm2r ⊢ ( ( ( ℂ ∈ V ∧ ℂ ∈ V ) ∧ ( 𝐹 : 𝑍 ⟶ ℂ ∧ 𝑍 ⊆ ℂ ) ) → 𝐹 ∈ ( ℂ ↑pm ℂ ) )
10 8 8 9 mpanl12 ⊢ ( ( 𝐹 : 𝑍 ⟶ ℂ ∧ 𝑍 ⊆ ℂ ) → 𝐹 ∈ ( ℂ ↑pm ℂ ) )
11 3 7 10 sylancl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℂ ) → 𝐹 ∈ ( ℂ ↑pm ℂ ) )
12 fdm ⊢ ( 𝐹 : 𝑍 ⟶ ℂ → dom 𝐹 = 𝑍 )
13 eqimss2 ⊢ ( dom 𝐹 = 𝑍 → 𝑍 ⊆ dom 𝐹 )
14 3 12 13 3syl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℂ ) → 𝑍 ⊆ dom 𝐹 )
15 1 2 lmclim ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹 ) → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( ℂ ↑pm ℂ ) ∧ 𝐹 ⇝ 𝑃 ) ) )
16 14 15 syldan ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℂ ) → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( ℂ ↑pm ℂ ) ∧ 𝐹 ⇝ 𝑃 ) ) )
17 11 16 mpbirand ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℂ ) → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ 𝐹 ⇝ 𝑃 ) )