Theorem nfitg

Description: Bound-variable hypothesis builder for an integral: if y is (effectively) not free in A and B , it is not free in S. A B _d x . (Contributed by Mario Carneiro, 28-Jun-2014)

	Ref	Expression
Hypotheses	nfitg.1	$$⊢\underset{\_}{Ⅎ}yA$$
	nfitg.2	$$⊢\underset{\_}{Ⅎ}yB$$
Assertion	nfitg	$$⊢\underset{\_}{Ⅎ}y{\int }_{A}Bdx$$

Proof

Step	Hyp	Ref	Expression
1		nfitg.1	$$⊢\underset{\_}{Ⅎ}yA$$
2		nfitg.2	$$⊢\underset{\_}{Ⅎ}yB$$
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		nfcv	$$⊢\underset{\_}{Ⅎ}y\left(0\dots 3\right)$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}y{\mathrm{i}}^k$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}y\times$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}y{\int }^2$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}yℝ$$
10	1	nfcri	$$⊢Ⅎyx\in A$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}y0$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}y\le$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}y\Re$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}y÷$$
15	2 14 6	nfov	$$⊢\underset{\_}{Ⅎ}y\left(\frac{B}{{\mathrm{i}}^k}\right)$$
16	13 15	nffv	$$⊢\underset{\_}{Ⅎ}y\Re \left(\frac{B}{{\mathrm{i}}^k}\right)$$
17	11 12 16	nfbr	$$⊢Ⅎy0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)$$
18	10 17	nfan	$$⊢Ⅎy\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right)$$
19	18 16 11	nfif	$$⊢\underset{\_}{Ⅎ}yif\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)$$
20	9 19	nfmpt	$$⊢\underset{\_}{Ⅎ}y\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)$$
21	8 20	nffv	$$⊢\underset{\_}{Ⅎ}y{\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)$$
22	6 7 21	nfov	$$⊢\underset{\_}{Ⅎ}y{\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)$$
23	5 22	nfsum	$$⊢\underset{\_}{Ⅎ}y\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)$$
24	4 23	nfcxfr	$$⊢\underset{\_}{Ⅎ}y{\int }_{A}Bdx$$