Metamath Proof Explorer

Theorem dvgt0

Description: A function on a closed interval with positive derivative is increasing. (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 ) )
dvgt0.d 
|- ( ph -> ( RR _D F ) : ( A (,) B ) --> RR+ )
Assertion dvgt0 
|- ( 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 dvgt0.d 
 |-  ( ph -> ( RR _D F ) : ( A (,) B ) --> RR+ )
5 ltso 
 |-  < 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. RR+ )
7 6 rpgt0d 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> 0 < ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) )
8 cncff 
 |-  ( F e. ( ( A [,] B ) -cn-> RR ) -> F : ( A [,] B ) --> RR )
9 3 8 syl 
 |-  ( ph -> F : ( A [,] B ) --> RR )
10 9 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> F : ( A [,] B ) --> RR )
11 simplrr 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> y e. ( A [,] B ) )
12 10 11 ffvelrnd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( F ` y ) e. RR )
13 simplrl 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> x e. ( A [,] B ) )
14 10 13 ffvelrnd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( F ` x ) e. RR )
15 12 14 resubcld 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F ` y ) - ( F ` x ) ) e. RR )
16 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
17 1 2 16 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
18 17 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( A [,] B ) C_ RR )
19 18 11 sseldd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> y e. RR )
20 18 13 sseldd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> x e. RR )
21 19 20 resubcld 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( y - x ) e. RR )
22 simpr 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> x < y )
23 20 19 posdifd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( x < y <-> 0 < ( y - x ) ) )
24 22 23 mpbid 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> 0 < ( y - x ) )
25 gt0div 
 |-  ( ( ( ( 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 ) ) ) )
26 15 21 24 25 syl3anc 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( 0 < ( ( F ` y ) - ( F ` x ) ) <-> 0 < ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) )
27 7 26 mpbird 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> 0 < ( ( F ` y ) - ( F ` x ) ) )
28 14 12 posdifd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F ` x ) < ( F ` y ) <-> 0 < ( ( F ` y ) - ( F ` x ) ) ) )
29 27 28 mpbird 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( F ` x ) < ( F ` y ) )
30 1 2 3 4 5 29 dvgt0lem2 
 |-  ( ph -> F Isom < , < ( ( A [,] B ) , ran F ) )