MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fsumsplit Structured version   Unicode version

Theorem fsumsplit 13744
Description: Split a sum into two parts. (Contributed by Mario Carneiro, 18-Aug-2013.) (Revised by Mario Carneiro, 22-Apr-2014.)
Hypotheses
Ref Expression
fsumsplit.1  |-  ( ph  ->  ( A  i^i  B
)  =  (/) )
fsumsplit.2  |-  ( ph  ->  U  =  ( A  u.  B ) )
fsumsplit.3  |-  ( ph  ->  U  e.  Fin )
fsumsplit.4  |-  ( (
ph  /\  k  e.  U )  ->  C  e.  CC )
Assertion
Ref Expression
fsumsplit  |-  ( ph  -> 
sum_ k  e.  U  C  =  ( sum_ k  e.  A  C  +  sum_ k  e.  B  C ) )
Distinct variable groups:    A, k    B, k    ph, k    U, k
Allowed substitution hint:    C( k)

Proof of Theorem fsumsplit
StepHypRef Expression
1 ssun1 3567 . . . . 5  |-  A  C_  ( A  u.  B
)
2 fsumsplit.2 . . . . 5  |-  ( ph  ->  U  =  ( A  u.  B ) )
31, 2syl5sseqr 3451 . . . 4  |-  ( ph  ->  A  C_  U )
43sselda 3402 . . . . . 6  |-  ( (
ph  /\  k  e.  A )  ->  k  e.  U )
5 fsumsplit.4 . . . . . 6  |-  ( (
ph  /\  k  e.  U )  ->  C  e.  CC )
64, 5syldan 472 . . . . 5  |-  ( (
ph  /\  k  e.  A )  ->  C  e.  CC )
76ralrimiva 2774 . . . 4  |-  ( ph  ->  A. k  e.  A  C  e.  CC )
8 fsumsplit.3 . . . . 5  |-  ( ph  ->  U  e.  Fin )
98olcd 394 . . . 4  |-  ( ph  ->  ( U  C_  ( ZZ>=
`  0 )  \/  U  e.  Fin )
)
10 sumss2 13730 . . . 4  |-  ( ( ( A  C_  U  /\  A. k  e.  A  C  e.  CC )  /\  ( U  C_  ( ZZ>=
`  0 )  \/  U  e.  Fin )
)  ->  sum_ k  e.  A  C  =  sum_ k  e.  U  if ( k  e.  A ,  C ,  0 ) )
113, 7, 9, 10syl21anc 1263 . . 3  |-  ( ph  -> 
sum_ k  e.  A  C  =  sum_ k  e.  U  if ( k  e.  A ,  C ,  0 ) )
12 ssun2 3568 . . . . 5  |-  B  C_  ( A  u.  B
)
1312, 2syl5sseqr 3451 . . . 4  |-  ( ph  ->  B  C_  U )
1413sselda 3402 . . . . . 6  |-  ( (
ph  /\  k  e.  B )  ->  k  e.  U )
1514, 5syldan 472 . . . . 5  |-  ( (
ph  /\  k  e.  B )  ->  C  e.  CC )
1615ralrimiva 2774 . . . 4  |-  ( ph  ->  A. k  e.  B  C  e.  CC )
17 sumss2 13730 . . . 4  |-  ( ( ( B  C_  U  /\  A. k  e.  B  C  e.  CC )  /\  ( U  C_  ( ZZ>=
`  0 )  \/  U  e.  Fin )
)  ->  sum_ k  e.  B  C  =  sum_ k  e.  U  if ( k  e.  B ,  C ,  0 ) )
1813, 16, 9, 17syl21anc 1263 . . 3  |-  ( ph  -> 
sum_ k  e.  B  C  =  sum_ k  e.  U  if ( k  e.  B ,  C ,  0 ) )
1911, 18oveq12d 6262 . 2  |-  ( ph  ->  ( sum_ k  e.  A  C  +  sum_ k  e.  B  C )  =  ( sum_ k  e.  U  if ( k  e.  A ,  C ,  0 )  +  sum_ k  e.  U  if ( k  e.  B ,  C ,  0 ) ) )
20 0cn 9581 . . . 4  |-  0  e.  CC
21 ifcl 3891 . . . 4  |-  ( ( C  e.  CC  /\  0  e.  CC )  ->  if ( k  e.  A ,  C , 
0 )  e.  CC )
225, 20, 21sylancl 666 . . 3  |-  ( (
ph  /\  k  e.  U )  ->  if ( k  e.  A ,  C ,  0 )  e.  CC )
23 ifcl 3891 . . . 4  |-  ( ( C  e.  CC  /\  0  e.  CC )  ->  if ( k  e.  B ,  C , 
0 )  e.  CC )
245, 20, 23sylancl 666 . . 3  |-  ( (
ph  /\  k  e.  U )  ->  if ( k  e.  B ,  C ,  0 )  e.  CC )
258, 22, 24fsumadd 13743 . 2  |-  ( ph  -> 
sum_ k  e.  U  ( if ( k  e.  A ,  C , 
0 )  +  if ( k  e.  B ,  C ,  0 ) )  =  ( sum_ k  e.  U  if ( k  e.  A ,  C ,  0 )  +  sum_ k  e.  U  if ( k  e.  B ,  C ,  0 ) ) )
262eleq2d 2486 . . . . . 6  |-  ( ph  ->  ( k  e.  U  <->  k  e.  ( A  u.  B ) ) )
27 elun 3544 . . . . . 6  |-  ( k  e.  ( A  u.  B )  <->  ( k  e.  A  \/  k  e.  B ) )
2826, 27syl6bb 264 . . . . 5  |-  ( ph  ->  ( k  e.  U  <->  ( k  e.  A  \/  k  e.  B )
) )
2928biimpa 486 . . . 4  |-  ( (
ph  /\  k  e.  U )  ->  (
k  e.  A  \/  k  e.  B )
)
30 iftrue 3855 . . . . . . . 8  |-  ( k  e.  A  ->  if ( k  e.  A ,  C ,  0 )  =  C )
3130adantl 467 . . . . . . 7  |-  ( (
ph  /\  k  e.  A )  ->  if ( k  e.  A ,  C ,  0 )  =  C )
32 noel 3703 . . . . . . . . . . 11  |-  -.  k  e.  (/)
33 elin 3587 . . . . . . . . . . . 12  |-  ( k  e.  ( A  i^i  B )  <->  ( k  e.  A  /\  k  e.  B ) )
34 fsumsplit.1 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A  i^i  B
)  =  (/) )
3534eleq2d 2486 . . . . . . . . . . . 12  |-  ( ph  ->  ( k  e.  ( A  i^i  B )  <-> 
k  e.  (/) ) )
3633, 35syl5rbbr 263 . . . . . . . . . . 11  |-  ( ph  ->  ( k  e.  (/)  <->  (
k  e.  A  /\  k  e.  B )
) )
3732, 36mtbii 303 . . . . . . . . . 10  |-  ( ph  ->  -.  ( k  e.  A  /\  k  e.  B ) )
38 imnan 423 . . . . . . . . . 10  |-  ( ( k  e.  A  ->  -.  k  e.  B
)  <->  -.  ( k  e.  A  /\  k  e.  B ) )
3937, 38sylibr 215 . . . . . . . . 9  |-  ( ph  ->  ( k  e.  A  ->  -.  k  e.  B
) )
4039imp 430 . . . . . . . 8  |-  ( (
ph  /\  k  e.  A )  ->  -.  k  e.  B )
4140iffalsed 3860 . . . . . . 7  |-  ( (
ph  /\  k  e.  A )  ->  if ( k  e.  B ,  C ,  0 )  =  0 )
4231, 41oveq12d 6262 . . . . . 6  |-  ( (
ph  /\  k  e.  A )  ->  ( if ( k  e.  A ,  C ,  0 )  +  if ( k  e.  B ,  C ,  0 ) )  =  ( C  + 
0 ) )
436addid1d 9779 . . . . . 6  |-  ( (
ph  /\  k  e.  A )  ->  ( C  +  0 )  =  C )
4442, 43eqtrd 2457 . . . . 5  |-  ( (
ph  /\  k  e.  A )  ->  ( if ( k  e.  A ,  C ,  0 )  +  if ( k  e.  B ,  C ,  0 ) )  =  C )
4539con2d 118 . . . . . . . . 9  |-  ( ph  ->  ( k  e.  B  ->  -.  k  e.  A
) )
4645imp 430 . . . . . . . 8  |-  ( (
ph  /\  k  e.  B )  ->  -.  k  e.  A )
4746iffalsed 3860 . . . . . . 7  |-  ( (
ph  /\  k  e.  B )  ->  if ( k  e.  A ,  C ,  0 )  =  0 )
48 iftrue 3855 . . . . . . . 8  |-  ( k  e.  B  ->  if ( k  e.  B ,  C ,  0 )  =  C )
4948adantl 467 . . . . . . 7  |-  ( (
ph  /\  k  e.  B )  ->  if ( k  e.  B ,  C ,  0 )  =  C )
5047, 49oveq12d 6262 . . . . . 6  |-  ( (
ph  /\  k  e.  B )  ->  ( if ( k  e.  A ,  C ,  0 )  +  if ( k  e.  B ,  C ,  0 ) )  =  ( 0  +  C ) )
5115addid2d 9780 . . . . . 6  |-  ( (
ph  /\  k  e.  B )  ->  (
0  +  C )  =  C )
5250, 51eqtrd 2457 . . . . 5  |-  ( (
ph  /\  k  e.  B )  ->  ( if ( k  e.  A ,  C ,  0 )  +  if ( k  e.  B ,  C ,  0 ) )  =  C )
5344, 52jaodan 792 . . . 4  |-  ( (
ph  /\  ( k  e.  A  \/  k  e.  B ) )  -> 
( if ( k  e.  A ,  C ,  0 )  +  if ( k  e.  B ,  C , 
0 ) )  =  C )
5429, 53syldan 472 . . 3  |-  ( (
ph  /\  k  e.  U )  ->  ( if ( k  e.  A ,  C ,  0 )  +  if ( k  e.  B ,  C ,  0 ) )  =  C )
5554sumeq2dv 13707 . 2  |-  ( ph  -> 
sum_ k  e.  U  ( if ( k  e.  A ,  C , 
0 )  +  if ( k  e.  B ,  C ,  0 ) )  =  sum_ k  e.  U  C )
5619, 25, 553eqtr2rd 2464 1  |-  ( ph  -> 
sum_ k  e.  U  C  =  ( sum_ k  e.  A  C  +  sum_ k  e.  B  C ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 369    /\ wa 370    = wceq 1437    e. wcel 1872   A.wral 2709    u. cun 3372    i^i cin 3373    C_ wss 3374   (/)c0 3699   ifcif 3849   ` cfv 5539  (class class class)co 6244   Fincfn 7519   CCcc 9483   0cc0 9485    + caddc 9488   ZZ>=cuz 11105   sum_csu 13690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-rep 4474  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-inf2 8094  ax-cnex 9541  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559  ax-pre-lttrn 9560  ax-pre-ltadd 9561  ax-pre-mulgt0 9562  ax-pre-sup 9563
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-int 4194  df-iun 4239  df-br 4362  df-opab 4421  df-mpt 4422  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-se 4751  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-pred 5337  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-isom 5548  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-om 6646  df-1st 6746  df-2nd 6747  df-wrecs 6978  df-recs 7040  df-rdg 7078  df-1o 7132  df-oadd 7136  df-er 7313  df-en 7520  df-dom 7521  df-sdom 7522  df-fin 7523  df-sup 7904  df-oi 7973  df-card 8320  df-pnf 9623  df-mnf 9624  df-xr 9625  df-ltxr 9626  df-le 9627  df-sub 9808  df-neg 9809  df-div 10216  df-nn 10556  df-2 10614  df-3 10615  df-n0 10816  df-z 10884  df-uz 11106  df-rp 11249  df-fz 11731  df-fzo 11862  df-seq 12159  df-exp 12218  df-hash 12461  df-cj 13101  df-re 13102  df-im 13103  df-sqrt 13237  df-abs 13238  df-clim 13490  df-sum 13691
This theorem is referenced by:  sumpr  13747  sumtp  13748  fsumm1  13750  fsum1p  13752  fsumsplitsnun  13754  fsum2dlem  13769  fsumless  13794  fsumabs  13799  fsumrlim  13809  fsumo1  13810  o1fsum  13811  cvgcmpce  13816  fsumiun  13819  incexclem  13832  incexc  13833  isumltss  13844  climcndslem1  13845  climcndslem2  13846  mertenslem1  13878  bitsinv1  14354  bitsinvp1  14361  sylow2a  17209  fsumcn  21839  ovolfiniun  22391  volfiniun  22437  uniioombllem3  22480  itgfsum  22721  dvmptfsum  22864  vieta1lem2  23201  mtest  23296  birthdaylem2  23815  fsumharmonic  23874  ftalem5  23938  ftalem5OLD  23940  chtprm  24017  chtdif  24022  perfectlem2  24095  lgsquadlem2  24220  dchrisumlem1  24264  dchrisumlem2  24265  rpvmasum2  24287  dchrisum0lem1b  24290  dchrisum0lem3  24294  pntrsumbnd2  24342  pntrlog2bndlem6  24358  pntpbnd2  24362  pntlemf  24380  axlowdimlem16  24924  axlowdimlem17  24925  signsplypnf  29386  jm2.22  35763  jm2.23  35764  sumpair  37272  fsumsplitf  37530  sumnnodd  37593  stoweidlem11  37754  stoweidlem26  37769  stoweidlem44  37788  sge0resplit  38099  sge0split  38102  perfectALTVlem2  38657  fsumsplitsndif  38866
  Copyright terms: Public domain W3C validator