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 φF:X
dvferm.b φX
dvferm.u φUAB
dvferm.s φABX
dvferm.d φUdomF
dvferm.r φyABFyFU
Assertion dvferm φFU=0

Proof

Step Hyp Ref Expression
1 dvferm.a φF:X
2 dvferm.b φX
3 dvferm.u φUAB
4 dvferm.s φABX
5 dvferm.d φUdomF
6 dvferm.r φyABFyFU
7 ne0i UABAB
8 ndmioo ¬A*B*AB=
9 8 necon1ai ABA*B*
10 3 7 9 3syl φA*B*
11 10 simpld φA*
12 ioossre AB
13 12 3 sselid φU
14 13 rexrd φU*
15 eliooord UABA<UU<B
16 3 15 syl φA<UU<B
17 16 simpld φA<U
18 11 14 17 xrltled φAU
19 iooss1 A*AUUBAB
20 11 18 19 syl2anc φUBAB
21 ssralv UBAByABFyFUyUBFyFU
22 20 6 21 sylc φyUBFyFU
23 1 2 3 4 5 22 dvferm1 φFU0
24 10 simprd φB*
25 16 simprd φU<B
26 14 24 25 xrltled φUB
27 iooss2 B*UBAUAB
28 24 26 27 syl2anc φAUAB
29 ssralv AUAByABFyFUyAUFyFU
30 28 6 29 sylc φyAUFyFU
31 1 2 3 4 5 30 dvferm2 φ0FU
32 dvfre F:XXF:domF
33 1 2 32 syl2anc φF:domF
34 33 5 ffvelrnd φFU
35 0re 0
36 letri3 FU0FU=0FU00FU
37 34 35 36 sylancl φFU=0FU00FU
38 23 31 37 mpbir2and φFU=0