rlimcl - Metamath Proof Explorer

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

Theorem rlimcl 15456

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.)

**Assertion**
Ref	Expression
rlimcl	⊢ (𝐹 ⇝_𝑟 𝐴 → 𝐴 ∈ ℂ)

Proof of Theorem rlimcl Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rlimf 15454	. . . 4 ⊢ (𝐹 ⇝_𝑟 𝐴 → 𝐹:dom 𝐹⟶ℂ)
2		rlimss 15455	. . . 4 ⊢ (𝐹 ⇝_𝑟 𝐴 → dom 𝐹 ⊆ ℝ)
3		eqidd 2738	. . . 4 ⊢ ((𝐹 ⇝_𝑟 𝐴 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) = (𝐹‘𝑥))
4	1, 2, 3	rlim 15448	. . 3 ⊢ (𝐹 ⇝_𝑟 𝐴 → (𝐹 ⇝_𝑟 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ ∀𝑥 ∈ dom 𝐹(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐴)) < 𝑦))))
5	4	ibi 267	. 2 ⊢ (𝐹 ⇝_𝑟 𝐴 → (𝐴 ∈ ℂ ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ ∀𝑥 ∈ dom 𝐹(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐴)) < 𝑦)))
6	5	simpld 494	1 ⊢ (𝐹 ⇝_𝑟 𝐴 → 𝐴 ∈ ℂ)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2114 ∀wral 3052 ∃wrex 3062 class class class wbr 5086 dom cdm 5624 ‘cfv 6492 (class class class)co 7360 ℂcc 11027 ℝcr 11028 < clt 11170 ≤ cle 11171 − cmin 11368 ℝ⁺crp 12933 abscabs 15187 ⇝_𝑟 crli 15438

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5231 ax-pow 5302 ax-pr 5370 ax-un 7682 ax-cnex 11085 ax-resscn 11086

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rab 3391 df-v 3432 df-sbc 3730 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-br 5087 df-opab 5149 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-fv 6500 df-ov 7363 df-oprab 7364 df-mpo 7365 df-pm 8769 df-rlim 15442

This theorem is referenced by: rlimi 15466 rlimclim1 15498 rlimuni 15503 rlimresb 15518 rlimcld2 15531 rlimabs 15562 rlimcj 15563 rlimre 15564 rlimim 15565 rlimo1 15570 rlimadd 15596 rlimsub 15597 rlimmul 15598 rlimdiv 15599 rlimsqzlem 15602 fsumrlim 15765 dchrisum0lem2a 27494 mulog2sumlem2 27512 mulog2sumlem3 27513

W3C validator