Metamath Proof Explorer

Theorem unblimceq0

Description: If F is unbounded near A it has no limit at A . (Contributed by Asger C. Ipsen, 12-May-2021)

Ref Expression
Hypotheses unblimceq0.0 
|- ( ph -> S C_ CC )
unblimceq0.1 
|- ( ph -> F : S --> CC )
unblimceq0.2 
|- ( ph -> A e. CC )
unblimceq0.3 
|- ( ph -> A. b e. RR+ A. d e. RR+ E. x e. S ( ( abs ` ( x - A ) ) < d /\ b <_ ( abs ` ( F ` x ) ) ) )
Assertion unblimceq0 
|- ( ph -> ( F limCC A ) = (/) )

Proof

Step Hyp Ref Expression
1 unblimceq0.0 
 |-  ( ph -> S C_ CC )
2 unblimceq0.1 
 |-  ( ph -> F : S --> CC )
3 unblimceq0.2 
 |-  ( ph -> A e. CC )
4 unblimceq0.3 
 |-  ( ph -> A. b e. RR+ A. d e. RR+ E. x e. S ( ( abs ` ( x - A ) ) < d /\ b <_ ( abs ` ( F ` x ) ) ) )
5 1rp 
 |-  1 e. RR+
6 5 a1i 
 |-  ( ( ph /\ y e. CC ) -> 1 e. RR+ )
7 breq2 
 |-  ( e = 1 -> ( ( abs ` ( ( F ` z ) - y ) ) < e <-> ( abs ` ( ( F ` z ) - y ) ) < 1 ) )
8 7 imbi2d 
 |-  ( e = 1 -> ( ( ( z =/= A /\ ( abs ` ( z - A ) ) < c ) -> ( abs ` ( ( F ` z ) - y ) ) < e ) <-> ( ( z =/= A /\ ( abs ` ( z - A ) ) < c ) -> ( abs ` ( ( F ` z ) - y ) ) < 1 ) ) )
9 8 rexralbidv 
 |-  ( e = 1 -> ( E. c e. RR+ A. z e. S ( ( z =/= A /\ ( abs ` ( z - A ) ) < c ) -> ( abs ` ( ( F ` z ) - y ) ) < e ) <-> E. c e. RR+ A. z e. S ( ( z =/= A /\ ( abs ` ( z - A ) ) < c ) -> ( abs ` ( ( F ` z ) - y ) ) < 1 ) ) )
10 9 notbid 
 |-  ( e = 1 -> ( -. E. c e. RR+ A. z e. S ( ( z =/= A /\ ( abs ` ( z - A ) ) < c ) -> ( abs ` ( ( F ` z ) - y ) ) < e ) <-> -. E. c e. RR+ A. z e. S ( ( z =/= A /\ ( abs ` ( z - A ) ) < c ) -> ( abs ` ( ( F ` z ) - y ) ) < 1 ) ) )
11 10 adantl 
 |-  ( ( ( ph /\ y e. CC ) /\ e = 1 ) -> ( -. E. c e. RR+ A. z e. S ( ( z =/= A /\ ( abs ` ( z - A ) ) < c ) -> ( abs ` ( ( F ` z ) - y ) ) < e ) <-> -. E. c e. RR+ A. z e. S ( ( z =/= A /\ ( abs ` ( z - A ) ) < c ) -> ( abs ` ( ( F ` z ) - y ) ) < 1 ) ) )
12 simprr1 
 |-  ( ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) /\ ( z e. S /\ ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) ) -> z =/= A )
13 simprr2 
 |-  ( ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) /\ ( z e. S /\ ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) ) -> ( abs ` ( z - A ) ) < c )
14 12 13 jca 
 |-  ( ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) /\ ( z e. S /\ ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) ) -> ( z =/= A /\ ( abs ` ( z - A ) ) < c ) )
15 1red 
 |-  ( ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) /\ ( z e. S /\ ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) ) -> 1 e. RR )
16 2 ad2antrr 
 |-  ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) -> F : S --> CC )
17 16 adantr 
 |-  ( ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) /\ ( z e. S /\ ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) ) -> F : S --> CC )
18 simprl 
 |-  ( ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) /\ ( z e. S /\ ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) ) -> z e. S )
19 17 18 ffvelrnd 
 |-  ( ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) /\ ( z e. S /\ ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) ) -> ( F ` z ) e. CC )
20 simplr 
 |-  ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) -> y e. CC )
21 20 adantr 
 |-  ( ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) /\ ( z e. S /\ ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) ) -> y e. CC )
22 19 21 subcld 
 |-  ( ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) /\ ( z e. S /\ ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) ) -> ( ( F ` z ) - y ) e. CC )
23 22 abscld 
 |-  ( ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) /\ ( z e. S /\ ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) ) -> ( abs ` ( ( F ` z ) - y ) ) e. RR )
24 19 abscld 
 |-  ( ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) /\ ( z e. S /\ ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) ) -> ( abs ` ( F ` z ) ) e. RR )
25 20 abscld 
 |-  ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) -> ( abs ` y ) e. RR )
26 25 adantr 
 |-  ( ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) /\ ( z e. S /\ ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) ) -> ( abs ` y ) e. RR )
27 24 26 resubcld 
 |-  ( ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) /\ ( z e. S /\ ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) ) -> ( ( abs ` ( F ` z ) ) - ( abs ` y ) ) e. RR )
28 1cnd 
 |-  ( ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) /\ ( z e. S /\ ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) ) -> 1 e. CC )
29 26 recnd 
 |-  ( ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) /\ ( z e. S /\ ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) ) -> ( abs ` y ) e. CC )
30 28 29 pncand 
 |-  ( ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) /\ ( z e. S /\ ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) ) -> ( ( 1 + ( abs ` y ) ) - ( abs ` y ) ) = 1 )
31 1red 
 |-  ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) -> 1 e. RR )
32 31 25 readdcld 
 |-  ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) -> ( 1 + ( abs ` y ) ) e. RR )
33 32 adantr 
 |-  ( ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) /\ ( z e. S /\ ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) ) -> ( 1 + ( abs ` y ) ) e. RR )
34 simprr3 
 |-  ( ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) /\ ( z e. S /\ ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) ) -> ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) )
35 33 24 26 34 lesub1dd 
 |-  ( ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) /\ ( z e. S /\ ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) ) -> ( ( 1 + ( abs ` y ) ) - ( abs ` y ) ) <_ ( ( abs ` ( F ` z ) ) - ( abs ` y ) ) )
36 30 35 eqbrtrrd 
 |-  ( ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) /\ ( z e. S /\ ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) ) -> 1 <_ ( ( abs ` ( F ` z ) ) - ( abs ` y ) ) )
37 19 21 abs2difd 
 |-  ( ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) /\ ( z e. S /\ ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) ) -> ( ( abs ` ( F ` z ) ) - ( abs ` y ) ) <_ ( abs ` ( ( F ` z ) - y ) ) )
38 15 27 23 36 37 letrd 
 |-  ( ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) /\ ( z e. S /\ ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) ) -> 1 <_ ( abs ` ( ( F ` z ) - y ) ) )
39 15 23 38 lensymd 
 |-  ( ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) /\ ( z e. S /\ ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) ) -> -. ( abs ` ( ( F ` z ) - y ) ) < 1 )
40 14 39 jcnd 
 |-  ( ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) /\ ( z e. S /\ ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) ) -> -. ( ( z =/= A /\ ( abs ` ( z - A ) ) < c ) -> ( abs ` ( ( F ` z ) - y ) ) < 1 ) )
41 breq2 
 |-  ( d = c -> ( ( abs ` ( z - A ) ) < d <-> ( abs ` ( z - A ) ) < c ) )
42 41 3anbi2d 
 |-  ( d = c -> ( ( z =/= A /\ ( abs ` ( z - A ) ) < d /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) <-> ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) )
43 42 rexbidv 
 |-  ( d = c -> ( E. z e. S ( z =/= A /\ ( abs ` ( z - A ) ) < d /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) <-> E. z e. S ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) )
44 breq1 
 |-  ( a = ( 1 + ( abs ` y ) ) -> ( a <_ ( abs ` ( F ` z ) ) <-> ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) )
45 44 3anbi3d 
 |-  ( a = ( 1 + ( abs ` y ) ) -> ( ( z =/= A /\ ( abs ` ( z - A ) ) < d /\ a <_ ( abs ` ( F ` z ) ) ) <-> ( z =/= A /\ ( abs ` ( z - A ) ) < d /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) )
46 45 rexbidv 
 |-  ( a = ( 1 + ( abs ` y ) ) -> ( E. z e. S ( z =/= A /\ ( abs ` ( z - A ) ) < d /\ a <_ ( abs ` ( F ` z ) ) ) <-> E. z e. S ( z =/= A /\ ( abs ` ( z - A ) ) < d /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) )
47 46 ralbidv 
 |-  ( a = ( 1 + ( abs ` y ) ) -> ( A. d e. RR+ E. z e. S ( z =/= A /\ ( abs ` ( z - A ) ) < d /\ a <_ ( abs ` ( F ` z ) ) ) <-> A. d e. RR+ E. z e. S ( z =/= A /\ ( abs ` ( z - A ) ) < d /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) ) )
48 1 2 3 4 unblimceq0lem 
 |-  ( ph -> A. a e. RR+ A. d e. RR+ E. z e. S ( z =/= A /\ ( abs ` ( z - A ) ) < d /\ a <_ ( abs ` ( F ` z ) ) ) )
49 48 ad2antrr 
 |-  ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) -> A. a e. RR+ A. d e. RR+ E. z e. S ( z =/= A /\ ( abs ` ( z - A ) ) < d /\ a <_ ( abs ` ( F ` z ) ) ) )
50 0lt1 
 |-  0 < 1
51 50 a1i 
 |-  ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) -> 0 < 1 )
52 20 absge0d 
 |-  ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) -> 0 <_ ( abs ` y ) )
53 31 25 51 52 addgtge0d 
 |-  ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) -> 0 < ( 1 + ( abs ` y ) ) )
54 32 53 elrpd 
 |-  ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) -> ( 1 + ( abs ` y ) ) e. RR+ )
55 47 49 54 rspcdva 
 |-  ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) -> A. d e. RR+ E. z e. S ( z =/= A /\ ( abs ` ( z - A ) ) < d /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) )
56 simpr 
 |-  ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) -> c e. RR+ )
57 43 55 56 rspcdva 
 |-  ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) -> E. z e. S ( z =/= A /\ ( abs ` ( z - A ) ) < c /\ ( 1 + ( abs ` y ) ) <_ ( abs ` ( F ` z ) ) ) )
58 40 57 reximddv 
 |-  ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) -> E. z e. S -. ( ( z =/= A /\ ( abs ` ( z - A ) ) < c ) -> ( abs ` ( ( F ` z ) - y ) ) < 1 ) )
59 rexnal 
 |-  ( E. z e. S -. ( ( z =/= A /\ ( abs ` ( z - A ) ) < c ) -> ( abs ` ( ( F ` z ) - y ) ) < 1 ) <-> -. A. z e. S ( ( z =/= A /\ ( abs ` ( z - A ) ) < c ) -> ( abs ` ( ( F ` z ) - y ) ) < 1 ) )
60 58 59 sylib 
 |-  ( ( ( ph /\ y e. CC ) /\ c e. RR+ ) -> -. A. z e. S ( ( z =/= A /\ ( abs ` ( z - A ) ) < c ) -> ( abs ` ( ( F ` z ) - y ) ) < 1 ) )
61 60 nrexdv 
 |-  ( ( ph /\ y e. CC ) -> -. E. c e. RR+ A. z e. S ( ( z =/= A /\ ( abs ` ( z - A ) ) < c ) -> ( abs ` ( ( F ` z ) - y ) ) < 1 ) )
62 6 11 61 rspcedvd 
 |-  ( ( ph /\ y e. CC ) -> E. e e. RR+ -. E. c e. RR+ A. z e. S ( ( z =/= A /\ ( abs ` ( z - A ) ) < c ) -> ( abs ` ( ( F ` z ) - y ) ) < e ) )
63 rexnal 
 |-  ( E. e e. RR+ -. E. c e. RR+ A. z e. S ( ( z =/= A /\ ( abs ` ( z - A ) ) < c ) -> ( abs ` ( ( F ` z ) - y ) ) < e ) <-> -. A. e e. RR+ E. c e. RR+ A. z e. S ( ( z =/= A /\ ( abs ` ( z - A ) ) < c ) -> ( abs ` ( ( F ` z ) - y ) ) < e ) )
64 62 63 sylib 
 |-  ( ( ph /\ y e. CC ) -> -. A. e e. RR+ E. c e. RR+ A. z e. S ( ( z =/= A /\ ( abs ` ( z - A ) ) < c ) -> ( abs ` ( ( F ` z ) - y ) ) < e ) )
65 64 ex 
 |-  ( ph -> ( y e. CC -> -. A. e e. RR+ E. c e. RR+ A. z e. S ( ( z =/= A /\ ( abs ` ( z - A ) ) < c ) -> ( abs ` ( ( F ` z ) - y ) ) < e ) ) )
66 imnan 
 |-  ( ( y e. CC -> -. A. e e. RR+ E. c e. RR+ A. z e. S ( ( z =/= A /\ ( abs ` ( z - A ) ) < c ) -> ( abs ` ( ( F ` z ) - y ) ) < e ) ) <-> -. ( y e. CC /\ A. e e. RR+ E. c e. RR+ A. z e. S ( ( z =/= A /\ ( abs ` ( z - A ) ) < c ) -> ( abs ` ( ( F ` z ) - y ) ) < e ) ) )
67 65 66 sylib 
 |-  ( ph -> -. ( y e. CC /\ A. e e. RR+ E. c e. RR+ A. z e. S ( ( z =/= A /\ ( abs ` ( z - A ) ) < c ) -> ( abs ` ( ( F ` z ) - y ) ) < e ) ) )
68 2 1 3 ellimc3 
 |-  ( ph -> ( y e. ( F limCC A ) <-> ( y e. CC /\ A. e e. RR+ E. c e. RR+ A. z e. S ( ( z =/= A /\ ( abs ` ( z - A ) ) < c ) -> ( abs ` ( ( F ` z ) - y ) ) < e ) ) ) )
69 67 68 mtbird 
 |-  ( ph -> -. y e. ( F limCC A ) )
70 69 eq0rdv 
 |-  ( ph -> ( F limCC A ) = (/) )