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

Metamath Proof Explorer

Theorem climeu

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

Ref Expression
Assertion climeu ( 𝐹 ⇝ 𝐴 → ∃! 𝑥 𝐹 ⇝ 𝑥 )

Proof

Step Hyp Ref Expression
1 climcl ⊢ ( 𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ )
2 breq2 ⊢ ( 𝑦 = 𝐴 → ( 𝐹 ⇝ 𝑦 ↔ 𝐹 ⇝ 𝐴 ) )
3 2 spcegv ⊢ ( 𝐴 ∈ ℂ → ( 𝐹 ⇝ 𝐴 → ∃ 𝑦 𝐹 ⇝ 𝑦 ) )
4 1 3 mpcom ⊢ ( 𝐹 ⇝ 𝐴 → ∃ 𝑦 𝐹 ⇝ 𝑦 )
5 climuni ⊢ ( ( 𝐹 ⇝ 𝑦 ∧ 𝐹 ⇝ 𝑥 ) → 𝑦 = 𝑥 )
6 5 gen2 ⊢ ∀ 𝑦 ∀ 𝑥 ( ( 𝐹 ⇝ 𝑦 ∧ 𝐹 ⇝ 𝑥 ) → 𝑦 = 𝑥 )
7 nfv ⊢ Ⅎ 𝑦 𝐹 ⇝ 𝑥
8 nfv ⊢ Ⅎ 𝑥 𝐹 ⇝ 𝑦
9 breq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ⇝ 𝑥 ↔ 𝐹 ⇝ 𝑦 ) )
10 7 8 9 cbveuw ⊢ ( ∃! 𝑥 𝐹 ⇝ 𝑥 ↔ ∃! 𝑦 𝐹 ⇝ 𝑦 )
11 breq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐹 ⇝ 𝑦 ↔ 𝐹 ⇝ 𝑥 ) )
12 11 eu4 ⊢ ( ∃! 𝑦 𝐹 ⇝ 𝑦 ↔ ( ∃ 𝑦 𝐹 ⇝ 𝑦 ∧ ∀ 𝑦 ∀ 𝑥 ( ( 𝐹 ⇝ 𝑦 ∧ 𝐹 ⇝ 𝑥 ) → 𝑦 = 𝑥 ) ) )
13 10 12 bitri ⊢ ( ∃! 𝑥 𝐹 ⇝ 𝑥 ↔ ( ∃ 𝑦 𝐹 ⇝ 𝑦 ∧ ∀ 𝑦 ∀ 𝑥 ( ( 𝐹 ⇝ 𝑦 ∧ 𝐹 ⇝ 𝑥 ) → 𝑦 = 𝑥 ) ) )
14 4 6 13 sylanblrc ⊢ ( 𝐹 ⇝ 𝐴 → ∃! 𝑥 𝐹 ⇝ 𝑥 )