Metamath Proof Explorer

Theorem dvlt0

Description: A function on a closed interval with negative derivative is decreasing. (Contributed by Mario Carneiro, 19-Feb-2015)

Ref Expression
Hypotheses dvgt0.a 
|- ( ph -> A e. RR )
dvgt0.b 
|- ( ph -> B e. RR )
dvgt0.f 
|- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )
dvlt0.d 
|- ( ph -> ( RR _D F ) : ( A (,) B ) --> ( -oo (,) 0 ) )
Assertion dvlt0 
|- ( ph -> F Isom < , `' < ( ( A [,] B ) , ran F ) )

Proof

Step Hyp Ref Expression
1 dvgt0.a 
 |-  ( ph -> A e. RR )
2 dvgt0.b 
 |-  ( ph -> B e. RR )
3 dvgt0.f 
 |-  ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )
4 dvlt0.d 
 |-  ( ph -> ( RR _D F ) : ( A (,) B ) --> ( -oo (,) 0 ) )
5 gtso 
 |-  `' < Or RR
6 1 2 3 4 dvgt0lem1 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) e. ( -oo (,) 0 ) )
7 eliooord 
 |-  ( ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) e. ( -oo (,) 0 ) -> ( -oo < ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) /\ ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) < 0 ) )
8 6 7 syl 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( -oo < ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) /\ ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) < 0 ) )
9 8 simprd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) < 0 )
10 cncff 
 |-  ( F e. ( ( A [,] B ) -cn-> RR ) -> F : ( A [,] B ) --> RR )
11 3 10 syl 
 |-  ( ph -> F : ( A [,] B ) --> RR )
12 11 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> F : ( A [,] B ) --> RR )
13 simplrr 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> y e. ( A [,] B ) )
14 12 13 ffvelrnd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( F ` y ) e. RR )
15 simplrl 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> x e. ( A [,] B ) )
16 12 15 ffvelrnd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( F ` x ) e. RR )
17 14 16 resubcld 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F ` y ) - ( F ` x ) ) e. RR )
18 0red 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> 0 e. RR )
19 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
20 1 2 19 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
21 20 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( A [,] B ) C_ RR )
22 21 13 sseldd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> y e. RR )
23 21 15 sseldd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> x e. RR )
24 22 23 resubcld 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( y - x ) e. RR )
25 simpr 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> x < y )
26 23 22 posdifd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( x < y <-> 0 < ( y - x ) ) )
27 25 26 mpbid 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> 0 < ( y - x ) )
28 ltdivmul 
 |-  ( ( ( ( F ` y ) - ( F ` x ) ) e. RR /\ 0 e. RR /\ ( ( y - x ) e. RR /\ 0 < ( y - x ) ) ) -> ( ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) < 0 <-> ( ( F ` y ) - ( F ` x ) ) < ( ( y - x ) x. 0 ) ) )
29 17 18 24 27 28 syl112anc 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) < 0 <-> ( ( F ` y ) - ( F ` x ) ) < ( ( y - x ) x. 0 ) ) )
30 9 29 mpbid 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F ` y ) - ( F ` x ) ) < ( ( y - x ) x. 0 ) )
31 24 recnd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( y - x ) e. CC )
32 31 mul01d 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( y - x ) x. 0 ) = 0 )
33 30 32 breqtrd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F ` y ) - ( F ` x ) ) < 0 )
34 14 16 18 ltsubaddd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( ( F ` y ) - ( F ` x ) ) < 0 <-> ( F ` y ) < ( 0 + ( F ` x ) ) ) )
35 33 34 mpbid 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( F ` y ) < ( 0 + ( F ` x ) ) )
36 16 recnd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( F ` x ) e. CC )
37 36 addid2d 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( 0 + ( F ` x ) ) = ( F ` x ) )
38 35 37 breqtrd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( F ` y ) < ( F ` x ) )
39 fvex 
 |-  ( F ` x ) e. _V
40 fvex 
 |-  ( F ` y ) e. _V
41 39 40 brcnv 
 |-  ( ( F ` x ) `' < ( F ` y ) <-> ( F ` y ) < ( F ` x ) )
42 38 41 sylibr 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( F ` x ) `' < ( F ` y ) )
43 1 2 3 4 5 42 dvgt0lem2 
 |-  ( ph -> F Isom < , `' < ( ( A [,] B ) , ran F ) )