# Metamath Proof Explorer

## Theorem rlimcld2

Description: If D is a closed set in the topology of the complex numbers (stated here in basic form), and all the elements of the sequence lie in D , then the limit of the sequence also lies in D . (Contributed by Mario Carneiro, 10-May-2016)

Ref Expression
Hypotheses rlimcld2.1 ${⊢}{\phi }\to sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }$
rlimcld2.2
rlimcld2.3 ${⊢}{\phi }\to {D}\subseteq ℂ$
rlimcld2.4 ${⊢}\left({\phi }\wedge {y}\in \left(ℂ\setminus {D}\right)\right)\to {R}\in {ℝ}^{+}$
rlimcld2.5 ${⊢}\left(\left({\phi }\wedge {y}\in \left(ℂ\setminus {D}\right)\right)\wedge {z}\in {D}\right)\to {R}\le \left|{z}-{y}\right|$
rlimcld2.6 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {D}$
Assertion rlimcld2 ${⊢}{\phi }\to {C}\in {D}$

### Proof

Step Hyp Ref Expression
1 rlimcld2.1 ${⊢}{\phi }\to sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }$
2 rlimcld2.2
3 rlimcld2.3 ${⊢}{\phi }\to {D}\subseteq ℂ$
4 rlimcld2.4 ${⊢}\left({\phi }\wedge {y}\in \left(ℂ\setminus {D}\right)\right)\to {R}\in {ℝ}^{+}$
5 rlimcld2.5 ${⊢}\left(\left({\phi }\wedge {y}\in \left(ℂ\setminus {D}\right)\right)\wedge {z}\in {D}\right)\to {R}\le \left|{z}-{y}\right|$
6 rlimcld2.6 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {D}$
7 6 ralrimiva ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {D}$
8 7 adantr ${⊢}\left({\phi }\wedge ¬{C}\in {D}\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {D}$
10 rlimcl
11 9 10 syl ${⊢}\left({\phi }\wedge ¬{C}\in {D}\right)\to {C}\in ℂ$
12 simpr ${⊢}\left({\phi }\wedge ¬{C}\in {D}\right)\to ¬{C}\in {D}$
13 11 12 eldifd ${⊢}\left({\phi }\wedge ¬{C}\in {D}\right)\to {C}\in \left(ℂ\setminus {D}\right)$
14 4 ralrimiva ${⊢}{\phi }\to \forall {y}\in \left(ℂ\setminus {D}\right)\phantom{\rule{.4em}{0ex}}{R}\in {ℝ}^{+}$
15 14 adantr ${⊢}\left({\phi }\wedge ¬{C}\in {D}\right)\to \forall {y}\in \left(ℂ\setminus {D}\right)\phantom{\rule{.4em}{0ex}}{R}\in {ℝ}^{+}$
16 nfcsb1v
17 16 nfel1
18 csbeq1a
19 18 eleq1d
20 17 19 rspc
21 13 15 20 sylc
22 8 21 9 rlimi
24 23 rpred
25 3 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge ¬{C}\in {D}\right)\wedge {r}\in ℝ\right)\wedge {x}\in {A}\right)\to {D}\subseteq ℂ$
26 6 ad4ant14 ${⊢}\left(\left(\left({\phi }\wedge ¬{C}\in {D}\right)\wedge {r}\in ℝ\right)\wedge {x}\in {A}\right)\to {B}\in {D}$
27 25 26 sseldd ${⊢}\left(\left(\left({\phi }\wedge ¬{C}\in {D}\right)\wedge {r}\in ℝ\right)\wedge {x}\in {A}\right)\to {B}\in ℂ$
28 11 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge ¬{C}\in {D}\right)\wedge {r}\in ℝ\right)\wedge {x}\in {A}\right)\to {C}\in ℂ$
29 27 28 subcld ${⊢}\left(\left(\left({\phi }\wedge ¬{C}\in {D}\right)\wedge {r}\in ℝ\right)\wedge {x}\in {A}\right)\to {B}-{C}\in ℂ$
30 29 abscld ${⊢}\left(\left(\left({\phi }\wedge ¬{C}\in {D}\right)\wedge {r}\in ℝ\right)\wedge {x}\in {A}\right)\to \left|{B}-{C}\right|\in ℝ$
31 5 ralrimiva ${⊢}\left({\phi }\wedge {y}\in \left(ℂ\setminus {D}\right)\right)\to \forall {z}\in {D}\phantom{\rule{.4em}{0ex}}{R}\le \left|{z}-{y}\right|$
32 31 ralrimiva ${⊢}{\phi }\to \forall {y}\in \left(ℂ\setminus {D}\right)\phantom{\rule{.4em}{0ex}}\forall {z}\in {D}\phantom{\rule{.4em}{0ex}}{R}\le \left|{z}-{y}\right|$
33 32 adantr ${⊢}\left({\phi }\wedge ¬{C}\in {D}\right)\to \forall {y}\in \left(ℂ\setminus {D}\right)\phantom{\rule{.4em}{0ex}}\forall {z}\in {D}\phantom{\rule{.4em}{0ex}}{R}\le \left|{z}-{y}\right|$
34 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{D}$
35 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\le$
36 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left|{z}-{C}\right|$
37 16 35 36 nfbr
38 34 37 nfralw
39 oveq2 ${⊢}{y}={C}\to {z}-{y}={z}-{C}$
40 39 fveq2d ${⊢}{y}={C}\to \left|{z}-{y}\right|=\left|{z}-{C}\right|$
41 18 40 breq12d
42 41 ralbidv
43 38 42 rspc
44 13 33 43 sylc
46 fvoveq1 ${⊢}{z}={B}\to \left|{z}-{C}\right|=\left|{B}-{C}\right|$
47 46 breq2d
48 47 rspcv
49 26 45 48 sylc
50 24 30 49 lensymd
51 id
52 51 imp
53 50 52 nsyl
54 53 nrexdv
55 eqid ${⊢}\left({x}\in {A}⟼{B}\right)=\left({x}\in {A}⟼{B}\right)$
56 55 6 dmmptd ${⊢}{\phi }\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)={A}$
57 rlimss
58 2 57 syl ${⊢}{\phi }\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)\subseteq ℝ$
59 56 58 eqsstrrd ${⊢}{\phi }\to {A}\subseteq ℝ$
60 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
61 59 60 sstrdi ${⊢}{\phi }\to {A}\subseteq {ℝ}^{*}$
62 supxrunb1 ${⊢}{A}\subseteq {ℝ}^{*}\to \left(\forall {r}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{r}\le {x}↔sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)$
63 61 62 syl ${⊢}{\phi }\to \left(\forall {r}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{r}\le {x}↔sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)$
64 1 63 mpbird ${⊢}{\phi }\to \forall {r}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{r}\le {x}$
65 64 adantr ${⊢}\left({\phi }\wedge ¬{C}\in {D}\right)\to \forall {r}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{r}\le {x}$
66 65 r19.21bi ${⊢}\left(\left({\phi }\wedge ¬{C}\in {D}\right)\wedge {r}\in ℝ\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{r}\le {x}$
67 r19.29
68 67 expcom
69 66 68 syl
70 54 69 mtod
71 70 nrexdv
72 22 71 condan ${⊢}{\phi }\to {C}\in {D}$