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 )