Theorem itgz

Description: The integral of zero on any set is zero. (Contributed by Mario Carneiro, 29-Jun-2014) (Revised by Mario Carneiro, 23-Aug-2014)

	Ref	Expression
Assertion	itgz	$$⊢{\int }_{A}0dx=0$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\Re \left(\frac{0}{{\mathrm{i}}^k}\right)=\Re \left(\frac{0}{{\mathrm{i}}^k}\right)$$
2	1	dfitg	$$⊢{\int }_{A}0dx=\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{0}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{0}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
3		ax-icn	$$⊢\mathrm{i}\in ℂ$$
4		elfznn0	$$⊢k\in \left(0\dots 3\right)\to k\in {\mathbb{N}}_0$$
5		expcl	$$⊢\left(\mathrm{i}\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{i}}^k\in ℂ$$
6	3 4 5	sylancr	$$⊢k\in \left(0\dots 3\right)\to {\mathrm{i}}^k\in ℂ$$
7		ine0	$$⊢\mathrm{i}\ne 0$$
8		elfzelz	$$⊢k\in \left(0\dots 3\right)\to k\in \mathbb{Z}$$
9		expne0i	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\wedge k\in \mathbb{Z}\right)\to {\mathrm{i}}^k\ne 0$$
10	3 7 8 9	mp3an12i	$$⊢k\in \left(0\dots 3\right)\to {\mathrm{i}}^k\ne 0$$
11	6 10	div0d	$$⊢k\in \left(0\dots 3\right)\to \frac{0}{{\mathrm{i}}^k}=0$$
12	11	fveq2d	$$⊢k\in \left(0\dots 3\right)\to \Re \left(\frac{0}{{\mathrm{i}}^k}\right)=\Re \left(0\right)$$
13		re0	$$⊢\Re \left(0\right)=0$$
14	12 13	eqtrdi	$$⊢k\in \left(0\dots 3\right)\to \Re \left(\frac{0}{{\mathrm{i}}^k}\right)=0$$
15	14	ifeq1d	$$⊢k\in \left(0\dots 3\right)\to if\left(\left(x\in A\wedge 0\le \Re \left(\frac{0}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{0}{{\mathrm{i}}^k}\right),0\right)=if\left(\left(x\in A\wedge 0\le \Re \left(\frac{0}{{\mathrm{i}}^k}\right)\right),0,0\right)$$
16		ifid	$$⊢if\left(\left(x\in A\wedge 0\le \Re \left(\frac{0}{{\mathrm{i}}^k}\right)\right),0,0\right)=0$$
17	15 16	eqtrdi	$$⊢k\in \left(0\dots 3\right)\to if\left(\left(x\in A\wedge 0\le \Re \left(\frac{0}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{0}{{\mathrm{i}}^k}\right),0\right)=0$$
18	17	mpteq2dv	$$⊢k\in \left(0\dots 3\right)\to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{0}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{0}{{\mathrm{i}}^k}\right),0\right)\right)=\left(x\in ℝ⟼0\right)$$
19		fconstmpt	$$⊢ℝ\times \left\{0\right\}=\left(x\in ℝ⟼0\right)$$
20	18 19	eqtr4di	$$⊢k\in \left(0\dots 3\right)\to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{0}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{0}{{\mathrm{i}}^k}\right),0\right)\right)=ℝ\times \left\{0\right\}$$
21	20	fveq2d	$$⊢k\in \left(0\dots 3\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{0}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{0}{{\mathrm{i}}^k}\right),0\right)\right)\right)={\int }^2\left(ℝ\times \left\{0\right\}\right)$$
22		itg20	$$⊢{\int }^2\left(ℝ\times \left\{0\right\}\right)=0$$
23	21 22	eqtrdi	$$⊢k\in \left(0\dots 3\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{0}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{0}{{\mathrm{i}}^k}\right),0\right)\right)\right)=0$$
24	23	oveq2d	$$⊢k\in \left(0\dots 3\right)\to {\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{0}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{0}{{\mathrm{i}}^k}\right),0\right)\right)\right)={\mathrm{i}}^k\cdot 0$$
25	6	mul01d	$$⊢k\in \left(0\dots 3\right)\to {\mathrm{i}}^k\cdot 0=0$$
26	24 25	eqtrd	$$⊢k\in \left(0\dots 3\right)\to {\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{0}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{0}{{\mathrm{i}}^k}\right),0\right)\right)\right)=0$$
27	26	sumeq2i	$$⊢\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{0}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{0}{{\mathrm{i}}^k}\right),0\right)\right)\right)=\sum _{k=0}^{3}0$$
28		fzfi	$$⊢\left(0\dots 3\right)\in \mathrm{Fin}$$
29	28	olci	$$⊢\left(\left(0\dots 3\right)\subseteq {\mathbb{Z}}_{\ge 0}\vee \left(0\dots 3\right)\in \mathrm{Fin}\right)$$
30		sumz	$$⊢\left(\left(0\dots 3\right)\subseteq {\mathbb{Z}}_{\ge 0}\vee \left(0\dots 3\right)\in \mathrm{Fin}\right)\to \sum _{k=0}^{3}0=0$$
31	29 30	ax-mp	$$⊢\sum _{k=0}^{3}0=0$$
32	2 27 31	3eqtri	$$⊢{\int }_{A}0dx=0$$