Theorem itggt0

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

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

Proof

Step	Hyp	Ref	Expression
1		itggt0.1	$$⊢\phi \to 0<vol\left(A\right)$$
2		itggt0.2	$$⊢\phi \to \left(x\in A⟼B\right)\in {𝐿}^1$$
3		itggt0.3	$$⊢\left(\phi \wedge x\in A\right)\to B\in {ℝ}^{+}$$
4		iblmbf	$$⊢\left(x\in A⟼B\right)\in {𝐿}^1\to \left(x\in A⟼B\right)\in MblFn$$
5	2 4	syl	$$⊢\phi \to \left(x\in A⟼B\right)\in MblFn$$
6	5 3	mbfdm2	$$⊢\phi \to A\in \mathrm{dom}vol$$
7	3	rpred	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
8	3	rpge0d	$$⊢\left(\phi \wedge x\in A\right)\to 0\le B$$
9		elrege0	$$⊢B\in \left[0,\mathrm{+\infty }\right)\leftrightarrow \left(B\in ℝ\wedge 0\le B\right)$$
10	7 8 9	sylanbrc	$$⊢\left(\phi \wedge x\in A\right)\to B\in \left[0,\mathrm{+\infty }\right)$$
11		0e0icopnf	$$⊢0\in \left[0,\mathrm{+\infty }\right)$$
12	11	a1i	$$⊢\left(\phi \wedge \neg x\in A\right)\to 0\in \left[0,\mathrm{+\infty }\right)$$
13	10 12	ifclda	$$⊢\phi \to if\left(x\in A,B,0\right)\in \left[0,\mathrm{+\infty }\right)$$
14	13	adantr	$$⊢\left(\phi \wedge x\in ℝ\right)\to if\left(x\in A,B,0\right)\in \left[0,\mathrm{+\infty }\right)$$
15	14	fmpttd	$$⊢\phi \to \left(x\in ℝ⟼if\left(x\in A,B,0\right)\right):ℝ⟶\left[0,\mathrm{+\infty }\right)$$
16		mblss	$$⊢A\in \mathrm{dom}vol\to A\subseteq ℝ$$
17	6 16	syl	$$⊢\phi \to A\subseteq ℝ$$
18		rembl	$$⊢ℝ\in \mathrm{dom}vol$$
19	18	a1i	$$⊢\phi \to ℝ\in \mathrm{dom}vol$$
20	13	adantr	$$⊢\left(\phi \wedge x\in A\right)\to if\left(x\in A,B,0\right)\in \left[0,\mathrm{+\infty }\right)$$
21		eldifn	$$⊢x\in \left(ℝ\setminus A\right)\to \neg x\in A$$
22	21	adantl	$$⊢\left(\phi \wedge x\in \left(ℝ\setminus A\right)\right)\to \neg x\in A$$
23	22	iffalsed	$$⊢\left(\phi \wedge x\in \left(ℝ\setminus A\right)\right)\to if\left(x\in A,B,0\right)=0$$
24		iftrue	$$⊢x\in A\to if\left(x\in A,B,0\right)=B$$
25	24	mpteq2ia	$$⊢\left(x\in A⟼if\left(x\in A,B,0\right)\right)=\left(x\in A⟼B\right)$$
26	25 5	eqeltrid	$$⊢\phi \to \left(x\in A⟼if\left(x\in A,B,0\right)\right)\in MblFn$$
27	17 19 20 23 26	mbfss	$$⊢\phi \to \left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\in MblFn$$
28	3	rpgt0d	$$⊢\left(\phi \wedge x\in A\right)\to 0<B$$
29	17	sselda	$$⊢\left(\phi \wedge x\in A\right)\to x\in ℝ$$
30	24	adantl	$$⊢\left(\phi \wedge x\in A\right)\to if\left(x\in A,B,0\right)=B$$
31	30 3	eqeltrd	$$⊢\left(\phi \wedge x\in A\right)\to if\left(x\in A,B,0\right)\in {ℝ}^{+}$$
32		eqid	$$⊢\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)=\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)$$
33	32	fvmpt2	$$⊢\left(x\in ℝ\wedge if\left(x\in A,B,0\right)\in {ℝ}^{+}\right)\to \left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\left(x\right)=if\left(x\in A,B,0\right)$$
34	29 31 33	syl2anc	$$⊢\left(\phi \wedge x\in A\right)\to \left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\left(x\right)=if\left(x\in A,B,0\right)$$
35	34 30	eqtrd	$$⊢\left(\phi \wedge x\in A\right)\to \left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\left(x\right)=B$$
36	28 35	breqtrrd	$$⊢\left(\phi \wedge x\in A\right)\to 0<\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\left(x\right)$$
37	36	ralrimiva	$$⊢\phi \to \forall x\in A0<\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\left(x\right)$$
38		nfcv	$$⊢\underset{\_}{Ⅎ}x0$$
39		nfcv	$$⊢\underset{\_}{Ⅎ}x<$$
40		nffvmpt1	$$⊢\underset{\_}{Ⅎ}x\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\left(y\right)$$
41	38 39 40	nfbr	$$⊢Ⅎx0<\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\left(y\right)$$
42		nfv	$$⊢Ⅎy0<\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\left(x\right)$$
43		fveq2	$$⊢y=x\to \left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\left(y\right)=\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\left(x\right)$$
44	43	breq2d	$$⊢y=x\to \left(0<\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\left(y\right)\leftrightarrow 0<\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\left(x\right)\right)$$
45	41 42 44	cbvralw	$$⊢\forall y\in A0<\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\left(y\right)\leftrightarrow \forall x\in A0<\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\left(x\right)$$
46	37 45	sylibr	$$⊢\phi \to \forall y\in A0<\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\left(y\right)$$
47	46	r19.21bi	$$⊢\left(\phi \wedge y\in A\right)\to 0<\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\left(y\right)$$
48	6 1 15 27 47	itg2gt0	$$⊢\phi \to 0<{\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\right)$$
49	7 2 8	itgposval	$$⊢\phi \to {\int }_{A}Bdx={\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,B,0\right)\right)\right)$$
50	48 49	breqtrrd	$$⊢\phi \to 0<{\int }_{A}Bdx$$