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 
|- ( 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 )