Theorem nfitg1

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

	Ref	Expression
Assertion	nfitg1	⊢ Ⅎ 𝑥 ∫ 𝐴 𝐵 d 𝑥

Proof

Step	Hyp	Ref	Expression
1		df-itg	⊢ ∫ 𝐴 𝐵 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑧 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑧 ) , 𝑧 , 0 ) ) ) )
2		nfcv	⊢ Ⅎ 𝑥 ( 0 ... 3 )
3		nfcv	⊢ Ⅎ 𝑥 ( i ↑ 𝑘 )
4		nfcv	⊢ Ⅎ 𝑥 ·
5		nfcv	⊢ Ⅎ 𝑥 ∫2
6		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑧 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑧 ) , 𝑧 , 0 ) )
7	5 6	nffv	⊢ Ⅎ 𝑥 ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑧 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑧 ) , 𝑧 , 0 ) ) )
8	3 4 7	nfov	⊢ Ⅎ 𝑥 ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑧 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑧 ) , 𝑧 , 0 ) ) ) )
9	2 8	nfsum	⊢ Ⅎ 𝑥 Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑧 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑧 ) , 𝑧 , 0 ) ) ) )
10	1 9	nfcxfr	⊢ Ⅎ 𝑥 ∫ 𝐴 𝐵 d 𝑥