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 ⊢ Ⅎ _ x ∫ A B dx

Proof

Step Hyp Ref Expression
1 df-itg ⊢ ∫ A B dx = ∑ k = 0 3 i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ B i k / z⦌ if x ∈ A ∧ 0 ≤ z z 0
2 nfcv ⊢ Ⅎ _ x 0 … 3
3 nfcv ⊢ Ⅎ _ x i k
4 nfcv ⊢ Ⅎ _ x ×
5 nfcv ⊢ Ⅎ _ x ∫ 2
6 nfmpt1 ⊢ Ⅎ _ x x ∈ ℝ ⟼ ⦋ ℜ ⁡ B i k / z⦌ if x ∈ A ∧ 0 ≤ z z 0
7 5 6 nffv ⊢ Ⅎ _ x ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ B i k / z⦌ if x ∈ A ∧ 0 ≤ z z 0
8 3 4 7 nfov ⊢ Ⅎ _ x i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ B i k / z⦌ if x ∈ A ∧ 0 ≤ z z 0
9 2 8 nfsum ⊢ Ⅎ _ x ∑ k = 0 3 i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ B i k / z⦌ if x ∈ A ∧ 0 ≤ z z 0
10 1 9 nfcxfr ⊢ Ⅎ _ x ∫ A B dx