Metamath Proof Explorer

Theorem fdvposlt

Description: Functions with a positive derivative, i.e. monotonously growing functions, preserve strict ordering. (Contributed by Thierry Arnoux, 20-Dec-2021)

Ref Expression
Hypotheses fdvposlt.d 
|- E = ( C (,) D )
fdvposlt.a 
|- ( ph -> A e. E )
fdvposlt.b 
|- ( ph -> B e. E )
fdvposlt.f 
|- ( ph -> F : E --> RR )
fdvposlt.c 
|- ( ph -> ( RR _D F ) e. ( E -cn-> RR ) )
fdvposlt.lt 
|- ( ph -> A < B )
fdvposlt.1 
|- ( ( ph /\ x e. ( A (,) B ) ) -> 0 < ( ( RR _D F ) ` x ) )
Assertion fdvposlt 
|- ( ph -> ( F ` A ) < ( F ` B ) )

Proof

Step Hyp Ref Expression
1 fdvposlt.d 
 |-  E = ( C (,) D )
2 fdvposlt.a 
 |-  ( ph -> A e. E )
3 fdvposlt.b 
 |-  ( ph -> B e. E )
4 fdvposlt.f 
 |-  ( ph -> F : E --> RR )
5 fdvposlt.c 
 |-  ( ph -> ( RR _D F ) e. ( E -cn-> RR ) )
6 fdvposlt.lt 
 |-  ( ph -> A < B )
7 fdvposlt.1 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 0 < ( ( RR _D F ) ` x ) )
8 ioossre 
 |-  ( C (,) D ) C_ RR
9 1 8 eqsstri 
 |-  E C_ RR
10 9 2 sselid 
 |-  ( ph -> A e. RR )
11 9 3 sselid 
 |-  ( ph -> B e. RR )
12 10 11 posdifd 
 |-  ( ph -> ( A < B <-> 0 < ( B - A ) ) )
13 6 12 mpbid 
 |-  ( ph -> 0 < ( B - A ) )
14 10 11 6 ltled 
 |-  ( ph -> A <_ B )
15 volioo 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol ` ( A (,) B ) ) = ( B - A ) )
16 10 11 14 15 syl3anc 
 |-  ( ph -> ( vol ` ( A (,) B ) ) = ( B - A ) )
17 13 16 breqtrrd 
 |-  ( ph -> 0 < ( vol ` ( A (,) B ) ) )
18 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
19 18 a1i 
 |-  ( ph -> ( A (,) B ) C_ ( A [,] B ) )
20 ioombl 
 |-  ( A (,) B ) e. dom vol
21 20 a1i 
 |-  ( ph -> ( A (,) B ) e. dom vol )
22 cncff 
 |-  ( ( RR _D F ) e. ( E -cn-> RR ) -> ( RR _D F ) : E --> RR )
23 5 22 syl 
 |-  ( ph -> ( RR _D F ) : E --> RR )
24 23 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( RR _D F ) : E --> RR )
25 1 2 3 fct2relem 
 |-  ( ph -> ( A [,] B ) C_ E )
26 25 sselda 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x e. E )
27 24 26 ffvelrnd 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( ( RR _D F ) ` x ) e. RR )
28 ax-resscn 
 |-  RR C_ CC
29 ssid 
 |-  CC C_ CC
30 cncfss 
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( ( A [,] B ) -cn-> RR ) C_ ( ( A [,] B ) -cn-> CC ) )
31 28 29 30 mp2an 
 |-  ( ( A [,] B ) -cn-> RR ) C_ ( ( A [,] B ) -cn-> CC )
32 23 25 feqresmpt 
 |-  ( ph -> ( ( RR _D F ) |` ( A [,] B ) ) = ( x e. ( A [,] B ) |-> ( ( RR _D F ) ` x ) ) )
33 rescncf 
 |-  ( ( A [,] B ) C_ E -> ( ( RR _D F ) e. ( E -cn-> RR ) -> ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) ) )
34 25 5 33 sylc 
 |-  ( ph -> ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )
35 32 34 eqeltrrd 
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( ( RR _D F ) ` x ) ) e. ( ( A [,] B ) -cn-> RR ) )
36 31 35 sselid 
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( ( RR _D F ) ` x ) ) e. ( ( A [,] B ) -cn-> CC ) )
37 cniccibl 
 |-  ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> ( ( RR _D F ) ` x ) ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( x e. ( A [,] B ) |-> ( ( RR _D F ) ` x ) ) e. L^1 )
38 10 11 36 37 syl3anc 
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( ( RR _D F ) ` x ) ) e. L^1 )
39 19 21 27 38 iblss 
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( ( RR _D F ) ` x ) ) e. L^1 )
40 23 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( RR _D F ) : E --> RR )
41 19 sselda 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( A [,] B ) )
42 41 26 syldan 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. E )
43 40 42 ffvelrnd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. RR )
44 elrp 
 |-  ( ( ( RR _D F ) ` x ) e. RR+ <-> ( ( ( RR _D F ) ` x ) e. RR /\ 0 < ( ( RR _D F ) ` x ) ) )
45 43 7 44 sylanbrc 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. RR+ )
46 17 39 45 itggt0 
 |-  ( ph -> 0 < S. ( A (,) B ) ( ( RR _D F ) ` x ) _d x )
47 fss 
 |-  ( ( F : E --> RR /\ RR C_ CC ) -> F : E --> CC )
48 4 28 47 sylancl 
 |-  ( ph -> F : E --> CC )
49 cncfss 
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( E -cn-> RR ) C_ ( E -cn-> CC ) )
50 28 29 49 mp2an 
 |-  ( E -cn-> RR ) C_ ( E -cn-> CC )
51 50 5 sselid 
 |-  ( ph -> ( RR _D F ) e. ( E -cn-> CC ) )
52 1 2 3 14 48 51 ftc2re 
 |-  ( ph -> S. ( A (,) B ) ( ( RR _D F ) ` x ) _d x = ( ( F ` B ) - ( F ` A ) ) )
53 46 52 breqtrd 
 |-  ( ph -> 0 < ( ( F ` B ) - ( F ` A ) ) )
54 4 2 ffvelrnd 
 |-  ( ph -> ( F ` A ) e. RR )
55 4 3 ffvelrnd 
 |-  ( ph -> ( F ` B ) e. RR )
56 54 55 posdifd 
 |-  ( ph -> ( ( F ` A ) < ( F ` B ) <-> 0 < ( ( F ` B ) - ( F ` A ) ) ) )
57 53 56 mpbird 
 |-  ( ph -> ( F ` A ) < ( F ` B ) )