# Metamath Proof Explorer

## Theorem unbdqndv2

Description: Variant of unbdqndv1 with the hypothesis that ( ( ( Fy ) - ( Fx ) ) / ( y - x ) ) is unbounded where x <_ A and A <_ y . (Contributed by Asger C. Ipsen, 12-May-2021)

Ref Expression
Hypotheses unbdqndv2.x ${⊢}{\phi }\to {X}\subseteq ℝ$
unbdqndv2.f ${⊢}{\phi }\to {F}:{X}⟶ℂ$
unbdqndv2.1 ${⊢}{\phi }\to \forall {b}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge {b}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)$
Assertion unbdqndv2 ${⊢}{\phi }\to ¬{A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }$

### Proof

Step Hyp Ref Expression
1 unbdqndv2.x ${⊢}{\phi }\to {X}\subseteq ℝ$
2 unbdqndv2.f ${⊢}{\phi }\to {F}:{X}⟶ℂ$
3 unbdqndv2.1 ${⊢}{\phi }\to \forall {b}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge {b}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)$
4 eqid ${⊢}\left({z}\in \left({X}\setminus \left\{{A}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({A}\right)}{{z}-{A}}\right)=\left({z}\in \left({X}\setminus \left\{{A}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({A}\right)}{{z}-{A}}\right)$
5 ax-resscn ${⊢}ℝ\subseteq ℂ$
6 5 a1i ${⊢}\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\to ℝ\subseteq ℂ$
7 1 adantr ${⊢}\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\to {X}\subseteq ℝ$
8 2 adantr ${⊢}\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\to {F}:{X}⟶ℂ$
9 breq1 ${⊢}{b}=2{c}\to \left({b}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}↔2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)$
10 9 3anbi3d ${⊢}{b}=2{c}\to \left(\left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge {b}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)↔\left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\right)$
11 10 rexbidv ${⊢}{b}=2{c}\to \left(\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge {b}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)↔\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\right)$
12 11 rexbidv ${⊢}{b}=2{c}\to \left(\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge {b}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)↔\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\right)$
13 12 ralbidv ${⊢}{b}=2{c}\to \left(\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge {b}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)↔\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\right)$
14 3 ad2antrr ${⊢}\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\to \forall {b}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge {b}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)$
15 2rp ${⊢}2\in {ℝ}^{+}$
16 15 a1i ${⊢}\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\to 2\in {ℝ}^{+}$
17 simprl ${⊢}\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\to {c}\in {ℝ}^{+}$
18 16 17 rpmulcld ${⊢}\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\to 2{c}\in {ℝ}^{+}$
19 13 14 18 rspcdva ${⊢}\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\to \forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)$
20 simprr ${⊢}\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\to {d}\in {ℝ}^{+}$
21 rsp ${⊢}\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\to \left({d}\in {ℝ}^{+}\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\right)$
22 19 20 21 sylc ${⊢}\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)$
23 eqid ${⊢}if\left({c}\left({y}-{x}\right)\le \left|{F}\left({x}\right)-{F}\left({A}\right)\right|,{x},{y}\right)=if\left({c}\left({y}-{x}\right)\le \left|{F}\left({x}\right)-{F}\left({A}\right)\right|,{x},{y}\right)$
24 7 ad3antrrr ${⊢}\left(\left(\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\right)\to {X}\subseteq ℝ$
25 8 ad3antrrr ${⊢}\left(\left(\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\right)\to {F}:{X}⟶ℂ$
26 6 8 7 dvbss ${⊢}\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\to \mathrm{dom}{{F}}_{ℝ}^{\prime }\subseteq {X}$
27 simpr ${⊢}\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\to {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }$
28 26 27 sseldd ${⊢}\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\to {A}\in {X}$
29 28 adantr ${⊢}\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\to {A}\in {X}$
30 29 adantr ${⊢}\left(\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {A}\in {X}$
31 30 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\right)\to {A}\in {X}$
32 17 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\right)\to {c}\in {ℝ}^{+}$
33 20 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\right)\to {d}\in {ℝ}^{+}$
34 simplrl ${⊢}\left(\left(\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\right)\to {x}\in {X}$
35 simplrr ${⊢}\left(\left(\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\right)\to {y}\in {X}$
36 simpr2r ${⊢}\left(\left(\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\right)\to {x}\ne {y}$
37 simpr1l ${⊢}\left(\left(\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\right)\to {x}\le {A}$
38 simpr1r ${⊢}\left(\left(\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\right)\to {A}\le {y}$
39 simpr2l ${⊢}\left(\left(\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\right)\to {y}-{x}<{d}$
40 simpr3 ${⊢}\left(\left(\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\right)\to 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}$
41 4 23 24 25 31 32 33 34 35 36 37 38 39 40 unbdqndv2lem2 ${⊢}\left(\left(\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\right)\to \left(if\left({c}\left({y}-{x}\right)\le \left|{F}\left({x}\right)-{F}\left({A}\right)\right|,{x},{y}\right)\in \left({X}\setminus \left\{{A}\right\}\right)\wedge \left(\left|if\left({c}\left({y}-{x}\right)\le \left|{F}\left({x}\right)-{F}\left({A}\right)\right|,{x},{y}\right)-{A}\right|<{d}\wedge {c}\le \left|\left({z}\in \left({X}\setminus \left\{{A}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({A}\right)}{{z}-{A}}\right)\left(if\left({c}\left({y}-{x}\right)\le \left|{F}\left({x}\right)-{F}\left({A}\right)\right|,{x},{y}\right)\right)\right|\right)\right)$
42 41 simpld ${⊢}\left(\left(\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\right)\to if\left({c}\left({y}-{x}\right)\le \left|{F}\left({x}\right)-{F}\left({A}\right)\right|,{x},{y}\right)\in \left({X}\setminus \left\{{A}\right\}\right)$
43 fvoveq1 ${⊢}{w}=if\left({c}\left({y}-{x}\right)\le \left|{F}\left({x}\right)-{F}\left({A}\right)\right|,{x},{y}\right)\to \left|{w}-{A}\right|=\left|if\left({c}\left({y}-{x}\right)\le \left|{F}\left({x}\right)-{F}\left({A}\right)\right|,{x},{y}\right)-{A}\right|$
44 43 breq1d ${⊢}{w}=if\left({c}\left({y}-{x}\right)\le \left|{F}\left({x}\right)-{F}\left({A}\right)\right|,{x},{y}\right)\to \left(\left|{w}-{A}\right|<{d}↔\left|if\left({c}\left({y}-{x}\right)\le \left|{F}\left({x}\right)-{F}\left({A}\right)\right|,{x},{y}\right)-{A}\right|<{d}\right)$
45 2fveq3 ${⊢}{w}=if\left({c}\left({y}-{x}\right)\le \left|{F}\left({x}\right)-{F}\left({A}\right)\right|,{x},{y}\right)\to \left|\left({z}\in \left({X}\setminus \left\{{A}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({A}\right)}{{z}-{A}}\right)\left({w}\right)\right|=\left|\left({z}\in \left({X}\setminus \left\{{A}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({A}\right)}{{z}-{A}}\right)\left(if\left({c}\left({y}-{x}\right)\le \left|{F}\left({x}\right)-{F}\left({A}\right)\right|,{x},{y}\right)\right)\right|$
46 45 breq2d ${⊢}{w}=if\left({c}\left({y}-{x}\right)\le \left|{F}\left({x}\right)-{F}\left({A}\right)\right|,{x},{y}\right)\to \left({c}\le \left|\left({z}\in \left({X}\setminus \left\{{A}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({A}\right)}{{z}-{A}}\right)\left({w}\right)\right|↔{c}\le \left|\left({z}\in \left({X}\setminus \left\{{A}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({A}\right)}{{z}-{A}}\right)\left(if\left({c}\left({y}-{x}\right)\le \left|{F}\left({x}\right)-{F}\left({A}\right)\right|,{x},{y}\right)\right)\right|\right)$
47 44 46 anbi12d ${⊢}{w}=if\left({c}\left({y}-{x}\right)\le \left|{F}\left({x}\right)-{F}\left({A}\right)\right|,{x},{y}\right)\to \left(\left(\left|{w}-{A}\right|<{d}\wedge {c}\le \left|\left({z}\in \left({X}\setminus \left\{{A}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({A}\right)}{{z}-{A}}\right)\left({w}\right)\right|\right)↔\left(\left|if\left({c}\left({y}-{x}\right)\le \left|{F}\left({x}\right)-{F}\left({A}\right)\right|,{x},{y}\right)-{A}\right|<{d}\wedge {c}\le \left|\left({z}\in \left({X}\setminus \left\{{A}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({A}\right)}{{z}-{A}}\right)\left(if\left({c}\left({y}-{x}\right)\le \left|{F}\left({x}\right)-{F}\left({A}\right)\right|,{x},{y}\right)\right)\right|\right)\right)$
48 47 adantl ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\right)\wedge {w}=if\left({c}\left({y}-{x}\right)\le \left|{F}\left({x}\right)-{F}\left({A}\right)\right|,{x},{y}\right)\right)\to \left(\left(\left|{w}-{A}\right|<{d}\wedge {c}\le \left|\left({z}\in \left({X}\setminus \left\{{A}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({A}\right)}{{z}-{A}}\right)\left({w}\right)\right|\right)↔\left(\left|if\left({c}\left({y}-{x}\right)\le \left|{F}\left({x}\right)-{F}\left({A}\right)\right|,{x},{y}\right)-{A}\right|<{d}\wedge {c}\le \left|\left({z}\in \left({X}\setminus \left\{{A}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({A}\right)}{{z}-{A}}\right)\left(if\left({c}\left({y}-{x}\right)\le \left|{F}\left({x}\right)-{F}\left({A}\right)\right|,{x},{y}\right)\right)\right|\right)\right)$
49 41 simprd ${⊢}\left(\left(\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\right)\to \left(\left|if\left({c}\left({y}-{x}\right)\le \left|{F}\left({x}\right)-{F}\left({A}\right)\right|,{x},{y}\right)-{A}\right|<{d}\wedge {c}\le \left|\left({z}\in \left({X}\setminus \left\{{A}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({A}\right)}{{z}-{A}}\right)\left(if\left({c}\left({y}-{x}\right)\le \left|{F}\left({x}\right)-{F}\left({A}\right)\right|,{x},{y}\right)\right)\right|\right)$
50 42 48 49 rspcedvd ${⊢}\left(\left(\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\wedge \left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\right)\to \exists {w}\in \left({X}\setminus \left\{{A}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left|{w}-{A}\right|<{d}\wedge {c}\le \left|\left({z}\in \left({X}\setminus \left\{{A}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({A}\right)}{{z}-{A}}\right)\left({w}\right)\right|\right)$
51 50 ex ${⊢}\left(\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to \left(\left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\to \exists {w}\in \left({X}\setminus \left\{{A}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left|{w}-{A}\right|<{d}\wedge {c}\le \left|\left({z}\in \left({X}\setminus \left\{{A}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({A}\right)}{{z}-{A}}\right)\left({w}\right)\right|\right)\right)$
52 51 rexlimdvva ${⊢}\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\to \left(\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}\le {A}\wedge {A}\le {y}\right)\wedge \left({y}-{x}<{d}\wedge {x}\ne {y}\right)\wedge 2{c}\le \frac{\left|{F}\left({y}\right)-{F}\left({x}\right)\right|}{{y}-{x}}\right)\to \exists {w}\in \left({X}\setminus \left\{{A}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left|{w}-{A}\right|<{d}\wedge {c}\le \left|\left({z}\in \left({X}\setminus \left\{{A}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({A}\right)}{{z}-{A}}\right)\left({w}\right)\right|\right)\right)$
53 22 52 mpd ${⊢}\left(\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\wedge \left({c}\in {ℝ}^{+}\wedge {d}\in {ℝ}^{+}\right)\right)\to \exists {w}\in \left({X}\setminus \left\{{A}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left|{w}-{A}\right|<{d}\wedge {c}\le \left|\left({z}\in \left({X}\setminus \left\{{A}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({A}\right)}{{z}-{A}}\right)\left({w}\right)\right|\right)$
54 53 ralrimivva ${⊢}\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\to \forall {c}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {w}\in \left({X}\setminus \left\{{A}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left|{w}-{A}\right|<{d}\wedge {c}\le \left|\left({z}\in \left({X}\setminus \left\{{A}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({A}\right)}{{z}-{A}}\right)\left({w}\right)\right|\right)$
55 4 6 7 8 54 unbdqndv1 ${⊢}\left({\phi }\wedge {A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\to ¬{A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }$
56 55 pm2.01da ${⊢}{\phi }\to ¬{A}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }$