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