Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rlimcl | Structured version Visualization version GIF version |
Description: Closure of the limit of a sequence of complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Ref | Expression |
---|---|
rlimcl | ⊢ (𝐹 ⇝𝑟 𝐴 → 𝐴 ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rlimf 15094 | . . . 4 ⊢ (𝐹 ⇝𝑟 𝐴 → 𝐹:dom 𝐹⟶ℂ) | |
2 | rlimss 15095 | . . . 4 ⊢ (𝐹 ⇝𝑟 𝐴 → dom 𝐹 ⊆ ℝ) | |
3 | eqidd 2740 | . . . 4 ⊢ ((𝐹 ⇝𝑟 𝐴 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) = (𝐹‘𝑥)) | |
4 | 1, 2, 3 | rlim 15088 | . . 3 ⊢ (𝐹 ⇝𝑟 𝐴 → (𝐹 ⇝𝑟 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑥 ∈ dom 𝐹(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐴)) < 𝑦)))) |
5 | 4 | ibi 270 | . 2 ⊢ (𝐹 ⇝𝑟 𝐴 → (𝐴 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑥 ∈ dom 𝐹(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐴)) < 𝑦))) |
6 | 5 | simpld 498 | 1 ⊢ (𝐹 ⇝𝑟 𝐴 → 𝐴 ∈ ℂ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2112 ∀wral 3064 ∃wrex 3065 class class class wbr 5069 dom cdm 5568 ‘cfv 6400 (class class class)co 7234 ℂcc 10756 ℝcr 10757 < clt 10896 ≤ cle 10897 − cmin 11091 ℝ+crp 12615 abscabs 14829 ⇝𝑟 crli 15078 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2710 ax-sep 5208 ax-nul 5215 ax-pow 5274 ax-pr 5338 ax-un 7544 ax-cnex 10814 ax-resscn 10815 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2818 df-nfc 2889 df-ne 2944 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3425 df-sbc 3712 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4456 df-pw 4531 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4836 df-br 5070 df-opab 5132 df-id 5471 df-xp 5574 df-rel 5575 df-cnv 5576 df-co 5577 df-dm 5578 df-rn 5579 df-iota 6358 df-fun 6402 df-fn 6403 df-f 6404 df-fv 6408 df-ov 7237 df-oprab 7238 df-mpo 7239 df-pm 8534 df-rlim 15082 |
This theorem is referenced by: rlimi 15106 rlimclim1 15138 rlimuni 15143 rlimresb 15158 rlimcld2 15171 rlimabs 15202 rlimcj 15203 rlimre 15204 rlimim 15205 rlimo1 15210 rlimadd 15236 rlimaddOLD 15237 rlimsub 15238 rlimmul 15239 rlimmulOLD 15240 rlimdiv 15241 rlimsqzlem 15244 fsumrlim 15407 dchrisum0lem2a 26429 mulog2sumlem2 26447 mulog2sumlem3 26448 |
Copyright terms: Public domain | W3C validator |