| 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 15391 | . . . . 5 ⊢ Rel ⇝ | |
| 2 | 1 | brrelex1i 5670 | . . . 4 ⊢ (𝐹 ⇝ 𝐴 → 𝐹 ∈ V) |
| 3 | eqidd 2731 | . . . 4 ⊢ ((𝐹 ⇝ 𝐴 ∧ 𝑘 ∈ ℤ) → (𝐹‘𝑘) = (𝐹‘𝑘)) | |
| 4 | 2, 3 | clim 15393 | . . 3 ⊢ (𝐹 ⇝ 𝐴 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥)))) |
| 5 | 4 | ibi 267 | . 2 ⊢ (𝐹 ⇝ 𝐴 → (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥))) |
| 6 | 5 | simpld 494 | 1 ⊢ (𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2110 ∀wral 3045 ∃wrex 3054 Vcvv 3434 class class class wbr 5089 ‘cfv 6477 (class class class)co 7341 ℂcc 10996 < clt 11138 − cmin 11336 ℤcz 12460 ℤ≥cuz 12724 ℝ+crp 12882 abscabs 15133 ⇝ cli 15383 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2112 ax-9 2120 ax-10 2143 ax-11 2159 ax-12 2179 ax-ext 2702 ax-sep 5232 ax-nul 5242 ax-pr 5368 ax-cnex 11054 ax-resscn 11055 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ral 3046 df-rex 3055 df-rab 3394 df-v 3436 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-nul 4282 df-if 4474 df-pw 4550 df-sn 4575 df-pr 4577 df-op 4581 df-uni 4858 df-br 5090 df-opab 5152 df-mpt 5171 df-id 5509 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-iota 6433 df-fun 6479 df-fn 6480 df-f 6481 df-fv 6485 df-ov 7344 df-neg 11339 df-z 12461 df-uz 12725 df-clim 15387 |
| This theorem is referenced by: rlimclim 15445 climrlim2 15446 climuni 15451 fclim 15452 climeu 15454 climreu 15455 2clim 15471 climcn1lem 15502 climadd 15531 climmul 15532 climsub 15533 climaddc2 15535 climcau 15570 clim2div 15788 ntrivcvgtail 15799 ntrivcvgmullem 15800 mbflim 25589 ulmcau 26324 emcllem6 26931 dchrmusum2 27425 dchrvmasumiflem1 27432 dchrvmasumiflem2 27433 dchrisum0lem1b 27446 dchrmusumlem 27453 iprodefisum 35753 climrec 45622 climexp 45624 climsuse 45627 climneg 45629 climdivf 45631 climleltrp 45693 climuzlem 45760 climxlim2lem 45862 climxlim2 45863 sge0isum 46444 |
| Copyright terms: Public domain | W3C validator |