Metamath Proof Explorer

Theorem limcdm0

Description: If a function has empty domain, every complex number is a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses limcdm0.f ⊢ φ → F : ∅ ⟶ ℂ
limcdm0.b ⊢ φ → B ∈ ℂ
Assertion limcdm0 ⊢ φ → F lim ℂ B = ℂ

Proof

Step Hyp Ref Expression
1 limcdm0.f ⊢ φ → F : ∅ ⟶ ℂ
2 limcdm0.b ⊢ φ → B ∈ ℂ
3 limccl ⊢ F lim ℂ B ⊆ ℂ
4 3 sseli ⊢ x ∈ F lim ℂ B → x ∈ ℂ
5 4 adantl ⊢ φ ∧ x ∈ F lim ℂ B → x ∈ ℂ
6 simpr ⊢ φ ∧ x ∈ ℂ → x ∈ ℂ
7 1rp ⊢ 1 ∈ ℝ +
8 ral0 ⊢ ∀ z ∈ ∅ z ≠ B ∧ z − B < 1 → F ⁡ z − x < y
9 brimralrspcev ⊢ 1 ∈ ℝ + ∧ ∀ z ∈ ∅ z ≠ B ∧ z − B < 1 → F ⁡ z − x < y → ∃ w ∈ ℝ + ∀ z ∈ ∅ z ≠ B ∧ z − B < w → F ⁡ z − x < y
10 7 8 9 mp2an ⊢ ∃ w ∈ ℝ + ∀ z ∈ ∅ z ≠ B ∧ z − B < w → F ⁡ z − x < y
11 10 rgenw ⊢ ∀ y ∈ ℝ + ∃ w ∈ ℝ + ∀ z ∈ ∅ z ≠ B ∧ z − B < w → F ⁡ z − x < y
12 11 a1i ⊢ φ ∧ x ∈ ℂ → ∀ y ∈ ℝ + ∃ w ∈ ℝ + ∀ z ∈ ∅ z ≠ B ∧ z − B < w → F ⁡ z − x < y
13 1 adantr ⊢ φ ∧ x ∈ ℂ → F : ∅ ⟶ ℂ
14 0ss ⊢ ∅ ⊆ ℂ
15 14 a1i ⊢ φ ∧ x ∈ ℂ → ∅ ⊆ ℂ
16 2 adantr ⊢ φ ∧ x ∈ ℂ → B ∈ ℂ
17 13 15 16 ellimc3 ⊢ φ ∧ x ∈ ℂ → x ∈ F lim ℂ B ↔ x ∈ ℂ ∧ ∀ y ∈ ℝ + ∃ w ∈ ℝ + ∀ z ∈ ∅ z ≠ B ∧ z − B < w → F ⁡ z − x < y
18 6 12 17 mpbir2and ⊢ φ ∧ x ∈ ℂ → x ∈ F lim ℂ B
19 5 18 impbida ⊢ φ → x ∈ F lim ℂ B ↔ x ∈ ℂ
20 19 eqrdv ⊢ φ → F lim ℂ B = ℂ