![]() |
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 14343 | . . . . 5 ⊢ Rel ⇝ | |
2 | 1 | brrelexi 5267 | . . . 4 ⊢ (𝐹 ⇝ 𝐴 → 𝐹 ∈ V) |
3 | eqidd 2725 | . . . 4 ⊢ ((𝐹 ⇝ 𝐴 ∧ 𝑘 ∈ ℤ) → (𝐹‘𝑘) = (𝐹‘𝑘)) | |
4 | 2, 3 | clim 14345 | . . 3 ⊢ (𝐹 ⇝ 𝐴 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥)))) |
5 | 4 | ibi 256 | . 2 ⊢ (𝐹 ⇝ 𝐴 → (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥))) |
6 | 5 | simpld 477 | 1 ⊢ (𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∈ wcel 2103 ∀wral 3014 ∃wrex 3015 Vcvv 3304 class class class wbr 4760 ‘cfv 6001 (class class class)co 6765 ℂcc 10047 < clt 10187 − cmin 10379 ℤcz 11490 ℤ≥cuz 11800 ℝ+crp 11946 abscabs 14094 ⇝ cli 14335 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1835 ax-4 1850 ax-5 1952 ax-6 2018 ax-7 2054 ax-8 2105 ax-9 2112 ax-10 2132 ax-11 2147 ax-12 2160 ax-13 2355 ax-ext 2704 ax-sep 4889 ax-nul 4897 ax-pow 4948 ax-pr 5011 ax-cnex 10105 ax-resscn 10106 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1599 df-ex 1818 df-nf 1823 df-sb 2011 df-eu 2575 df-mo 2576 df-clab 2711 df-cleq 2717 df-clel 2720 df-nfc 2855 df-ne 2897 df-ral 3019 df-rex 3020 df-rab 3023 df-v 3306 df-sbc 3542 df-dif 3683 df-un 3685 df-in 3687 df-ss 3694 df-nul 4024 df-if 4195 df-pw 4268 df-sn 4286 df-pr 4288 df-op 4292 df-uni 4545 df-br 4761 df-opab 4821 df-mpt 4838 df-id 5128 df-xp 5224 df-rel 5225 df-cnv 5226 df-co 5227 df-dm 5228 df-rn 5229 df-res 5230 df-ima 5231 df-iota 5964 df-fun 6003 df-fn 6004 df-f 6005 df-fv 6009 df-ov 6768 df-neg 10382 df-z 11491 df-uz 11801 df-clim 14339 |
This theorem is referenced by: rlimclim 14397 climrlim2 14398 climuni 14403 fclim 14404 climeu 14406 climreu 14407 2clim 14423 climcn1lem 14453 climadd 14482 climmul 14483 climsub 14484 climaddc2 14486 climcau 14521 clim2div 14741 ntrivcvgtail 14752 ntrivcvgmullem 14753 mbflim 23555 ulmcau 24269 emcllem6 24847 dchrmusum2 25303 dchrvmasumiflem1 25310 dchrvmasumiflem2 25311 dchrisum0lem1b 25324 dchrmusumlem 25331 iprodefisum 31855 climrec 40255 climexp 40257 climsuse 40260 climneg 40262 climdivf 40264 climleltrp 40328 climuzlem 40395 climxlim2lem 40491 climxlim2 40492 sge0isum 41064 |
Copyright terms: Public domain | W3C validator |