Metamath Proof Explorer

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 𝑥