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 𝑥