Metamath Proof Explorer

Theorem itg2le

Description: If one function dominates another, then the integral of the larger is also larger. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Assertion itg2le 
|- ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) /\ F oR <_ G ) -> ( S.2 ` F ) <_ ( S.2 ` G ) )

Proof

Step Hyp Ref Expression
1 reex 
 |-  RR e. _V
2 1 a1i 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) ) /\ h e. dom S.1 ) -> RR e. _V )
3 i1ff 
 |-  ( h e. dom S.1 -> h : RR --> RR )
4 3 adantl 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) ) /\ h e. dom S.1 ) -> h : RR --> RR )
5 ressxr 
 |-  RR C_ RR*
6 fss 
 |-  ( ( h : RR --> RR /\ RR C_ RR* ) -> h : RR --> RR* )
7 4 5 6 sylancl 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) ) /\ h e. dom S.1 ) -> h : RR --> RR* )
8 simpll 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) ) /\ h e. dom S.1 ) -> F : RR --> ( 0 [,] +oo ) )
9 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
10 fss 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( 0 [,] +oo ) C_ RR* ) -> F : RR --> RR* )
11 8 9 10 sylancl 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) ) /\ h e. dom S.1 ) -> F : RR --> RR* )
12 simplr 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) ) /\ h e. dom S.1 ) -> G : RR --> ( 0 [,] +oo ) )
13 fss 
 |-  ( ( G : RR --> ( 0 [,] +oo ) /\ ( 0 [,] +oo ) C_ RR* ) -> G : RR --> RR* )
14 12 9 13 sylancl 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) ) /\ h e. dom S.1 ) -> G : RR --> RR* )
15 xrletr 
 |-  ( ( x e. RR* /\ y e. RR* /\ z e. RR* ) -> ( ( x <_ y /\ y <_ z ) -> x <_ z ) )
16 15 adantl 
 |-  ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) ) /\ h e. dom S.1 ) /\ ( x e. RR* /\ y e. RR* /\ z e. RR* ) ) -> ( ( x <_ y /\ y <_ z ) -> x <_ z ) )
17 2 7 11 14 16 caoftrn 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) ) /\ h e. dom S.1 ) -> ( ( h oR <_ F /\ F oR <_ G ) -> h oR <_ G ) )
18 simplr 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) ) /\ ( h e. dom S.1 /\ h oR <_ G ) ) -> G : RR --> ( 0 [,] +oo ) )
19 simprl 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) ) /\ ( h e. dom S.1 /\ h oR <_ G ) ) -> h e. dom S.1 )
20 simprr 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) ) /\ ( h e. dom S.1 /\ h oR <_ G ) ) -> h oR <_ G )
21 itg2ub 
 |-  ( ( G : RR --> ( 0 [,] +oo ) /\ h e. dom S.1 /\ h oR <_ G ) -> ( S.1 ` h ) <_ ( S.2 ` G ) )
22 18 19 20 21 syl3anc 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) ) /\ ( h e. dom S.1 /\ h oR <_ G ) ) -> ( S.1 ` h ) <_ ( S.2 ` G ) )
23 22 expr 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) ) /\ h e. dom S.1 ) -> ( h oR <_ G -> ( S.1 ` h ) <_ ( S.2 ` G ) ) )
24 17 23 syld 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) ) /\ h e. dom S.1 ) -> ( ( h oR <_ F /\ F oR <_ G ) -> ( S.1 ` h ) <_ ( S.2 ` G ) ) )
25 24 ancomsd 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) ) /\ h e. dom S.1 ) -> ( ( F oR <_ G /\ h oR <_ F ) -> ( S.1 ` h ) <_ ( S.2 ` G ) ) )
26 25 exp4b 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) ) -> ( h e. dom S.1 -> ( F oR <_ G -> ( h oR <_ F -> ( S.1 ` h ) <_ ( S.2 ` G ) ) ) ) )
27 26 com23 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) ) -> ( F oR <_ G -> ( h e. dom S.1 -> ( h oR <_ F -> ( S.1 ` h ) <_ ( S.2 ` G ) ) ) ) )
28 27 3impia 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) /\ F oR <_ G ) -> ( h e. dom S.1 -> ( h oR <_ F -> ( S.1 ` h ) <_ ( S.2 ` G ) ) ) )
29 28 ralrimiv 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) /\ F oR <_ G ) -> A. h e. dom S.1 ( h oR <_ F -> ( S.1 ` h ) <_ ( S.2 ` G ) ) )
30 simp1 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) /\ F oR <_ G ) -> F : RR --> ( 0 [,] +oo ) )
31 itg2cl 
 |-  ( G : RR --> ( 0 [,] +oo ) -> ( S.2 ` G ) e. RR* )
32 31 3ad2ant2 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) /\ F oR <_ G ) -> ( S.2 ` G ) e. RR* )
33 itg2leub 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( S.2 ` G ) e. RR* ) -> ( ( S.2 ` F ) <_ ( S.2 ` G ) <-> A. h e. dom S.1 ( h oR <_ F -> ( S.1 ` h ) <_ ( S.2 ` G ) ) ) )
34 30 32 33 syl2anc 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) /\ F oR <_ G ) -> ( ( S.2 ` F ) <_ ( S.2 ` G ) <-> A. h e. dom S.1 ( h oR <_ F -> ( S.1 ` h ) <_ ( S.2 ` G ) ) ) )
35 29 34 mpbird 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) /\ F oR <_ G ) -> ( S.2 ` F ) <_ ( S.2 ` G ) )