climreu

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

		Ref	Expression
	Assertion	climreu	$⊢ F ⇝ A \to \exists! x \in ℂ F ⇝ x$

Step	Hyp	Ref	Expression
1		climeu	$⊢ F ⇝ A \to \exists! x F ⇝ x$
2		climcl	$⊢ F ⇝ x \to x \in ℂ$
3	2	pm4.71ri	$⊢ F ⇝ x \leftrightarrow (x \in ℂ \land F ⇝ x)$
4	3	eubii	$⊢ \exists! x F ⇝ x \leftrightarrow \exists! x (x \in ℂ \land F ⇝ x)$
5		df-reu	$⊢ \exists! x \in ℂ F ⇝ x \leftrightarrow \exists! x (x \in ℂ \land F ⇝ x)$
6	4 5	bitr4i	$⊢ \exists! x F ⇝ x \leftrightarrow \exists! x \in ℂ F ⇝ x$
7	1 6	sylib	$⊢ F ⇝ A \to \exists! x \in ℂ F ⇝ x$

Metamath Proof Explorer