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 ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ 𝐿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 𝑥 )