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	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℂ ) → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ 𝐹 ⇝ 𝑃 ) )