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 ⊢ φ → sup A ℝ * < = +∞
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 ⊢ φ → sup A ℝ * < = +∞
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 ∈ A B ∈ D
8 7 adantr ⊢ φ ∧ ¬ C ∈ D → ∀ x ∈ A B ∈ 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 ∈ ℂ ∖ D R ∈ ℝ +
15 14 adantr ⊢ φ ∧ ¬ C ∈ D → ∀ y ∈ ℂ ∖ D R ∈ ℝ +
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 ∈ ℂ ∖ D R ∈ ℝ + → ⦋ C / y⦌ R ∈ ℝ +
21 13 15 20 sylc ⊢ φ ∧ ¬ C ∈ D → ⦋ C / y⦌ R ∈ ℝ +
22 8 21 9 rlimi ⊢ φ ∧ ¬ C ∈ D → ∃ r ∈ ℝ ∀ x ∈ A r ≤ 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 ∈ D R ≤ z − y
32 31 ralrimiva ⊢ φ → ∀ y ∈ ℂ ∖ D ∀ z ∈ D R ≤ z − y
33 32 adantr ⊢ φ ∧ ¬ C ∈ D → ∀ y ∈ ℂ ∖ D ∀ z ∈ D R ≤ z − y
34 nfcv ⊢ Ⅎ _ y D
35 nfcv ⊢ Ⅎ _ y ≤
36 nfcv ⊢ Ⅎ _ y z − 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 ∈ D R ≤ z − y ↔ ∀ z ∈ D ⦋ C / y⦌ R ≤ z − C
43 38 42 rspc ⊢ C ∈ ℂ ∖ D → ∀ y ∈ ℂ ∖ D ∀ z ∈ D R ≤ 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 ∈ A r ≤ 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 ∈ A r ≤ x ↔ sup A ℝ * < = +∞
63 61 62 syl ⊢ φ → ∀ r ∈ ℝ ∃ x ∈ A r ≤ x ↔ sup A ℝ * < = +∞
64 1 63 mpbird ⊢ φ → ∀ r ∈ ℝ ∃ x ∈ A r ≤ x
65 64 adantr ⊢ φ ∧ ¬ C ∈ D → ∀ r ∈ ℝ ∃ x ∈ A r ≤ x
66 65 r19.21bi ⊢ φ ∧ ¬ C ∈ D ∧ r ∈ ℝ → ∃ x ∈ A r ≤ x
67 r19.29 ⊢ ∀ x ∈ A r ≤ x → B − C < ⦋ C / y⦌ R ∧ ∃ x ∈ A r ≤ x → ∃ x ∈ A r ≤ x → B − C < ⦋ C / y⦌ R ∧ r ≤ x
68 67 expcom ⊢ ∃ x ∈ A r ≤ x → ∀ x ∈ A r ≤ x → B − C < ⦋ C / y⦌ R → ∃ x ∈ A r ≤ x → B − C < ⦋ C / y⦌ R ∧ r ≤ x
69 66 68 syl ⊢ φ ∧ ¬ C ∈ D ∧ r ∈ ℝ → ∀ x ∈ A r ≤ x → B − C < ⦋ C / y⦌ R → ∃ x ∈ A r ≤ x → B − C < ⦋ C / y⦌ R ∧ r ≤ x
70 54 69 mtod ⊢ φ ∧ ¬ C ∈ D ∧ r ∈ ℝ → ¬ ∀ x ∈ A r ≤ x → B − C < ⦋ C / y⦌ R
71 70 nrexdv ⊢ φ ∧ ¬ C ∈ D → ¬ ∃ r ∈ ℝ ∀ x ∈ A r ≤ x → B − C < ⦋ C / y⦌ R
72 22 71 condan ⊢ φ → C ∈ D