Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  climuni Structured version   Visualization version   GIF version

Theorem climuni 14957
 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.)
Assertion
Ref Expression
climuni ((𝐹𝐴𝐹𝐵) → 𝐴 = 𝐵)

Proof of Theorem climuni
Dummy variables 𝑗 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1z 12051 . 2 1 ∈ ℤ
2 nnuz 12321 . . . . . . 7 ℕ = (ℤ‘1)
3 1zzd 12052 . . . . . . 7 ((𝐹𝐴𝐹𝐵𝐴𝐵) → 1 ∈ ℤ)
4 climcl 14904 . . . . . . . . . . 11 (𝐹𝐴𝐴 ∈ ℂ)
543ad2ant1 1130 . . . . . . . . . 10 ((𝐹𝐴𝐹𝐵𝐴𝐵) → 𝐴 ∈ ℂ)
6 climcl 14904 . . . . . . . . . . 11 (𝐹𝐵𝐵 ∈ ℂ)
763ad2ant2 1131 . . . . . . . . . 10 ((𝐹𝐴𝐹𝐵𝐴𝐵) → 𝐵 ∈ ℂ)
85, 7subcld 11035 . . . . . . . . 9 ((𝐹𝐴𝐹𝐵𝐴𝐵) → (𝐴𝐵) ∈ ℂ)
9 simp3 1135 . . . . . . . . . 10 ((𝐹𝐴𝐹𝐵𝐴𝐵) → 𝐴𝐵)
105, 7, 9subne0d 11044 . . . . . . . . 9 ((𝐹𝐴𝐹𝐵𝐴𝐵) → (𝐴𝐵) ≠ 0)
118, 10absrpcld 14856 . . . . . . . 8 ((𝐹𝐴𝐹𝐵𝐴𝐵) → (abs‘(𝐴𝐵)) ∈ ℝ+)
1211rphalfcld 12484 . . . . . . 7 ((𝐹𝐴𝐹𝐵𝐴𝐵) → ((abs‘(𝐴𝐵)) / 2) ∈ ℝ+)
13 eqidd 2759 . . . . . . 7 (((𝐹𝐴𝐹𝐵𝐴𝐵) ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) = (𝐹𝑘))
14 simp1 1133 . . . . . . 7 ((𝐹𝐴𝐹𝐵𝐴𝐵) → 𝐹𝐴)
152, 3, 12, 13, 14climi 14915 . . . . . 6 ((𝐹𝐴𝐹𝐵𝐴𝐵) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < ((abs‘(𝐴𝐵)) / 2)))
16 simp2 1134 . . . . . . 7 ((𝐹𝐴𝐹𝐵𝐴𝐵) → 𝐹𝐵)
172, 3, 12, 13, 16climi 14915 . . . . . 6 ((𝐹𝐴𝐹𝐵𝐴𝐵) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐵)) < ((abs‘(𝐴𝐵)) / 2)))
182rexanuz2 14757 . . . . . 6 (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < ((abs‘(𝐴𝐵)) / 2)) ∧ ((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐵)) < ((abs‘(𝐴𝐵)) / 2))) ↔ (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < ((abs‘(𝐴𝐵)) / 2)) ∧ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐵)) < ((abs‘(𝐴𝐵)) / 2))))
1915, 17, 18sylanbrc 586 . . . . 5 ((𝐹𝐴𝐹𝐵𝐴𝐵) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < ((abs‘(𝐴𝐵)) / 2)) ∧ ((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐵)) < ((abs‘(𝐴𝐵)) / 2))))
20 nnz 12043 . . . . . . . . 9 (𝑗 ∈ ℕ → 𝑗 ∈ ℤ)
21 uzid 12297 . . . . . . . . 9 (𝑗 ∈ ℤ → 𝑗 ∈ (ℤ𝑗))
22 ne0i 4233 . . . . . . . . 9 (𝑗 ∈ (ℤ𝑗) → (ℤ𝑗) ≠ ∅)
23 r19.2z 4388 . . . . . . . . . 10 (((ℤ𝑗) ≠ ∅ ∧ ∀𝑘 ∈ (ℤ𝑗)(((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < ((abs‘(𝐴𝐵)) / 2)) ∧ ((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐵)) < ((abs‘(𝐴𝐵)) / 2)))) → ∃𝑘 ∈ (ℤ𝑗)(((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < ((abs‘(𝐴𝐵)) / 2)) ∧ ((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐵)) < ((abs‘(𝐴𝐵)) / 2))))
2423ex 416 . . . . . . . . 9 ((ℤ𝑗) ≠ ∅ → (∀𝑘 ∈ (ℤ𝑗)(((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < ((abs‘(𝐴𝐵)) / 2)) ∧ ((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐵)) < ((abs‘(𝐴𝐵)) / 2))) → ∃𝑘 ∈ (ℤ𝑗)(((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < ((abs‘(𝐴𝐵)) / 2)) ∧ ((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐵)) < ((abs‘(𝐴𝐵)) / 2)))))
2520, 21, 22, 244syl 19 . . . . . . . 8 (𝑗 ∈ ℕ → (∀𝑘 ∈ (ℤ𝑗)(((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < ((abs‘(𝐴𝐵)) / 2)) ∧ ((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐵)) < ((abs‘(𝐴𝐵)) / 2))) → ∃𝑘 ∈ (ℤ𝑗)(((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < ((abs‘(𝐴𝐵)) / 2)) ∧ ((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐵)) < ((abs‘(𝐴𝐵)) / 2)))))
26 simpr 488 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐹𝑘) ∈ ℂ) → (𝐹𝑘) ∈ ℂ)
27 simpll 766 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐹𝑘) ∈ ℂ) → 𝐴 ∈ ℂ)
2826, 27abssubd 14861 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐹𝑘) ∈ ℂ) → (abs‘((𝐹𝑘) − 𝐴)) = (abs‘(𝐴 − (𝐹𝑘))))
2928breq1d 5042 . . . . . . . . . . . . 13 (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐹𝑘) ∈ ℂ) → ((abs‘((𝐹𝑘) − 𝐴)) < ((abs‘(𝐴𝐵)) / 2) ↔ (abs‘(𝐴 − (𝐹𝑘))) < ((abs‘(𝐴𝐵)) / 2)))
30 simplr 768 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐹𝑘) ∈ ℂ) → 𝐵 ∈ ℂ)
31 subcl 10923 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐵) ∈ ℂ)
3231adantr 484 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐹𝑘) ∈ ℂ) → (𝐴𝐵) ∈ ℂ)
3332abscld 14844 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐹𝑘) ∈ ℂ) → (abs‘(𝐴𝐵)) ∈ ℝ)
34 abs3lem 14746 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐹𝑘) ∈ ℂ ∧ (abs‘(𝐴𝐵)) ∈ ℝ)) → (((abs‘(𝐴 − (𝐹𝑘))) < ((abs‘(𝐴𝐵)) / 2) ∧ (abs‘((𝐹𝑘) − 𝐵)) < ((abs‘(𝐴𝐵)) / 2)) → (abs‘(𝐴𝐵)) < (abs‘(𝐴𝐵))))
3527, 30, 26, 33, 34syl22anc 837 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐹𝑘) ∈ ℂ) → (((abs‘(𝐴 − (𝐹𝑘))) < ((abs‘(𝐴𝐵)) / 2) ∧ (abs‘((𝐹𝑘) − 𝐵)) < ((abs‘(𝐴𝐵)) / 2)) → (abs‘(𝐴𝐵)) < (abs‘(𝐴𝐵))))
3633ltnrd 10812 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐹𝑘) ∈ ℂ) → ¬ (abs‘(𝐴𝐵)) < (abs‘(𝐴𝐵)))
3736pm2.21d 121 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐹𝑘) ∈ ℂ) → ((abs‘(𝐴𝐵)) < (abs‘(𝐴𝐵)) → ¬ 1 ∈ ℤ))
3835, 37syld 47 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐹𝑘) ∈ ℂ) → (((abs‘(𝐴 − (𝐹𝑘))) < ((abs‘(𝐴𝐵)) / 2) ∧ (abs‘((𝐹𝑘) − 𝐵)) < ((abs‘(𝐴𝐵)) / 2)) → ¬ 1 ∈ ℤ))
3938expd 419 . . . . . . . . . . . . 13 (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐹𝑘) ∈ ℂ) → ((abs‘(𝐴 − (𝐹𝑘))) < ((abs‘(𝐴𝐵)) / 2) → ((abs‘((𝐹𝑘) − 𝐵)) < ((abs‘(𝐴𝐵)) / 2) → ¬ 1 ∈ ℤ)))
4029, 39sylbid 243 . . . . . . . . . . . 12 (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐹𝑘) ∈ ℂ) → ((abs‘((𝐹𝑘) − 𝐴)) < ((abs‘(𝐴𝐵)) / 2) → ((abs‘((𝐹𝑘) − 𝐵)) < ((abs‘(𝐴𝐵)) / 2) → ¬ 1 ∈ ℤ)))
4140impr 458 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < ((abs‘(𝐴𝐵)) / 2))) → ((abs‘((𝐹𝑘) − 𝐵)) < ((abs‘(𝐴𝐵)) / 2) → ¬ 1 ∈ ℤ))
4241adantld 494 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < ((abs‘(𝐴𝐵)) / 2))) → (((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐵)) < ((abs‘(𝐴𝐵)) / 2)) → ¬ 1 ∈ ℤ))
4342expimpd 457 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < ((abs‘(𝐴𝐵)) / 2)) ∧ ((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐵)) < ((abs‘(𝐴𝐵)) / 2))) → ¬ 1 ∈ ℤ))
4443rexlimdvw 3214 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (∃𝑘 ∈ (ℤ𝑗)(((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < ((abs‘(𝐴𝐵)) / 2)) ∧ ((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐵)) < ((abs‘(𝐴𝐵)) / 2))) → ¬ 1 ∈ ℤ))
4525, 44sylan9r 512 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑗 ∈ ℕ) → (∀𝑘 ∈ (ℤ𝑗)(((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < ((abs‘(𝐴𝐵)) / 2)) ∧ ((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐵)) < ((abs‘(𝐴𝐵)) / 2))) → ¬ 1 ∈ ℤ))
4645rexlimdva 3208 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < ((abs‘(𝐴𝐵)) / 2)) ∧ ((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐵)) < ((abs‘(𝐴𝐵)) / 2))) → ¬ 1 ∈ ℤ))
475, 7, 46syl2anc 587 . . . . 5 ((𝐹𝐴𝐹𝐵𝐴𝐵) → (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < ((abs‘(𝐴𝐵)) / 2)) ∧ ((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐵)) < ((abs‘(𝐴𝐵)) / 2))) → ¬ 1 ∈ ℤ))
4819, 47mpd 15 . . . 4 ((𝐹𝐴𝐹𝐵𝐴𝐵) → ¬ 1 ∈ ℤ)
49483expia 1118 . . 3 ((𝐹𝐴𝐹𝐵) → (𝐴𝐵 → ¬ 1 ∈ ℤ))
5049necon4ad 2970 . 2 ((𝐹𝐴𝐹𝐵) → (1 ∈ ℤ → 𝐴 = 𝐵))
511, 50mpi 20 1 ((𝐹𝐴𝐹𝐵) → 𝐴 = 𝐵)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2951  ∀wral 3070  ∃wrex 3071  ∅c0 4225   class class class wbr 5032  ‘cfv 6335  (class class class)co 7150  ℂcc 10573  ℝcr 10574  1c1 10576   < clt 10713   − cmin 10908   / cdiv 11335  ℕcn 11674  2c2 11729  ℤcz 12020  ℤ≥cuz 12282  abscabs 14641   ⇝ cli 14889 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-cnex 10631  ax-resscn 10632  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-addrcl 10636  ax-mulcl 10637  ax-mulrcl 10638  ax-mulcom 10639  ax-addass 10640  ax-mulass 10641  ax-distr 10642  ax-i2m1 10643  ax-1ne0 10644  ax-1rid 10645  ax-rnegex 10646  ax-rrecex 10647  ax-cnre 10648  ax-pre-lttri 10649  ax-pre-lttrn 10650  ax-pre-ltadd 10651  ax-pre-mulgt0 10652  ax-pre-sup 10653 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7580  df-2nd 7694  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-er 8299  df-en 8528  df-dom 8529  df-sdom 8530  df-sup 8939  df-pnf 10715  df-mnf 10716  df-xr 10717  df-ltxr 10718  df-le 10719  df-sub 10910  df-neg 10911  df-div 11336  df-nn 11675  df-2 11737  df-3 11738  df-n0 11935  df-z 12021  df-uz 12283  df-rp 12431  df-seq 13419  df-exp 13480  df-cj 14506  df-re 14507  df-im 14508  df-sqrt 14642  df-abs 14643  df-clim 14893 This theorem is referenced by:  fclim  14958  climeu  14960  summolem2  15121  summo  15122  prodmolem2  15337  prodmo  15338  ef0  15492  efcj  15493  efaddlem  15494  ioombl1lem4  24261  mbflimlem  24367  itg2i1fseq  24455  itg2addlem  24458  plyeq0lem  24906  ulmuni  25086  leibpi  25627  lgamp1  25741  lgam1  25748  sumnnodd  42638  climfveq  42677  climfveqf  42688  climfv  42699  climlimsupcex  42777  climliminflimsupd  42809  stirlinglem15  43096  fouriersw  43239  sge0isum  43432  vonioolem2  43686  vonicclem2  43689
 Copyright terms: Public domain W3C validator