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 sseldi 
 |-  ( ph -> A e. RR )
21 19 3 sseldi 
 |-  ( 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 sseldi 
 |-  ( 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 sseldi 
 |-  ( 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 ) )