Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > climcl | Structured version Visualization version GIF version |
Description: Closure of the limit of a sequence of complex numbers. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Ref | Expression |
---|---|
climcl | ⊢ (𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | climrel 14932 | . . . . 5 ⊢ Rel ⇝ | |
2 | 1 | brrelex1i 5573 | . . . 4 ⊢ (𝐹 ⇝ 𝐴 → 𝐹 ∈ V) |
3 | eqidd 2739 | . . . 4 ⊢ ((𝐹 ⇝ 𝐴 ∧ 𝑘 ∈ ℤ) → (𝐹‘𝑘) = (𝐹‘𝑘)) | |
4 | 2, 3 | clim 14934 | . . 3 ⊢ (𝐹 ⇝ 𝐴 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥)))) |
5 | 4 | ibi 270 | . 2 ⊢ (𝐹 ⇝ 𝐴 → (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥))) |
6 | 5 | simpld 498 | 1 ⊢ (𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2113 ∀wral 3053 ∃wrex 3054 Vcvv 3397 class class class wbr 5027 ‘cfv 6333 (class class class)co 7164 ℂcc 10606 < clt 10746 − cmin 10941 ℤcz 12055 ℤ≥cuz 12317 ℝ+crp 12465 abscabs 14676 ⇝ cli 14924 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-sep 5164 ax-nul 5171 ax-pr 5293 ax-cnex 10664 ax-resscn 10665 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-ral 3058 df-rex 3059 df-rab 3062 df-v 3399 df-sbc 3680 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-nul 4210 df-if 4412 df-pw 4487 df-sn 4514 df-pr 4516 df-op 4520 df-uni 4794 df-br 5028 df-opab 5090 df-mpt 5108 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6291 df-fun 6335 df-fn 6336 df-f 6337 df-fv 6341 df-ov 7167 df-neg 10944 df-z 12056 df-uz 12318 df-clim 14928 |
This theorem is referenced by: rlimclim 14986 climrlim2 14987 climuni 14992 fclim 14993 climeu 14995 climreu 14996 2clim 15012 climcn1lem 15043 climadd 15072 climmul 15073 climsub 15074 climaddc2 15076 climcau 15113 clim2div 15330 ntrivcvgtail 15341 ntrivcvgmullem 15342 mbflim 24413 ulmcau 25134 emcllem6 25730 dchrmusum2 26222 dchrvmasumiflem1 26229 dchrvmasumiflem2 26230 dchrisum0lem1b 26243 dchrmusumlem 26250 iprodefisum 33270 climrec 42670 climexp 42672 climsuse 42675 climneg 42677 climdivf 42679 climleltrp 42743 climuzlem 42810 climxlim2lem 42912 climxlim2 42913 sge0isum 43491 |
Copyright terms: Public domain | W3C validator |