Theorem itgcl

Description: The integral of an integrable function is a complex number. This is Metamath 100 proof #86. (Contributed by Mario Carneiro, 29-Jun-2014)

	Ref	Expression
Hypotheses	itgmpt.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
	itgcl.2	$$⊢\phi \to \left(x\in A⟼B\right)\in {𝐿}^1$$
Assertion	itgcl	$$⊢\phi \to {\int }_{A}Bdx\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		itgmpt.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
2		itgcl.2	$$⊢\phi \to \left(x\in A⟼B\right)\in {𝐿}^1$$
3		eqid	$$⊢\Re \left(\frac{B}{{\mathrm{i}}^k}\right)=\Re \left(\frac{B}{{\mathrm{i}}^k}\right)$$
4	3	dfitg	$$⊢{\int }_{A}Bdx=\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{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
5		fzfid	$$⊢\phi \to \left(0\dots 3\right)\in \mathrm{Fin}$$
6		ax-icn	$$⊢\mathrm{i}\in ℂ$$
7		elfznn0	$$⊢k\in \left(0\dots 3\right)\to k\in {\mathbb{N}}_0$$
8	7	adantl	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to k\in {\mathbb{N}}_0$$
9		expcl	$$⊢\left(\mathrm{i}\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{i}}^k\in ℂ$$
10	6 8 9	sylancr	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to {\mathrm{i}}^k\in ℂ$$
11		elfzelz	$$⊢k\in \left(0\dots 3\right)\to k\in \mathbb{Z}$$
12		eqidd	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)$$
13		eqidd	$$⊢\left(\phi \wedge x\in A\right)\to \Re \left(\frac{B}{{\mathrm{i}}^k}\right)=\Re \left(\frac{B}{{\mathrm{i}}^k}\right)$$
14	12 13 2 1	iblitg	$$⊢\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{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ$$
15	11 14	sylan2	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ$$
16	15	recnd	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℂ$$
17	10 16	mulcld	$$⊢\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{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℂ$$
18	5 17	fsumcl	$$⊢\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{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℂ$$
19	4 18	eqeltrid	$$⊢\phi \to {\int }_{A}Bdx\in ℂ$$