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

Metamath Proof Explorer

Theorem itgge0

Description: The integral of a positive function is positive. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses itgge0.1 
|- ( ph -> ( x e. A |-> B ) e. L^1 )
itgge0.2 
|- ( ( ph /\ x e. A ) -> B e. RR )
itgge0.3 
|- ( ( ph /\ x e. A ) -> 0 <_ B )
Assertion itgge0 
|- ( ph -> 0 <_ S. A B _d x )

Proof

Step Hyp Ref Expression
1 itgge0.1 
 |-  ( ph -> ( x e. A |-> B ) e. L^1 )
2 itgge0.2 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
3 itgge0.3 
 |-  ( ( ph /\ x e. A ) -> 0 <_ B )
4 itgz 
 |-  S. A 0 _d x = 0
5 fconstmpt 
 |-  ( A X. { 0 } ) = ( x e. A |-> 0 )
6 iblmbf 
 |-  ( ( x e. A |-> B ) e. L^1 -> ( x e. A |-> B ) e. MblFn )
7 1 6 syl 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
8 7 2 mbfdm2 
 |-  ( ph -> A e. dom vol )
9 ibl0 
 |-  ( A e. dom vol -> ( A X. { 0 } ) e. L^1 )
10 8 9 syl 
 |-  ( ph -> ( A X. { 0 } ) e. L^1 )
11 5 10 eqeltrrid 
 |-  ( ph -> ( x e. A |-> 0 ) e. L^1 )
12 0red 
 |-  ( ( ph /\ x e. A ) -> 0 e. RR )
13 11 1 12 2 3 itgle 
 |-  ( ph -> S. A 0 _d x <_ S. A B _d x )
14 4 13 eqbrtrrid 
 |-  ( ph -> 0 <_ S. A B _d x )