Metamath Proof Explorer


Theorem fdvposle

Description: Functions with a nonnegative derivative, i.e. monotonously growing functions, preserve 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 ) )
fdvposle.le
|- ( ph -> A <_ B )
fdvposle.1
|- ( ( ph /\ x e. ( A (,) B ) ) -> 0 <_ ( ( RR _D F ) ` x ) )
Assertion fdvposle
|- ( 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 fdvposle.le
 |-  ( ph -> A <_ B )
7 fdvposle.1
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 0 <_ ( ( RR _D F ) ` x ) )
8 ioossicc
 |-  ( A (,) B ) C_ ( A [,] B )
9 8 a1i
 |-  ( ph -> ( A (,) B ) C_ ( A [,] B ) )
10 ioombl
 |-  ( A (,) B ) e. dom vol
11 10 a1i
 |-  ( ph -> ( A (,) B ) e. dom vol )
12 cncff
 |-  ( ( RR _D F ) e. ( E -cn-> RR ) -> ( RR _D F ) : E --> RR )
13 5 12 syl
 |-  ( ph -> ( RR _D F ) : E --> RR )
14 13 adantr
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( RR _D F ) : E --> RR )
15 1 2 3 fct2relem
 |-  ( ph -> ( A [,] B ) C_ E )
16 15 sselda
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x e. E )
17 14 16 ffvelrnd
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( ( RR _D F ) ` x ) e. RR )
18 ioossre
 |-  ( C (,) D ) C_ RR
19 1 18 eqsstri
 |-  E C_ RR
20 19 2 sselid
 |-  ( ph -> A e. RR )
21 19 3 sselid
 |-  ( ph -> B e. RR )
22 ax-resscn
 |-  RR C_ CC
23 ssid
 |-  CC C_ CC
24 cncfss
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( ( A [,] B ) -cn-> RR ) C_ ( ( A [,] B ) -cn-> CC ) )
25 22 23 24 mp2an
 |-  ( ( A [,] B ) -cn-> RR ) C_ ( ( A [,] B ) -cn-> CC )
26 13 15 feqresmpt
 |-  ( ph -> ( ( RR _D F ) |` ( A [,] B ) ) = ( x e. ( A [,] B ) |-> ( ( RR _D F ) ` x ) ) )
27 rescncf
 |-  ( ( A [,] B ) C_ E -> ( ( RR _D F ) e. ( E -cn-> RR ) -> ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) ) )
28 15 5 27 sylc
 |-  ( ph -> ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )
29 26 28 eqeltrrd
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( ( RR _D F ) ` x ) ) e. ( ( A [,] B ) -cn-> RR ) )
30 25 29 sselid
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( ( RR _D F ) ` x ) ) e. ( ( A [,] B ) -cn-> CC ) )
31 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 )
32 20 21 30 31 syl3anc
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( ( RR _D F ) ` x ) ) e. L^1 )
33 9 11 17 32 iblss
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( ( RR _D F ) ` x ) ) e. L^1 )
34 13 adantr
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( RR _D F ) : E --> RR )
35 9 sselda
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( A [,] B ) )
36 35 16 syldan
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. E )
37 34 36 ffvelrnd
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. RR )
38 33 37 7 itgge0
 |-  ( ph -> 0 <_ S. ( A (,) B ) ( ( RR _D F ) ` x ) _d x )
39 fss
 |-  ( ( F : E --> RR /\ RR C_ CC ) -> F : E --> CC )
40 4 22 39 sylancl
 |-  ( ph -> F : E --> CC )
41 cncfss
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( E -cn-> RR ) C_ ( E -cn-> CC ) )
42 22 23 41 mp2an
 |-  ( E -cn-> RR ) C_ ( E -cn-> CC )
43 42 5 sselid
 |-  ( ph -> ( RR _D F ) e. ( E -cn-> CC ) )
44 1 2 3 6 40 43 ftc2re
 |-  ( ph -> S. ( A (,) B ) ( ( RR _D F ) ` x ) _d x = ( ( F ` B ) - ( F ` A ) ) )
45 38 44 breqtrd
 |-  ( ph -> 0 <_ ( ( F ` B ) - ( F ` A ) ) )
46 4 3 ffvelrnd
 |-  ( ph -> ( F ` B ) e. RR )
47 4 2 ffvelrnd
 |-  ( ph -> ( F ` A ) e. RR )
48 46 47 subge0d
 |-  ( ph -> ( 0 <_ ( ( F ` B ) - ( F ` A ) ) <-> ( F ` A ) <_ ( F ` B ) ) )
49 45 48 mpbid
 |-  ( ph -> ( F ` A ) <_ ( F ` B ) )