Theorem itgss

Description: Expand the set of an integral by adding zeroes outside the domain. (Contributed by Mario Carneiro, 11-Aug-2014) (Revised by Mario Carneiro, 23-Aug-2014)

	Ref	Expression
Hypotheses	itgss.1	$$⊢\phi \to A\subseteq B$$
	itgss.2	$$⊢\left(\phi \wedge x\in \left(B\setminus A\right)\right)\to C=0$$
Assertion	itgss	$$⊢\phi \to {\int }_{A}Cdx={\int }_{B}Cdx$$

Proof

Step	Hyp	Ref	Expression
1		itgss.1	$$⊢\phi \to A\subseteq B$$
2		itgss.2	$$⊢\left(\phi \wedge x\in \left(B\setminus A\right)\right)\to C=0$$
3		elfzelz	$$⊢k\in \left(0\dots 3\right)\to k\in \mathbb{Z}$$
4		iffalse	$$⊢\neg x\in A\to if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=0$$
5	4	ad2antll	$$⊢\left(\left(\phi \wedge k\in \mathbb{Z}\right)\wedge \left(x\in B\wedge \neg x\in A\right)\right)\to if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=0$$
6		eldif	$$⊢x\in \left(B\setminus A\right)\leftrightarrow \left(x\in B\wedge \neg x\in A\right)$$
7	2	adantlr	$$⊢\left(\left(\phi \wedge k\in \mathbb{Z}\right)\wedge x\in \left(B\setminus A\right)\right)\to C=0$$
8	7	oveq1d	$$⊢\left(\left(\phi \wedge k\in \mathbb{Z}\right)\wedge x\in \left(B\setminus A\right)\right)\to \frac{C}{{\mathrm{i}}^k}=\frac{0}{{\mathrm{i}}^k}$$
9		ax-icn	$$⊢\mathrm{i}\in ℂ$$
10		ine0	$$⊢\mathrm{i}\ne 0$$
11		expclz	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\wedge k\in \mathbb{Z}\right)\to {\mathrm{i}}^k\in ℂ$$
12	9 10 11	mp3an12	$$⊢k\in \mathbb{Z}\to {\mathrm{i}}^k\in ℂ$$
13		expne0i	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\wedge k\in \mathbb{Z}\right)\to {\mathrm{i}}^k\ne 0$$
14	9 10 13	mp3an12	$$⊢k\in \mathbb{Z}\to {\mathrm{i}}^k\ne 0$$
15	12 14	div0d	$$⊢k\in \mathbb{Z}\to \frac{0}{{\mathrm{i}}^k}=0$$
16	15	ad2antlr	$$⊢\left(\left(\phi \wedge k\in \mathbb{Z}\right)\wedge x\in \left(B\setminus A\right)\right)\to \frac{0}{{\mathrm{i}}^k}=0$$
17	8 16	eqtrd	$$⊢\left(\left(\phi \wedge k\in \mathbb{Z}\right)\wedge x\in \left(B\setminus A\right)\right)\to \frac{C}{{\mathrm{i}}^k}=0$$
18	17	fveq2d	$$⊢\left(\left(\phi \wedge k\in \mathbb{Z}\right)\wedge x\in \left(B\setminus A\right)\right)\to \Re \left(\frac{C}{{\mathrm{i}}^k}\right)=\Re \left(0\right)$$
19		re0	$$⊢\Re \left(0\right)=0$$
20	18 19	eqtrdi	$$⊢\left(\left(\phi \wedge k\in \mathbb{Z}\right)\wedge x\in \left(B\setminus A\right)\right)\to \Re \left(\frac{C}{{\mathrm{i}}^k}\right)=0$$
21	20	ifeq1d	$$⊢\left(\left(\phi \wedge k\in \mathbb{Z}\right)\wedge x\in \left(B\setminus A\right)\right)\to if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)=if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),0,0\right)$$
22		ifid	$$⊢if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),0,0\right)=0$$
23	21 22	eqtrdi	$$⊢\left(\left(\phi \wedge k\in \mathbb{Z}\right)\wedge x\in \left(B\setminus A\right)\right)\to if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)=0$$
24	6 23	sylan2br	$$⊢\left(\left(\phi \wedge k\in \mathbb{Z}\right)\wedge \left(x\in B\wedge \neg x\in A\right)\right)\to if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)=0$$
25	5 24	eqtr4d	$$⊢\left(\left(\phi \wedge k\in \mathbb{Z}\right)\wedge \left(x\in B\wedge \neg x\in A\right)\right)\to if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
26	25	expr	$$⊢\left(\left(\phi \wedge k\in \mathbb{Z}\right)\wedge x\in B\right)\to \left(\neg x\in A\to if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)$$
27		iftrue	$$⊢x\in A\to if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
28	26 27	pm2.61d2	$$⊢\left(\left(\phi \wedge k\in \mathbb{Z}\right)\wedge x\in B\right)\to if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
29		iftrue	$$⊢x\in B\to if\left(x\in B,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
30	29	adantl	$$⊢\left(\left(\phi \wedge k\in \mathbb{Z}\right)\wedge x\in B\right)\to if\left(x\in B,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
31	28 30	eqtr4d	$$⊢\left(\left(\phi \wedge k\in \mathbb{Z}\right)\wedge x\in B\right)\to if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=if\left(x\in B,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)$$
32	1	adantr	$$⊢\left(\phi \wedge k\in \mathbb{Z}\right)\to A\subseteq B$$
33	32	sseld	$$⊢\left(\phi \wedge k\in \mathbb{Z}\right)\to \left(x\in A\to x\in B\right)$$
34	33	con3dimp	$$⊢\left(\left(\phi \wedge k\in \mathbb{Z}\right)\wedge \neg x\in B\right)\to \neg x\in A$$
35	34 4	syl	$$⊢\left(\left(\phi \wedge k\in \mathbb{Z}\right)\wedge \neg x\in B\right)\to if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=0$$
36		iffalse	$$⊢\neg x\in B\to if\left(x\in B,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=0$$
37	36	adantl	$$⊢\left(\left(\phi \wedge k\in \mathbb{Z}\right)\wedge \neg x\in B\right)\to if\left(x\in B,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=0$$
38	35 37	eqtr4d	$$⊢\left(\left(\phi \wedge k\in \mathbb{Z}\right)\wedge \neg x\in B\right)\to if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=if\left(x\in B,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)$$
39	31 38	pm2.61dan	$$⊢\left(\phi \wedge k\in \mathbb{Z}\right)\to if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=if\left(x\in B,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)$$
40		ifan	$$⊢if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)=if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)$$
41		ifan	$$⊢if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)=if\left(x\in B,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)$$
42	39 40 41	3eqtr4g	$$⊢\left(\phi \wedge k\in \mathbb{Z}\right)\to if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)=if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
43	42	mpteq2dv	$$⊢\left(\phi \wedge k\in \mathbb{Z}\right)\to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)$$
44	43	fveq2d	$$⊢\left(\phi \wedge k\in \mathbb{Z}\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
45	44	oveq2d	$$⊢\left(\phi \wedge k\in \mathbb{Z}\right)\to {\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)={\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
46	3 45	sylan2	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to {\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)={\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
47	46	sumeq2dv	$$⊢\phi \to \sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)=\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
48		eqid	$$⊢\Re \left(\frac{C}{{\mathrm{i}}^k}\right)=\Re \left(\frac{C}{{\mathrm{i}}^k}\right)$$
49	48	dfitg	$$⊢{\int }_{A}Cdx=\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
50	48	dfitg	$$⊢{\int }_{B}Cdx=\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
51	47 49 50	3eqtr4g	$$⊢\phi \to {\int }_{A}Cdx={\int }_{B}Cdx$$