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 
|- F/_ y A
nfitg.2 
|- F/_ y B
Assertion nfitg 
|- F/_ y S. A B _d x

Proof

Step Hyp Ref Expression
1 nfitg.1 
 |-  F/_ y A
2 nfitg.2 
 |-  F/_ y B
3 eqid 
 |-  ( Re ` ( B / ( _i ^ k ) ) ) = ( Re ` ( B / ( _i ^ k ) ) )
4 3 dfitg 
 |-  S. A B _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) )
5 nfcv 
 |-  F/_ y ( 0 ... 3 )
6 nfcv 
 |-  F/_ y ( _i ^ k )
7 nfcv 
 |-  F/_ y x.
8 nfcv 
 |-  F/_ y S.2
9 nfcv 
 |-  F/_ y RR
10 1 nfcri 
 |-  F/ y x e. A
11 nfcv 
 |-  F/_ y 0
12 nfcv 
 |-  F/_ y <_
13 nfcv 
 |-  F/_ y Re
14 nfcv 
 |-  F/_ y /
15 2 14 6 nfov 
 |-  F/_ y ( B / ( _i ^ k ) )
16 13 15 nffv 
 |-  F/_ y ( Re ` ( B / ( _i ^ k ) ) )
17 11 12 16 nfbr 
 |-  F/ y 0 <_ ( Re ` ( B / ( _i ^ k ) ) )
18 10 17 nfan 
 |-  F/ y ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) )
19 18 16 11 nfif 
 |-  F/_ y if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 )
20 9 19 nfmpt 
 |-  F/_ y ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) )
21 8 20 nffv 
 |-  F/_ y ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) )
22 6 7 21 nfov 
 |-  F/_ y ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) )
23 5 22 nfsum 
 |-  F/_ y sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) )
24 4 23 nfcxfr 
 |-  F/_ y S. A B _d x