Metamath Proof Explorer

Theorem dvle

Description: If A ( x ) , C ( x ) are differentiable functions and A<_ C` , then for x <_ y , A ( y ) - A ( x ) <_ C ( y ) - C ( x ) ` . (Contributed by Mario Carneiro, 16-May-2016)

Ref Expression
Hypotheses dvle.m 
|- ( ph -> M e. RR )
dvle.n 
|- ( ph -> N e. RR )
dvle.a 
|- ( ph -> ( x e. ( M [,] N ) |-> A ) e. ( ( M [,] N ) -cn-> RR ) )
dvle.b 
|- ( ph -> ( RR _D ( x e. ( M (,) N ) |-> A ) ) = ( x e. ( M (,) N ) |-> B ) )
dvle.c 
|- ( ph -> ( x e. ( M [,] N ) |-> C ) e. ( ( M [,] N ) -cn-> RR ) )
dvle.d 
|- ( ph -> ( RR _D ( x e. ( M (,) N ) |-> C ) ) = ( x e. ( M (,) N ) |-> D ) )
dvle.f 
|- ( ( ph /\ x e. ( M (,) N ) ) -> B <_ D )
dvle.x 
|- ( ph -> X e. ( M [,] N ) )
dvle.y 
|- ( ph -> Y e. ( M [,] N ) )
dvle.l 
|- ( ph -> X <_ Y )
dvle.p 
|- ( x = X -> A = P )
dvle.q 
|- ( x = X -> C = Q )
dvle.r 
|- ( x = Y -> A = R )
dvle.s 
|- ( x = Y -> C = S )
Assertion dvle 
|- ( ph -> ( R - P ) <_ ( S - Q ) )

Proof

Step Hyp Ref Expression
1 dvle.m 
 |-  ( ph -> M e. RR )
2 dvle.n 
 |-  ( ph -> N e. RR )
3 dvle.a 
 |-  ( ph -> ( x e. ( M [,] N ) |-> A ) e. ( ( M [,] N ) -cn-> RR ) )
4 dvle.b 
 |-  ( ph -> ( RR _D ( x e. ( M (,) N ) |-> A ) ) = ( x e. ( M (,) N ) |-> B ) )
5 dvle.c 
 |-  ( ph -> ( x e. ( M [,] N ) |-> C ) e. ( ( M [,] N ) -cn-> RR ) )
6 dvle.d 
 |-  ( ph -> ( RR _D ( x e. ( M (,) N ) |-> C ) ) = ( x e. ( M (,) N ) |-> D ) )
7 dvle.f 
 |-  ( ( ph /\ x e. ( M (,) N ) ) -> B <_ D )
8 dvle.x 
 |-  ( ph -> X e. ( M [,] N ) )
9 dvle.y 
 |-  ( ph -> Y e. ( M [,] N ) )
10 dvle.l 
 |-  ( ph -> X <_ Y )
11 dvle.p 
 |-  ( x = X -> A = P )
12 dvle.q 
 |-  ( x = X -> C = Q )
13 dvle.r 
 |-  ( x = Y -> A = R )
14 dvle.s 
 |-  ( x = Y -> C = S )
15 13 eleq1d 
 |-  ( x = Y -> ( A e. RR <-> R e. RR ) )
16 cncff 
 |-  ( ( x e. ( M [,] N ) |-> A ) e. ( ( M [,] N ) -cn-> RR ) -> ( x e. ( M [,] N ) |-> A ) : ( M [,] N ) --> RR )
17 3 16 syl 
 |-  ( ph -> ( x e. ( M [,] N ) |-> A ) : ( M [,] N ) --> RR )
18 eqid 
 |-  ( x e. ( M [,] N ) |-> A ) = ( x e. ( M [,] N ) |-> A )
19 18 fmpt 
 |-  ( A. x e. ( M [,] N ) A e. RR <-> ( x e. ( M [,] N ) |-> A ) : ( M [,] N ) --> RR )
20 17 19 sylibr 
 |-  ( ph -> A. x e. ( M [,] N ) A e. RR )
21 15 20 9 rspcdva 
 |-  ( ph -> R e. RR )
22 14 eleq1d 
 |-  ( x = Y -> ( C e. RR <-> S e. RR ) )
23 cncff 
 |-  ( ( x e. ( M [,] N ) |-> C ) e. ( ( M [,] N ) -cn-> RR ) -> ( x e. ( M [,] N ) |-> C ) : ( M [,] N ) --> RR )
24 5 23 syl 
 |-  ( ph -> ( x e. ( M [,] N ) |-> C ) : ( M [,] N ) --> RR )
25 eqid 
 |-  ( x e. ( M [,] N ) |-> C ) = ( x e. ( M [,] N ) |-> C )
26 25 fmpt 
 |-  ( A. x e. ( M [,] N ) C e. RR <-> ( x e. ( M [,] N ) |-> C ) : ( M [,] N ) --> RR )
27 24 26 sylibr 
 |-  ( ph -> A. x e. ( M [,] N ) C e. RR )
28 22 27 9 rspcdva 
 |-  ( ph -> S e. RR )
29 12 eleq1d 
 |-  ( x = X -> ( C e. RR <-> Q e. RR ) )
30 29 27 8 rspcdva 
 |-  ( ph -> Q e. RR )
31 28 30 resubcld 
 |-  ( ph -> ( S - Q ) e. RR )
32 11 eleq1d 
 |-  ( x = X -> ( A e. RR <-> P e. RR ) )
33 32 20 8 rspcdva 
 |-  ( ph -> P e. RR )
34 21 recnd 
 |-  ( ph -> R e. CC )
35 30 recnd 
 |-  ( ph -> Q e. CC )
36 28 recnd 
 |-  ( ph -> S e. CC )
37 35 36 subcld 
 |-  ( ph -> ( Q - S ) e. CC )
38 34 37 addcomd 
 |-  ( ph -> ( R + ( Q - S ) ) = ( ( Q - S ) + R ) )
39 34 36 35 subsub2d 
 |-  ( ph -> ( R - ( S - Q ) ) = ( R + ( Q - S ) ) )
40 35 36 34 subsubd 
 |-  ( ph -> ( Q - ( S - R ) ) = ( ( Q - S ) + R ) )
41 38 39 40 3eqtr4d 
 |-  ( ph -> ( R - ( S - Q ) ) = ( Q - ( S - R ) ) )
42 28 21 resubcld 
 |-  ( ph -> ( S - R ) e. RR )
43 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
44 43 subcn 
 |-  - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
45 ax-resscn 
 |-  RR C_ CC
46 resubcl 
 |-  ( ( C e. RR /\ A e. RR ) -> ( C - A ) e. RR )
47 43 44 5 3 45 46 cncfmpt2ss 
 |-  ( ph -> ( x e. ( M [,] N ) |-> ( C - A ) ) e. ( ( M [,] N ) -cn-> RR ) )
48 45 a1i 
 |-  ( ph -> RR C_ CC )
49 iccssre 
 |-  ( ( M e. RR /\ N e. RR ) -> ( M [,] N ) C_ RR )
50 1 2 49 syl2anc 
 |-  ( ph -> ( M [,] N ) C_ RR )
51 24 fvmptelrn 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> C e. RR )
52 17 fvmptelrn 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> A e. RR )
53 51 52 resubcld 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> ( C - A ) e. RR )
54 53 recnd 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> ( C - A ) e. CC )
55 43 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
56 iccntr 
 |-  ( ( M e. RR /\ N e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( M [,] N ) ) = ( M (,) N ) )
57 1 2 56 syl2anc 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( M [,] N ) ) = ( M (,) N ) )
58 48 50 54 55 43 57 dvmptntr 
 |-  ( ph -> ( RR _D ( x e. ( M [,] N ) |-> ( C - A ) ) ) = ( RR _D ( x e. ( M (,) N ) |-> ( C - A ) ) ) )
59 reelprrecn 
 |-  RR e. { RR , CC }
60 59 a1i 
 |-  ( ph -> RR e. { RR , CC } )
61 ioossicc 
 |-  ( M (,) N ) C_ ( M [,] N )
62 61 sseli 
 |-  ( x e. ( M (,) N ) -> x e. ( M [,] N ) )
63 51 recnd 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> C e. CC )
64 62 63 sylan2 
 |-  ( ( ph /\ x e. ( M (,) N ) ) -> C e. CC )
65 lerel 
 |-  Rel <_
66 65 brrelex2i 
 |-  ( B <_ D -> D e. _V )
67 7 66 syl 
 |-  ( ( ph /\ x e. ( M (,) N ) ) -> D e. _V )
68 52 recnd 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> A e. CC )
69 62 68 sylan2 
 |-  ( ( ph /\ x e. ( M (,) N ) ) -> A e. CC )
70 65 brrelex1i 
 |-  ( B <_ D -> B e. _V )
71 7 70 syl 
 |-  ( ( ph /\ x e. ( M (,) N ) ) -> B e. _V )
72 60 64 67 6 69 71 4 dvmptsub 
 |-  ( ph -> ( RR _D ( x e. ( M (,) N ) |-> ( C - A ) ) ) = ( x e. ( M (,) N ) |-> ( D - B ) ) )
73 58 72 eqtrd 
 |-  ( ph -> ( RR _D ( x e. ( M [,] N ) |-> ( C - A ) ) ) = ( x e. ( M (,) N ) |-> ( D - B ) ) )
74 62 51 sylan2 
 |-  ( ( ph /\ x e. ( M (,) N ) ) -> C e. RR )
75 74 fmpttd 
 |-  ( ph -> ( x e. ( M (,) N ) |-> C ) : ( M (,) N ) --> RR )
76 ioossre 
 |-  ( M (,) N ) C_ RR
77 dvfre 
 |-  ( ( ( x e. ( M (,) N ) |-> C ) : ( M (,) N ) --> RR /\ ( M (,) N ) C_ RR ) -> ( RR _D ( x e. ( M (,) N ) |-> C ) ) : dom ( RR _D ( x e. ( M (,) N ) |-> C ) ) --> RR )
78 75 76 77 sylancl 
 |-  ( ph -> ( RR _D ( x e. ( M (,) N ) |-> C ) ) : dom ( RR _D ( x e. ( M (,) N ) |-> C ) ) --> RR )
79 6 dmeqd 
 |-  ( ph -> dom ( RR _D ( x e. ( M (,) N ) |-> C ) ) = dom ( x e. ( M (,) N ) |-> D ) )
80 67 ralrimiva 
 |-  ( ph -> A. x e. ( M (,) N ) D e. _V )
81 dmmptg 
 |-  ( A. x e. ( M (,) N ) D e. _V -> dom ( x e. ( M (,) N ) |-> D ) = ( M (,) N ) )
82 80 81 syl 
 |-  ( ph -> dom ( x e. ( M (,) N ) |-> D ) = ( M (,) N ) )
83 79 82 eqtrd 
 |-  ( ph -> dom ( RR _D ( x e. ( M (,) N ) |-> C ) ) = ( M (,) N ) )
84 6 83 feq12d 
 |-  ( ph -> ( ( RR _D ( x e. ( M (,) N ) |-> C ) ) : dom ( RR _D ( x e. ( M (,) N ) |-> C ) ) --> RR <-> ( x e. ( M (,) N ) |-> D ) : ( M (,) N ) --> RR ) )
85 78 84 mpbid 
 |-  ( ph -> ( x e. ( M (,) N ) |-> D ) : ( M (,) N ) --> RR )
86 85 fvmptelrn 
 |-  ( ( ph /\ x e. ( M (,) N ) ) -> D e. RR )
87 62 52 sylan2 
 |-  ( ( ph /\ x e. ( M (,) N ) ) -> A e. RR )
88 87 fmpttd 
 |-  ( ph -> ( x e. ( M (,) N ) |-> A ) : ( M (,) N ) --> RR )
89 dvfre 
 |-  ( ( ( x e. ( M (,) N ) |-> A ) : ( M (,) N ) --> RR /\ ( M (,) N ) C_ RR ) -> ( RR _D ( x e. ( M (,) N ) |-> A ) ) : dom ( RR _D ( x e. ( M (,) N ) |-> A ) ) --> RR )
90 88 76 89 sylancl 
 |-  ( ph -> ( RR _D ( x e. ( M (,) N ) |-> A ) ) : dom ( RR _D ( x e. ( M (,) N ) |-> A ) ) --> RR )
91 4 dmeqd 
 |-  ( ph -> dom ( RR _D ( x e. ( M (,) N ) |-> A ) ) = dom ( x e. ( M (,) N ) |-> B ) )
92 71 ralrimiva 
 |-  ( ph -> A. x e. ( M (,) N ) B e. _V )
93 dmmptg 
 |-  ( A. x e. ( M (,) N ) B e. _V -> dom ( x e. ( M (,) N ) |-> B ) = ( M (,) N ) )
94 92 93 syl 
 |-  ( ph -> dom ( x e. ( M (,) N ) |-> B ) = ( M (,) N ) )
95 91 94 eqtrd 
 |-  ( ph -> dom ( RR _D ( x e. ( M (,) N ) |-> A ) ) = ( M (,) N ) )
96 4 95 feq12d 
 |-  ( ph -> ( ( RR _D ( x e. ( M (,) N ) |-> A ) ) : dom ( RR _D ( x e. ( M (,) N ) |-> A ) ) --> RR <-> ( x e. ( M (,) N ) |-> B ) : ( M (,) N ) --> RR ) )
97 90 96 mpbid 
 |-  ( ph -> ( x e. ( M (,) N ) |-> B ) : ( M (,) N ) --> RR )
98 97 fvmptelrn 
 |-  ( ( ph /\ x e. ( M (,) N ) ) -> B e. RR )
99 86 98 resubcld 
 |-  ( ( ph /\ x e. ( M (,) N ) ) -> ( D - B ) e. RR )
100 86 98 subge0d 
 |-  ( ( ph /\ x e. ( M (,) N ) ) -> ( 0 <_ ( D - B ) <-> B <_ D ) )
101 7 100 mpbird 
 |-  ( ( ph /\ x e. ( M (,) N ) ) -> 0 <_ ( D - B ) )
102 elrege0 
 |-  ( ( D - B ) e. ( 0 [,) +oo ) <-> ( ( D - B ) e. RR /\ 0 <_ ( D - B ) ) )
103 99 101 102 sylanbrc 
 |-  ( ( ph /\ x e. ( M (,) N ) ) -> ( D - B ) e. ( 0 [,) +oo ) )
104 73 103 fmpt3d 
 |-  ( ph -> ( RR _D ( x e. ( M [,] N ) |-> ( C - A ) ) ) : ( M (,) N ) --> ( 0 [,) +oo ) )
105 1 2 47 104 8 9 10 dvge0 
 |-  ( ph -> ( ( x e. ( M [,] N ) |-> ( C - A ) ) ` X ) <_ ( ( x e. ( M [,] N ) |-> ( C - A ) ) ` Y ) )
106 12 11 oveq12d 
 |-  ( x = X -> ( C - A ) = ( Q - P ) )
107 eqid 
 |-  ( x e. ( M [,] N ) |-> ( C - A ) ) = ( x e. ( M [,] N ) |-> ( C - A ) )
108 ovex 
 |-  ( C - A ) e. _V
109 106 107 108 fvmpt3i 
 |-  ( X e. ( M [,] N ) -> ( ( x e. ( M [,] N ) |-> ( C - A ) ) ` X ) = ( Q - P ) )
110 8 109 syl 
 |-  ( ph -> ( ( x e. ( M [,] N ) |-> ( C - A ) ) ` X ) = ( Q - P ) )
111 14 13 oveq12d 
 |-  ( x = Y -> ( C - A ) = ( S - R ) )
112 111 107 108 fvmpt3i 
 |-  ( Y e. ( M [,] N ) -> ( ( x e. ( M [,] N ) |-> ( C - A ) ) ` Y ) = ( S - R ) )
113 9 112 syl 
 |-  ( ph -> ( ( x e. ( M [,] N ) |-> ( C - A ) ) ` Y ) = ( S - R ) )
114 105 110 113 3brtr3d 
 |-  ( ph -> ( Q - P ) <_ ( S - R ) )
115 30 33 42 114 subled 
 |-  ( ph -> ( Q - ( S - R ) ) <_ P )
116 41 115 eqbrtrd 
 |-  ( ph -> ( R - ( S - Q ) ) <_ P )
117 21 31 33 116 subled 
 |-  ( ph -> ( R - P ) <_ ( S - Q ) )