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	⊢ Ⅎ 𝑦 𝐴
	nfitg.2	⊢ Ⅎ 𝑦 𝐵
Assertion	nfitg	⊢ Ⅎ 𝑦 ∫ 𝐴 𝐵 d 𝑥

Proof

Step	Hyp	Ref	Expression
1		nfitg.1	⊢ Ⅎ 𝑦 𝐴
2		nfitg.2	⊢ Ⅎ 𝑦 𝐵
3		eqid	⊢ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) )
4	3	dfitg	⊢ ∫ 𝐴 𝐵 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
5		nfcv	⊢ Ⅎ 𝑦 ( 0 ... 3 )
6		nfcv	⊢ Ⅎ 𝑦 ( i ↑ 𝑘 )
7		nfcv	⊢ Ⅎ 𝑦 ·
8		nfcv	⊢ Ⅎ 𝑦 ∫2
9		nfcv	⊢ Ⅎ 𝑦 ℝ
10	1	nfcri	⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴
11		nfcv	⊢ Ⅎ 𝑦 0
12		nfcv	⊢ Ⅎ 𝑦 ≤
13		nfcv	⊢ Ⅎ 𝑦 ℜ
14		nfcv	⊢ Ⅎ 𝑦 /
15	2 14 6	nfov	⊢ Ⅎ 𝑦 ( 𝐵 / ( i ↑ 𝑘 ) )
16	13 15	nffv	⊢ Ⅎ 𝑦 ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) )
17	11 12 16	nfbr	⊢ Ⅎ 𝑦 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) )
18	10 17	nfan	⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) )
19	18 16 11	nfif	⊢ Ⅎ 𝑦 if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 )
20	9 19	nfmpt	⊢ Ⅎ 𝑦 ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) )
21	8 20	nffv	⊢ Ⅎ 𝑦 ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
22	6 7 21	nfov	⊢ Ⅎ 𝑦 ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
23	5 22	nfsum	⊢ Ⅎ 𝑦 Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
24	4 23	nfcxfr	⊢ Ⅎ 𝑦 ∫ 𝐴 𝐵 d 𝑥