Theorem itgge0

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

	Ref	Expression
Hypotheses	itgge0.1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
	itgge0.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
	itgge0.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ 𝐵 )
Assertion	itgge0	⊢ ( 𝜑 → 0 ≤ ∫ 𝐴 𝐵 d 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		itgge0.1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
2		itgge0.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
3		itgge0.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ 𝐵 )
4		itgz	⊢ ∫ 𝐴 0 d 𝑥 = 0
5		fconstmpt	⊢ ( 𝐴 × { 0 } ) = ( 𝑥 ∈ 𝐴 ↦ 0 )
6		iblmbf	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
7	1 6	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
8	7 2	mbfdm2	⊢ ( 𝜑 → 𝐴 ∈ dom vol )
9		ibl0	⊢ ( 𝐴 ∈ dom vol → ( 𝐴 × { 0 } ) ∈ 𝐿1 )
10	8 9	syl	⊢ ( 𝜑 → ( 𝐴 × { 0 } ) ∈ 𝐿1 )
11	5 10	eqeltrrid	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 0 ) ∈ 𝐿1 )
12		0red	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ∈ ℝ )
13	11 1 12 2 3	itgle	⊢ ( 𝜑 → ∫ 𝐴 0 d 𝑥 ≤ ∫ 𝐴 𝐵 d 𝑥 )
14	4 13	eqbrtrrid	⊢ ( 𝜑 → 0 ≤ ∫ 𝐴 𝐵 d 𝑥 )