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 F A F B A = B

Proof

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