Theorem itg0

Description: The integral of anything on the empty set is zero. (Contributed by Mario Carneiro, 13-Aug-2014)

	Ref	Expression
Assertion	itg0	$$⊢{\int }_{\varnothing }Adx=0$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\Re \left(\frac{A}{{\mathrm{i}}^k}\right)=\Re \left(\frac{A}{{\mathrm{i}}^k}\right)$$
2	1	dfitg	$$⊢{\int }_{\varnothing }Adx=\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in \varnothing \wedge 0\le \Re \left(\frac{A}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{A}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
3		ifan	$$⊢if\left(\left(x\in \varnothing \wedge 0\le \Re \left(\frac{A}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{A}{{\mathrm{i}}^k}\right),0\right)=if\left(x\in \varnothing ,if\left(0\le \Re \left(\frac{A}{{\mathrm{i}}^k}\right),\Re \left(\frac{A}{{\mathrm{i}}^k}\right),0\right),0\right)$$
4		noel	$$⊢\neg x\in \varnothing$$
5	4	iffalsei	$$⊢if\left(x\in \varnothing ,if\left(0\le \Re \left(\frac{A}{{\mathrm{i}}^k}\right),\Re \left(\frac{A}{{\mathrm{i}}^k}\right),0\right),0\right)=0$$
6	3 5	eqtri	$$⊢if\left(\left(x\in \varnothing \wedge 0\le \Re \left(\frac{A}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{A}{{\mathrm{i}}^k}\right),0\right)=0$$
7	6	mpteq2i	$$⊢\left(x\in ℝ⟼if\left(\left(x\in \varnothing \wedge 0\le \Re \left(\frac{A}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{A}{{\mathrm{i}}^k}\right),0\right)\right)=\left(x\in ℝ⟼0\right)$$
8		fconstmpt	$$⊢ℝ\times \left\{0\right\}=\left(x\in ℝ⟼0\right)$$
9	7 8	eqtr4i	$$⊢\left(x\in ℝ⟼if\left(\left(x\in \varnothing \wedge 0\le \Re \left(\frac{A}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{A}{{\mathrm{i}}^k}\right),0\right)\right)=ℝ\times \left\{0\right\}$$
10	9	fveq2i	$$⊢{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in \varnothing \wedge 0\le \Re \left(\frac{A}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{A}{{\mathrm{i}}^k}\right),0\right)\right)\right)={\int }^2\left(ℝ\times \left\{0\right\}\right)$$
11		itg20	$$⊢{\int }^2\left(ℝ\times \left\{0\right\}\right)=0$$
12	10 11	eqtri	$$⊢{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in \varnothing \wedge 0\le \Re \left(\frac{A}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{A}{{\mathrm{i}}^k}\right),0\right)\right)\right)=0$$
13	12	oveq2i	$$⊢{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in \varnothing \wedge 0\le \Re \left(\frac{A}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{A}{{\mathrm{i}}^k}\right),0\right)\right)\right)={\mathrm{i}}^k\cdot 0$$
14		ax-icn	$$⊢\mathrm{i}\in ℂ$$
15		elfznn0	$$⊢k\in \left(0\dots 3\right)\to k\in {\mathbb{N}}_0$$
16		expcl	$$⊢\left(\mathrm{i}\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{i}}^k\in ℂ$$
17	14 15 16	sylancr	$$⊢k\in \left(0\dots 3\right)\to {\mathrm{i}}^k\in ℂ$$
18	17	mul01d	$$⊢k\in \left(0\dots 3\right)\to {\mathrm{i}}^k\cdot 0=0$$
19	13 18	syl5eq	$$⊢k\in \left(0\dots 3\right)\to {\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in \varnothing \wedge 0\le \Re \left(\frac{A}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{A}{{\mathrm{i}}^k}\right),0\right)\right)\right)=0$$
20	19	sumeq2i	$$⊢\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in \varnothing \wedge 0\le \Re \left(\frac{A}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{A}{{\mathrm{i}}^k}\right),0\right)\right)\right)=\sum _{k=0}^{3}0$$
21		fzfi	$$⊢\left(0\dots 3\right)\in \mathrm{Fin}$$
22	21	olci	$$⊢\left(\left(0\dots 3\right)\subseteq {\mathbb{Z}}_{\ge 0}\vee \left(0\dots 3\right)\in \mathrm{Fin}\right)$$
23		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$$
24	22 23	ax-mp	$$⊢\sum _{k=0}^{3}0=0$$
25	20 24	eqtri	$$⊢\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in \varnothing \wedge 0\le \Re \left(\frac{A}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{A}{{\mathrm{i}}^k}\right),0\right)\right)\right)=0$$
26	2 25	eqtri	$$⊢{\int }_{\varnothing }Adx=0$$