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

Metamath Proof Explorer

Theorem climcl

Description: Closure of the limit of a sequence of complex numbers. (Contributed by NM, 28-Aug-2005) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion climcl ( 𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ )

Proof

Step Hyp Ref Expression
1 climrel ⊢ Rel ⇝
2 1 brrelex1i ⊢ ( 𝐹 ⇝ 𝐴 → 𝐹 ∈ V )
3 eqidd ⊢ ( ( 𝐹 ⇝ 𝐴 ∧ 𝑘 ∈ ℤ ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
4 2 3 clim ⊢ ( 𝐹 ⇝ 𝐴 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) ) )
5 4 ibi ⊢ ( 𝐹 ⇝ 𝐴 → ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
6 5 simpld ⊢ ( 𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ )