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 ( ( 𝐹𝐴𝐹𝐵 ) → 𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 1z 1 ∈ ℤ
2 nnuz ℕ = ( ℤ ‘ 1 )
3 1zzd ( ( 𝐹𝐴𝐹𝐵𝐴𝐵 ) → 1 ∈ ℤ )
4 climcl ( 𝐹𝐴𝐴 ∈ ℂ )
5 4 3ad2ant1 ( ( 𝐹𝐴𝐹𝐵𝐴𝐵 ) → 𝐴 ∈ ℂ )
6 climcl ( 𝐹𝐵𝐵 ∈ ℂ )
7 6 3ad2ant2 ( ( 𝐹𝐴𝐹𝐵𝐴𝐵 ) → 𝐵 ∈ ℂ )
8 5 7 subcld ( ( 𝐹𝐴𝐹𝐵𝐴𝐵 ) → ( 𝐴𝐵 ) ∈ ℂ )
9 simp3 ( ( 𝐹𝐴𝐹𝐵𝐴𝐵 ) → 𝐴𝐵 )
10 5 7 9 subne0d ( ( 𝐹𝐴𝐹𝐵𝐴𝐵 ) → ( 𝐴𝐵 ) ≠ 0 )
11 8 10 absrpcld ( ( 𝐹𝐴𝐹𝐵𝐴𝐵 ) → ( abs ‘ ( 𝐴𝐵 ) ) ∈ ℝ+ )
12 11 rphalfcld ( ( 𝐹𝐴𝐹𝐵𝐴𝐵 ) → ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ∈ ℝ+ )
13 eqidd ( ( ( 𝐹𝐴𝐹𝐵𝐴𝐵 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐹𝑘 ) = ( 𝐹𝑘 ) )
14 simp1 ( ( 𝐹𝐴𝐹𝐵𝐴𝐵 ) → 𝐹𝐴 )
15 2 3 12 13 14 climi ( ( 𝐹𝐴𝐹𝐵𝐴𝐵 ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) )
16 simp2 ( ( 𝐹𝐴𝐹𝐵𝐴𝐵 ) → 𝐹𝐵 )
17 2 3 12 13 16 climi ( ( 𝐹𝐴𝐹𝐵𝐴𝐵 ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) )
18 2 rexanuz2 ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ) ↔ ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ∧ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ) )
19 15 17 18 sylanbrc ( ( 𝐹𝐴𝐹𝐵𝐴𝐵 ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ) )
20 nnz ( 𝑗 ∈ ℕ → 𝑗 ∈ ℤ )
21 uzid ( 𝑗 ∈ ℤ → 𝑗 ∈ ( ℤ𝑗 ) )
22 ne0i ( 𝑗 ∈ ( ℤ𝑗 ) → ( ℤ𝑗 ) ≠ ∅ )
23 r19.2z ( ( ( ℤ𝑗 ) ≠ ∅ ∧ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ) ) → ∃ 𝑘 ∈ ( ℤ𝑗 ) ( ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ) )
24 23 ex ( ( ℤ𝑗 ) ≠ ∅ → ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ) → ∃ 𝑘 ∈ ( ℤ𝑗 ) ( ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ) ) )
25 20 21 22 24 4syl ( 𝑗 ∈ ℕ → ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ) → ∃ 𝑘 ∈ ( ℤ𝑗 ) ( ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ) ) )
26 simpr ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹𝑘 ) ∈ ℂ ) → ( 𝐹𝑘 ) ∈ ℂ )
27 simpll ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹𝑘 ) ∈ ℂ ) → 𝐴 ∈ ℂ )
28 26 27 abssubd ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹𝑘 ) ∈ ℂ ) → ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) = ( abs ‘ ( 𝐴 − ( 𝐹𝑘 ) ) ) )
29 28 breq1d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹𝑘 ) ∈ ℂ ) → ( ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ↔ ( abs ‘ ( 𝐴 − ( 𝐹𝑘 ) ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) )
30 simplr ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹𝑘 ) ∈ ℂ ) → 𝐵 ∈ ℂ )
31 subcl ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴𝐵 ) ∈ ℂ )
32 31 adantr ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹𝑘 ) ∈ ℂ ) → ( 𝐴𝐵 ) ∈ ℂ )
33 32 abscld ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹𝑘 ) ∈ ℂ ) → ( abs ‘ ( 𝐴𝐵 ) ) ∈ ℝ )
34 abs3lem ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( 𝐴𝐵 ) ) ∈ ℝ ) ) → ( ( ( abs ‘ ( 𝐴 − ( 𝐹𝑘 ) ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) → ( abs ‘ ( 𝐴𝐵 ) ) < ( abs ‘ ( 𝐴𝐵 ) ) ) )
35 27 30 26 33 34 syl22anc ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹𝑘 ) ∈ ℂ ) → ( ( ( abs ‘ ( 𝐴 − ( 𝐹𝑘 ) ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) → ( abs ‘ ( 𝐴𝐵 ) ) < ( abs ‘ ( 𝐴𝐵 ) ) ) )
36 33 ltnrd ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹𝑘 ) ∈ ℂ ) → ¬ ( abs ‘ ( 𝐴𝐵 ) ) < ( abs ‘ ( 𝐴𝐵 ) ) )
37 36 pm2.21d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹𝑘 ) ∈ ℂ ) → ( ( abs ‘ ( 𝐴𝐵 ) ) < ( abs ‘ ( 𝐴𝐵 ) ) → ¬ 1 ∈ ℤ ) )
38 35 37 syld ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹𝑘 ) ∈ ℂ ) → ( ( ( abs ‘ ( 𝐴 − ( 𝐹𝑘 ) ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) → ¬ 1 ∈ ℤ ) )
39 38 expd ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹𝑘 ) ∈ ℂ ) → ( ( abs ‘ ( 𝐴 − ( 𝐹𝑘 ) ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) → ( ( abs ‘ ( ( 𝐹𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) → ¬ 1 ∈ ℤ ) ) )
40 29 39 sylbid ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹𝑘 ) ∈ ℂ ) → ( ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) → ( ( abs ‘ ( ( 𝐹𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) → ¬ 1 ∈ ℤ ) ) )
41 40 impr ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ) → ( ( abs ‘ ( ( 𝐹𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) → ¬ 1 ∈ ℤ ) )
42 41 adantld ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ) → ( ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) → ¬ 1 ∈ ℤ ) )
43 42 expimpd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ) → ¬ 1 ∈ ℤ ) )
44 43 rexlimdvw ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∃ 𝑘 ∈ ( ℤ𝑗 ) ( ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ) → ¬ 1 ∈ ℤ ) )
45 25 44 sylan9r ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑗 ∈ ℕ ) → ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ) → ¬ 1 ∈ ℤ ) )
46 45 rexlimdva ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ) → ¬ 1 ∈ ℤ ) )
47 5 7 46 syl2anc ( ( 𝐹𝐴𝐹𝐵𝐴𝐵 ) → ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴𝐵 ) ) / 2 ) ) ) → ¬ 1 ∈ ℤ ) )
48 19 47 mpd ( ( 𝐹𝐴𝐹𝐵𝐴𝐵 ) → ¬ 1 ∈ ℤ )
49 48 3expia ( ( 𝐹𝐴𝐹𝐵 ) → ( 𝐴𝐵 → ¬ 1 ∈ ℤ ) )
50 49 necon4ad ( ( 𝐹𝐴𝐹𝐵 ) → ( 1 ∈ ℤ → 𝐴 = 𝐵 ) )
51 1 50 mpi ( ( 𝐹𝐴𝐹𝐵 ) → 𝐴 = 𝐵 )