This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑥