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 e. ZZ
2 nnuz 
 |-  NN = ( ZZ>= ` 1 )
3 1zzd 
 |-  ( ( F ~~> A /\ F ~~> B /\ A =/= B ) -> 1 e. ZZ )
4 climcl 
 |-  ( F ~~> A -> A e. CC )
5 4 3ad2ant1 
 |-  ( ( F ~~> A /\ F ~~> B /\ A =/= B ) -> A e. CC )
6 climcl 
 |-  ( F ~~> B -> B e. CC )
7 6 3ad2ant2 
 |-  ( ( F ~~> A /\ F ~~> B /\ A =/= B ) -> B e. CC )
8 5 7 subcld 
 |-  ( ( F ~~> A /\ F ~~> B /\ A =/= B ) -> ( A - B ) e. CC )
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 ) -> ( abs ` ( A - B ) ) e. RR+ )
12 11 rphalfcld 
 |-  ( ( F ~~> A /\ F ~~> B /\ A =/= B ) -> ( ( abs ` ( A - B ) ) / 2 ) e. RR+ )
13 eqidd 
 |-  ( ( ( F ~~> A /\ F ~~> B /\ A =/= B ) /\ k e. NN ) -> ( 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 ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( ( abs ` ( 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 ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) )
18 2 rexanuz2 
 |-  ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) ) <-> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) /\ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) ) )
19 15 17 18 sylanbrc 
 |-  ( ( F ~~> A /\ F ~~> B /\ A =/= B ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) ) )
20 nnz 
 |-  ( j e. NN -> j e. ZZ )
21 uzid 
 |-  ( j e. ZZ -> j e. ( ZZ>= ` j ) )
22 ne0i 
 |-  ( j e. ( ZZ>= ` j ) -> ( ZZ>= ` j ) =/= (/) )
23 r19.2z 
 |-  ( ( ( ZZ>= ` j ) =/= (/) /\ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) ) ) -> E. k e. ( ZZ>= ` j ) ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) ) )
24 23 ex 
 |-  ( ( ZZ>= ` j ) =/= (/) -> ( A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) ) -> E. k e. ( ZZ>= ` j ) ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) ) ) )
25 20 21 22 24 4syl 
 |-  ( j e. NN -> ( A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) ) -> E. k e. ( ZZ>= ` j ) ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) ) ) )
26 simpr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( F ` k ) e. CC ) -> ( F ` k ) e. CC )
27 simpll 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( F ` k ) e. CC ) -> A e. CC )
28 26 27 abssubd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( F ` k ) e. CC ) -> ( abs ` ( ( F ` k ) - A ) ) = ( abs ` ( A - ( F ` k ) ) ) )
29 28 breq1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( F ` k ) e. CC ) -> ( ( abs ` ( ( F ` k ) - A ) ) < ( ( abs ` ( A - B ) ) / 2 ) <-> ( abs ` ( A - ( F ` k ) ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) )
30 simplr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( F ` k ) e. CC ) -> B e. CC )
31 subcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
32 31 adantr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( F ` k ) e. CC ) -> ( A - B ) e. CC )
33 32 abscld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( F ` k ) e. CC ) -> ( abs ` ( A - B ) ) e. RR )
34 abs3lem 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( A - B ) ) e. RR ) ) -> ( ( ( abs ` ( A - ( F ` k ) ) ) < ( ( abs ` ( A - B ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) -> ( abs ` ( A - B ) ) < ( abs ` ( A - B ) ) ) )
35 27 30 26 33 34 syl22anc 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( F ` k ) e. CC ) -> ( ( ( abs ` ( A - ( F ` k ) ) ) < ( ( abs ` ( A - B ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) -> ( abs ` ( A - B ) ) < ( abs ` ( A - B ) ) ) )
36 33 ltnrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( F ` k ) e. CC ) -> -. ( abs ` ( A - B ) ) < ( abs ` ( A - B ) ) )
37 36 pm2.21d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( F ` k ) e. CC ) -> ( ( abs ` ( A - B ) ) < ( abs ` ( A - B ) ) -> -. 1 e. ZZ ) )
38 35 37 syld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( F ` k ) e. CC ) -> ( ( ( abs ` ( A - ( F ` k ) ) ) < ( ( abs ` ( A - B ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) -> -. 1 e. ZZ ) )
39 38 expd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( F ` k ) e. CC ) -> ( ( abs ` ( A - ( F ` k ) ) ) < ( ( abs ` ( A - B ) ) / 2 ) -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( A - B ) ) / 2 ) -> -. 1 e. ZZ ) ) )
40 29 39 sylbid 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( F ` k ) e. CC ) -> ( ( abs ` ( ( F ` k ) - A ) ) < ( ( abs ` ( A - B ) ) / 2 ) -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( A - B ) ) / 2 ) -> -. 1 e. ZZ ) ) )
41 40 impr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) ) -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( A - B ) ) / 2 ) -> -. 1 e. ZZ ) )
42 41 adantld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) ) -> ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) -> -. 1 e. ZZ ) )
43 42 expimpd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) ) -> -. 1 e. ZZ ) )
44 43 rexlimdvw 
 |-  ( ( A e. CC /\ B e. CC ) -> ( E. k e. ( ZZ>= ` j ) ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) ) -> -. 1 e. ZZ ) )
45 25 44 sylan9r 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) ) -> -. 1 e. ZZ ) )
46 45 rexlimdva 
 |-  ( ( A e. CC /\ B e. CC ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) ) -> -. 1 e. ZZ ) )
47 5 7 46 syl2anc 
 |-  ( ( F ~~> A /\ F ~~> B /\ A =/= B ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( A - B ) ) / 2 ) ) ) -> -. 1 e. ZZ ) )
48 19 47 mpd 
 |-  ( ( F ~~> A /\ F ~~> B /\ A =/= B ) -> -. 1 e. ZZ )
49 48 3expia 
 |-  ( ( F ~~> A /\ F ~~> B ) -> ( A =/= B -> -. 1 e. ZZ ) )
50 49 necon4ad 
 |-  ( ( F ~~> A /\ F ~~> B ) -> ( 1 e. ZZ -> A = B ) )
51 1 50 mpi 
 |-  ( ( F ~~> A /\ F ~~> B ) -> A = B )