Theorem itgvallem

Description: Substitution lemma. (Contributed by Mario Carneiro, 7-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

	Ref	Expression
Hypothesis	itgvallem.1	$$⊢{\mathrm{i}}^K=T$$
Assertion	itgvallem	$$⊢k=K\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}{T}\right)\right),\Re \left(\frac{B}{T}\right),0\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		itgvallem.1	$$⊢{\mathrm{i}}^K=T$$
2		oveq2	$$⊢k=K\to {\mathrm{i}}^k={\mathrm{i}}^K$$
3	2 1	eqtrdi	$$⊢k=K\to {\mathrm{i}}^k=T$$
4	3	oveq2d	$$⊢k=K\to \frac{B}{{\mathrm{i}}^k}=\frac{B}{T}$$
5	4	fveq2d	$$⊢k=K\to \Re \left(\frac{B}{{\mathrm{i}}^k}\right)=\Re \left(\frac{B}{T}\right)$$
6	5	breq2d	$$⊢k=K\to \left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\leftrightarrow 0\le \Re \left(\frac{B}{T}\right)\right)$$
7	6	anbi2d	$$⊢k=K\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}{T}\right)\right)\right)$$
8	7 5	ifbieq1d	$$⊢k=K\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}{T}\right)\right),\Re \left(\frac{B}{T}\right),0\right)$$
9	8	mpteq2dv	$$⊢k=K\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}{T}\right)\right),\Re \left(\frac{B}{T}\right),0\right)\right)$$
10	9	fveq2d	$$⊢k=K\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}{T}\right)\right),\Re \left(\frac{B}{T}\right),0\right)\right)\right)$$