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ℂ 𝐵 ) = ℂ )