Metamath Proof Explorer

Theorem unblimceq0lem

Description: Lemma for unblimceq0 . (Contributed by Asger C. Ipsen, 12-May-2021)

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

Proof

Step Hyp Ref Expression
1 unblimceq0lem.0 
 |-  ( ph -> S C_ CC )
2 unblimceq0lem.1 
 |-  ( ph -> F : S --> CC )
3 unblimceq0lem.2 
 |-  ( ph -> A e. CC )
4 unblimceq0lem.3 
 |-  ( ph -> A. b e. RR+ A. d e. RR+ E. x e. S ( ( abs ` ( x - A ) ) < d /\ b <_ ( abs ` ( F ` x ) ) ) )
5 breq1 
 |-  ( b = if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) -> ( b <_ ( abs ` ( F ` x ) ) <-> if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) )
6 5 anbi2d 
 |-  ( b = if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) -> ( ( ( abs ` ( x - A ) ) < d /\ b <_ ( abs ` ( F ` x ) ) ) <-> ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) )
7 6 rexbidv 
 |-  ( b = if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) -> ( E. x e. S ( ( abs ` ( x - A ) ) < d /\ b <_ ( abs ` ( F ` x ) ) ) <-> E. x e. S ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) )
8 7 ralbidv 
 |-  ( b = if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) -> ( A. d e. RR+ E. x e. S ( ( abs ` ( x - A ) ) < d /\ b <_ ( abs ` ( F ` x ) ) ) <-> A. d e. RR+ E. x e. S ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) )
9 4 adantr 
 |-  ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) -> A. b e. RR+ A. d e. RR+ E. x e. S ( ( abs ` ( x - A ) ) < d /\ b <_ ( abs ` ( F ` x ) ) ) )
10 2 ad2antrr 
 |-  ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ A e. S ) -> F : S --> CC )
11 simpr 
 |-  ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ A e. S ) -> A e. S )
12 10 11 ffvelcdmd 
 |-  ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ A e. S ) -> ( F ` A ) e. CC )
13 12 abscld 
 |-  ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ A e. S ) -> ( abs ` ( F ` A ) ) e. RR )
14 simprl 
 |-  ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) -> c e. RR+ )
15 14 rpred 
 |-  ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) -> c e. RR )
16 15 adantr 
 |-  ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ A e. S ) -> c e. RR )
17 13 16 readdcld 
 |-  ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ A e. S ) -> ( ( abs ` ( F ` A ) ) + c ) e. RR )
18 12 absge0d 
 |-  ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ A e. S ) -> 0 <_ ( abs ` ( F ` A ) ) )
19 14 rpgt0d 
 |-  ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) -> 0 < c )
20 19 adantr 
 |-  ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ A e. S ) -> 0 < c )
21 13 16 18 20 addgegt0d 
 |-  ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ A e. S ) -> 0 < ( ( abs ` ( F ` A ) ) + c ) )
22 17 21 elrpd 
 |-  ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ A e. S ) -> ( ( abs ` ( F ` A ) ) + c ) e. RR+ )
23 simplrl 
 |-  ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ -. A e. S ) -> c e. RR+ )
24 22 23 ifclda 
 |-  ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) -> if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) e. RR+ )
25 8 9 24 rspcdva 
 |-  ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) -> A. d e. RR+ E. x e. S ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) )
26 simprr 
 |-  ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) -> d e. RR+ )
27 rsp 
 |-  ( A. d e. RR+ E. x e. S ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) -> ( d e. RR+ -> E. x e. S ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) )
28 25 26 27 sylc 
 |-  ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) -> E. x e. S ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) )
29 simprl 
 |-  ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) -> x e. S )
30 neeq1 
 |-  ( y = x -> ( y =/= A <-> x =/= A ) )
31 fvoveq1 
 |-  ( y = x -> ( abs ` ( y - A ) ) = ( abs ` ( x - A ) ) )
32 31 breq1d 
 |-  ( y = x -> ( ( abs ` ( y - A ) ) < d <-> ( abs ` ( x - A ) ) < d ) )
33 2fveq3 
 |-  ( y = x -> ( abs ` ( F ` y ) ) = ( abs ` ( F ` x ) ) )
34 33 breq2d 
 |-  ( y = x -> ( c <_ ( abs ` ( F ` y ) ) <-> c <_ ( abs ` ( F ` x ) ) ) )
35 30 32 34 3anbi123d 
 |-  ( y = x -> ( ( y =/= A /\ ( abs ` ( y - A ) ) < d /\ c <_ ( abs ` ( F ` y ) ) ) <-> ( x =/= A /\ ( abs ` ( x - A ) ) < d /\ c <_ ( abs ` ( F ` x ) ) ) ) )
36 35 adantl 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ y = x ) -> ( ( y =/= A /\ ( abs ` ( y - A ) ) < d /\ c <_ ( abs ` ( F ` y ) ) ) <-> ( x =/= A /\ ( abs ` ( x - A ) ) < d /\ c <_ ( abs ` ( F ` x ) ) ) ) )
37 17 adantlr 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ A e. S ) -> ( ( abs ` ( F ` A ) ) + c ) e. RR )
38 2 ad2antrr 
 |-  ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) -> F : S --> CC )
39 38 29 ffvelcdmd 
 |-  ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) -> ( F ` x ) e. CC )
40 39 abscld 
 |-  ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) -> ( abs ` ( F ` x ) ) e. RR )
41 40 adantr 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ A e. S ) -> ( abs ` ( F ` x ) ) e. RR )
42 simpr 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ A e. S ) -> A e. S )
43 42 iftrued 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ A e. S ) -> if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) = ( ( abs ` ( F ` A ) ) + c ) )
44 43 eqcomd 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ A e. S ) -> ( ( abs ` ( F ` A ) ) + c ) = if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) )
45 simprrr 
 |-  ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) -> if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) )
46 45 adantr 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ A e. S ) -> if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) )
47 44 46 eqbrtrd 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ A e. S ) -> ( ( abs ` ( F ` A ) ) + c ) <_ ( abs ` ( F ` x ) ) )
48 37 41 47 lensymd 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ A e. S ) -> -. ( abs ` ( F ` x ) ) < ( ( abs ` ( F ` A ) ) + c ) )
49 2fveq3 
 |-  ( x = A -> ( abs ` ( F ` x ) ) = ( abs ` ( F ` A ) ) )
50 49 adantl 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ A e. S ) /\ x = A ) -> ( abs ` ( F ` x ) ) = ( abs ` ( F ` A ) ) )
51 16 13 ltaddposd 
 |-  ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ A e. S ) -> ( 0 < c <-> ( abs ` ( F ` A ) ) < ( ( abs ` ( F ` A ) ) + c ) ) )
52 20 51 mpbid 
 |-  ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ A e. S ) -> ( abs ` ( F ` A ) ) < ( ( abs ` ( F ` A ) ) + c ) )
53 52 adantr 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ A e. S ) /\ x = A ) -> ( abs ` ( F ` A ) ) < ( ( abs ` ( F ` A ) ) + c ) )
54 50 53 eqbrtrd 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ A e. S ) /\ x = A ) -> ( abs ` ( F ` x ) ) < ( ( abs ` ( F ` A ) ) + c ) )
55 54 ex 
 |-  ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ A e. S ) -> ( x = A -> ( abs ` ( F ` x ) ) < ( ( abs ` ( F ` A ) ) + c ) ) )
56 55 adantlr 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ A e. S ) -> ( x = A -> ( abs ` ( F ` x ) ) < ( ( abs ` ( F ` A ) ) + c ) ) )
57 56 necon3bd 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ A e. S ) -> ( -. ( abs ` ( F ` x ) ) < ( ( abs ` ( F ` A ) ) + c ) -> x =/= A ) )
58 48 57 mpd 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ A e. S ) -> x =/= A )
59 simprrl 
 |-  ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) -> ( abs ` ( x - A ) ) < d )
60 59 adantr 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ A e. S ) -> ( abs ` ( x - A ) ) < d )
61 16 adantlr 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ A e. S ) -> c e. RR )
62 12 adantlr 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ A e. S ) -> ( F ` A ) e. CC )
63 62 absge0d 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ A e. S ) -> 0 <_ ( abs ` ( F ` A ) ) )
64 13 adantlr 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ A e. S ) -> ( abs ` ( F ` A ) ) e. RR )
65 61 64 addge02d 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ A e. S ) -> ( 0 <_ ( abs ` ( F ` A ) ) <-> c <_ ( ( abs ` ( F ` A ) ) + c ) ) )
66 63 65 mpbid 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ A e. S ) -> c <_ ( ( abs ` ( F ` A ) ) + c ) )
67 61 37 41 66 47 letrd 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ A e. S ) -> c <_ ( abs ` ( F ` x ) ) )
68 58 60 67 3jca 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ A e. S ) -> ( x =/= A /\ ( abs ` ( x - A ) ) < d /\ c <_ ( abs ` ( F ` x ) ) ) )
69 simpr 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ -. A e. S ) -> -. A e. S )
70 simpr 
 |-  ( ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ -. A e. S ) /\ x = A ) -> x = A )
71 29 adantr 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ -. A e. S ) -> x e. S )
72 71 adantr 
 |-  ( ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ -. A e. S ) /\ x = A ) -> x e. S )
73 70 72 eqeltrrd 
 |-  ( ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ -. A e. S ) /\ x = A ) -> A e. S )
74 73 ex 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ -. A e. S ) -> ( x = A -> A e. S ) )
75 74 necon3bd 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ -. A e. S ) -> ( -. A e. S -> x =/= A ) )
76 69 75 mpd 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ -. A e. S ) -> x =/= A )
77 59 adantr 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ -. A e. S ) -> ( abs ` ( x - A ) ) < d )
78 69 iffalsed 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ -. A e. S ) -> if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) = c )
79 78 eqcomd 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ -. A e. S ) -> c = if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) )
80 45 adantr 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ -. A e. S ) -> if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) )
81 79 80 eqbrtrd 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ -. A e. S ) -> c <_ ( abs ` ( F ` x ) ) )
82 76 77 81 3jca 
 |-  ( ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) /\ -. A e. S ) -> ( x =/= A /\ ( abs ` ( x - A ) ) < d /\ c <_ ( abs ` ( F ` x ) ) ) )
83 68 82 pm2.61dan 
 |-  ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) -> ( x =/= A /\ ( abs ` ( x - A ) ) < d /\ c <_ ( abs ` ( F ` x ) ) ) )
84 29 36 83 rspcedvd 
 |-  ( ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) /\ ( x e. S /\ ( ( abs ` ( x - A ) ) < d /\ if ( A e. S , ( ( abs ` ( F ` A ) ) + c ) , c ) <_ ( abs ` ( F ` x ) ) ) ) ) -> E. y e. S ( y =/= A /\ ( abs ` ( y - A ) ) < d /\ c <_ ( abs ` ( F ` y ) ) ) )
85 28 84 rexlimddv 
 |-  ( ( ph /\ ( c e. RR+ /\ d e. RR+ ) ) -> E. y e. S ( y =/= A /\ ( abs ` ( y - A ) ) < d /\ c <_ ( abs ` ( F ` y ) ) ) )
86 85 ralrimivva 
 |-  ( ph -> A. c e. RR+ A. d e. RR+ E. y e. S ( y =/= A /\ ( abs ` ( y - A ) ) < d /\ c <_ ( abs ` ( F ` y ) ) ) )