Theorem rlimcl

Description: Closure of the limit of a sequence of complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014) (Revised by Mario Carneiro, 28-Apr-2015)

	Ref	Expression
Assertion	rlimcl	⊢ ( 𝐹 ⇝𝑟 𝐴 → 𝐴 ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		rlimf	⊢ ( 𝐹 ⇝𝑟 𝐴 → 𝐹 : dom 𝐹 ⟶ ℂ )
2		rlimss	⊢ ( 𝐹 ⇝𝑟 𝐴 → dom 𝐹 ⊆ ℝ )
3		eqidd	⊢ ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
4	1 2 3	rlim	⊢ ( 𝐹 ⇝𝑟 𝐴 → ( 𝐹 ⇝𝑟 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ dom 𝐹 ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐴 ) ) < 𝑦 ) ) ) )
5	4	ibi	⊢ ( 𝐹 ⇝𝑟 𝐴 → ( 𝐴 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ dom 𝐹 ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐴 ) ) < 𝑦 ) ) )
6	5	simpld	⊢ ( 𝐹 ⇝𝑟 𝐴 → 𝐴 ∈ ℂ )