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 15465

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 15463	. . . 4 ⊢ (𝐹 ⇝_𝑟 𝐴 → 𝐹:dom 𝐹⟶ℂ)
2		rlimss 15464	. . . 4 ⊢ (𝐹 ⇝_𝑟 𝐴 → dom 𝐹 ⊆ ℝ)
3		eqidd 2737	. . . 4 ⊢ ((𝐹 ⇝_𝑟 𝐴 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) = (𝐹‘𝑥))
4	1, 2, 3	rlim 15457	. . 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 3051 ∃wrex 3061 class class class wbr 5085 dom cdm 5631 ‘cfv 6498 (class class class)co 7367 ℂcc 11036 ℝcr 11037 < clt 11179 ≤ cle 11180 − cmin 11377 ℝ⁺crp 12942 abscabs 15196 ⇝_𝑟 crli 15447

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 2708 ax-sep 5231 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-cnex 11094 ax-resscn 11095

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 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3062 df-rab 3390 df-v 3431 df-sbc 3729 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-br 5086 df-opab 5148 df-id 5526 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-fv 6506 df-ov 7370 df-oprab 7371 df-mpo 7372 df-pm 8776 df-rlim 15451

This theorem is referenced by: rlimi 15475 rlimclim1 15507 rlimuni 15512 rlimresb 15527 rlimcld2 15540 rlimabs 15571 rlimcj 15572 rlimre 15573 rlimim 15574 rlimo1 15579 rlimadd 15605 rlimsub 15606 rlimmul 15607 rlimdiv 15608 rlimsqzlem 15611 fsumrlim 15774 dchrisum0lem2a 27480 mulog2sumlem2 27498 mulog2sumlem3 27499

W3C validator