Theorem itgge0

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

	Ref	Expression
Hypotheses	itgge0.1	$$⊢\phi \to \left(x\in A⟼B\right)\in {𝐿}^1$$
	itgge0.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
	itgge0.3	$$⊢\left(\phi \wedge x\in A\right)\to 0\le B$$
Assertion	itgge0	$$⊢\phi \to 0\le {\int }_{A}Bdx$$

Proof

Step	Hyp	Ref	Expression
1		itgge0.1	$$⊢\phi \to \left(x\in A⟼B\right)\in {𝐿}^1$$
2		itgge0.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
3		itgge0.3	$$⊢\left(\phi \wedge x\in A\right)\to 0\le B$$
4		itgz	$$⊢{\int }_{A}0dx=0$$
5		fconstmpt	$$⊢A\times \left\{0\right\}=\left(x\in A⟼0\right)$$
6		iblmbf	$$⊢\left(x\in A⟼B\right)\in {𝐿}^1\to \left(x\in A⟼B\right)\in MblFn$$
7	1 6	syl	$$⊢\phi \to \left(x\in A⟼B\right)\in MblFn$$
8	7 2	mbfdm2	$$⊢\phi \to A\in \mathrm{dom}vol$$
9		ibl0	$$⊢A\in \mathrm{dom}vol\to A\times \left\{0\right\}\in {𝐿}^1$$
10	8 9	syl	$$⊢\phi \to A\times \left\{0\right\}\in {𝐿}^1$$
11	5 10	eqeltrrid	$$⊢\phi \to \left(x\in A⟼0\right)\in {𝐿}^1$$
12		0red	$$⊢\left(\phi \wedge x\in A\right)\to 0\in ℝ$$
13	11 1 12 2 3	itgle	$$⊢\phi \to {\int }_{A}0dx\le {\int }_{A}Bdx$$
14	4 13	eqbrtrrid	$$⊢\phi \to 0\le {\int }_{A}Bdx$$