Metamath Proof Explorer

Theorem itgss

Description: 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)

Ref Expression
Hypotheses itgss.1 
|- ( ph -> A C_ B )
itgss.2 
|- ( ( ph /\ x e. ( B \ A ) ) -> C = 0 )
Assertion itgss 
|- ( ph -> S. A C _d x = S. B C _d x )

Proof

Step Hyp Ref Expression
1 itgss.1 
 |-  ( ph -> A C_ B )
2 itgss.2 
 |-  ( ( ph /\ x e. ( B \ A ) ) -> C = 0 )
3 elfzelz 
 |-  ( k e. ( 0 ... 3 ) -> k e. ZZ )
4 iffalse 
 |-  ( -. x e. A -> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = 0 )
5 4 ad2antll 
 |-  ( ( ( ph /\ k e. ZZ ) /\ ( x e. B /\ -. x e. A ) ) -> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = 0 )
6 eldif 
 |-  ( x e. ( B \ A ) <-> ( x e. B /\ -. x e. A ) )
7 2 adantlr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ x e. ( B \ A ) ) -> C = 0 )
8 7 oveq1d 
 |-  ( ( ( ph /\ k e. ZZ ) /\ x e. ( B \ A ) ) -> ( C / ( _i ^ k ) ) = ( 0 / ( _i ^ k ) ) )
9 ax-icn 
 |-  _i e. CC
10 ine0 
 |-  _i =/= 0
11 expclz 
 |-  ( ( _i e. CC /\ _i =/= 0 /\ k e. ZZ ) -> ( _i ^ k ) e. CC )
12 9 10 11 mp3an12 
 |-  ( k e. ZZ -> ( _i ^ k ) e. CC )
13 expne0i 
 |-  ( ( _i e. CC /\ _i =/= 0 /\ k e. ZZ ) -> ( _i ^ k ) =/= 0 )
14 9 10 13 mp3an12 
 |-  ( k e. ZZ -> ( _i ^ k ) =/= 0 )
15 12 14 div0d 
 |-  ( k e. ZZ -> ( 0 / ( _i ^ k ) ) = 0 )
16 15 ad2antlr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ x e. ( B \ A ) ) -> ( 0 / ( _i ^ k ) ) = 0 )
17 8 16 eqtrd 
 |-  ( ( ( ph /\ k e. ZZ ) /\ x e. ( B \ A ) ) -> ( C / ( _i ^ k ) ) = 0 )
18 17 fveq2d 
 |-  ( ( ( ph /\ k e. ZZ ) /\ x e. ( B \ A ) ) -> ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` 0 ) )
19 re0 
 |-  ( Re ` 0 ) = 0
20 18 19 eqtrdi 
 |-  ( ( ( ph /\ k e. ZZ ) /\ x e. ( B \ A ) ) -> ( Re ` ( C / ( _i ^ k ) ) ) = 0 )
21 20 ifeq1d 
 |-  ( ( ( ph /\ k e. ZZ ) /\ x e. ( B \ A ) ) -> if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) = if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , 0 , 0 ) )
22 ifid 
 |-  if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , 0 , 0 ) = 0
23 21 22 eqtrdi 
 |-  ( ( ( ph /\ k e. ZZ ) /\ x e. ( B \ A ) ) -> if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) = 0 )
24 6 23 sylan2br 
 |-  ( ( ( ph /\ k e. ZZ ) /\ ( x e. B /\ -. x e. A ) ) -> if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) = 0 )
25 5 24 eqtr4d 
 |-  ( ( ( ph /\ k e. ZZ ) /\ ( x e. B /\ -. x e. A ) ) -> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
26 25 expr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ x e. B ) -> ( -. x e. A -> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) )
27 iftrue 
 |-  ( x e. A -> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
28 26 27 pm2.61d2 
 |-  ( ( ( ph /\ k e. ZZ ) /\ x e. B ) -> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
29 iftrue 
 |-  ( x e. B -> if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
30 29 adantl 
 |-  ( ( ( ph /\ k e. ZZ ) /\ x e. B ) -> if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
31 28 30 eqtr4d 
 |-  ( ( ( ph /\ k e. ZZ ) /\ x e. B ) -> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) )
32 1 adantr 
 |-  ( ( ph /\ k e. ZZ ) -> A C_ B )
33 32 sseld 
 |-  ( ( ph /\ k e. ZZ ) -> ( x e. A -> x e. B ) )
34 33 con3dimp 
 |-  ( ( ( ph /\ k e. ZZ ) /\ -. x e. B ) -> -. x e. A )
35 34 4 syl 
 |-  ( ( ( ph /\ k e. ZZ ) /\ -. x e. B ) -> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = 0 )
36 iffalse 
 |-  ( -. x e. B -> if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = 0 )
37 36 adantl 
 |-  ( ( ( ph /\ k e. ZZ ) /\ -. x e. B ) -> if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = 0 )
38 35 37 eqtr4d 
 |-  ( ( ( ph /\ k e. ZZ ) /\ -. x e. B ) -> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) )
39 31 38 pm2.61dan 
 |-  ( ( ph /\ k e. ZZ ) -> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) )
40 ifan 
 |-  if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) = if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 )
41 ifan 
 |-  if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) = if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 )
42 39 40 41 3eqtr4g 
 |-  ( ( ph /\ k e. ZZ ) -> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) = if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
43 42 mpteq2dv 
 |-  ( ( ph /\ k e. ZZ ) -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) )
44 43 fveq2d 
 |-  ( ( ph /\ k e. ZZ ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) )
45 44 oveq2d 
 |-  ( ( ph /\ k e. ZZ ) -> ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) = ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) )
46 3 45 sylan2 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) = ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) )
47 46 sumeq2dv 
 |-  ( ph -> sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) )
48 eqid 
 |-  ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( C / ( _i ^ k ) ) )
49 48 dfitg 
 |-  S. A C _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) )
50 48 dfitg 
 |-  S. B C _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) )
51 47 49 50 3eqtr4g 
 |-  ( ph -> S. A C _d x = S. B C _d x )