This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itgless

Description: Expand the integral of a nonnegative function. (Contributed by Mario Carneiro, 31-Aug-2014)

Ref Expression
Hypotheses itgless.1 
|- ( ph -> A C_ B )
itgless.2 
|- ( ph -> A e. dom vol )
itgless.3 
|- ( ( ph /\ x e. B ) -> C e. RR )
itgless.4 
|- ( ( ph /\ x e. B ) -> 0 <_ C )
itgless.5 
|- ( ph -> ( x e. B |-> C ) e. L^1 )
Assertion itgless 
|- ( ph -> S. A C _d x <_ S. B C _d x )

Proof

Step Hyp Ref Expression
1 itgless.1 
 |-  ( ph -> A C_ B )
2 itgless.2 
 |-  ( ph -> A e. dom vol )
3 itgless.3 
 |-  ( ( ph /\ x e. B ) -> C e. RR )
4 itgless.4 
 |-  ( ( ph /\ x e. B ) -> 0 <_ C )
5 itgless.5 
 |-  ( ph -> ( x e. B |-> C ) e. L^1 )
6 itgss2 
 |-  ( A C_ B -> S. A C _d x = S. B if ( x e. A , C , 0 ) _d x )
7 1 6 syl 
 |-  ( ph -> S. A C _d x = S. B if ( x e. A , C , 0 ) _d x )
8 iblmbf 
 |-  ( ( x e. B |-> C ) e. L^1 -> ( x e. B |-> C ) e. MblFn )
9 5 8 syl 
 |-  ( ph -> ( x e. B |-> C ) e. MblFn )
10 9 3 mbfdm2 
 |-  ( ph -> B e. dom vol )
11 1 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. B )
12 11 3 syldan 
 |-  ( ( ph /\ x e. A ) -> C e. RR )
13 0re 
 |-  0 e. RR
14 ifcl 
 |-  ( ( C e. RR /\ 0 e. RR ) -> if ( x e. A , C , 0 ) e. RR )
15 12 13 14 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , C , 0 ) e. RR )
16 eldifn 
 |-  ( x e. ( B \ A ) -> -. x e. A )
17 16 adantl 
 |-  ( ( ph /\ x e. ( B \ A ) ) -> -. x e. A )
18 17 iffalsed 
 |-  ( ( ph /\ x e. ( B \ A ) ) -> if ( x e. A , C , 0 ) = 0 )
19 iftrue 
 |-  ( x e. A -> if ( x e. A , C , 0 ) = C )
20 19 mpteq2ia 
 |-  ( x e. A |-> if ( x e. A , C , 0 ) ) = ( x e. A |-> C )
21 1 2 3 5 iblss 
 |-  ( ph -> ( x e. A |-> C ) e. L^1 )
22 20 21 eqeltrid 
 |-  ( ph -> ( x e. A |-> if ( x e. A , C , 0 ) ) e. L^1 )
23 1 10 15 18 22 iblss2 
 |-  ( ph -> ( x e. B |-> if ( x e. A , C , 0 ) ) e. L^1 )
24 3 13 14 sylancl 
 |-  ( ( ph /\ x e. B ) -> if ( x e. A , C , 0 ) e. RR )
25 3 leidd 
 |-  ( ( ph /\ x e. B ) -> C <_ C )
26 breq1 
 |-  ( C = if ( x e. A , C , 0 ) -> ( C <_ C <-> if ( x e. A , C , 0 ) <_ C ) )
27 breq1 
 |-  ( 0 = if ( x e. A , C , 0 ) -> ( 0 <_ C <-> if ( x e. A , C , 0 ) <_ C ) )
28 26 27 ifboth 
 |-  ( ( C <_ C /\ 0 <_ C ) -> if ( x e. A , C , 0 ) <_ C )
29 25 4 28 syl2anc 
 |-  ( ( ph /\ x e. B ) -> if ( x e. A , C , 0 ) <_ C )
30 23 5 24 3 29 itgle 
 |-  ( ph -> S. B if ( x e. A , C , 0 ) _d x <_ S. B C _d x )
31 7 30 eqbrtrd 
 |-  ( ph -> S. A C _d x <_ S. B C _d x )