Metamath Proof Explorer

Theorem unbdqndv2lem2

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

Ref Expression
Hypotheses unbdqndv2lem2.g 
|- G = ( z e. ( X \ { A } ) |-> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) )
unbdqndv2lem2.w 
|- W = if ( ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) , U , V )
unbdqndv2lem2.x 
|- ( ph -> X C_ RR )
unbdqndv2lem2.f 
|- ( ph -> F : X --> CC )
unbdqndv2lem2.a 
|- ( ph -> A e. X )
unbdqndv2lem2.b 
|- ( ph -> B e. RR+ )
unbdqndv2lem2.d 
|- ( ph -> D e. RR+ )
unbdqndv2lem2.u 
|- ( ph -> U e. X )
unbdqndv2lem2.v 
|- ( ph -> V e. X )
unbdqndv2lem2.1 
|- ( ph -> U =/= V )
unbdqndv2lem2.2 
|- ( ph -> U <_ A )
unbdqndv2lem2.3 
|- ( ph -> A <_ V )
unbdqndv2lem2.4 
|- ( ph -> ( V - U ) < D )
unbdqndv2lem2.5 
|- ( ph -> ( 2 x. B ) <_ ( ( abs ` ( ( F ` V ) - ( F ` U ) ) ) / ( V - U ) ) )
Assertion unbdqndv2lem2 
|- ( ph -> ( W e. ( X \ { A } ) /\ ( ( abs ` ( W - A ) ) < D /\ B <_ ( abs ` ( G ` W ) ) ) ) )

Proof

Step Hyp Ref Expression
1 unbdqndv2lem2.g 
 |-  G = ( z e. ( X \ { A } ) |-> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) )
2 unbdqndv2lem2.w 
 |-  W = if ( ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) , U , V )
3 unbdqndv2lem2.x 
 |-  ( ph -> X C_ RR )
4 unbdqndv2lem2.f 
 |-  ( ph -> F : X --> CC )
5 unbdqndv2lem2.a 
 |-  ( ph -> A e. X )
6 unbdqndv2lem2.b 
 |-  ( ph -> B e. RR+ )
7 unbdqndv2lem2.d 
 |-  ( ph -> D e. RR+ )
8 unbdqndv2lem2.u 
 |-  ( ph -> U e. X )
9 unbdqndv2lem2.v 
 |-  ( ph -> V e. X )
10 unbdqndv2lem2.1 
 |-  ( ph -> U =/= V )
11 unbdqndv2lem2.2 
 |-  ( ph -> U <_ A )
12 unbdqndv2lem2.3 
 |-  ( ph -> A <_ V )
13 unbdqndv2lem2.4 
 |-  ( ph -> ( V - U ) < D )
14 unbdqndv2lem2.5 
 |-  ( ph -> ( 2 x. B ) <_ ( ( abs ` ( ( F ` V ) - ( F ` U ) ) ) / ( V - U ) ) )
15 2 a1i 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> W = if ( ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) , U , V ) )
16 iftrue 
 |-  ( ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) -> if ( ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) , U , V ) = U )
17 16 adantl 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> if ( ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) , U , V ) = U )
18 15 17 eqtrd 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> W = U )
19 8 adantr 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> U e. X )
20 simplr 
 |-  ( ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) /\ U = A ) -> ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) )
21 fveq2 
 |-  ( U = A -> ( F ` U ) = ( F ` A ) )
22 21 eqcomd 
 |-  ( U = A -> ( F ` A ) = ( F ` U ) )
23 22 oveq2d 
 |-  ( U = A -> ( ( F ` U ) - ( F ` A ) ) = ( ( F ` U ) - ( F ` U ) ) )
24 23 fveq2d 
 |-  ( U = A -> ( abs ` ( ( F ` U ) - ( F ` A ) ) ) = ( abs ` ( ( F ` U ) - ( F ` U ) ) ) )
25 24 adantl 
 |-  ( ( ph /\ U = A ) -> ( abs ` ( ( F ` U ) - ( F ` A ) ) ) = ( abs ` ( ( F ` U ) - ( F ` U ) ) ) )
26 4 8 ffvelcdmd 
 |-  ( ph -> ( F ` U ) e. CC )
27 26 subidd 
 |-  ( ph -> ( ( F ` U ) - ( F ` U ) ) = 0 )
28 27 fveq2d 
 |-  ( ph -> ( abs ` ( ( F ` U ) - ( F ` U ) ) ) = ( abs ` 0 ) )
29 28 adantr 
 |-  ( ( ph /\ U = A ) -> ( abs ` ( ( F ` U ) - ( F ` U ) ) ) = ( abs ` 0 ) )
30 abs0 
 |-  ( abs ` 0 ) = 0
31 30 a1i 
 |-  ( ( ph /\ U = A ) -> ( abs ` 0 ) = 0 )
32 29 31 eqtrd 
 |-  ( ( ph /\ U = A ) -> ( abs ` ( ( F ` U ) - ( F ` U ) ) ) = 0 )
33 25 32 eqtrd 
 |-  ( ( ph /\ U = A ) -> ( abs ` ( ( F ` U ) - ( F ` A ) ) ) = 0 )
34 33 adantlr 
 |-  ( ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) /\ U = A ) -> ( abs ` ( ( F ` U ) - ( F ` A ) ) ) = 0 )
35 20 34 breqtrd 
 |-  ( ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) /\ U = A ) -> ( B x. ( V - U ) ) <_ 0 )
36 6 rpred 
 |-  ( ph -> B e. RR )
37 3 9 sseldd 
 |-  ( ph -> V e. RR )
38 3 8 sseldd 
 |-  ( ph -> U e. RR )
39 37 38 resubcld 
 |-  ( ph -> ( V - U ) e. RR )
40 6 rpgt0d 
 |-  ( ph -> 0 < B )
41 3 5 sseldd 
 |-  ( ph -> A e. RR )
42 38 41 37 11 12 letrd 
 |-  ( ph -> U <_ V )
43 10 necomd 
 |-  ( ph -> V =/= U )
44 38 37 42 43 leneltd 
 |-  ( ph -> U < V )
45 38 37 posdifd 
 |-  ( ph -> ( U < V <-> 0 < ( V - U ) ) )
46 44 45 mpbid 
 |-  ( ph -> 0 < ( V - U ) )
47 36 39 40 46 mulgt0d 
 |-  ( ph -> 0 < ( B x. ( V - U ) ) )
48 0red 
 |-  ( ph -> 0 e. RR )
49 36 39 remulcld 
 |-  ( ph -> ( B x. ( V - U ) ) e. RR )
50 48 49 ltnled 
 |-  ( ph -> ( 0 < ( B x. ( V - U ) ) <-> -. ( B x. ( V - U ) ) <_ 0 ) )
51 47 50 mpbid 
 |-  ( ph -> -. ( B x. ( V - U ) ) <_ 0 )
52 51 adantr 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> -. ( B x. ( V - U ) ) <_ 0 )
53 52 adantr 
 |-  ( ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) /\ U = A ) -> -. ( B x. ( V - U ) ) <_ 0 )
54 35 53 pm2.65da 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> -. U = A )
55 54 neqned 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> U =/= A )
56 19 55 jca 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( U e. X /\ U =/= A ) )
57 eldifsn 
 |-  ( U e. ( X \ { A } ) <-> ( U e. X /\ U =/= A ) )
58 56 57 sylibr 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> U e. ( X \ { A } ) )
59 18 58 eqeltrd 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> W e. ( X \ { A } ) )
60 18 oveq1d 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( W - A ) = ( U - A ) )
61 60 fveq2d 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( abs ` ( W - A ) ) = ( abs ` ( U - A ) ) )
62 38 41 11 abssuble0d 
 |-  ( ph -> ( abs ` ( U - A ) ) = ( A - U ) )
63 62 adantr 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( abs ` ( U - A ) ) = ( A - U ) )
64 61 63 eqtrd 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( abs ` ( W - A ) ) = ( A - U ) )
65 41 38 resubcld 
 |-  ( ph -> ( A - U ) e. RR )
66 7 rpred 
 |-  ( ph -> D e. RR )
67 41 37 38 12 lesub1dd 
 |-  ( ph -> ( A - U ) <_ ( V - U ) )
68 65 39 66 67 13 lelttrd 
 |-  ( ph -> ( A - U ) < D )
69 68 adantr 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( A - U ) < D )
70 64 69 eqbrtrd 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( abs ` ( W - A ) ) < D )
71 36 65 remulcld 
 |-  ( ph -> ( B x. ( A - U ) ) e. RR )
72 71 adantr 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( B x. ( A - U ) ) e. RR )
73 49 adantr 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( B x. ( V - U ) ) e. RR )
74 4 5 ffvelcdmd 
 |-  ( ph -> ( F ` A ) e. CC )
75 26 74 subcld 
 |-  ( ph -> ( ( F ` U ) - ( F ` A ) ) e. CC )
76 75 abscld 
 |-  ( ph -> ( abs ` ( ( F ` U ) - ( F ` A ) ) ) e. RR )
77 76 adantr 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( abs ` ( ( F ` U ) - ( F ` A ) ) ) e. RR )
78 48 36 40 ltled 
 |-  ( ph -> 0 <_ B )
79 65 39 36 78 67 lemul2ad 
 |-  ( ph -> ( B x. ( A - U ) ) <_ ( B x. ( V - U ) ) )
80 79 adantr 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( B x. ( A - U ) ) <_ ( B x. ( V - U ) ) )
81 simpr 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) )
82 72 73 77 80 81 letrd 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( B x. ( A - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) )
83 36 adantr 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> B e. RR )
84 65 adantr 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( A - U ) e. RR )
85 11 adantr 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> U <_ A )
86 55 necomd 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> A =/= U )
87 85 86 jca 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( U <_ A /\ A =/= U ) )
88 38 41 ltlend 
 |-  ( ph -> ( U < A <-> ( U <_ A /\ A =/= U ) ) )
89 88 adantr 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( U < A <-> ( U <_ A /\ A =/= U ) ) )
90 87 89 mpbird 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> U < A )
91 38 41 posdifd 
 |-  ( ph -> ( U < A <-> 0 < ( A - U ) ) )
92 91 adantr 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( U < A <-> 0 < ( A - U ) ) )
93 90 92 mpbid 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> 0 < ( A - U ) )
94 84 93 jca 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( ( A - U ) e. RR /\ 0 < ( A - U ) ) )
95 elrp 
 |-  ( ( A - U ) e. RR+ <-> ( ( A - U ) e. RR /\ 0 < ( A - U ) ) )
96 94 95 sylibr 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( A - U ) e. RR+ )
97 83 77 96 lemuldivd 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( ( B x. ( A - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) <-> B <_ ( ( abs ` ( ( F ` U ) - ( F ` A ) ) ) / ( A - U ) ) ) )
98 82 97 mpbid 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> B <_ ( ( abs ` ( ( F ` U ) - ( F ` A ) ) ) / ( A - U ) ) )
99 18 fveq2d 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( G ` W ) = ( G ` U ) )
100 fveq2 
 |-  ( z = U -> ( F ` z ) = ( F ` U ) )
101 100 oveq1d 
 |-  ( z = U -> ( ( F ` z ) - ( F ` A ) ) = ( ( F ` U ) - ( F ` A ) ) )
102 oveq1 
 |-  ( z = U -> ( z - A ) = ( U - A ) )
103 101 102 oveq12d 
 |-  ( z = U -> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) = ( ( ( F ` U ) - ( F ` A ) ) / ( U - A ) ) )
104 ovexd 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( ( ( F ` U ) - ( F ` A ) ) / ( U - A ) ) e. _V )
105 1 103 58 104 fvmptd3 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( G ` U ) = ( ( ( F ` U ) - ( F ` A ) ) / ( U - A ) ) )
106 99 105 eqtrd 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( G ` W ) = ( ( ( F ` U ) - ( F ` A ) ) / ( U - A ) ) )
107 106 fveq2d 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( abs ` ( G ` W ) ) = ( abs ` ( ( ( F ` U ) - ( F ` A ) ) / ( U - A ) ) ) )
108 75 adantr 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( ( F ` U ) - ( F ` A ) ) e. CC )
109 38 recnd 
 |-  ( ph -> U e. CC )
110 41 recnd 
 |-  ( ph -> A e. CC )
111 109 110 subcld 
 |-  ( ph -> ( U - A ) e. CC )
112 111 adantr 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( U - A ) e. CC )
113 109 adantr 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> U e. CC )
114 110 adantr 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> A e. CC )
115 113 114 55 subne0d 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( U - A ) =/= 0 )
116 108 112 115 absdivd 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( abs ` ( ( ( F ` U ) - ( F ` A ) ) / ( U - A ) ) ) = ( ( abs ` ( ( F ` U ) - ( F ` A ) ) ) / ( abs ` ( U - A ) ) ) )
117 63 oveq2d 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( ( abs ` ( ( F ` U ) - ( F ` A ) ) ) / ( abs ` ( U - A ) ) ) = ( ( abs ` ( ( F ` U ) - ( F ` A ) ) ) / ( A - U ) ) )
118 116 117 eqtrd 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( abs ` ( ( ( F ` U ) - ( F ` A ) ) / ( U - A ) ) ) = ( ( abs ` ( ( F ` U ) - ( F ` A ) ) ) / ( A - U ) ) )
119 107 118 eqtrd 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( abs ` ( G ` W ) ) = ( ( abs ` ( ( F ` U ) - ( F ` A ) ) ) / ( A - U ) ) )
120 119 eqcomd 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( ( abs ` ( ( F ` U ) - ( F ` A ) ) ) / ( A - U ) ) = ( abs ` ( G ` W ) ) )
121 98 120 breqtrd 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> B <_ ( abs ` ( G ` W ) ) )
122 70 121 jca 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( ( abs ` ( W - A ) ) < D /\ B <_ ( abs ` ( G ` W ) ) ) )
123 59 122 jca 
 |-  ( ( ph /\ ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( W e. ( X \ { A } ) /\ ( ( abs ` ( W - A ) ) < D /\ B <_ ( abs ` ( G ` W ) ) ) ) )
124 2 a1i 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> W = if ( ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) , U , V ) )
125 simpr 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) )
126 125 iffalsed 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> if ( ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) , U , V ) = V )
127 124 126 eqtrd 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> W = V )
128 9 adantr 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> V e. X )
129 38 37 42 abssubge0d 
 |-  ( ph -> ( abs ` ( V - U ) ) = ( V - U ) )
130 129 oveq2d 
 |-  ( ph -> ( B x. ( abs ` ( V - U ) ) ) = ( B x. ( V - U ) ) )
131 130 breq1d 
 |-  ( ph -> ( ( B x. ( abs ` ( V - U ) ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) <-> ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) )
132 131 adantr 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( ( B x. ( abs ` ( V - U ) ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) <-> ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) )
133 125 132 mtbird 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> -. ( B x. ( abs ` ( V - U ) ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) )
134 4 9 ffvelcdmd 
 |-  ( ph -> ( F ` V ) e. CC )
135 39 recnd 
 |-  ( ph -> ( V - U ) e. CC )
136 48 46 gtned 
 |-  ( ph -> ( V - U ) =/= 0 )
137 134 26 subcld 
 |-  ( ph -> ( ( F ` V ) - ( F ` U ) ) e. CC )
138 137 135 136 absdivd 
 |-  ( ph -> ( abs ` ( ( ( F ` V ) - ( F ` U ) ) / ( V - U ) ) ) = ( ( abs ` ( ( F ` V ) - ( F ` U ) ) ) / ( abs ` ( V - U ) ) ) )
139 129 oveq2d 
 |-  ( ph -> ( ( abs ` ( ( F ` V ) - ( F ` U ) ) ) / ( abs ` ( V - U ) ) ) = ( ( abs ` ( ( F ` V ) - ( F ` U ) ) ) / ( V - U ) ) )
140 138 139 eqtrd 
 |-  ( ph -> ( abs ` ( ( ( F ` V ) - ( F ` U ) ) / ( V - U ) ) ) = ( ( abs ` ( ( F ` V ) - ( F ` U ) ) ) / ( V - U ) ) )
141 140 eqcomd 
 |-  ( ph -> ( ( abs ` ( ( F ` V ) - ( F ` U ) ) ) / ( V - U ) ) = ( abs ` ( ( ( F ` V ) - ( F ` U ) ) / ( V - U ) ) ) )
142 14 141 breqtrd 
 |-  ( ph -> ( 2 x. B ) <_ ( abs ` ( ( ( F ` V ) - ( F ` U ) ) / ( V - U ) ) ) )
143 134 26 74 135 6 136 142 unbdqndv2lem1 
 |-  ( ph -> ( ( B x. ( abs ` ( V - U ) ) ) <_ ( abs ` ( ( F ` V ) - ( F ` A ) ) ) \/ ( B x. ( abs ` ( V - U ) ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) )
144 143 adantr 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( ( B x. ( abs ` ( V - U ) ) ) <_ ( abs ` ( ( F ` V ) - ( F ` A ) ) ) \/ ( B x. ( abs ` ( V - U ) ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) )
145 orel2 
 |-  ( -. ( B x. ( abs ` ( V - U ) ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) -> ( ( ( B x. ( abs ` ( V - U ) ) ) <_ ( abs ` ( ( F ` V ) - ( F ` A ) ) ) \/ ( B x. ( abs ` ( V - U ) ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( B x. ( abs ` ( V - U ) ) ) <_ ( abs ` ( ( F ` V ) - ( F ` A ) ) ) ) )
146 133 144 145 sylc 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( B x. ( abs ` ( V - U ) ) ) <_ ( abs ` ( ( F ` V ) - ( F ` A ) ) ) )
147 146 adantr 
 |-  ( ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) /\ V = A ) -> ( B x. ( abs ` ( V - U ) ) ) <_ ( abs ` ( ( F ` V ) - ( F ` A ) ) ) )
148 fveq2 
 |-  ( V = A -> ( F ` V ) = ( F ` A ) )
149 148 oveq1d 
 |-  ( V = A -> ( ( F ` V ) - ( F ` A ) ) = ( ( F ` A ) - ( F ` A ) ) )
150 149 adantl 
 |-  ( ( ph /\ V = A ) -> ( ( F ` V ) - ( F ` A ) ) = ( ( F ` A ) - ( F ` A ) ) )
151 74 subidd 
 |-  ( ph -> ( ( F ` A ) - ( F ` A ) ) = 0 )
152 151 adantr 
 |-  ( ( ph /\ V = A ) -> ( ( F ` A ) - ( F ` A ) ) = 0 )
153 150 152 eqtrd 
 |-  ( ( ph /\ V = A ) -> ( ( F ` V ) - ( F ` A ) ) = 0 )
154 153 fveq2d 
 |-  ( ( ph /\ V = A ) -> ( abs ` ( ( F ` V ) - ( F ` A ) ) ) = ( abs ` 0 ) )
155 30 a1i 
 |-  ( ( ph /\ V = A ) -> ( abs ` 0 ) = 0 )
156 154 155 eqtrd 
 |-  ( ( ph /\ V = A ) -> ( abs ` ( ( F ` V ) - ( F ` A ) ) ) = 0 )
157 156 adantlr 
 |-  ( ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) /\ V = A ) -> ( abs ` ( ( F ` V ) - ( F ` A ) ) ) = 0 )
158 147 157 breqtrd 
 |-  ( ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) /\ V = A ) -> ( B x. ( abs ` ( V - U ) ) ) <_ 0 )
159 130 breq1d 
 |-  ( ph -> ( ( B x. ( abs ` ( V - U ) ) ) <_ 0 <-> ( B x. ( V - U ) ) <_ 0 ) )
160 51 159 mtbird 
 |-  ( ph -> -. ( B x. ( abs ` ( V - U ) ) ) <_ 0 )
161 160 adantr 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> -. ( B x. ( abs ` ( V - U ) ) ) <_ 0 )
162 161 adantr 
 |-  ( ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) /\ V = A ) -> -. ( B x. ( abs ` ( V - U ) ) ) <_ 0 )
163 158 162 pm2.65da 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> -. V = A )
164 163 neqned 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> V =/= A )
165 128 164 jca 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( V e. X /\ V =/= A ) )
166 eldifsn 
 |-  ( V e. ( X \ { A } ) <-> ( V e. X /\ V =/= A ) )
167 165 166 sylibr 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> V e. ( X \ { A } ) )
168 127 167 eqeltrd 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> W e. ( X \ { A } ) )
169 127 oveq1d 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( W - A ) = ( V - A ) )
170 169 fveq2d 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( abs ` ( W - A ) ) = ( abs ` ( V - A ) ) )
171 41 37 12 abssubge0d 
 |-  ( ph -> ( abs ` ( V - A ) ) = ( V - A ) )
172 171 adantr 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( abs ` ( V - A ) ) = ( V - A ) )
173 170 172 eqtrd 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( abs ` ( W - A ) ) = ( V - A ) )
174 37 41 resubcld 
 |-  ( ph -> ( V - A ) e. RR )
175 38 41 37 11 lesub2dd 
 |-  ( ph -> ( V - A ) <_ ( V - U ) )
176 174 39 66 175 13 lelttrd 
 |-  ( ph -> ( V - A ) < D )
177 176 adantr 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( V - A ) < D )
178 173 177 eqbrtrd 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( abs ` ( W - A ) ) < D )
179 171 174 eqeltrd 
 |-  ( ph -> ( abs ` ( V - A ) ) e. RR )
180 36 179 remulcld 
 |-  ( ph -> ( B x. ( abs ` ( V - A ) ) ) e. RR )
181 180 adantr 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( B x. ( abs ` ( V - A ) ) ) e. RR )
182 130 49 eqeltrd 
 |-  ( ph -> ( B x. ( abs ` ( V - U ) ) ) e. RR )
183 182 adantr 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( B x. ( abs ` ( V - U ) ) ) e. RR )
184 134 74 subcld 
 |-  ( ph -> ( ( F ` V ) - ( F ` A ) ) e. CC )
185 184 abscld 
 |-  ( ph -> ( abs ` ( ( F ` V ) - ( F ` A ) ) ) e. RR )
186 185 adantr 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( abs ` ( ( F ` V ) - ( F ` A ) ) ) e. RR )
187 129 39 eqeltrd 
 |-  ( ph -> ( abs ` ( V - U ) ) e. RR )
188 175 171 129 3brtr4d 
 |-  ( ph -> ( abs ` ( V - A ) ) <_ ( abs ` ( V - U ) ) )
189 179 187 36 78 188 lemul2ad 
 |-  ( ph -> ( B x. ( abs ` ( V - A ) ) ) <_ ( B x. ( abs ` ( V - U ) ) ) )
190 189 adantr 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( B x. ( abs ` ( V - A ) ) ) <_ ( B x. ( abs ` ( V - U ) ) ) )
191 181 183 186 190 146 letrd 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( B x. ( abs ` ( V - A ) ) ) <_ ( abs ` ( ( F ` V ) - ( F ` A ) ) ) )
192 36 adantr 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> B e. RR )
193 174 recnd 
 |-  ( ph -> ( V - A ) e. CC )
194 193 adantr 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( V - A ) e. CC )
195 37 recnd 
 |-  ( ph -> V e. CC )
196 195 adantr 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> V e. CC )
197 110 adantr 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> A e. CC )
198 196 197 164 subne0d 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( V - A ) =/= 0 )
199 194 198 absrpcld 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( abs ` ( V - A ) ) e. RR+ )
200 192 186 199 lemuldivd 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( ( B x. ( abs ` ( V - A ) ) ) <_ ( abs ` ( ( F ` V ) - ( F ` A ) ) ) <-> B <_ ( ( abs ` ( ( F ` V ) - ( F ` A ) ) ) / ( abs ` ( V - A ) ) ) ) )
201 191 200 mpbid 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> B <_ ( ( abs ` ( ( F ` V ) - ( F ` A ) ) ) / ( abs ` ( V - A ) ) ) )
202 127 fveq2d 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( G ` W ) = ( G ` V ) )
203 fveq2 
 |-  ( z = V -> ( F ` z ) = ( F ` V ) )
204 203 oveq1d 
 |-  ( z = V -> ( ( F ` z ) - ( F ` A ) ) = ( ( F ` V ) - ( F ` A ) ) )
205 oveq1 
 |-  ( z = V -> ( z - A ) = ( V - A ) )
206 204 205 oveq12d 
 |-  ( z = V -> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) = ( ( ( F ` V ) - ( F ` A ) ) / ( V - A ) ) )
207 ovexd 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( ( ( F ` V ) - ( F ` A ) ) / ( V - A ) ) e. _V )
208 1 206 167 207 fvmptd3 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( G ` V ) = ( ( ( F ` V ) - ( F ` A ) ) / ( V - A ) ) )
209 202 208 eqtrd 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( G ` W ) = ( ( ( F ` V ) - ( F ` A ) ) / ( V - A ) ) )
210 209 fveq2d 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( abs ` ( G ` W ) ) = ( abs ` ( ( ( F ` V ) - ( F ` A ) ) / ( V - A ) ) ) )
211 184 adantr 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( ( F ` V ) - ( F ` A ) ) e. CC )
212 211 194 198 absdivd 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( abs ` ( ( ( F ` V ) - ( F ` A ) ) / ( V - A ) ) ) = ( ( abs ` ( ( F ` V ) - ( F ` A ) ) ) / ( abs ` ( V - A ) ) ) )
213 210 212 eqtrd 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( abs ` ( G ` W ) ) = ( ( abs ` ( ( F ` V ) - ( F ` A ) ) ) / ( abs ` ( V - A ) ) ) )
214 213 eqcomd 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( ( abs ` ( ( F ` V ) - ( F ` A ) ) ) / ( abs ` ( V - A ) ) ) = ( abs ` ( G ` W ) ) )
215 201 214 breqtrd 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> B <_ ( abs ` ( G ` W ) ) )
216 178 215 jca 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( ( abs ` ( W - A ) ) < D /\ B <_ ( abs ` ( G ` W ) ) ) )
217 168 216 jca 
 |-  ( ( ph /\ -. ( B x. ( V - U ) ) <_ ( abs ` ( ( F ` U ) - ( F ` A ) ) ) ) -> ( W e. ( X \ { A } ) /\ ( ( abs ` ( W - A ) ) < D /\ B <_ ( abs ` ( G ` W ) ) ) ) )
218 123 217 pm2.61dan 
 |-  ( ph -> ( W e. ( X \ { A } ) /\ ( ( abs ` ( W - A ) ) < D /\ B <_ ( abs ` ( G ` W ) ) ) ) )