Metamath Proof Explorer

Theorem climreu

Description: An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005)

Ref Expression
Assertion climreu ( 𝐹 ⇝ 𝐴 → ∃! 𝑥 ∈ ℂ 𝐹 ⇝ 𝑥 )

Proof

Step Hyp Ref Expression
1 climeu ⊢ ( 𝐹 ⇝ 𝐴 → ∃! 𝑥 𝐹 ⇝ 𝑥 )
2 climcl ⊢ ( 𝐹 ⇝ 𝑥 → 𝑥 ∈ ℂ )
3 2 pm4.71ri ⊢ ( 𝐹 ⇝ 𝑥 ↔ ( 𝑥 ∈ ℂ ∧ 𝐹 ⇝ 𝑥 ) )
4 3 eubii ⊢ ( ∃! 𝑥 𝐹 ⇝ 𝑥 ↔ ∃! 𝑥 ( 𝑥 ∈ ℂ ∧ 𝐹 ⇝ 𝑥 ) )
5 df-reu ⊢ ( ∃! 𝑥 ∈ ℂ 𝐹 ⇝ 𝑥 ↔ ∃! 𝑥 ( 𝑥 ∈ ℂ ∧ 𝐹 ⇝ 𝑥 ) )
6 4 5 bitr4i ⊢ ( ∃! 𝑥 𝐹 ⇝ 𝑥 ↔ ∃! 𝑥 ∈ ℂ 𝐹 ⇝ 𝑥 )
7 1 6 sylib ⊢ ( 𝐹 ⇝ 𝐴 → ∃! 𝑥 ∈ ℂ 𝐹 ⇝ 𝑥 )