# Metamath Proof Explorer

## Theorem dvferm2

Description: One-sided version of dvferm . A point U which is the local maximum of its left neighborhood has derivative at least zero. (Contributed by Mario Carneiro, 24-Feb-2015) (Proof shortened by Mario Carneiro, 28-Dec-2016)

Ref Expression
Hypotheses dvferm.a ${⊢}{\phi }\to {F}:{X}⟶ℝ$
dvferm.b ${⊢}{\phi }\to {X}\subseteq ℝ$
dvferm.u ${⊢}{\phi }\to {U}\in \left({A},{B}\right)$
dvferm.s ${⊢}{\phi }\to \left({A},{B}\right)\subseteq {X}$
dvferm.d ${⊢}{\phi }\to {U}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }$
dvferm2.r ${⊢}{\phi }\to \forall {y}\in \left({A},{U}\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {F}\left({U}\right)$
Assertion dvferm2 ${⊢}{\phi }\to 0\le {{F}}_{ℝ}^{\prime }\left({U}\right)$

### Proof

Step Hyp Ref Expression
1 dvferm.a ${⊢}{\phi }\to {F}:{X}⟶ℝ$
2 dvferm.b ${⊢}{\phi }\to {X}\subseteq ℝ$
3 dvferm.u ${⊢}{\phi }\to {U}\in \left({A},{B}\right)$
4 dvferm.s ${⊢}{\phi }\to \left({A},{B}\right)\subseteq {X}$
5 dvferm.d ${⊢}{\phi }\to {U}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }$
6 dvferm2.r ${⊢}{\phi }\to \forall {y}\in \left({A},{U}\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {F}\left({U}\right)$
7 fveq2 ${⊢}{x}={z}\to {F}\left({x}\right)={F}\left({z}\right)$
8 7 oveq1d ${⊢}{x}={z}\to {F}\left({x}\right)-{F}\left({U}\right)={F}\left({z}\right)-{F}\left({U}\right)$
9 oveq1 ${⊢}{x}={z}\to {x}-{U}={z}-{U}$
10 8 9 oveq12d ${⊢}{x}={z}\to \frac{{F}\left({x}\right)-{F}\left({U}\right)}{{x}-{U}}=\frac{{F}\left({z}\right)-{F}\left({U}\right)}{{z}-{U}}$
11 eqid ${⊢}\left({x}\in \left({X}\setminus \left\{{U}\right\}\right)⟼\frac{{F}\left({x}\right)-{F}\left({U}\right)}{{x}-{U}}\right)=\left({x}\in \left({X}\setminus \left\{{U}\right\}\right)⟼\frac{{F}\left({x}\right)-{F}\left({U}\right)}{{x}-{U}}\right)$
12 ovex ${⊢}\frac{{F}\left({z}\right)-{F}\left({U}\right)}{{z}-{U}}\in \mathrm{V}$
13 10 11 12 fvmpt ${⊢}{z}\in \left({X}\setminus \left\{{U}\right\}\right)\to \left({x}\in \left({X}\setminus \left\{{U}\right\}\right)⟼\frac{{F}\left({x}\right)-{F}\left({U}\right)}{{x}-{U}}\right)\left({z}\right)=\frac{{F}\left({z}\right)-{F}\left({U}\right)}{{z}-{U}}$
14 13 fvoveq1d ${⊢}{z}\in \left({X}\setminus \left\{{U}\right\}\right)\to \left|\left({x}\in \left({X}\setminus \left\{{U}\right\}\right)⟼\frac{{F}\left({x}\right)-{F}\left({U}\right)}{{x}-{U}}\right)\left({z}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|=\left|\left(\frac{{F}\left({z}\right)-{F}\left({U}\right)}{{z}-{U}}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|$
15 id ${⊢}{y}=-{{F}}_{ℝ}^{\prime }\left({U}\right)\to {y}=-{{F}}_{ℝ}^{\prime }\left({U}\right)$
16 14 15 breqan12rd ${⊢}\left({y}=-{{F}}_{ℝ}^{\prime }\left({U}\right)\wedge {z}\in \left({X}\setminus \left\{{U}\right\}\right)\right)\to \left(\left|\left({x}\in \left({X}\setminus \left\{{U}\right\}\right)⟼\frac{{F}\left({x}\right)-{F}\left({U}\right)}{{x}-{U}}\right)\left({z}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<{y}↔\left|\left(\frac{{F}\left({z}\right)-{F}\left({U}\right)}{{z}-{U}}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<-{{F}}_{ℝ}^{\prime }\left({U}\right)\right)$
17 16 imbi2d ${⊢}\left({y}=-{{F}}_{ℝ}^{\prime }\left({U}\right)\wedge {z}\in \left({X}\setminus \left\{{U}\right\}\right)\right)\to \left(\left(\left({z}\ne {U}\wedge \left|{z}-{U}\right|<{u}\right)\to \left|\left({x}\in \left({X}\setminus \left\{{U}\right\}\right)⟼\frac{{F}\left({x}\right)-{F}\left({U}\right)}{{x}-{U}}\right)\left({z}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<{y}\right)↔\left(\left({z}\ne {U}\wedge \left|{z}-{U}\right|<{u}\right)\to \left|\left(\frac{{F}\left({z}\right)-{F}\left({U}\right)}{{z}-{U}}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<-{{F}}_{ℝ}^{\prime }\left({U}\right)\right)\right)$
18 17 ralbidva ${⊢}{y}=-{{F}}_{ℝ}^{\prime }\left({U}\right)\to \left(\forall {z}\in \left({X}\setminus \left\{{U}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {U}\wedge \left|{z}-{U}\right|<{u}\right)\to \left|\left({x}\in \left({X}\setminus \left\{{U}\right\}\right)⟼\frac{{F}\left({x}\right)-{F}\left({U}\right)}{{x}-{U}}\right)\left({z}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<{y}\right)↔\forall {z}\in \left({X}\setminus \left\{{U}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {U}\wedge \left|{z}-{U}\right|<{u}\right)\to \left|\left(\frac{{F}\left({z}\right)-{F}\left({U}\right)}{{z}-{U}}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<-{{F}}_{ℝ}^{\prime }\left({U}\right)\right)\right)$
19 18 rexbidv ${⊢}{y}=-{{F}}_{ℝ}^{\prime }\left({U}\right)\to \left(\exists {u}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in \left({X}\setminus \left\{{U}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {U}\wedge \left|{z}-{U}\right|<{u}\right)\to \left|\left({x}\in \left({X}\setminus \left\{{U}\right\}\right)⟼\frac{{F}\left({x}\right)-{F}\left({U}\right)}{{x}-{U}}\right)\left({z}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<{y}\right)↔\exists {u}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in \left({X}\setminus \left\{{U}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {U}\wedge \left|{z}-{U}\right|<{u}\right)\to \left|\left(\frac{{F}\left({z}\right)-{F}\left({U}\right)}{{z}-{U}}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<-{{F}}_{ℝ}^{\prime }\left({U}\right)\right)\right)$
20 dvf ${⊢}{{F}}_{ℝ}^{\prime }:\mathrm{dom}{{F}}_{ℝ}^{\prime }⟶ℂ$
21 ffun ${⊢}{{F}}_{ℝ}^{\prime }:\mathrm{dom}{{F}}_{ℝ}^{\prime }⟶ℂ\to \mathrm{Fun}{{F}}_{ℝ}^{\prime }$
22 funfvbrb ${⊢}\mathrm{Fun}{{F}}_{ℝ}^{\prime }\to \left({U}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }↔{U}{{F}}_{ℝ}^{\prime }{{F}}_{ℝ}^{\prime }\left({U}\right)\right)$
23 20 21 22 mp2b ${⊢}{U}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }↔{U}{{F}}_{ℝ}^{\prime }{{F}}_{ℝ}^{\prime }\left({U}\right)$
24 5 23 sylib ${⊢}{\phi }\to {U}{{F}}_{ℝ}^{\prime }{{F}}_{ℝ}^{\prime }\left({U}\right)$
25 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ$
26 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
27 ax-resscn ${⊢}ℝ\subseteq ℂ$
28 27 a1i ${⊢}{\phi }\to ℝ\subseteq ℂ$
29 fss ${⊢}\left({F}:{X}⟶ℝ\wedge ℝ\subseteq ℂ\right)\to {F}:{X}⟶ℂ$
30 1 27 29 sylancl ${⊢}{\phi }\to {F}:{X}⟶ℂ$
31 25 26 11 28 30 2 eldv ${⊢}{\phi }\to \left({U}{{F}}_{ℝ}^{\prime }{{F}}_{ℝ}^{\prime }\left({U}\right)↔\left({U}\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)\left({X}\right)\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)\in \left(\left({x}\in \left({X}\setminus \left\{{U}\right\}\right)⟼\frac{{F}\left({x}\right)-{F}\left({U}\right)}{{x}-{U}}\right){lim}_{ℂ}{U}\right)\right)\right)$
32 24 31 mpbid ${⊢}{\phi }\to \left({U}\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)\left({X}\right)\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)\in \left(\left({x}\in \left({X}\setminus \left\{{U}\right\}\right)⟼\frac{{F}\left({x}\right)-{F}\left({U}\right)}{{x}-{U}}\right){lim}_{ℂ}{U}\right)\right)$
33 32 simprd ${⊢}{\phi }\to {{F}}_{ℝ}^{\prime }\left({U}\right)\in \left(\left({x}\in \left({X}\setminus \left\{{U}\right\}\right)⟼\frac{{F}\left({x}\right)-{F}\left({U}\right)}{{x}-{U}}\right){lim}_{ℂ}{U}\right)$
34 33 adantr ${⊢}\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\to {{F}}_{ℝ}^{\prime }\left({U}\right)\in \left(\left({x}\in \left({X}\setminus \left\{{U}\right\}\right)⟼\frac{{F}\left({x}\right)-{F}\left({U}\right)}{{x}-{U}}\right){lim}_{ℂ}{U}\right)$
35 2 27 sstrdi ${⊢}{\phi }\to {X}\subseteq ℂ$
36 4 3 sseldd ${⊢}{\phi }\to {U}\in {X}$
37 30 35 36 dvlem ${⊢}\left({\phi }\wedge {x}\in \left({X}\setminus \left\{{U}\right\}\right)\right)\to \frac{{F}\left({x}\right)-{F}\left({U}\right)}{{x}-{U}}\in ℂ$
38 37 fmpttd ${⊢}{\phi }\to \left({x}\in \left({X}\setminus \left\{{U}\right\}\right)⟼\frac{{F}\left({x}\right)-{F}\left({U}\right)}{{x}-{U}}\right):{X}\setminus \left\{{U}\right\}⟶ℂ$
39 38 adantr ${⊢}\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\to \left({x}\in \left({X}\setminus \left\{{U}\right\}\right)⟼\frac{{F}\left({x}\right)-{F}\left({U}\right)}{{x}-{U}}\right):{X}\setminus \left\{{U}\right\}⟶ℂ$
40 35 adantr ${⊢}\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\to {X}\subseteq ℂ$
41 40 ssdifssd ${⊢}\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\to {X}\setminus \left\{{U}\right\}\subseteq ℂ$
42 35 36 sseldd ${⊢}{\phi }\to {U}\in ℂ$
43 42 adantr ${⊢}\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\to {U}\in ℂ$
44 39 41 43 ellimc3 ${⊢}\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\to \left({{F}}_{ℝ}^{\prime }\left({U}\right)\in \left(\left({x}\in \left({X}\setminus \left\{{U}\right\}\right)⟼\frac{{F}\left({x}\right)-{F}\left({U}\right)}{{x}-{U}}\right){lim}_{ℂ}{U}\right)↔\left({{F}}_{ℝ}^{\prime }\left({U}\right)\in ℂ\wedge \forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {u}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in \left({X}\setminus \left\{{U}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {U}\wedge \left|{z}-{U}\right|<{u}\right)\to \left|\left({x}\in \left({X}\setminus \left\{{U}\right\}\right)⟼\frac{{F}\left({x}\right)-{F}\left({U}\right)}{{x}-{U}}\right)\left({z}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<{y}\right)\right)\right)$
45 34 44 mpbid ${⊢}\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\to \left({{F}}_{ℝ}^{\prime }\left({U}\right)\in ℂ\wedge \forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {u}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in \left({X}\setminus \left\{{U}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {U}\wedge \left|{z}-{U}\right|<{u}\right)\to \left|\left({x}\in \left({X}\setminus \left\{{U}\right\}\right)⟼\frac{{F}\left({x}\right)-{F}\left({U}\right)}{{x}-{U}}\right)\left({z}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<{y}\right)\right)$
46 45 simprd ${⊢}\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\to \forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {u}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in \left({X}\setminus \left\{{U}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {U}\wedge \left|{z}-{U}\right|<{u}\right)\to \left|\left({x}\in \left({X}\setminus \left\{{U}\right\}\right)⟼\frac{{F}\left({x}\right)-{F}\left({U}\right)}{{x}-{U}}\right)\left({z}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<{y}\right)$
47 dvfre ${⊢}\left({F}:{X}⟶ℝ\wedge {X}\subseteq ℝ\right)\to {{F}}_{ℝ}^{\prime }:\mathrm{dom}{{F}}_{ℝ}^{\prime }⟶ℝ$
48 1 2 47 syl2anc ${⊢}{\phi }\to {{F}}_{ℝ}^{\prime }:\mathrm{dom}{{F}}_{ℝ}^{\prime }⟶ℝ$
49 48 5 ffvelrnd ${⊢}{\phi }\to {{F}}_{ℝ}^{\prime }\left({U}\right)\in ℝ$
50 49 adantr ${⊢}\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\to {{F}}_{ℝ}^{\prime }\left({U}\right)\in ℝ$
51 50 renegcld ${⊢}\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\to -{{F}}_{ℝ}^{\prime }\left({U}\right)\in ℝ$
52 49 lt0neg1d ${⊢}{\phi }\to \left({{F}}_{ℝ}^{\prime }\left({U}\right)<0↔0<-{{F}}_{ℝ}^{\prime }\left({U}\right)\right)$
53 52 biimpa ${⊢}\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\to 0<-{{F}}_{ℝ}^{\prime }\left({U}\right)$
54 51 53 elrpd ${⊢}\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\to -{{F}}_{ℝ}^{\prime }\left({U}\right)\in {ℝ}^{+}$
55 19 46 54 rspcdva ${⊢}\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\to \exists {u}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in \left({X}\setminus \left\{{U}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {U}\wedge \left|{z}-{U}\right|<{u}\right)\to \left|\left(\frac{{F}\left({z}\right)-{F}\left({U}\right)}{{z}-{U}}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<-{{F}}_{ℝ}^{\prime }\left({U}\right)\right)$
56 1 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\wedge {u}\in {ℝ}^{+}\right)\wedge \forall {z}\in \left({X}\setminus \left\{{U}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {U}\wedge \left|{z}-{U}\right|<{u}\right)\to \left|\left(\frac{{F}\left({z}\right)-{F}\left({U}\right)}{{z}-{U}}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<-{{F}}_{ℝ}^{\prime }\left({U}\right)\right)\right)\to {F}:{X}⟶ℝ$
57 2 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\wedge {u}\in {ℝ}^{+}\right)\wedge \forall {z}\in \left({X}\setminus \left\{{U}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {U}\wedge \left|{z}-{U}\right|<{u}\right)\to \left|\left(\frac{{F}\left({z}\right)-{F}\left({U}\right)}{{z}-{U}}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<-{{F}}_{ℝ}^{\prime }\left({U}\right)\right)\right)\to {X}\subseteq ℝ$
58 3 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\wedge {u}\in {ℝ}^{+}\right)\wedge \forall {z}\in \left({X}\setminus \left\{{U}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {U}\wedge \left|{z}-{U}\right|<{u}\right)\to \left|\left(\frac{{F}\left({z}\right)-{F}\left({U}\right)}{{z}-{U}}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<-{{F}}_{ℝ}^{\prime }\left({U}\right)\right)\right)\to {U}\in \left({A},{B}\right)$
59 4 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\wedge {u}\in {ℝ}^{+}\right)\wedge \forall {z}\in \left({X}\setminus \left\{{U}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {U}\wedge \left|{z}-{U}\right|<{u}\right)\to \left|\left(\frac{{F}\left({z}\right)-{F}\left({U}\right)}{{z}-{U}}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<-{{F}}_{ℝ}^{\prime }\left({U}\right)\right)\right)\to \left({A},{B}\right)\subseteq {X}$
60 5 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\wedge {u}\in {ℝ}^{+}\right)\wedge \forall {z}\in \left({X}\setminus \left\{{U}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {U}\wedge \left|{z}-{U}\right|<{u}\right)\to \left|\left(\frac{{F}\left({z}\right)-{F}\left({U}\right)}{{z}-{U}}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<-{{F}}_{ℝ}^{\prime }\left({U}\right)\right)\right)\to {U}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }$
61 6 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\wedge {u}\in {ℝ}^{+}\right)\wedge \forall {z}\in \left({X}\setminus \left\{{U}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {U}\wedge \left|{z}-{U}\right|<{u}\right)\to \left|\left(\frac{{F}\left({z}\right)-{F}\left({U}\right)}{{z}-{U}}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<-{{F}}_{ℝ}^{\prime }\left({U}\right)\right)\right)\to \forall {y}\in \left({A},{U}\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {F}\left({U}\right)$
62 simpllr ${⊢}\left(\left(\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\wedge {u}\in {ℝ}^{+}\right)\wedge \forall {z}\in \left({X}\setminus \left\{{U}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {U}\wedge \left|{z}-{U}\right|<{u}\right)\to \left|\left(\frac{{F}\left({z}\right)-{F}\left({U}\right)}{{z}-{U}}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<-{{F}}_{ℝ}^{\prime }\left({U}\right)\right)\right)\to {{F}}_{ℝ}^{\prime }\left({U}\right)<0$
63 simplr ${⊢}\left(\left(\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\wedge {u}\in {ℝ}^{+}\right)\wedge \forall {z}\in \left({X}\setminus \left\{{U}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {U}\wedge \left|{z}-{U}\right|<{u}\right)\to \left|\left(\frac{{F}\left({z}\right)-{F}\left({U}\right)}{{z}-{U}}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<-{{F}}_{ℝ}^{\prime }\left({U}\right)\right)\right)\to {u}\in {ℝ}^{+}$
64 simpr ${⊢}\left(\left(\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\wedge {u}\in {ℝ}^{+}\right)\wedge \forall {z}\in \left({X}\setminus \left\{{U}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {U}\wedge \left|{z}-{U}\right|<{u}\right)\to \left|\left(\frac{{F}\left({z}\right)-{F}\left({U}\right)}{{z}-{U}}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<-{{F}}_{ℝ}^{\prime }\left({U}\right)\right)\right)\to \forall {z}\in \left({X}\setminus \left\{{U}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {U}\wedge \left|{z}-{U}\right|<{u}\right)\to \left|\left(\frac{{F}\left({z}\right)-{F}\left({U}\right)}{{z}-{U}}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<-{{F}}_{ℝ}^{\prime }\left({U}\right)\right)$
65 eqid ${⊢}\frac{if\left({A}\le {U}-{u},{U}-{u},{A}\right)+{U}}{2}=\frac{if\left({A}\le {U}-{u},{U}-{u},{A}\right)+{U}}{2}$
66 56 57 58 59 60 61 62 63 64 65 dvferm2lem ${⊢}¬\left(\left(\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\wedge {u}\in {ℝ}^{+}\right)\wedge \forall {z}\in \left({X}\setminus \left\{{U}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {U}\wedge \left|{z}-{U}\right|<{u}\right)\to \left|\left(\frac{{F}\left({z}\right)-{F}\left({U}\right)}{{z}-{U}}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<-{{F}}_{ℝ}^{\prime }\left({U}\right)\right)\right)$
67 66 imnani ${⊢}\left(\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\wedge {u}\in {ℝ}^{+}\right)\to ¬\forall {z}\in \left({X}\setminus \left\{{U}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {U}\wedge \left|{z}-{U}\right|<{u}\right)\to \left|\left(\frac{{F}\left({z}\right)-{F}\left({U}\right)}{{z}-{U}}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<-{{F}}_{ℝ}^{\prime }\left({U}\right)\right)$
68 67 nrexdv ${⊢}\left({\phi }\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)\to ¬\exists {u}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in \left({X}\setminus \left\{{U}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {U}\wedge \left|{z}-{U}\right|<{u}\right)\to \left|\left(\frac{{F}\left({z}\right)-{F}\left({U}\right)}{{z}-{U}}\right)-{{F}}_{ℝ}^{\prime }\left({U}\right)\right|<-{{F}}_{ℝ}^{\prime }\left({U}\right)\right)$
69 55 68 pm2.65da ${⊢}{\phi }\to ¬{{F}}_{ℝ}^{\prime }\left({U}\right)<0$
70 0re ${⊢}0\in ℝ$
71 lenlt ${⊢}\left(0\in ℝ\wedge {{F}}_{ℝ}^{\prime }\left({U}\right)\in ℝ\right)\to \left(0\le {{F}}_{ℝ}^{\prime }\left({U}\right)↔¬{{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)$
72 70 49 71 sylancr ${⊢}{\phi }\to \left(0\le {{F}}_{ℝ}^{\prime }\left({U}\right)↔¬{{F}}_{ℝ}^{\prime }\left({U}\right)<0\right)$
73 69 72 mpbird ${⊢}{\phi }\to 0\le {{F}}_{ℝ}^{\prime }\left({U}\right)$