Theorem unbdqndv2lem2

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

	Ref	Expression
Hypotheses	unbdqndv2lem2.g	$$⊢G=\left(z\in \left(X\setminus \left\{A\right\}\right)⟼\frac{F\left(z\right)-F\left(A\right)}{z-A}\right)$$
	unbdqndv2lem2.w	$$⊢W=if\left(B\left(V-U\right)\le \left|F\left(U\right)-F\left(A\right)\right|,U,V\right)$$
	unbdqndv2lem2.x	$$⊢\phi \to X\subseteq ℝ$$
	unbdqndv2lem2.f	$$⊢\phi \to F:X⟶ℂ$$
	unbdqndv2lem2.a	$$⊢\phi \to A\in X$$
	unbdqndv2lem2.b	$$⊢\phi \to B\in {ℝ}^{+}$$
	unbdqndv2lem2.d	$$⊢\phi \to D\in {ℝ}^{+}$$
	unbdqndv2lem2.u	$$⊢\phi \to U\in X$$
	unbdqndv2lem2.v	$$⊢\phi \to V\in X$$
	unbdqndv2lem2.1	$$⊢\phi \to U\ne V$$
	unbdqndv2lem2.2	$$⊢\phi \to U\le A$$
	unbdqndv2lem2.3	$$⊢\phi \to A\le V$$
	unbdqndv2lem2.4	$$⊢\phi \to V-U<D$$
	unbdqndv2lem2.5	$$⊢\phi \to 2B\le \frac{\left|F\left(V\right)-F\left(U\right)\right|}{V-U}$$
Assertion	unbdqndv2lem2	$$⊢\phi \to \left(W\in \left(X\setminus \left\{A\right\}\right)\wedge \left(\left|W-A\right|<D\wedge B\le \left|G\left(W\right)\right|\right)\right)$$

Proof

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