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 
|- ( ph -> F : X --> RR )
dvferm.b 
|- ( ph -> X C_ RR )
dvferm.u 
|- ( ph -> U e. ( A (,) B ) )
dvferm.s 
|- ( ph -> ( A (,) B ) C_ X )
dvferm.d 
|- ( ph -> U e. dom ( RR _D F ) )
dvferm.r 
|- ( ph -> A. y e. ( A (,) B ) ( F ` y ) <_ ( F ` U ) )
Assertion dvferm 
|- ( ph -> ( ( RR _D F ) ` U ) = 0 )

Proof

Step Hyp Ref Expression
1 dvferm.a 
 |-  ( ph -> F : X --> RR )
2 dvferm.b 
 |-  ( ph -> X C_ RR )
3 dvferm.u 
 |-  ( ph -> U e. ( A (,) B ) )
4 dvferm.s 
 |-  ( ph -> ( A (,) B ) C_ X )
5 dvferm.d 
 |-  ( ph -> U e. dom ( RR _D F ) )
6 dvferm.r 
 |-  ( ph -> A. y e. ( A (,) B ) ( F ` y ) <_ ( F ` U ) )
7 ne0i 
 |-  ( U e. ( A (,) B ) -> ( A (,) B ) =/= (/) )
8 ndmioo 
 |-  ( -. ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) = (/) )
9 8 necon1ai 
 |-  ( ( A (,) B ) =/= (/) -> ( A e. RR* /\ B e. RR* ) )
10 3 7 9 3syl 
 |-  ( ph -> ( A e. RR* /\ B e. RR* ) )
11 10 simpld 
 |-  ( ph -> A e. RR* )
12 ioossre 
 |-  ( A (,) B ) C_ RR
13 12 3 sseldi 
 |-  ( ph -> U e. RR )
14 13 rexrd 
 |-  ( ph -> U e. RR* )
15 eliooord 
 |-  ( U e. ( A (,) B ) -> ( A < U /\ U < B ) )
16 3 15 syl 
 |-  ( ph -> ( A < U /\ U < B ) )
17 16 simpld 
 |-  ( ph -> A < U )
18 11 14 17 xrltled 
 |-  ( ph -> A <_ U )
19 iooss1 
 |-  ( ( A e. RR* /\ A <_ U ) -> ( U (,) B ) C_ ( A (,) B ) )
20 11 18 19 syl2anc 
 |-  ( ph -> ( U (,) B ) C_ ( A (,) B ) )
21 ssralv 
 |-  ( ( U (,) B ) C_ ( A (,) B ) -> ( A. y e. ( A (,) B ) ( F ` y ) <_ ( F ` U ) -> A. y e. ( U (,) B ) ( F ` y ) <_ ( F ` U ) ) )
22 20 6 21 sylc 
 |-  ( ph -> A. y e. ( U (,) B ) ( F ` y ) <_ ( F ` U ) )
23 1 2 3 4 5 22 dvferm1 
 |-  ( ph -> ( ( RR _D F ) ` U ) <_ 0 )
24 10 simprd 
 |-  ( ph -> B e. RR* )
25 16 simprd 
 |-  ( ph -> U < B )
26 14 24 25 xrltled 
 |-  ( ph -> U <_ B )
27 iooss2 
 |-  ( ( B e. RR* /\ U <_ B ) -> ( A (,) U ) C_ ( A (,) B ) )
28 24 26 27 syl2anc 
 |-  ( ph -> ( A (,) U ) C_ ( A (,) B ) )
29 ssralv 
 |-  ( ( A (,) U ) C_ ( A (,) B ) -> ( A. y e. ( A (,) B ) ( F ` y ) <_ ( F ` U ) -> A. y e. ( A (,) U ) ( F ` y ) <_ ( F ` U ) ) )
30 28 6 29 sylc 
 |-  ( ph -> A. y e. ( A (,) U ) ( F ` y ) <_ ( F ` U ) )
31 1 2 3 4 5 30 dvferm2 
 |-  ( ph -> 0 <_ ( ( RR _D F ) ` U ) )
32 dvfre 
 |-  ( ( F : X --> RR /\ X C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
33 1 2 32 syl2anc 
 |-  ( ph -> ( RR _D F ) : dom ( RR _D F ) --> RR )
34 33 5 ffvelrnd 
 |-  ( ph -> ( ( RR _D F ) ` U ) e. RR )
35 0re 
 |-  0 e. RR
36 letri3 
 |-  ( ( ( ( RR _D F ) ` U ) e. RR /\ 0 e. RR ) -> ( ( ( RR _D F ) ` U ) = 0 <-> ( ( ( RR _D F ) ` U ) <_ 0 /\ 0 <_ ( ( RR _D F ) ` U ) ) ) )
37 34 35 36 sylancl 
 |-  ( ph -> ( ( ( RR _D F ) ` U ) = 0 <-> ( ( ( RR _D F ) ` U ) <_ 0 /\ 0 <_ ( ( RR _D F ) ` U ) ) ) )
38 23 31 37 mpbir2and 
 |-  ( ph -> ( ( RR _D F ) ` U ) = 0 )