Theorem iblitg

Description: If a function is integrable, then the S.2 integrals of the function's decompositions all exist. (Contributed by Mario Carneiro, 7-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

	Ref	Expression
Hypotheses	iblitg.1	$$⊢\phi \to G=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le T\right),T,0\right)\right)$$
	iblitg.2	$$⊢\left(\phi \wedge x\in A\right)\to T=\Re \left(\frac{B}{{\mathrm{i}}^K}\right)$$
	iblitg.3	$$⊢\phi \to \left(x\in A⟼B\right)\in {𝐿}^1$$
	iblitg.4	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
Assertion	iblitg	$$⊢\left(\phi \wedge K\in \mathbb{Z}\right)\to {\int }^2\left(G\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		iblitg.1	$$⊢\phi \to G=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le T\right),T,0\right)\right)$$
2		iblitg.2	$$⊢\left(\phi \wedge x\in A\right)\to T=\Re \left(\frac{B}{{\mathrm{i}}^K}\right)$$
3		iblitg.3	$$⊢\phi \to \left(x\in A⟼B\right)\in {𝐿}^1$$
4		iblitg.4	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
5	1	adantr	$$⊢\left(\phi \wedge K\in \mathbb{Z}\right)\to G=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le T\right),T,0\right)\right)$$
6	2	adantlr	$$⊢\left(\left(\phi \wedge K\in \mathbb{Z}\right)\wedge x\in A\right)\to T=\Re \left(\frac{B}{{\mathrm{i}}^K}\right)$$
7		iexpcyc	$$⊢K\in \mathbb{Z}\to {\mathrm{i}}^{K\mathrm{mod}4}={\mathrm{i}}^K$$
8	7	oveq2d	$$⊢K\in \mathbb{Z}\to \frac{B}{{\mathrm{i}}^{K\mathrm{mod}4}}=\frac{B}{{\mathrm{i}}^K}$$
9	8	fveq2d	$$⊢K\in \mathbb{Z}\to \Re \left(\frac{B}{{\mathrm{i}}^{K\mathrm{mod}4}}\right)=\Re \left(\frac{B}{{\mathrm{i}}^K}\right)$$
10	9	ad2antlr	$$⊢\left(\left(\phi \wedge K\in \mathbb{Z}\right)\wedge x\in A\right)\to \Re \left(\frac{B}{{\mathrm{i}}^{K\mathrm{mod}4}}\right)=\Re \left(\frac{B}{{\mathrm{i}}^K}\right)$$
11	6 10	eqtr4d	$$⊢\left(\left(\phi \wedge K\in \mathbb{Z}\right)\wedge x\in A\right)\to T=\Re \left(\frac{B}{{\mathrm{i}}^{K\mathrm{mod}4}}\right)$$
12	11	ibllem	$$⊢\left(\phi \wedge K\in \mathbb{Z}\right)\to if\left(\left(x\in A\wedge 0\le T\right),T,0\right)=if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^{K\mathrm{mod}4}}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^{K\mathrm{mod}4}}\right),0\right)$$
13	12	mpteq2dv	$$⊢\left(\phi \wedge K\in \mathbb{Z}\right)\to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le T\right),T,0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^{K\mathrm{mod}4}}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^{K\mathrm{mod}4}}\right),0\right)\right)$$
14	5 13	eqtrd	$$⊢\left(\phi \wedge K\in \mathbb{Z}\right)\to G=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^{K\mathrm{mod}4}}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^{K\mathrm{mod}4}}\right),0\right)\right)$$
15	14	fveq2d	$$⊢\left(\phi \wedge K\in \mathbb{Z}\right)\to {\int }^2\left(G\right)={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^{K\mathrm{mod}4}}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^{K\mathrm{mod}4}}\right),0\right)\right)\right)$$
16		oveq2	$$⊢k=K\mathrm{mod}4\to {\mathrm{i}}^k={\mathrm{i}}^{K\mathrm{mod}4}$$
17	16	oveq2d	$$⊢k=K\mathrm{mod}4\to \frac{B}{{\mathrm{i}}^k}=\frac{B}{{\mathrm{i}}^{K\mathrm{mod}4}}$$
18	17	fveq2d	$$⊢k=K\mathrm{mod}4\to \Re \left(\frac{B}{{\mathrm{i}}^k}\right)=\Re \left(\frac{B}{{\mathrm{i}}^{K\mathrm{mod}4}}\right)$$
19	18	breq2d	$$⊢k=K\mathrm{mod}4\to \left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\leftrightarrow 0\le \Re \left(\frac{B}{{\mathrm{i}}^{K\mathrm{mod}4}}\right)\right)$$
20	19	anbi2d	$$⊢k=K\mathrm{mod}4\to \left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right)\leftrightarrow \left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^{K\mathrm{mod}4}}\right)\right)\right)$$
21	20 18	ifbieq1d	$$⊢k=K\mathrm{mod}4\to 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)=if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^{K\mathrm{mod}4}}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^{K\mathrm{mod}4}}\right),0\right)$$
22	21	mpteq2dv	$$⊢k=K\mathrm{mod}4\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\mathrm{mod}4}}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^{K\mathrm{mod}4}}\right),0\right)\right)$$
23	22	fveq2d	$$⊢k=K\mathrm{mod}4\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)={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^{K\mathrm{mod}4}}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^{K\mathrm{mod}4}}\right),0\right)\right)\right)$$
24	23	eleq1d	$$⊢k=K\mathrm{mod}4\to \left({\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 ℝ\leftrightarrow {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^{K\mathrm{mod}4}}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^{K\mathrm{mod}4}}\right),0\right)\right)\right)\in ℝ\right)$$
25		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)$$
26		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)$$
27	25 26 4	isibl2	$$⊢\phi \to \left(\left(x\in A⟼B\right)\in {𝐿}^1\leftrightarrow \left(\left(x\in A⟼B\right)\in MblFn\wedge \forall k\in \left(0\dots 3\right){\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 ℝ\right)\right)$$
28	3 27	mpbid	$$⊢\phi \to \left(\left(x\in A⟼B\right)\in MblFn\wedge \forall k\in \left(0\dots 3\right){\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 ℝ\right)$$
29	28	simprd	$$⊢\phi \to \forall k\in \left(0\dots 3\right){\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 ℝ$$
30	29	adantr	$$⊢\left(\phi \wedge K\in \mathbb{Z}\right)\to \forall k\in \left(0\dots 3\right){\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 ℝ$$
31		4nn	$$⊢4\in \mathbb{N}$$
32		zmodfz	$$⊢\left(K\in \mathbb{Z}\wedge 4\in \mathbb{N}\right)\to K\mathrm{mod}4\in \left(0\dots 4-1\right)$$
33	31 32	mpan2	$$⊢K\in \mathbb{Z}\to K\mathrm{mod}4\in \left(0\dots 4-1\right)$$
34		4m1e3	$$⊢4-1=3$$
35	34	oveq2i	$$⊢\left(0\dots 4-1\right)=\left(0\dots 3\right)$$
36	33 35	eleqtrdi	$$⊢K\in \mathbb{Z}\to K\mathrm{mod}4\in \left(0\dots 3\right)$$
37	36	adantl	$$⊢\left(\phi \wedge K\in \mathbb{Z}\right)\to K\mathrm{mod}4\in \left(0\dots 3\right)$$
38	24 30 37	rspcdva	$$⊢\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\mathrm{mod}4}}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^{K\mathrm{mod}4}}\right),0\right)\right)\right)\in ℝ$$
39	15 38	eqeltrd	$$⊢\left(\phi \wedge K\in \mathbb{Z}\right)\to {\int }^2\left(G\right)\in ℝ$$