Metamath Proof Explorer

Theorem nfitg1

Description: Bound-variable hypothesis builder for an integral. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Assertion nfitg1 
|- F/_ x S. A B _d x

Proof

Step Hyp Ref Expression
1 df-itg 
 |-  S. A B _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / z ]_ if ( ( x e. A /\ 0 <_ z ) , z , 0 ) ) ) )
2 nfcv 
 |-  F/_ x ( 0 ... 3 )
3 nfcv 
 |-  F/_ x ( _i ^ k )
4 nfcv 
 |-  F/_ x x.
5 nfcv 
 |-  F/_ x S.2
6 nfmpt1 
 |-  F/_ x ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / z ]_ if ( ( x e. A /\ 0 <_ z ) , z , 0 ) )
7 5 6 nffv 
 |-  F/_ x ( S.2 ` ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / z ]_ if ( ( x e. A /\ 0 <_ z ) , z , 0 ) ) )
8 3 4 7 nfov 
 |-  F/_ x ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / z ]_ if ( ( x e. A /\ 0 <_ z ) , z , 0 ) ) ) )
9 2 8 nfsum 
 |-  F/_ x sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / z ]_ if ( ( x e. A /\ 0 <_ z ) , z , 0 ) ) ) )
10 1 9 nfcxfr 
 |-  F/_ x S. A B _d x