# Metamath Proof Explorer

## Theorem dvferm

Description: Fermat's theorem on stationary points. A point U which is a local maximum has derivative equal to zero. (Contributed by Mario Carneiro, 1-Sep-2014)

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 }$
dvferm.r ${⊢}{\phi }\to \forall {y}\in \left({A},{B}\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {F}\left({U}\right)$
Assertion dvferm ${⊢}{\phi }\to {{F}}_{ℝ}^{\prime }\left({U}\right)=0$

### 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 dvferm.r ${⊢}{\phi }\to \forall {y}\in \left({A},{B}\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {F}\left({U}\right)$
7 ne0i ${⊢}{U}\in \left({A},{B}\right)\to \left({A},{B}\right)\ne \varnothing$
8 ndmioo ${⊢}¬\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({A},{B}\right)=\varnothing$
9 8 necon1ai ${⊢}\left({A},{B}\right)\ne \varnothing \to \left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)$
10 3 7 9 3syl ${⊢}{\phi }\to \left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)$
11 10 simpld ${⊢}{\phi }\to {A}\in {ℝ}^{*}$
12 ioossre ${⊢}\left({A},{B}\right)\subseteq ℝ$
13 12 3 sseldi ${⊢}{\phi }\to {U}\in ℝ$
14 13 rexrd ${⊢}{\phi }\to {U}\in {ℝ}^{*}$
15 eliooord ${⊢}{U}\in \left({A},{B}\right)\to \left({A}<{U}\wedge {U}<{B}\right)$
16 3 15 syl ${⊢}{\phi }\to \left({A}<{U}\wedge {U}<{B}\right)$
17 16 simpld ${⊢}{\phi }\to {A}<{U}$
18 11 14 17 xrltled ${⊢}{\phi }\to {A}\le {U}$
19 iooss1 ${⊢}\left({A}\in {ℝ}^{*}\wedge {A}\le {U}\right)\to \left({U},{B}\right)\subseteq \left({A},{B}\right)$
20 11 18 19 syl2anc ${⊢}{\phi }\to \left({U},{B}\right)\subseteq \left({A},{B}\right)$
21 ssralv ${⊢}\left({U},{B}\right)\subseteq \left({A},{B}\right)\to \left(\forall {y}\in \left({A},{B}\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {F}\left({U}\right)\to \forall {y}\in \left({U},{B}\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {F}\left({U}\right)\right)$
22 20 6 21 sylc ${⊢}{\phi }\to \forall {y}\in \left({U},{B}\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {F}\left({U}\right)$
23 1 2 3 4 5 22 dvferm1 ${⊢}{\phi }\to {{F}}_{ℝ}^{\prime }\left({U}\right)\le 0$
24 10 simprd ${⊢}{\phi }\to {B}\in {ℝ}^{*}$
25 16 simprd ${⊢}{\phi }\to {U}<{B}$
26 14 24 25 xrltled ${⊢}{\phi }\to {U}\le {B}$
27 iooss2 ${⊢}\left({B}\in {ℝ}^{*}\wedge {U}\le {B}\right)\to \left({A},{U}\right)\subseteq \left({A},{B}\right)$
28 24 26 27 syl2anc ${⊢}{\phi }\to \left({A},{U}\right)\subseteq \left({A},{B}\right)$
29 ssralv ${⊢}\left({A},{U}\right)\subseteq \left({A},{B}\right)\to \left(\forall {y}\in \left({A},{B}\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {F}\left({U}\right)\to \forall {y}\in \left({A},{U}\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {F}\left({U}\right)\right)$
30 28 6 29 sylc ${⊢}{\phi }\to \forall {y}\in \left({A},{U}\right)\phantom{\rule{.4em}{0ex}}{F}\left({y}\right)\le {F}\left({U}\right)$
31 1 2 3 4 5 30 dvferm2 ${⊢}{\phi }\to 0\le {{F}}_{ℝ}^{\prime }\left({U}\right)$
32 dvfre ${⊢}\left({F}:{X}⟶ℝ\wedge {X}\subseteq ℝ\right)\to {{F}}_{ℝ}^{\prime }:\mathrm{dom}{{F}}_{ℝ}^{\prime }⟶ℝ$
33 1 2 32 syl2anc ${⊢}{\phi }\to {{F}}_{ℝ}^{\prime }:\mathrm{dom}{{F}}_{ℝ}^{\prime }⟶ℝ$
34 33 5 ffvelrnd ${⊢}{\phi }\to {{F}}_{ℝ}^{\prime }\left({U}\right)\in ℝ$
35 0re ${⊢}0\in ℝ$
36 letri3 ${⊢}\left({{F}}_{ℝ}^{\prime }\left({U}\right)\in ℝ\wedge 0\in ℝ\right)\to \left({{F}}_{ℝ}^{\prime }\left({U}\right)=0↔\left({{F}}_{ℝ}^{\prime }\left({U}\right)\le 0\wedge 0\le {{F}}_{ℝ}^{\prime }\left({U}\right)\right)\right)$
37 34 35 36 sylancl ${⊢}{\phi }\to \left({{F}}_{ℝ}^{\prime }\left({U}\right)=0↔\left({{F}}_{ℝ}^{\prime }\left({U}\right)\le 0\wedge 0\le {{F}}_{ℝ}^{\prime }\left({U}\right)\right)\right)$
38 23 31 37 mpbir2and ${⊢}{\phi }\to {{F}}_{ℝ}^{\prime }\left({U}\right)=0$