Metamath Proof Explorer

Theorem 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 ${⊢}\left({F}⇝{A}\wedge {F}⇝{B}\right)\to {A}={B}$

Proof

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