Theorem itgless

Description: Expand the integral of a nonnegative function. (Contributed by Mario Carneiro, 31-Aug-2014)

	Ref	Expression
Hypotheses	itgless.1	$$⊢\phi \to A\subseteq B$$
	itgless.2	$$⊢\phi \to A\in \mathrm{dom}vol$$
	itgless.3	$$⊢\left(\phi \wedge x\in B\right)\to C\in ℝ$$
	itgless.4	$$⊢\left(\phi \wedge x\in B\right)\to 0\le C$$
	itgless.5	$$⊢\phi \to \left(x\in B⟼C\right)\in {𝐿}^1$$
Assertion	itgless	$$⊢\phi \to {\int }_{A}Cdx\le {\int }_{B}Cdx$$

Proof

Step	Hyp	Ref	Expression
1		itgless.1	$$⊢\phi \to A\subseteq B$$
2		itgless.2	$$⊢\phi \to A\in \mathrm{dom}vol$$
3		itgless.3	$$⊢\left(\phi \wedge x\in B\right)\to C\in ℝ$$
4		itgless.4	$$⊢\left(\phi \wedge x\in B\right)\to 0\le C$$
5		itgless.5	$$⊢\phi \to \left(x\in B⟼C\right)\in {𝐿}^1$$
6		itgss2	$$⊢A\subseteq B\to {\int }_{A}Cdx={\int }_{B}if\left(x\in A,C,0\right)dx$$
7	1 6	syl	$$⊢\phi \to {\int }_{A}Cdx={\int }_{B}if\left(x\in A,C,0\right)dx$$
8		iblmbf	$$⊢\left(x\in B⟼C\right)\in {𝐿}^1\to \left(x\in B⟼C\right)\in MblFn$$
9	5 8	syl	$$⊢\phi \to \left(x\in B⟼C\right)\in MblFn$$
10	9 3	mbfdm2	$$⊢\phi \to B\in \mathrm{dom}vol$$
11	1	sselda	$$⊢\left(\phi \wedge x\in A\right)\to x\in B$$
12	11 3	syldan	$$⊢\left(\phi \wedge x\in A\right)\to C\in ℝ$$
13		0re	$$⊢0\in ℝ$$
14		ifcl	$$⊢\left(C\in ℝ\wedge 0\in ℝ\right)\to if\left(x\in A,C,0\right)\in ℝ$$
15	12 13 14	sylancl	$$⊢\left(\phi \wedge x\in A\right)\to if\left(x\in A,C,0\right)\in ℝ$$
16		eldifn	$$⊢x\in \left(B\setminus A\right)\to \neg x\in A$$
17	16	adantl	$$⊢\left(\phi \wedge x\in \left(B\setminus A\right)\right)\to \neg x\in A$$
18	17	iffalsed	$$⊢\left(\phi \wedge x\in \left(B\setminus A\right)\right)\to if\left(x\in A,C,0\right)=0$$
19		iftrue	$$⊢x\in A\to if\left(x\in A,C,0\right)=C$$
20	19	mpteq2ia	$$⊢\left(x\in A⟼if\left(x\in A,C,0\right)\right)=\left(x\in A⟼C\right)$$
21	1 2 3 5	iblss	$$⊢\phi \to \left(x\in A⟼C\right)\in {𝐿}^1$$
22	20 21	eqeltrid	$$⊢\phi \to \left(x\in A⟼if\left(x\in A,C,0\right)\right)\in {𝐿}^1$$
23	1 10 15 18 22	iblss2	$$⊢\phi \to \left(x\in B⟼if\left(x\in A,C,0\right)\right)\in {𝐿}^1$$
24	3 13 14	sylancl	$$⊢\left(\phi \wedge x\in B\right)\to if\left(x\in A,C,0\right)\in ℝ$$
25	3	leidd	$$⊢\left(\phi \wedge x\in B\right)\to C\le C$$
26		breq1	$$⊢C=if\left(x\in A,C,0\right)\to \left(C\le C\leftrightarrow if\left(x\in A,C,0\right)\le C\right)$$
27		breq1	$$⊢0=if\left(x\in A,C,0\right)\to \left(0\le C\leftrightarrow if\left(x\in A,C,0\right)\le C\right)$$
28	26 27	ifboth	$$⊢\left(C\le C\wedge 0\le C\right)\to if\left(x\in A,C,0\right)\le C$$
29	25 4 28	syl2anc	$$⊢\left(\phi \wedge x\in B\right)\to if\left(x\in A,C,0\right)\le C$$
30	23 5 24 3 29	itgle	$$⊢\phi \to {\int }_{B}if\left(x\in A,C,0\right)dx\le {\int }_{B}Cdx$$
31	7 30	eqbrtrd	$$⊢\phi \to {\int }_{A}Cdx\le {\int }_{B}Cdx$$