This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐹 : ∅ ⟶ ℂ )
limcdm0.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
Assertion limcdm0 ( 𝜑 → ( 𝐹 limℂ 𝐵 ) = ℂ )

Proof

Step Hyp Ref Expression
1 limcdm0.f ⊢ ( 𝜑 → 𝐹 : ∅ ⟶ ℂ )
2 limcdm0.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3 limccl ⊢ ( 𝐹 limℂ 𝐵 ) ⊆ ℂ
4 3 sseli ⊢ ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) → 𝑥 ∈ ℂ )
5 4 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) ) → 𝑥 ∈ ℂ )
6 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
7 1rp ⊢ 1 ∈ ℝ+
8 ral0 ⊢ ∀ 𝑧 ∈ ∅ ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 1 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑥 ) ) < 𝑦 )
9 brimralrspcev ⊢ ( ( 1 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ∅ ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 1 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑥 ) ) < 𝑦 ) ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑧 ∈ ∅ ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑥 ) ) < 𝑦 ) )
10 7 8 9 mp2an ⊢ ∃ 𝑤 ∈ ℝ+ ∀ 𝑧 ∈ ∅ ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑥 ) ) < 𝑦 )
11 10 rgenw ⊢ ∀ 𝑦 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑧 ∈ ∅ ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑥 ) ) < 𝑦 )
12 11 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ∀ 𝑦 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑧 ∈ ∅ ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑥 ) ) < 𝑦 ) )
13 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝐹 : ∅ ⟶ ℂ )
14 0ss ⊢ ∅ ⊆ ℂ
15 14 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ∅ ⊆ ℂ )
16 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝐵 ∈ ℂ )
17 13 15 16 ellimc3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) ↔ ( 𝑥 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑧 ∈ ∅ ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑥 ) ) < 𝑦 ) ) ) )
18 6 12 17 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) )
19 5 18 impbida ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) ↔ 𝑥 ∈ ℂ ) )
20 19 eqrdv ⊢ ( 𝜑 → ( 𝐹 limℂ 𝐵 ) = ℂ )