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	⊢ ( 𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ )