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 ⊢φ→supAℝ*<=+∞
rlimcld2.2 ⊢φ→x∈A⟼B⇝ℝC
rlimcld2.3 ⊢φ→D⊆ℂ
rlimcld2.4 ⊢φ∧y∈ℂ∖D→R∈ℝ+
rlimcld2.5 ⊢φ∧y∈ℂ∖D∧z∈D→R≤z−y
rlimcld2.6 ⊢φ∧x∈A→B∈D
Assertion rlimcld2 ⊢φ→C∈D

Proof

Step Hyp Ref Expression
1 rlimcld2.1 ⊢φ→supAℝ*<=+∞
2 rlimcld2.2 ⊢φ→x∈A⟼B⇝ℝC
3 rlimcld2.3 ⊢φ→D⊆ℂ
4 rlimcld2.4 ⊢φ∧y∈ℂ∖D→R∈ℝ+
5 rlimcld2.5 ⊢φ∧y∈ℂ∖D∧z∈D→R≤z−y
6 rlimcld2.6 ⊢φ∧x∈A→B∈D
7 6 ralrimiva ⊢φ→∀x∈AB∈D
8 7 adantr ⊢φ∧¬C∈D→∀x∈AB∈D
9 2 adantr ⊢φ∧¬C∈D→x∈A⟼B⇝ℝC
10 rlimcl ⊢x∈A⟼B⇝ℝC→C∈ℂ
11 9 10 syl ⊢φ∧¬C∈D→C∈ℂ
12 simpr ⊢φ∧¬C∈D→¬C∈D
13 11 12 eldifd ⊢φ∧¬C∈D→C∈ℂ∖D
14 4 ralrimiva ⊢φ→∀y∈ℂ∖DR∈ℝ+
15 14 adantr ⊢φ∧¬C∈D→∀y∈ℂ∖DR∈ℝ+
16 nfcsb1v ⊢Ⅎ_y⦋C/y⦌R
17 16 nfel1 ⊢Ⅎy⦋C/y⦌R∈ℝ+
18 csbeq1a ⊢y=C→R=⦋C/y⦌R
19 18 eleq1d ⊢y=C→R∈ℝ+↔⦋C/y⦌R∈ℝ+
20 17 19 rspc ⊢C∈ℂ∖D→∀y∈ℂ∖DR∈ℝ+→⦋C/y⦌R∈ℝ+
21 13 15 20 sylc ⊢φ∧¬C∈D→⦋C/y⦌R∈ℝ+
22 8 21 9 rlimi ⊢φ∧¬C∈D→∃r∈ℝ∀x∈Ar≤x→B−C<⦋C/y⦌R
23 21 ad2antrr ⊢φ∧¬C∈D∧r∈ℝ∧x∈A→⦋C/y⦌R∈ℝ+
24 23 rpred ⊢φ∧¬C∈D∧r∈ℝ∧x∈A→⦋C/y⦌R∈ℝ
25 3 ad3antrrr ⊢φ∧¬C∈D∧r∈ℝ∧x∈A→D⊆ℂ
26 6 ad4ant14 ⊢φ∧¬C∈D∧r∈ℝ∧x∈A→B∈D
27 25 26 sseldd ⊢φ∧¬C∈D∧r∈ℝ∧x∈A→B∈ℂ
28 11 ad2antrr ⊢φ∧¬C∈D∧r∈ℝ∧x∈A→C∈ℂ
29 27 28 subcld ⊢φ∧¬C∈D∧r∈ℝ∧x∈A→B−C∈ℂ
30 29 abscld ⊢φ∧¬C∈D∧r∈ℝ∧x∈A→B−C∈ℝ
31 5 ralrimiva ⊢φ∧y∈ℂ∖D→∀z∈DR≤z−y
32 31 ralrimiva ⊢φ→∀y∈ℂ∖D∀z∈DR≤z−y
33 32 adantr ⊢φ∧¬C∈D→∀y∈ℂ∖D∀z∈DR≤z−y
34 nfcv ⊢Ⅎ_yD
35 nfcv ⊢Ⅎ_y≤
36 nfcv ⊢Ⅎ_yz−C
37 16 35 36 nfbr ⊢Ⅎy⦋C/y⦌R≤z−C
38 34 37 nfralw ⊢Ⅎy∀z∈D⦋C/y⦌R≤z−C
39 oveq2 ⊢y=C→z−y=z−C
40 39 fveq2d ⊢y=C→z−y=z−C
41 18 40 breq12d ⊢y=C→R≤z−y↔⦋C/y⦌R≤z−C
42 41 ralbidv ⊢y=C→∀z∈DR≤z−y↔∀z∈D⦋C/y⦌R≤z−C
43 38 42 rspc ⊢C∈ℂ∖D→∀y∈ℂ∖D∀z∈DR≤z−y→∀z∈D⦋C/y⦌R≤z−C
44 13 33 43 sylc ⊢φ∧¬C∈D→∀z∈D⦋C/y⦌R≤z−C
45 44 ad2antrr ⊢φ∧¬C∈D∧r∈ℝ∧x∈A→∀z∈D⦋C/y⦌R≤z−C
46 fvoveq1 ⊢z=B→z−C=B−C
47 46 breq2d ⊢z=B→⦋C/y⦌R≤z−C↔⦋C/y⦌R≤B−C
48 47 rspcv ⊢B∈D→∀z∈D⦋C/y⦌R≤z−C→⦋C/y⦌R≤B−C
49 26 45 48 sylc ⊢φ∧¬C∈D∧r∈ℝ∧x∈A→⦋C/y⦌R≤B−C
50 24 30 49 lensymd ⊢φ∧¬C∈D∧r∈ℝ∧x∈A→¬B−C<⦋C/y⦌R
51 id ⊢r≤x→B−C<⦋C/y⦌R→r≤x→B−C<⦋C/y⦌R
52 51 imp ⊢r≤x→B−C<⦋C/y⦌R∧r≤x→B−C<⦋C/y⦌R
53 50 52 nsyl ⊢φ∧¬C∈D∧r∈ℝ∧x∈A→¬r≤x→B−C<⦋C/y⦌R∧r≤x
54 53 nrexdv ⊢φ∧¬C∈D∧r∈ℝ→¬∃x∈Ar≤x→B−C<⦋C/y⦌R∧r≤x
55 eqid ⊢x∈A⟼B=x∈A⟼B
56 55 6 dmmptd ⊢φ→dom⁡x∈A⟼B=A
57 rlimss ⊢x∈A⟼B⇝ℝC→dom⁡x∈A⟼B⊆ℝ
58 2 57 syl ⊢φ→dom⁡x∈A⟼B⊆ℝ
59 56 58 eqsstrrd ⊢φ→A⊆ℝ
60 ressxr ⊢ℝ⊆ℝ*
61 59 60 sstrdi ⊢φ→A⊆ℝ*
62 supxrunb1 ⊢A⊆ℝ*→∀r∈ℝ∃x∈Ar≤x↔supAℝ*<=+∞
63 61 62 syl ⊢φ→∀r∈ℝ∃x∈Ar≤x↔supAℝ*<=+∞
64 1 63 mpbird ⊢φ→∀r∈ℝ∃x∈Ar≤x
65 64 adantr ⊢φ∧¬C∈D→∀r∈ℝ∃x∈Ar≤x
66 65 r19.21bi ⊢φ∧¬C∈D∧r∈ℝ→∃x∈Ar≤x
67 r19.29 ⊢∀x∈Ar≤x→B−C<⦋C/y⦌R∧∃x∈Ar≤x→∃x∈Ar≤x→B−C<⦋C/y⦌R∧r≤x
68 67 expcom ⊢∃x∈Ar≤x→∀x∈Ar≤x→B−C<⦋C/y⦌R→∃x∈Ar≤x→B−C<⦋C/y⦌R∧r≤x
69 66 68 syl ⊢φ∧¬C∈D∧r∈ℝ→∀x∈Ar≤x→B−C<⦋C/y⦌R→∃x∈Ar≤x→B−C<⦋C/y⦌R∧r≤x
70 54 69 mtod ⊢φ∧¬C∈D∧r∈ℝ→¬∀x∈Ar≤x→B−C<⦋C/y⦌R
71 70 nrexdv ⊢φ∧¬C∈D→¬∃r∈ℝ∀x∈Ar≤x→B−C<⦋C/y⦌R
72 22 71 condan ⊢φ→C∈D