P. 236 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23501-23600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	itg2leub 23501*	Any upper bound on the integrals of all simple functions G dominated by F is greater than ( S.2 ` F ), the least upper bound. (Contributed by Mario Carneiro, 28-Jun-2014.)
|- ( ( F : RR --> ( 0 [,] +oo ) /\ A e. RR* ) -> ( ( S.2 ` F ) <_ A <-> A. g e. dom S.1 ( g oR <_ F -> ( S.1 ` g ) <_ A ) ) )
Theorem	itg2ge0 23502	The integral of a nonnegative real function is greater or equal to zero. (Contributed by Mario Carneiro, 28-Jun-2014.)
|- ( F : RR --> ( 0 [,] +oo ) -> 0 <_ ( S.2 ` F ) )
Theorem	itg2itg1 23503	The integral of a nonnegative simple function using S.2 is the same as its value under S.1. (Contributed by Mario Carneiro, 28-Jun-2014.)
|- ( ( F e. dom S.1 /\ 0p oR <_ F ) -> ( S.2 ` F ) = ( S.1 ` F ) )
Theorem	itg20 23504	The integral of the zero function. (Contributed by Mario Carneiro, 28-Jun-2014.)
|- ( S.2 ` ( RR X. { 0 } ) ) = 0
Theorem	itg2lecl 23505	If an S.2 integral is bounded above, then it is real. (Contributed by Mario Carneiro, 28-Jun-2014.)
|- ( ( F : RR --> ( 0 [,] +oo ) /\ A e. RR /\ ( S.2 ` F ) <_ A ) -> ( S.2 ` F ) e. RR )
Theorem	itg2le 23506	If one function dominates another, then the integral of the larger is also larger. (Contributed by Mario Carneiro, 28-Jun-2014.)
|- ( ( F : RR --> ( 0 [,] +oo ) /\ G : RR --> ( 0 [,] +oo ) /\ F oR <_ G ) -> ( S.2 ` F ) <_ ( S.2 ` G ) )
Theorem	itg2const 23507*	Integral of a constant function. (Contributed by Mario Carneiro, 12-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. ( 0 [,) +oo ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) = ( B x. ( vol ` A ) ) )
Theorem	itg2const2 23508*	When the base set of a constant function has infinite volume, the integral is also infinite and vice-versa. (Contributed by Mario Carneiro, 30-Aug-2014.)
|- ( ( A e. dom vol /\ B e. RR+ ) -> ( ( vol ` A ) e. RR <-> ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) )
Theorem	itg2seq 23509*	Definitional property of the S.2 integral: for any function F there is a countable sequence g of simple functions less than F whose integrals converge to the integral of F. (This theorem is for the most part unnecessary in lieu of itg2i1fseq 23522, but unlike that theorem this one doesn't require F to be measurable.) (Contributed by Mario Carneiro, 14-Aug-2014.)
|- ( F : RR --> ( 0 [,] +oo ) -> E. g ( g : NN --> dom S.1 /\ A. n e. NN ( g ` n ) oR <_ F /\ ( S.2 ` F ) = sup ( ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) , RR* , < ) ) )
Theorem	itg2uba 23510*	Approximate version of itg2ub 23500. If F approximately dominates G, then S.1 G <_ S.2 F. (Contributed by Mario Carneiro, 11-Aug-2014.)
|- ( ph -> F : RR --> ( 0 [,] +oo ) )   &    |- ( ph -> G e. dom S.1 )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> ( vol* ` A ) = 0 )   &    |- ( ( ph /\ x e. ( RR \ A ) ) -> ( G ` x ) <_ ( F ` x ) )   =>    |- ( ph -> ( S.1 ` G ) <_ ( S.2 ` F ) )
Theorem	itg2lea 23511*	Approximate version of itg2le 23506. If F <_ G for almost all x, then S.2 F <_ S.2 G. (Contributed by Mario Carneiro, 11-Aug-2014.)
|- ( ph -> F : RR --> ( 0 [,] +oo ) )   &    |- ( ph -> G : RR --> ( 0 [,] +oo ) )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> ( vol* ` A ) = 0 )   &    |- ( ( ph /\ x e. ( RR \ A ) ) -> ( F ` x ) <_ ( G ` x ) )   =>    |- ( ph -> ( S.2 ` F ) <_ ( S.2 ` G ) )
Theorem	itg2eqa 23512*	Approximate equality of integrals. If F = G for almost all x, then S.2 F = S.2 G. (Contributed by Mario Carneiro, 12-Aug-2014.)
|- ( ph -> F : RR --> ( 0 [,] +oo ) )   &    |- ( ph -> G : RR --> ( 0 [,] +oo ) )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> ( vol* ` A ) = 0 )   &    |- ( ( ph /\ x e. ( RR \ A ) ) -> ( F ` x ) = ( G ` x ) )   =>    |- ( ph -> ( S.2 ` F ) = ( S.2 ` G ) )
Theorem	itg2mulclem 23513	Lemma for itg2mulc 23514. (Contributed by Mario Carneiro, 8-Jul-2014.)
|- ( ph -> F : RR --> ( 0 [,) +oo ) )   &    |- ( ph -> ( S.2 ` F ) e. RR )   &    |- ( ph -> A e. RR+ )   =>    |- ( ph -> ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) <_ ( A x. ( S.2 ` F ) ) )
Theorem	itg2mulc 23514	The integral of a nonnegative constant times a function is the constant times the integral of the original function. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( ph -> F : RR --> ( 0 [,) +oo ) )   &    |- ( ph -> ( S.2 ` F ) e. RR )   &    |- ( ph -> A e. ( 0 [,) +oo ) )   =>    |- ( ph -> ( S.2 ` ( ( RR X. { A } ) oF x. F ) ) = ( A x. ( S.2 ` F ) ) )
Theorem	itg2splitlem 23515*	Lemma for itg2split 23516. (Contributed by Mario Carneiro, 11-Aug-2014.)
|- ( ph -> A e. dom vol )   &    |- ( ph -> B e. dom vol )   &    |- ( ph -> ( vol* ` ( A i^i B ) ) = 0 )   &    |- ( ph -> U = ( A u. B ) )   &    |- ( ( ph /\ x e. U ) -> C e. ( 0 [,] +oo ) )   &    |- F = ( x e. RR |-> if ( x e. A , C , 0 ) )   &    |- G = ( x e. RR |-> if ( x e. B , C , 0 ) )   &    |- H = ( x e. RR |-> if ( x e. U , C , 0 ) )   &    |- ( ph -> ( S.2 ` F ) e. RR )   &    |- ( ph -> ( S.2 ` G ) e. RR )   =>    |- ( ph -> ( S.2 ` H ) <_ ( ( S.2 ` F ) + ( S.2 ` G ) ) )
Theorem	itg2split 23516*	The S.2 integral splits under an almost disjoint union. (The proof avoids the use of itg2add 23526 which requires CC.) (Contributed by Mario Carneiro, 11-Aug-2014.)
|- ( ph -> A e. dom vol )   &    |- ( ph -> B e. dom vol )   &    |- ( ph -> ( vol* ` ( A i^i B ) ) = 0 )   &    |- ( ph -> U = ( A u. B ) )   &    |- ( ( ph /\ x e. U ) -> C e. ( 0 [,] +oo ) )   &    |- F = ( x e. RR |-> if ( x e. A , C , 0 ) )   &    |- G = ( x e. RR |-> if ( x e. B , C , 0 ) )   &    |- H = ( x e. RR |-> if ( x e. U , C , 0 ) )   &    |- ( ph -> ( S.2 ` F ) e. RR )   &    |- ( ph -> ( S.2 ` G ) e. RR )   =>    |- ( ph -> ( S.2 ` H ) = ( ( S.2 ` F ) + ( S.2 ` G ) ) )
Theorem	itg2monolem1 23517*	Lemma for itg2mono 23520. We show that for any constant t less than one, t x. S.1 H is less than S, and so S.1 H <_ S, which is one half of the equality in itg2mono 23520. Consider the sequence A ( n ) = { x | t x. H <_ F ( n ) }. This is an increasing sequence of measurable sets whose union is RR, and so H |` A ( n ) has an integral which equals S.1 H in the limit, by itg1climres 23481. Then by taking the limit in ( t x. H ) |` A ( n ) <_ F ( n ), we get t x. S.1 H <_ S as desired. (Contributed by Mario Carneiro, 16-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- G = ( x e. RR |-> sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) )   &    |- ( ( ph /\ n e. NN ) -> ( F ` n ) e. MblFn )   &    |- ( ( ph /\ n e. NN ) -> ( F ` n ) : RR --> ( 0 [,) +oo ) )   &    |- ( ( ph /\ n e. NN ) -> ( F ` n ) oR <_ ( F ` ( n + 1 ) ) )   &    |- ( ( ph /\ x e. RR ) -> E. y e. RR A. n e. NN ( ( F ` n ) ` x ) <_ y )   &    |- S = sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < )   &    |- ( ph -> T e. ( 0 (,) 1 ) )   &    |- ( ph -> H e. dom S.1 )   &    |- ( ph -> H oR <_ G )   &    |- ( ph -> S e. RR )   &    |- A = ( n e. NN |-> { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) } )   =>    |- ( ph -> ( T x. ( S.1 ` H ) ) <_ S )
Theorem	itg2monolem2 23518*	Lemma for itg2mono 23520. (Contributed by Mario Carneiro, 16-Aug-2014.)
|- G = ( x e. RR |-> sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) )   &    |- ( ( ph /\ n e. NN ) -> ( F ` n ) e. MblFn )   &    |- ( ( ph /\ n e. NN ) -> ( F ` n ) : RR --> ( 0 [,) +oo ) )   &    |- ( ( ph /\ n e. NN ) -> ( F ` n ) oR <_ ( F ` ( n + 1 ) ) )   &    |- ( ( ph /\ x e. RR ) -> E. y e. RR A. n e. NN ( ( F ` n ) ` x ) <_ y )   &    |- S = sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < )   &    |- ( ph -> P e. dom S.1 )   &    |- ( ph -> P oR <_ G )   &    |- ( ph -> -. ( S.1 ` P ) <_ S )   =>    |- ( ph -> S e. RR )
Theorem	itg2monolem3 23519*	Lemma for itg2mono 23520. (Contributed by Mario Carneiro, 16-Aug-2014.)
|- G = ( x e. RR |-> sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) )   &    |- ( ( ph /\ n e. NN ) -> ( F ` n ) e. MblFn )   &    |- ( ( ph /\ n e. NN ) -> ( F ` n ) : RR --> ( 0 [,) +oo ) )   &    |- ( ( ph /\ n e. NN ) -> ( F ` n ) oR <_ ( F ` ( n + 1 ) ) )   &    |- ( ( ph /\ x e. RR ) -> E. y e. RR A. n e. NN ( ( F ` n ) ` x ) <_ y )   &    |- S = sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < )   &    |- ( ph -> P e. dom S.1 )   &    |- ( ph -> P oR <_ G )   &    |- ( ph -> -. ( S.1 ` P ) <_ S )   =>    |- ( ph -> ( S.1 ` P ) <_ S )
Theorem	itg2mono 23520*	The Monotone Convergence Theorem for nonnegative functions. If { ( F ` n ) : n e. NN } is a monotone increasing sequence of positive, measurable, real-valued functions, and G is the pointwise limit of the sequence, then ( S.2 ` G ) is the limit of the sequence { ( S.2 ` ( F ` n ) ) : n e. NN }. (Contributed by Mario Carneiro, 16-Aug-2014.)
|- G = ( x e. RR |-> sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) )   &    |- ( ( ph /\ n e. NN ) -> ( F ` n ) e. MblFn )   &    |- ( ( ph /\ n e. NN ) -> ( F ` n ) : RR --> ( 0 [,) +oo ) )   &    |- ( ( ph /\ n e. NN ) -> ( F ` n ) oR <_ ( F ` ( n + 1 ) ) )   &    |- ( ( ph /\ x e. RR ) -> E. y e. RR A. n e. NN ( ( F ` n ) ` x ) <_ y )   &    |- S = sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < )   =>    |- ( ph -> ( S.2 ` G ) = S )
Theorem	itg2i1fseqle 23521*	Subject to the conditions coming from mbfi1fseq 23488, the sequence of simple functions are all less than the target function F. (Contributed by Mario Carneiro, 17-Aug-2014.)
|- ( ph -> F e. MblFn )   &    |- ( ph -> F : RR --> ( 0 [,) +oo ) )   &    |- ( ph -> P : NN --> dom S.1 )   &    |- ( ph -> A. n e. NN ( 0p oR <_ ( P ` n ) /\ ( P ` n ) oR <_ ( P ` ( n + 1 ) ) ) )   &    |- ( ph -> A. x e. RR ( n e. NN |-> ( ( P ` n ) ` x ) ) ~~> ( F ` x ) )   =>    |- ( ( ph /\ M e. NN ) -> ( P ` M ) oR <_ F )
Theorem	itg2i1fseq 23522*	Subject to the conditions coming from mbfi1fseq 23488, the integral of the sequence of simple functions converges to the integral of the target function. (Contributed by Mario Carneiro, 17-Aug-2014.)
|- ( ph -> F e. MblFn )   &    |- ( ph -> F : RR --> ( 0 [,) +oo ) )   &    |- ( ph -> P : NN --> dom S.1 )   &    |- ( ph -> A. n e. NN ( 0p oR <_ ( P ` n ) /\ ( P ` n ) oR <_ ( P ` ( n + 1 ) ) ) )   &    |- ( ph -> A. x e. RR ( n e. NN |-> ( ( P ` n ) ` x ) ) ~~> ( F ` x ) )   &    |- S = ( m e. NN |-> ( S.1 ` ( P ` m ) ) )   =>    |- ( ph -> ( S.2 ` F ) = sup ( ran S , RR* , < ) )
Theorem	itg2i1fseq2 23523*	In an extension to the results of itg2i1fseq 23522, if there is an upper bound on the integrals of the simple functions approaching F, then S.2 F is real and the standard limit relation applies. (Contributed by Mario Carneiro, 17-Aug-2014.)
|- ( ph -> F e. MblFn )   &    |- ( ph -> F : RR --> ( 0 [,) +oo ) )   &    |- ( ph -> P : NN --> dom S.1 )   &    |- ( ph -> A. n e. NN ( 0p oR <_ ( P ` n ) /\ ( P ` n ) oR <_ ( P ` ( n + 1 ) ) ) )   &    |- ( ph -> A. x e. RR ( n e. NN |-> ( ( P ` n ) ` x ) ) ~~> ( F ` x ) )   &    |- S = ( m e. NN |-> ( S.1 ` ( P ` m ) ) )   &    |- ( ph -> M e. RR )   &    |- ( ( ph /\ k e. NN ) -> ( S.1 ` ( P ` k ) ) <_ M )   =>    |- ( ph -> S ~~> ( S.2 ` F ) )
Theorem	itg2i1fseq3 23524*	Special case of itg2i1fseq2 23523: if the integral of F is a real number, then the standard limit relation holds on the integrals of simple functions approaching F. (Contributed by Mario Carneiro, 17-Aug-2014.)
|- ( ph -> F e. MblFn )   &    |- ( ph -> F : RR --> ( 0 [,) +oo ) )   &    |- ( ph -> P : NN --> dom S.1 )   &    |- ( ph -> A. n e. NN ( 0p oR <_ ( P ` n ) /\ ( P ` n ) oR <_ ( P ` ( n + 1 ) ) ) )   &    |- ( ph -> A. x e. RR ( n e. NN |-> ( ( P ` n ) ` x ) ) ~~> ( F ` x ) )   &    |- S = ( m e. NN |-> ( S.1 ` ( P ` m ) ) )   &    |- ( ph -> ( S.2 ` F ) e. RR )   =>    |- ( ph -> S ~~> ( S.2 ` F ) )
Theorem	itg2addlem 23525*	Lemma for itg2add 23526. (Contributed by Mario Carneiro, 17-Aug-2014.)
|- ( ph -> F e. MblFn )   &    |- ( ph -> F : RR --> ( 0 [,) +oo ) )   &    |- ( ph -> ( S.2 ` F ) e. RR )   &    |- ( ph -> G e. MblFn )   &    |- ( ph -> G : RR --> ( 0 [,) +oo ) )   &    |- ( ph -> ( S.2 ` G ) e. RR )   &    |- ( ph -> P : NN --> dom S.1 )   &    |- ( ph -> A. n e. NN ( 0p oR <_ ( P ` n ) /\ ( P ` n ) oR <_ ( P ` ( n + 1 ) ) ) )   &    |- ( ph -> A. x e. RR ( n e. NN |-> ( ( P ` n ) ` x ) ) ~~> ( F ` x ) )   &    |- ( ph -> Q : NN --> dom S.1 )   &    |- ( ph -> A. n e. NN ( 0p oR <_ ( Q ` n ) /\ ( Q ` n ) oR <_ ( Q ` ( n + 1 ) ) ) )   &    |- ( ph -> A. x e. RR ( n e. NN |-> ( ( Q ` n ) ` x ) ) ~~> ( G ` x ) )   =>    |- ( ph -> ( S.2 ` ( F oF + G ) ) = ( ( S.2 ` F ) + ( S.2 ` G ) ) )
Theorem	itg2add 23526	The S.2 integral is linear. (Measurability is an essential component of this theorem; otherwise consider the characteristic function of a nonmeasurable set and its complement.) (Contributed by Mario Carneiro, 17-Aug-2014.)
|- ( ph -> F e. MblFn )   &    |- ( ph -> F : RR --> ( 0 [,) +oo ) )   &    |- ( ph -> ( S.2 ` F ) e. RR )   &    |- ( ph -> G e. MblFn )   &    |- ( ph -> G : RR --> ( 0 [,) +oo ) )   &    |- ( ph -> ( S.2 ` G ) e. RR )   =>    |- ( ph -> ( S.2 ` ( F oF + G ) ) = ( ( S.2 ` F ) + ( S.2 ` G ) ) )
Theorem	itg2gt0 23527*	If the function F is strictly positive on a set of positive measure, then the integral of the function is positive. (Contributed by Mario Carneiro, 30-Aug-2014.)
|- ( ph -> A e. dom vol )   &    |- ( ph -> 0 < ( vol ` A ) )   &    |- ( ph -> F : RR --> ( 0 [,) +oo ) )   &    |- ( ph -> F e. MblFn )   &    |- ( ( ph /\ x e. A ) -> 0 < ( F ` x ) )   =>    |- ( ph -> 0 < ( S.2 ` F ) )
Theorem	itg2cnlem1 23528*	Lemma for itgcn 23609. (Contributed by Mario Carneiro, 30-Aug-2014.)
|- ( ph -> F : RR --> ( 0 [,) +oo ) )   &    |- ( ph -> F e. MblFn )   &    |- ( ph -> ( S.2 ` F ) e. RR )   =>    |- ( ph -> sup ( ran ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) , RR* , < ) = ( S.2 ` F ) )
Theorem	itg2cnlem2 23529*	Lemma for itgcn 23609. (Contributed by Mario Carneiro, 31-Aug-2014.)
|- ( ph -> F : RR --> ( 0 [,) +oo ) )   &    |- ( ph -> F e. MblFn )   &    |- ( ph -> ( S.2 ` F ) e. RR )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> M e. NN )   &    |- ( ph -> -. ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ M , ( F ` x ) , 0 ) ) ) <_ ( ( S.2 ` F ) - ( C / 2 ) ) )   =>    |- ( ph -> E. d e. RR+ A. u e. dom vol ( ( vol ` u ) < d -> ( S.2 ` ( x e. RR |-> if ( x e. u , ( F ` x ) , 0 ) ) ) < C ) )
Theorem	itg2cn 23530*	A sort of absolute continuity of the Lebesgue integral (this is the core of ftc1a 23800 which is about actual absolute continuity). (Contributed by Mario Carneiro, 1-Sep-2014.)
|- ( ph -> F : RR --> ( 0 [,) +oo ) )   &    |- ( ph -> F e. MblFn )   &    |- ( ph -> ( S.2 ` F ) e. RR )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> E. d e. RR+ A. u e. dom vol ( ( vol ` u ) < d -> ( S.2 ` ( x e. RR |-> if ( x e. u , ( F ` x ) , 0 ) ) ) < C ) )
Theorem	ibllem 23531	Conditioned equality theorem for the if statement. (Contributed by Mario Carneiro, 31-Jul-2014.)
|- ( ( ph /\ x e. A ) -> B = C )   =>    |- ( ph -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) = if ( ( x e. A /\ 0 <_ C ) , C , 0 ) )
Theorem	isibl 23532*	The predicate " F is integrable". The "integrable" predicate corresponds roughly to the range of validity of S. A B _d x, which is to say that the expression S. A B _d x doesn't make sense unless ( x e. A |-> B ) e. L^1. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( ph -> G = ( x e. RR |-> if ( ( x e. A /\ 0 <_ T ) , T , 0 ) ) )   &    |- ( ( ph /\ x e. A ) -> T = ( Re ` ( B / ( _i ^ k ) ) ) )   &    |- ( ph -> dom F = A )   &    |- ( ( ph /\ x e. A ) -> ( F ` x ) = B )   =>    |- ( ph -> ( F e. L^1 <-> ( F e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` G ) e. RR ) ) )
Theorem	isibl2 23533*	The predicate " F is integrable" when F is a mapping operation. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( ph -> G = ( x e. RR |-> if ( ( x e. A /\ 0 <_ T ) , T , 0 ) ) )   &    |- ( ( ph /\ x e. A ) -> T = ( Re ` ( B / ( _i ^ k ) ) ) )   &    |- ( ( ph /\ x e. A ) -> B e. V )   =>    |- ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` G ) e. RR ) ) )
Theorem	iblmbf 23534	An integrable function is measurable. (Contributed by Mario Carneiro, 7-Jul-2014.)
|- ( F e. L^1 -> F e. MblFn )
Theorem	iblitg 23535*	If a function is integrable, then the S.2 integrals of the function's decompositions all exist. (Contributed by Mario Carneiro, 7-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( ph -> G = ( x e. RR |-> if ( ( x e. A /\ 0 <_ T ) , T , 0 ) ) )   &    |- ( ( ph /\ x e. A ) -> T = ( Re ` ( B / ( _i ^ K ) ) ) )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   &    |- ( ( ph /\ x e. A ) -> B e. V )   =>    |- ( ( ph /\ K e. ZZ ) -> ( S.2 ` G ) e. RR )
Theorem	dfitg 23536*	Evaluate the class substitution in df-itg 23392. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- T = ( Re ` ( B / ( _i ^ k ) ) )   =>    |- S. A B _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ T ) , T , 0 ) ) ) )
Theorem	itgex 23537	An integral is a set. (Contributed by Mario Carneiro, 28-Jun-2014.)
|- S. A B _d x e. _V
Theorem	itgeq1f 23538	Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( A = B -> S. A C _d x = S. B C _d x )
Theorem	itgeq1 23539*	Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
|- ( A = B -> S. A C _d x = S. B C _d x )
Theorem	nfitg1 23540	Bound-variable hypothesis builder for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
|- F/_ x S. A B _d x
Theorem	nfitg 23541*	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.)
|- F/_ y A   &    |- F/_ y B   =>    |- F/_ y S. A B _d x
Theorem	cbvitg 23542*	Change bound variable in an integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
|- ( x = y -> B = C )   &    |- F/_ y B   &    |- F/_ x C   =>    |- S. A B _d x = S. A C _d y
Theorem	cbvitgv 23543*	Change bound variable in an integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
|- ( x = y -> B = C )   =>    |- S. A B _d x = S. A C _d y
Theorem	itgeq2 23544	Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
|- ( A. x e. A B = C -> S. A B _d x = S. A C _d x )
Theorem	itgresr 23545	The domain of an integral only matters in its intersection with RR. (Contributed by Mario Carneiro, 29-Jun-2014.)
|- S. A B _d x = S. ( A i^i RR ) B _d x
Theorem	itg0 23546	The integral of anything on the empty set is zero. (Contributed by Mario Carneiro, 13-Aug-2014.)
|- S. (/) A _d x = 0
Theorem	itgz 23547	The integral of zero on any set is zero. (Contributed by Mario Carneiro, 29-Jun-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- S. A 0 _d x = 0
Theorem	itgeq2dv 23548*	Equality theorem for an integral. (Contributed by Mario Carneiro, 7-Jul-2014.)
|- ( ( ph /\ x e. A ) -> B = C )   =>    |- ( ph -> S. A B _d x = S. A C _d x )
Theorem	itgmpt 23549*	Change bound variable in an integral. (Contributed by Mario Carneiro, 29-Jun-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   =>    |- ( ph -> S. A B _d x = S. A ( ( x e. A |-> B ) ` y ) _d y )
Theorem	itgcl 23550*	The integral of an integrable function is a complex number. This is Metamath 100 proof #86. (Contributed by Mario Carneiro, 29-Jun-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   =>    |- ( ph -> S. A B _d x e. CC )
Theorem	itgvallem 23551*	Substitution lemma. (Contributed by Mario Carneiro, 7-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( _i ^ K ) = T   =>    |- ( k = K -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / T ) ) ) , ( Re ` ( B / T ) ) , 0 ) ) ) )
Theorem	itgvallem3 23552*	Lemma for itgposval 23562 and itgreval 23563. (Contributed by Mario Carneiro, 7-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B = 0 )   =>    |- ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) = 0 )
Theorem	ibl0 23553	The zero function is integrable on any measurable set. (Unlike iblconst 23584, this does not require A to have finite measure.) (Contributed by Mario Carneiro, 23-Aug-2014.)
|- ( A e. dom vol -> ( A X. { 0 } ) e. L^1 )
Theorem	iblcnlem1 23554*	Lemma for iblcnlem 23555. (Contributed by Mario Carneiro, 6-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- R = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) )   &    |- S = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) )   &    |- T = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) )   &    |- U = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   =>    |- ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) e. MblFn /\ ( R e. RR /\ S e. RR ) /\ ( T e. RR /\ U e. RR ) ) ) )
Theorem	iblcnlem 23555*	Expand out the forall in isibl2 23533. (Contributed by Mario Carneiro, 6-Aug-2014.)
|- R = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) )   &    |- S = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) )   &    |- T = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) )   &    |- U = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) )   &    |- ( ( ph /\ x e. A ) -> B e. V )   =>    |- ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) e. MblFn /\ ( R e. RR /\ S e. RR ) /\ ( T e. RR /\ U e. RR ) ) ) )
Theorem	itgcnlem 23556*	Expand out the sum in dfitg 23536. (Contributed by Mario Carneiro, 1-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- R = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) )   &    |- S = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) )   &    |- T = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) )   &    |- U = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) )   &    |- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   =>    |- ( ph -> S. A B _d x = ( ( R - S ) + ( _i x. ( T - U ) ) ) )
Theorem	iblrelem 23557*	Integrability of a real function. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. RR )   =>    |- ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) e. RR ) ) )
Theorem	iblposlem 23558*	Lemma for iblpos 23559. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ( ph /\ x e. A ) -> 0 <_ B )   =>    |- ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) = 0 )
Theorem	iblpos 23559*	Integrability of a nonnegative function. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ( ph /\ x e. A ) -> 0 <_ B )   =>    |- ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) ) )
Theorem	iblre 23560*	Integrability of a real function. (Contributed by Mario Carneiro, 11-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. RR )   =>    |- ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. L^1 /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. L^1 ) ) )
Theorem	itgrevallem1 23561*	Lemma for itgposval 23562 and itgreval 23563. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   =>    |- ( ph -> S. A B _d x = ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) - ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) ) )
Theorem	itgposval 23562*	The integral of a nonnegative function. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   &    |- ( ( ph /\ x e. A ) -> 0 <_ B )   =>    |- ( ph -> S. A B _d x = ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) )
Theorem	itgreval 23563*	Decompose the integral of a real function into positive and negative parts. (Contributed by Mario Carneiro, 31-Jul-2014.)
|- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   =>    |- ( ph -> S. A B _d x = ( S. A if ( 0 <_ B , B , 0 ) _d x - S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) )
Theorem	itgrecl 23564*	Real closure of an integral. (Contributed by Mario Carneiro, 11-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   =>    |- ( ph -> S. A B _d x e. RR )
Theorem	iblcn 23565*	Integrability of a complex function. (Contributed by Mario Carneiro, 6-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. CC )   =>    |- ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> ( Re ` B ) ) e. L^1 /\ ( x e. A |-> ( Im ` B ) ) e. L^1 ) ) )
Theorem	itgcnval 23566*	Decompose the integral of a complex function into real and imaginary parts. (Contributed by Mario Carneiro, 6-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   =>    |- ( ph -> S. A B _d x = ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) )
Theorem	itgre 23567*	Real part of an integral. (Contributed by Mario Carneiro, 14-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   =>    |- ( ph -> ( Re ` S. A B _d x ) = S. A ( Re ` B ) _d x )
Theorem	itgim 23568*	Imaginary part of an integral. (Contributed by Mario Carneiro, 14-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   =>    |- ( ph -> ( Im ` S. A B _d x ) = S. A ( Im ` B ) _d x )
Theorem	iblneg 23569*	The negative of an integrable function is integrable. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   =>    |- ( ph -> ( x e. A |-> -u B ) e. L^1 )
Theorem	itgneg 23570*	Negation of an integral. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   =>    |- ( ph -> -u S. A B _d x = S. A -u B _d x )
Theorem	iblss 23571*	A subset of an integrable function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.)
|- ( ph -> A C_ B )   &    |- ( ph -> A e. dom vol )   &    |- ( ( ph /\ x e. B ) -> C e. V )   &    |- ( ph -> ( x e. B |-> C ) e. L^1 )   =>    |- ( ph -> ( x e. A |-> C ) e. L^1 )
Theorem	iblss2 23572*	Change the domain of an integrability predicate. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( ph -> A C_ B )   &    |- ( ph -> B e. dom vol )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ( ph /\ x e. ( B \ A ) ) -> C = 0 )   &    |- ( ph -> ( x e. A |-> C ) e. L^1 )   =>    |- ( ph -> ( x e. B |-> C ) e. L^1 )
Theorem	itgitg2 23573*	Transfer an integral using S.2 to an equivalent integral using S.. (Contributed by Mario Carneiro, 6-Aug-2014.)
|- ( ( ph /\ x e. RR ) -> A e. RR )   &    |- ( ( ph /\ x e. RR ) -> 0 <_ A )   &    |- ( ph -> ( x e. RR |-> A ) e. L^1 )   =>    |- ( ph -> S. RR A _d x = ( S.2 ` ( x e. RR |-> A ) ) )
Theorem	i1fibl 23574	A simple function is integrable. (Contributed by Mario Carneiro, 6-Aug-2014.)
|- ( F e. dom S.1 -> F e. L^1 )
Theorem	itgitg1 23575*	Transfer an integral using S.1 to an equivalent integral using S.. (Contributed by Mario Carneiro, 6-Aug-2014.)
|- ( F e. dom S.1 -> S. RR ( F ` x ) _d x = ( S.1 ` F ) )
Theorem	itgle 23576*	Monotonicity of an integral. (Contributed by Mario Carneiro, 11-Aug-2014.)
|- ( ph -> ( x e. A |-> B ) e. L^1 )   &    |- ( ph -> ( x e. A |-> C ) e. L^1 )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ( ph /\ x e. A ) -> C e. RR )   &    |- ( ( ph /\ x e. A ) -> B <_ C )   =>    |- ( ph -> S. A B _d x <_ S. A C _d x )
Theorem	itgge0 23577*	The integral of a positive function is positive. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( ph -> ( x e. A |-> B ) e. L^1 )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ( ph /\ x e. A ) -> 0 <_ B )   =>    |- ( ph -> 0 <_ S. A B _d x )
Theorem	itgss 23578*	Expand the set of an integral by adding zeroes outside the domain. (Contributed by Mario Carneiro, 11-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( ph -> A C_ B )   &    |- ( ( ph /\ x e. ( B \ A ) ) -> C = 0 )   =>    |- ( ph -> S. A C _d x = S. B C _d x )
Theorem	itgss2 23579*	Expand the set of an integral by adding zeroes outside the domain. (Contributed by Mario Carneiro, 11-Aug-2014.)
|- ( A C_ B -> S. A C _d x = S. B if ( x e. A , C , 0 ) _d x )
Theorem	itgeqa 23580*	Approximate equality of integrals. If C ( x ) = D ( x ) for almost all x, then S. B C ( x ) _d x = S. B D ( x ) _d x and one is integrable iff the other is. (Contributed by Mario Carneiro, 12-Aug-2014.) (Revised by Mario Carneiro, 2-Sep-2014.)
|- ( ( ph /\ x e. B ) -> C e. CC )   &    |- ( ( ph /\ x e. B ) -> D e. CC )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> ( vol* ` A ) = 0 )   &    |- ( ( ph /\ x e. ( B \ A ) ) -> C = D )   =>    |- ( ph -> ( ( ( x e. B |-> C ) e. L^1 <-> ( x e. B |-> D ) e. L^1 ) /\ S. B C _d x = S. B D _d x ) )
Theorem	itgss3 23581*	Expand the set of an integral by a nullset. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Mario Carneiro, 2-Sep-2014.)
|- ( ph -> A C_ B )   &    |- ( ph -> B C_ RR )   &    |- ( ph -> ( vol* ` ( B \ A ) ) = 0 )   &    |- ( ( ph /\ x e. B ) -> C e. CC )   =>    |- ( ph -> ( ( ( x e. A |-> C ) e. L^1 <-> ( x e. B |-> C ) e. L^1 ) /\ S. A C _d x = S. B C _d x ) )
Theorem	itgioo 23582*	Equality of integrals on open and closed intervals. (Contributed by Mario Carneiro, 2-Sep-2014.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> C e. CC )   =>    |- ( ph -> S. ( A (,) B ) C _d x = S. ( A [,] B ) C _d x )
Theorem	itgless 23583*	Expand the integral of a nonnegative function. (Contributed by Mario Carneiro, 31-Aug-2014.)
|- ( ph -> A C_ B )   &    |- ( ph -> A e. dom vol )   &    |- ( ( ph /\ x e. B ) -> C e. RR )   &    |- ( ( ph /\ x e. B ) -> 0 <_ C )   &    |- ( ph -> ( x e. B |-> C ) e. L^1 )   =>    |- ( ph -> S. A C _d x <_ S. B C _d x )
Theorem	iblconst 23584	A constant function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.)
|- ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( A X. { B } ) e. L^1 )
Theorem	itgconst 23585*	Integral of a constant function. (Contributed by Mario Carneiro, 12-Aug-2014.)
|- ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> S. A B _d x = ( B x. ( vol ` A ) ) )
Theorem	ibladdlem 23586*	Lemma for ibladd 23587. (Contributed by Mario Carneiro, 17-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ( ph /\ x e. A ) -> C e. RR )   &    |- ( ( ph /\ x e. A ) -> D = ( B + C ) )   &    |- ( ph -> ( x e. A |-> B ) e. MblFn )   &    |- ( ph -> ( x e. A |-> C ) e. MblFn )   &    |- ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) e. RR )   &    |- ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ C ) , C , 0 ) ) ) e. RR )   =>    |- ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ D ) , D , 0 ) ) ) e. RR )
Theorem	ibladd 23587*	Add two integrals over the same domain. (Contributed by Mario Carneiro, 17-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> C ) e. L^1 )   =>    |- ( ph -> ( x e. A |-> ( B + C ) ) e. L^1 )
Theorem	iblsub 23588*	Subtract two integrals over the same domain. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> C ) e. L^1 )   =>    |- ( ph -> ( x e. A |-> ( B - C ) ) e. L^1 )
Theorem	itgaddlem1 23589*	Lemma for itgadd 23591. (Contributed by Mario Carneiro, 17-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> C ) e. L^1 )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ( ph /\ x e. A ) -> C e. RR )   &    |- ( ( ph /\ x e. A ) -> 0 <_ B )   &    |- ( ( ph /\ x e. A ) -> 0 <_ C )   =>    |- ( ph -> S. A ( B + C ) _d x = ( S. A B _d x + S. A C _d x ) )
Theorem	itgaddlem2 23590*	Lemma for itgadd 23591. (Contributed by Mario Carneiro, 17-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> C ) e. L^1 )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ( ph /\ x e. A ) -> C e. RR )   =>    |- ( ph -> S. A ( B + C ) _d x = ( S. A B _d x + S. A C _d x ) )
Theorem	itgadd 23591*	Add two integrals over the same domain. (Contributed by Mario Carneiro, 17-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> C ) e. L^1 )   =>    |- ( ph -> S. A ( B + C ) _d x = ( S. A B _d x + S. A C _d x ) )
Theorem	itgsub 23592*	Subtract two integrals over the same domain. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> C ) e. L^1 )   =>    |- ( ph -> S. A ( B - C ) _d x = ( S. A B _d x - S. A C _d x ) )
Theorem	itgfsum 23593*	Take a finite sum of integrals over the same domain. (Contributed by Mario Carneiro, 24-Aug-2014.)
|- ( ph -> A e. dom vol )   &    |- ( ph -> B e. Fin )   &    |- ( ( ph /\ ( x e. A /\ k e. B ) ) -> C e. V )   &    |- ( ( ph /\ k e. B ) -> ( x e. A |-> C ) e. L^1 )   =>    |- ( ph -> ( ( x e. A |-> sum_ k e. B C ) e. L^1 /\ S. A sum_ k e. B C _d x = sum_ k e. B S. A C _d x ) )
Theorem	iblabslem 23594*	Lemma for iblabs 23595. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   &    |- G = ( x e. RR |-> if ( x e. A , ( abs ` ( F ` B ) ) , 0 ) )   &    |- ( ph -> ( x e. A |-> ( F ` B ) ) e. L^1 )   &    |- ( ( ph /\ x e. A ) -> ( F ` B ) e. RR )   =>    |- ( ph -> ( G e. MblFn /\ ( S.2 ` G ) e. RR ) )
Theorem	iblabs 23595*	The absolute value of an integrable function is integrable. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   =>    |- ( ph -> ( x e. A |-> ( abs ` B ) ) e. L^1 )
Theorem	iblabsr 23596*	A measurable function is integrable iff its absolute value is integrable. (See iblabs 23595 for the forward implication.) (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. MblFn )   &    |- ( ph -> ( x e. A |-> ( abs ` B ) ) e. L^1 )   =>    |- ( ph -> ( x e. A |-> B ) e. L^1 )
Theorem	iblmulc2 23597*	Multiply an integral by a constant. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( ph -> C e. CC )   &    |- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   =>    |- ( ph -> ( x e. A |-> ( C x. B ) ) e. L^1 )
Theorem	itgmulc2lem1 23598*	Lemma for itgmulc2 23600: positive real case. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( ph -> C e. CC )   &    |- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   &    |- ( ph -> C e. RR )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> 0 <_ C )   &    |- ( ( ph /\ x e. A ) -> 0 <_ B )   =>    |- ( ph -> ( C x. S. A B _d x ) = S. A ( C x. B ) _d x )
Theorem	itgmulc2lem2 23599*	Lemma for itgmulc2 23600: real case. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( ph -> C e. CC )   &    |- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   &    |- ( ph -> C e. RR )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   =>    |- ( ph -> ( C x. S. A B _d x ) = S. A ( C x. B ) _d x )
Theorem	itgmulc2 23600*	Multiply an integral by a constant. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( ph -> C e. CC )   &    |- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   =>    |- ( ph -> ( C x. S. A B _d x ) = S. A ( C x. B ) _d x )