climuni

Description: An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 2-Oct-1999) (Proof shortened by Mario Carneiro, 31-Jan-2014)

		Ref	Expression
	Assertion	climuni	$⊢ (F ⇝ A \land F ⇝ B) \to A = B$

Proof

Step	Hyp	Ref	Expression
1		1z	$⊢ 1 \in ℤ$
2		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
3		1zzd	$⊢ (F ⇝ A \land F ⇝ B \land A \neq B) \to 1 \in ℤ$
4		climcl	$⊢ F ⇝ A \to A \in ℂ$
5	4	3ad2ant1	$⊢ (F ⇝ A \land F ⇝ B \land A \neq B) \to A \in ℂ$
6		climcl	$⊢ F ⇝ B \to B \in ℂ$
7	6	3ad2ant2	$⊢ (F ⇝ A \land F ⇝ B \land A \neq B) \to B \in ℂ$
8	5 7	subcld	$⊢ (F ⇝ A \land F ⇝ B \land A \neq B) \to A - B \in ℂ$
9		simp3	$⊢ (F ⇝ A \land F ⇝ B \land A \neq B) \to A \neq B$
10	5 7 9	subne0d	$⊢ (F ⇝ A \land F ⇝ B \land A \neq B) \to A - B \neq 0$
11	8 10	absrpcld	$⊢ (F ⇝ A \land F ⇝ B \land A \neq B) \to \|A - B\| \in ℝ^{+}$
12	11	rphalfcld	$⊢ (F ⇝ A \land F ⇝ B \land A \neq B) \to \frac{\|A - B\|}{2} \in ℝ^{+}$
13		eqidd	$⊢ ((F ⇝ A \land F ⇝ B \land A \neq B) \land k \in ℕ) \to F (k) = F (k)$
14		simp1	$⊢ (F ⇝ A \land F ⇝ B \land A \neq B) \to F ⇝ A$
15	2 3 12 13 14	climi	$⊢ (F ⇝ A \land F ⇝ B \land A \neq B) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < \frac{\|A - B\|}{2})$
16		simp2	$⊢ (F ⇝ A \land F ⇝ B \land A \neq B) \to F ⇝ B$
17	2 3 12 13 16	climi	$⊢ (F ⇝ A \land F ⇝ B \land A \neq B) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - B\| < \frac{\|A - B\|}{2})$
18	2	rexanuz2	$⊢ \exists j \in ℕ \forall k \in ℤ_{\geq j} ((F (k) \in ℂ \land \|F (k) - A\| < \frac{\|A - B\|}{2}) \land (F (k) \in ℂ \land \|F (k) - B\| < \frac{\|A - B\|}{2})) \leftrightarrow (\exists j \in ℕ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < \frac{\|A - B\|}{2}) \land \exists j \in ℕ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - B\| < \frac{\|A - B\|}{2}))$
19	15 17 18	sylanbrc	$⊢ (F ⇝ A \land F ⇝ B \land A \neq B) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} ((F (k) \in ℂ \land \|F (k) - A\| < \frac{\|A - B\|}{2}) \land (F (k) \in ℂ \land \|F (k) - B\| < \frac{\|A - B\|}{2}))$
20		nnz	$⊢ j \in ℕ \to j \in ℤ$
21		uzid	$⊢ j \in ℤ \to j \in ℤ_{\geq j}$
22		ne0i	$⊢ j \in ℤ_{\geq j} \to ℤ_{\geq j} \neq \emptyset$
23		r19.2z	$⊢ (ℤ_{\geq j} \neq \emptyset \land \forall k \in ℤ_{\geq j} ((F (k) \in ℂ \land \|F (k) - A\| < \frac{\|A - B\|}{2}) \land (F (k) \in ℂ \land \|F (k) - B\| < \frac{\|A - B\|}{2}))) \to \exists k \in ℤ_{\geq j} ((F (k) \in ℂ \land \|F (k) - A\| < \frac{\|A - B\|}{2}) \land (F (k) \in ℂ \land \|F (k) - B\| < \frac{\|A - B\|}{2}))$
24	23	ex	$⊢ ℤ_{\geq j} \neq \emptyset \to (\forall k \in ℤ_{\geq j} ((F (k) \in ℂ \land \|F (k) - A\| < \frac{\|A - B\|}{2}) \land (F (k) \in ℂ \land \|F (k) - B\| < \frac{\|A - B\|}{2})) \to \exists k \in ℤ_{\geq j} ((F (k) \in ℂ \land \|F (k) - A\| < \frac{\|A - B\|}{2}) \land (F (k) \in ℂ \land \|F (k) - B\| < \frac{\|A - B\|}{2})))$
25	20 21 22 24	4syl	$⊢ j \in ℕ \to (\forall k \in ℤ_{\geq j} ((F (k) \in ℂ \land \|F (k) - A\| < \frac{\|A - B\|}{2}) \land (F (k) \in ℂ \land \|F (k) - B\| < \frac{\|A - B\|}{2})) \to \exists k \in ℤ_{\geq j} ((F (k) \in ℂ \land \|F (k) - A\| < \frac{\|A - B\|}{2}) \land (F (k) \in ℂ \land \|F (k) - B\| < \frac{\|A - B\|}{2})))$
26		simpr	$⊢ ((A \in ℂ \land B \in ℂ) \land F (k) \in ℂ) \to F (k) \in ℂ$
27		simpll	$⊢ ((A \in ℂ \land B \in ℂ) \land F (k) \in ℂ) \to A \in ℂ$
28	26 27	abssubd	$⊢ ((A \in ℂ \land B \in ℂ) \land F (k) \in ℂ) \to \|F (k) - A\| = \|A - F (k)\|$
29	28	breq1d	$⊢ ((A \in ℂ \land B \in ℂ) \land F (k) \in ℂ) \to (\|F (k) - A\| < \frac{\|A - B\|}{2} \leftrightarrow \|A - F (k)\| < \frac{\|A - B\|}{2})$
30		simplr	$⊢ ((A \in ℂ \land B \in ℂ) \land F (k) \in ℂ) \to B \in ℂ$
31		subcl	$⊢ (A \in ℂ \land B \in ℂ) \to A - B \in ℂ$
32	31	adantr	$⊢ ((A \in ℂ \land B \in ℂ) \land F (k) \in ℂ) \to A - B \in ℂ$
33	32	abscld	$⊢ ((A \in ℂ \land B \in ℂ) \land F (k) \in ℂ) \to \|A - B\| \in ℝ$
34		abs3lem	$⊢ ((A \in ℂ \land B \in ℂ) \land (F (k) \in ℂ \land \|A - B\| \in ℝ)) \to ((\|A - F (k)\| < \frac{\|A - B\|}{2} \land \|F (k) - B\| < \frac{\|A - B\|}{2}) \to \|A - B\| < \|A - B\|)$
35	27 30 26 33 34	syl22anc	$⊢ ((A \in ℂ \land B \in ℂ) \land F (k) \in ℂ) \to ((\|A - F (k)\| < \frac{\|A - B\|}{2} \land \|F (k) - B\| < \frac{\|A - B\|}{2}) \to \|A - B\| < \|A - B\|)$
36	33	ltnrd	$⊢ ((A \in ℂ \land B \in ℂ) \land F (k) \in ℂ) \to \neg \|A - B\| < \|A - B\|$
37	36	pm2.21d	$⊢ ((A \in ℂ \land B \in ℂ) \land F (k) \in ℂ) \to (\|A - B\| < \|A - B\| \to \neg 1 \in ℤ)$
38	35 37	syld	$⊢ ((A \in ℂ \land B \in ℂ) \land F (k) \in ℂ) \to ((\|A - F (k)\| < \frac{\|A - B\|}{2} \land \|F (k) - B\| < \frac{\|A - B\|}{2}) \to \neg 1 \in ℤ)$
39	38	expd	$⊢ ((A \in ℂ \land B \in ℂ) \land F (k) \in ℂ) \to (\|A - F (k)\| < \frac{\|A - B\|}{2} \to (\|F (k) - B\| < \frac{\|A - B\|}{2} \to \neg 1 \in ℤ))$
40	29 39	sylbid	$⊢ ((A \in ℂ \land B \in ℂ) \land F (k) \in ℂ) \to (\|F (k) - A\| < \frac{\|A - B\|}{2} \to (\|F (k) - B\| < \frac{\|A - B\|}{2} \to \neg 1 \in ℤ))$
41	40	impr	$⊢ ((A \in ℂ \land B \in ℂ) \land (F (k) \in ℂ \land \|F (k) - A\| < \frac{\|A - B\|}{2})) \to (\|F (k) - B\| < \frac{\|A - B\|}{2} \to \neg 1 \in ℤ)$
42	41	adantld	$⊢ ((A \in ℂ \land B \in ℂ) \land (F (k) \in ℂ \land \|F (k) - A\| < \frac{\|A - B\|}{2})) \to ((F (k) \in ℂ \land \|F (k) - B\| < \frac{\|A - B\|}{2}) \to \neg 1 \in ℤ)$
43	42	expimpd	$⊢ (A \in ℂ \land B \in ℂ) \to (((F (k) \in ℂ \land \|F (k) - A\| < \frac{\|A - B\|}{2}) \land (F (k) \in ℂ \land \|F (k) - B\| < \frac{\|A - B\|}{2})) \to \neg 1 \in ℤ)$
44	43	rexlimdvw	$⊢ (A \in ℂ \land B \in ℂ) \to (\exists k \in ℤ_{\geq j} ((F (k) \in ℂ \land \|F (k) - A\| < \frac{\|A - B\|}{2}) \land (F (k) \in ℂ \land \|F (k) - B\| < \frac{\|A - B\|}{2})) \to \neg 1 \in ℤ)$
45	25 44	sylan9r	$⊢ ((A \in ℂ \land B \in ℂ) \land j \in ℕ) \to (\forall k \in ℤ_{\geq j} ((F (k) \in ℂ \land \|F (k) - A\| < \frac{\|A - B\|}{2}) \land (F (k) \in ℂ \land \|F (k) - B\| < \frac{\|A - B\|}{2})) \to \neg 1 \in ℤ)$
46	45	rexlimdva	$⊢ (A \in ℂ \land B \in ℂ) \to (\exists j \in ℕ \forall k \in ℤ_{\geq j} ((F (k) \in ℂ \land \|F (k) - A\| < \frac{\|A - B\|}{2}) \land (F (k) \in ℂ \land \|F (k) - B\| < \frac{\|A - B\|}{2})) \to \neg 1 \in ℤ)$
47	5 7 46	syl2anc	$⊢ (F ⇝ A \land F ⇝ B \land A \neq B) \to (\exists j \in ℕ \forall k \in ℤ_{\geq j} ((F (k) \in ℂ \land \|F (k) - A\| < \frac{\|A - B\|}{2}) \land (F (k) \in ℂ \land \|F (k) - B\| < \frac{\|A - B\|}{2})) \to \neg 1 \in ℤ)$
48	19 47	mpd	$⊢ (F ⇝ A \land F ⇝ B \land A \neq B) \to \neg 1 \in ℤ$
49	48	3expia	$⊢ (F ⇝ A \land F ⇝ B) \to (A \neq B \to \neg 1 \in ℤ)$
50	49	necon4ad	$⊢ (F ⇝ A \land F ⇝ B) \to (1 \in ℤ \to A = B)$
51	1 50	mpi	$⊢ (F ⇝ A \land F ⇝ B) \to A = B$

Metamath Proof Explorer

Theorem climuni

Proof