Theorem nfitg1

Description: Bound-variable hypothesis builder for an integral. (Contributed by Mario Carneiro, 28-Jun-2014)

	Ref	Expression
Assertion	nfitg1	$$⊢\underset{\_}{Ⅎ}x{\int }_{A}Bdx$$

Proof

Step	Hyp	Ref	Expression
1		df-itg	$$⊢{\int }_{A}Bdx=\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/z⦌if\left(\left(x\in A\wedge 0\le z\right),z,0\right)\right)\right)$$
2		nfcv	$$⊢\underset{\_}{Ⅎ}x\left(0\dots 3\right)$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}x{\mathrm{i}}^k$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}x\times$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}x{\int }^2$$
6		nfmpt1	$$⊢\underset{\_}{Ⅎ}x\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/z⦌if\left(\left(x\in A\wedge 0\le z\right),z,0\right)\right)$$
7	5 6	nffv	$$⊢\underset{\_}{Ⅎ}x{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/z⦌if\left(\left(x\in A\wedge 0\le z\right),z,0\right)\right)\right)$$
8	3 4 7	nfov	$$⊢\underset{\_}{Ⅎ}x{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/z⦌if\left(\left(x\in A\wedge 0\le z\right),z,0\right)\right)\right)$$
9	2 8	nfsum	$$⊢\underset{\_}{Ⅎ}x\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/z⦌if\left(\left(x\in A\wedge 0\le z\right),z,0\right)\right)\right)$$
10	1 9	nfcxfr	$$⊢\underset{\_}{Ⅎ}x{\int }_{A}Bdx$$