itgge0

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

Step	Hyp	Ref	Expression
1		itgge0.1	$⊢ φ \to (x \in A ⟼ B) \in 𝐿^{1}$
2		itgge0.2	$⊢ (φ \land x \in A) \to B \in ℝ$
3		itgge0.3	$⊢ (φ \land x \in A) \to 0 \leq B$
4		itgz	$⊢ \int_{A} 0 d x = 0$
5		fconstmpt	$⊢ A \times \{0\} = (x \in A ⟼ 0)$
6		iblmbf	$⊢ (x \in A ⟼ B) \in 𝐿^{1} \to (x \in A ⟼ B) \in MblFn$
7	1 6	syl	$⊢ φ \to (x \in A ⟼ B) \in MblFn$
8	7 2	mbfdm2	$⊢ φ \to A \in dom vol$
9		ibl0	$⊢ A \in dom vol \to A \times \{0\} \in 𝐿^{1}$
10	8 9	syl	$⊢ φ \to A \times \{0\} \in 𝐿^{1}$
11	5 10	eqeltrrid	$⊢ φ \to (x \in A ⟼ 0) \in 𝐿^{1}$
12		0red	$⊢ (φ \land x \in A) \to 0 \in ℝ$
13	11 1 12 2 3	itgle	$⊢ φ \to \int_{A} 0 d x \leq \int_{A} B d x$
14	4 13	eqbrtrrid	$⊢ φ \to 0 \leq \int_{A} B d x$

Metamath Proof Explorer