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