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	\|- ( ph -> F : (/) --> CC )
	limcdm0.b	\|- ( ph -> B e. CC )
Assertion	limcdm0	\|- ( ph -> ( F limCC B ) = CC )

Proof

Step	Hyp	Ref	Expression
1		limcdm0.f	\|- ( ph -> F : (/) --> CC )
2		limcdm0.b	\|- ( ph -> B e. CC )
3		limccl	\|- ( F limCC B ) C_ CC
4	3	sseli	\|- ( x e. ( F limCC B ) -> x e. CC )
5	4	adantl	\|- ( ( ph /\ x e. ( F limCC B ) ) -> x e. CC )
6		simpr	\|- ( ( ph /\ x e. CC ) -> x e. CC )
7		1rp	\|- 1 e. RR+
8		ral0	\|- A. z e. (/) ( ( z =/= B /\ ( abs ` ( z - B ) ) < 1 ) -> ( abs ` ( ( F ` z ) - x ) ) < y )
9		brimralrspcev	\|- ( ( 1 e. RR+ /\ A. z e. (/) ( ( z =/= B /\ ( abs ` ( z - B ) ) < 1 ) -> ( abs ` ( ( F ` z ) - x ) ) < y ) ) -> E. w e. RR+ A. z e. (/) ( ( z =/= B /\ ( abs ` ( z - B ) ) < w ) -> ( abs ` ( ( F ` z ) - x ) ) < y ) )
10	7 8 9	mp2an	\|- E. w e. RR+ A. z e. (/) ( ( z =/= B /\ ( abs ` ( z - B ) ) < w ) -> ( abs ` ( ( F ` z ) - x ) ) < y )
11	10	rgenw	\|- A. y e. RR+ E. w e. RR+ A. z e. (/) ( ( z =/= B /\ ( abs ` ( z - B ) ) < w ) -> ( abs ` ( ( F ` z ) - x ) ) < y )
12	11	a1i	\|- ( ( ph /\ x e. CC ) -> A. y e. RR+ E. w e. RR+ A. z e. (/) ( ( z =/= B /\ ( abs ` ( z - B ) ) < w ) -> ( abs ` ( ( F ` z ) - x ) ) < y ) )
13	1	adantr	\|- ( ( ph /\ x e. CC ) -> F : (/) --> CC )
14		0ss	\|- (/) C_ CC
15	14	a1i	\|- ( ( ph /\ x e. CC ) -> (/) C_ CC )
16	2	adantr	\|- ( ( ph /\ x e. CC ) -> B e. CC )
17	13 15 16	ellimc3	\|- ( ( ph /\ x e. CC ) -> ( x e. ( F limCC B ) <-> ( x e. CC /\ A. y e. RR+ E. w e. RR+ A. z e. (/) ( ( z =/= B /\ ( abs ` ( z - B ) ) < w ) -> ( abs ` ( ( F ` z ) - x ) ) < y ) ) ) )
18	6 12 17	mpbir2and	\|- ( ( ph /\ x e. CC ) -> x e. ( F limCC B ) )
19	5 18	impbida	\|- ( ph -> ( x e. ( F limCC B ) <-> x e. CC ) )
20	19	eqrdv	\|- ( ph -> ( F limCC B ) = CC )

Metamath Proof Explorer

Theorem limcdm0

Proof