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	$⊢ φ \to F : \emptyset ⟶ ℂ$
	limcdm0.b	$⊢ φ \to B \in ℂ$
Assertion	limcdm0	$⊢ φ \to F {lim}_{ℂ} B = ℂ$

Proof

Step	Hyp	Ref	Expression
1		limcdm0.f	$⊢ φ \to F : \emptyset ⟶ ℂ$
2		limcdm0.b	$⊢ φ \to B \in ℂ$
3		limccl	$⊢ F {lim}_{ℂ} B \subseteq ℂ$
4	3	sseli	$⊢ x \in (F {lim}_{ℂ} B) \to x \in ℂ$
5	4	adantl	$⊢ (φ \land x \in (F {lim}_{ℂ} B)) \to x \in ℂ$
6		simpr	$⊢ (φ \land x \in ℂ) \to x \in ℂ$
7		1rp	$⊢ 1 \in ℝ^{+}$
8		ral0	$⊢ \forall z \in \emptyset ((z \neq B \land \|z - B\| < 1) \to \|F (z) - x\| < y)$
9		brimralrspcev	$⊢ (1 \in ℝ^{+} \land \forall z \in \emptyset ((z \neq B \land \|z - B\| < 1) \to \|F (z) - x\| < y)) \to \exists w \in ℝ^{+} \forall z \in \emptyset ((z \neq B \land \|z - B\| < w) \to \|F (z) - x\| < y)$
10	7 8 9	mp2an	$⊢ \exists w \in ℝ^{+} \forall z \in \emptyset ((z \neq B \land \|z - B\| < w) \to \|F (z) - x\| < y)$
11	10	rgenw	$⊢ \forall y \in ℝ^{+} \exists w \in ℝ^{+} \forall z \in \emptyset ((z \neq B \land \|z - B\| < w) \to \|F (z) - x\| < y)$
12	11	a1i	$⊢ (φ \land x \in ℂ) \to \forall y \in ℝ^{+} \exists w \in ℝ^{+} \forall z \in \emptyset ((z \neq B \land \|z - B\| < w) \to \|F (z) - x\| < y)$
13	1	adantr	$⊢ (φ \land x \in ℂ) \to F : \emptyset ⟶ ℂ$
14		0ss	$⊢ \emptyset \subseteq ℂ$
15	14	a1i	$⊢ (φ \land x \in ℂ) \to \emptyset \subseteq ℂ$
16	2	adantr	$⊢ (φ \land x \in ℂ) \to B \in ℂ$
17	13 15 16	ellimc3	$⊢ (φ \land x \in ℂ) \to (x \in (F {lim}_{ℂ} B) \leftrightarrow (x \in ℂ \land \forall y \in ℝ^{+} \exists w \in ℝ^{+} \forall z \in \emptyset ((z \neq B \land \|z - B\| < w) \to \|F (z) - x\| < y)))$
18	6 12 17	mpbir2and	$⊢ (φ \land x \in ℂ) \to x \in (F {lim}_{ℂ} B)$
19	5 18	impbida	$⊢ φ \to (x \in (F {lim}_{ℂ} B) \leftrightarrow x \in ℂ)$
20	19	eqrdv	$⊢ φ \to F {lim}_{ℂ} B = ℂ$

Metamath Proof Explorer

Theorem limcdm0

Proof