climeu

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

		Ref	Expression
	Assertion	climeu	$⊢ F ⇝ A \to \exists! x F ⇝ x$

Step	Hyp	Ref	Expression
1		climcl	$⊢ F ⇝ A \to A \in ℂ$
2		breq2	$⊢ y = A \to (F ⇝ y \leftrightarrow F ⇝ A)$
3	2	spcegv	$⊢ A \in ℂ \to (F ⇝ A \to \exists y F ⇝ y)$
4	1 3	mpcom	$⊢ F ⇝ A \to \exists y F ⇝ y$
5		climuni	$⊢ (F ⇝ y \land F ⇝ x) \to y = x$
6	5	gen2	$⊢ \forall y \forall x ((F ⇝ y \land F ⇝ x) \to y = x)$
7		nfv	$⊢ Ⅎ y F ⇝ x$
8		nfv	$⊢ Ⅎ x F ⇝ y$
9		breq2	$⊢ x = y \to (F ⇝ x \leftrightarrow F ⇝ y)$
10	7 8 9	cbveuw	$⊢ \exists! x F ⇝ x \leftrightarrow \exists! y F ⇝ y$
11		breq2	$⊢ y = x \to (F ⇝ y \leftrightarrow F ⇝ x)$
12	11	eu4	$⊢ \exists! y F ⇝ y \leftrightarrow (\exists y F ⇝ y \land \forall y \forall x ((F ⇝ y \land F ⇝ x) \to y = x))$
13	10 12	bitri	$⊢ \exists! x F ⇝ x \leftrightarrow (\exists y F ⇝ y \land \forall y \forall x ((F ⇝ y \land F ⇝ x) \to y = x))$
14	4 6 13	sylanblrc	$⊢ F ⇝ A \to \exists! x F ⇝ x$

Metamath Proof Explorer