Metamath Proof Explorer

Theorem dvge0

Description: A function on a closed interval with nonnegative derivative is weakly increasing. (Contributed by Mario Carneiro, 30-Apr-2016)

Ref Expression
Hypotheses dvgt0.a 
|- ( ph -> A e. RR )
dvgt0.b 
|- ( ph -> B e. RR )
dvgt0.f 
|- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )
dvge0.d 
|- ( ph -> ( RR _D F ) : ( A (,) B ) --> ( 0 [,) +oo ) )
dvge0.x 
|- ( ph -> X e. ( A [,] B ) )
dvge0.y 
|- ( ph -> Y e. ( A [,] B ) )
dvge0.l 
|- ( ph -> X <_ Y )
Assertion dvge0 
|- ( ph -> ( F ` X ) <_ ( F ` Y ) )

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 dvge0.d 
 |-  ( ph -> ( RR _D F ) : ( A (,) B ) --> ( 0 [,) +oo ) )
5 dvge0.x 
 |-  ( ph -> X e. ( A [,] B ) )
6 dvge0.y 
 |-  ( ph -> Y e. ( A [,] B ) )
7 dvge0.l 
 |-  ( ph -> X <_ Y )
8 1 2 3 4 dvgt0lem1 
 |-  ( ( ( ph /\ ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) ) /\ X < Y ) -> ( ( ( F ` Y ) - ( F ` X ) ) / ( Y - X ) ) e. ( 0 [,) +oo ) )
9 8 exp31 
 |-  ( ph -> ( ( X e. ( A [,] B ) /\ Y e. ( A [,] B ) ) -> ( X < Y -> ( ( ( F ` Y ) - ( F ` X ) ) / ( Y - X ) ) e. ( 0 [,) +oo ) ) ) )
10 5 6 9 mp2and 
 |-  ( ph -> ( X < Y -> ( ( ( F ` Y ) - ( F ` X ) ) / ( Y - X ) ) e. ( 0 [,) +oo ) ) )
11 10 imp 
 |-  ( ( ph /\ X < Y ) -> ( ( ( F ` Y ) - ( F ` X ) ) / ( Y - X ) ) e. ( 0 [,) +oo ) )
12 elrege0 
 |-  ( ( ( ( F ` Y ) - ( F ` X ) ) / ( Y - X ) ) e. ( 0 [,) +oo ) <-> ( ( ( ( F ` Y ) - ( F ` X ) ) / ( Y - X ) ) e. RR /\ 0 <_ ( ( ( F ` Y ) - ( F ` X ) ) / ( Y - X ) ) ) )
13 12 simprbi 
 |-  ( ( ( ( F ` Y ) - ( F ` X ) ) / ( Y - X ) ) e. ( 0 [,) +oo ) -> 0 <_ ( ( ( F ` Y ) - ( F ` X ) ) / ( Y - X ) ) )
14 11 13 syl 
 |-  ( ( ph /\ X < Y ) -> 0 <_ ( ( ( F ` Y ) - ( F ` X ) ) / ( Y - X ) ) )
15 cncff 
 |-  ( F e. ( ( A [,] B ) -cn-> RR ) -> F : ( A [,] B ) --> RR )
16 3 15 syl 
 |-  ( ph -> F : ( A [,] B ) --> RR )
17 16 6 ffvelrnd 
 |-  ( ph -> ( F ` Y ) e. RR )
18 16 5 ffvelrnd 
 |-  ( ph -> ( F ` X ) e. RR )
19 17 18 resubcld 
 |-  ( ph -> ( ( F ` Y ) - ( F ` X ) ) e. RR )
20 19 adantr 
 |-  ( ( ph /\ X < Y ) -> ( ( F ` Y ) - ( F ` X ) ) e. RR )
21 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
22 1 2 21 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
23 22 6 sseldd 
 |-  ( ph -> Y e. RR )
24 22 5 sseldd 
 |-  ( ph -> X e. RR )
25 23 24 resubcld 
 |-  ( ph -> ( Y - X ) e. RR )
26 25 adantr 
 |-  ( ( ph /\ X < Y ) -> ( Y - X ) e. RR )
27 24 23 posdifd 
 |-  ( ph -> ( X < Y <-> 0 < ( Y - X ) ) )
28 27 biimpa 
 |-  ( ( ph /\ X < Y ) -> 0 < ( Y - X ) )
29 ge0div 
 |-  ( ( ( ( F ` Y ) - ( F ` X ) ) e. RR /\ ( Y - X ) e. RR /\ 0 < ( Y - X ) ) -> ( 0 <_ ( ( F ` Y ) - ( F ` X ) ) <-> 0 <_ ( ( ( F ` Y ) - ( F ` X ) ) / ( Y - X ) ) ) )
30 20 26 28 29 syl3anc 
 |-  ( ( ph /\ X < Y ) -> ( 0 <_ ( ( F ` Y ) - ( F ` X ) ) <-> 0 <_ ( ( ( F ` Y ) - ( F ` X ) ) / ( Y - X ) ) ) )
31 14 30 mpbird 
 |-  ( ( ph /\ X < Y ) -> 0 <_ ( ( F ` Y ) - ( F ` X ) ) )
32 31 ex 
 |-  ( ph -> ( X < Y -> 0 <_ ( ( F ` Y ) - ( F ` X ) ) ) )
33 17 18 subge0d 
 |-  ( ph -> ( 0 <_ ( ( F ` Y ) - ( F ` X ) ) <-> ( F ` X ) <_ ( F ` Y ) ) )
34 32 33 sylibd 
 |-  ( ph -> ( X < Y -> ( F ` X ) <_ ( F ` Y ) ) )
35 17 leidd 
 |-  ( ph -> ( F ` Y ) <_ ( F ` Y ) )
36 fveq2 
 |-  ( X = Y -> ( F ` X ) = ( F ` Y ) )
37 36 breq1d 
 |-  ( X = Y -> ( ( F ` X ) <_ ( F ` Y ) <-> ( F ` Y ) <_ ( F ` Y ) ) )
38 35 37 syl5ibrcom 
 |-  ( ph -> ( X = Y -> ( F ` X ) <_ ( F ` Y ) ) )
39 24 23 leloed 
 |-  ( ph -> ( X <_ Y <-> ( X < Y \/ X = Y ) ) )
40 7 39 mpbid 
 |-  ( ph -> ( X < Y \/ X = Y ) )
41 34 38 40 mpjaod 
 |-  ( ph -> ( F ` X ) <_ ( F ` Y ) )