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

Theorem fsumsplit 13855
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 3609 . . . . 5  |-  A  C_  ( A  u.  B
)
2 fsumsplit.2 . . . . 5  |-  ( ph  ->  U  =  ( A  u.  B ) )
31, 2syl5sseqr 3493 . . . 4  |-  ( ph  ->  A  C_  U )
43sselda 3444 . . . . . 6  |-  ( (
ph  /\  k  e.  A )  ->  k  e.  U )
5 fsumsplit.4 . . . . . 6  |-  ( (
ph  /\  k  e.  U )  ->  C  e.  CC )
64, 5syldan 477 . . . . 5  |-  ( (
ph  /\  k  e.  A )  ->  C  e.  CC )
76ralrimiva 2814 . . . 4  |-  ( ph  ->  A. k  e.  A  C  e.  CC )
8 fsumsplit.3 . . . . 5  |-  ( ph  ->  U  e.  Fin )
98olcd 399 . . . 4  |-  ( ph  ->  ( U  C_  ( ZZ>=
`  0 )  \/  U  e.  Fin )
)
10 sumss2 13841 . . . 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 1275 . . 3  |-  ( ph  -> 
sum_ k  e.  A  C  =  sum_ k  e.  U  if ( k  e.  A ,  C ,  0 ) )
12 ssun2 3610 . . . . 5  |-  B  C_  ( A  u.  B
)
1312, 2syl5sseqr 3493 . . . 4  |-  ( ph  ->  B  C_  U )
1413sselda 3444 . . . . . 6  |-  ( (
ph  /\  k  e.  B )  ->  k  e.  U )
1514, 5syldan 477 . . . . 5  |-  ( (
ph  /\  k  e.  B )  ->  C  e.  CC )
1615ralrimiva 2814 . . . 4  |-  ( ph  ->  A. k  e.  B  C  e.  CC )
17 sumss2 13841 . . . 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 1275 . . 3  |-  ( ph  -> 
sum_ k  e.  B  C  =  sum_ k  e.  U  if ( k  e.  B ,  C ,  0 ) )
1911, 18oveq12d 6333 . 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 9661 . . . 4  |-  0  e.  CC
21 ifcl 3935 . . . 4  |-  ( ( C  e.  CC  /\  0  e.  CC )  ->  if ( k  e.  A ,  C , 
0 )  e.  CC )
225, 20, 21sylancl 673 . . 3  |-  ( (
ph  /\  k  e.  U )  ->  if ( k  e.  A ,  C ,  0 )  e.  CC )
23 ifcl 3935 . . . 4  |-  ( ( C  e.  CC  /\  0  e.  CC )  ->  if ( k  e.  B ,  C , 
0 )  e.  CC )
245, 20, 23sylancl 673 . . 3  |-  ( (
ph  /\  k  e.  U )  ->  if ( k  e.  B ,  C ,  0 )  e.  CC )
258, 22, 24fsumadd 13854 . 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 2525 . . . . . 6  |-  ( ph  ->  ( k  e.  U  <->  k  e.  ( A  u.  B ) ) )
27 elun 3586 . . . . . 6  |-  ( k  e.  ( A  u.  B )  <->  ( k  e.  A  \/  k  e.  B ) )
2826, 27syl6bb 269 . . . . 5  |-  ( ph  ->  ( k  e.  U  <->  ( k  e.  A  \/  k  e.  B )
) )
2928biimpa 491 . . . 4  |-  ( (
ph  /\  k  e.  U )  ->  (
k  e.  A  \/  k  e.  B )
)
30 iftrue 3899 . . . . . . . 8  |-  ( k  e.  A  ->  if ( k  e.  A ,  C ,  0 )  =  C )
3130adantl 472 . . . . . . 7  |-  ( (
ph  /\  k  e.  A )  ->  if ( k  e.  A ,  C ,  0 )  =  C )
32 noel 3747 . . . . . . . . . . 11  |-  -.  k  e.  (/)
33 elin 3629 . . . . . . . . . . . 12  |-  ( k  e.  ( A  i^i  B )  <->  ( k  e.  A  /\  k  e.  B ) )
34 fsumsplit.1 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A  i^i  B
)  =  (/) )
3534eleq2d 2525 . . . . . . . . . . . 12  |-  ( ph  ->  ( k  e.  ( A  i^i  B )  <-> 
k  e.  (/) ) )
3633, 35syl5rbbr 268 . . . . . . . . . . 11  |-  ( ph  ->  ( k  e.  (/)  <->  (
k  e.  A  /\  k  e.  B )
) )
3732, 36mtbii 308 . . . . . . . . . 10  |-  ( ph  ->  -.  ( k  e.  A  /\  k  e.  B ) )
38 imnan 428 . . . . . . . . . 10  |-  ( ( k  e.  A  ->  -.  k  e.  B
)  <->  -.  ( k  e.  A  /\  k  e.  B ) )
3937, 38sylibr 217 . . . . . . . . 9  |-  ( ph  ->  ( k  e.  A  ->  -.  k  e.  B
) )
4039imp 435 . . . . . . . 8  |-  ( (
ph  /\  k  e.  A )  ->  -.  k  e.  B )
4140iffalsed 3904 . . . . . . 7  |-  ( (
ph  /\  k  e.  A )  ->  if ( k  e.  B ,  C ,  0 )  =  0 )
4231, 41oveq12d 6333 . . . . . 6  |-  ( (
ph  /\  k  e.  A )  ->  ( if ( k  e.  A ,  C ,  0 )  +  if ( k  e.  B ,  C ,  0 ) )  =  ( C  + 
0 ) )
436addid1d 9859 . . . . . 6  |-  ( (
ph  /\  k  e.  A )  ->  ( C  +  0 )  =  C )
4442, 43eqtrd 2496 . . . . 5  |-  ( (
ph  /\  k  e.  A )  ->  ( if ( k  e.  A ,  C ,  0 )  +  if ( k  e.  B ,  C ,  0 ) )  =  C )
4539con2d 120 . . . . . . . . 9  |-  ( ph  ->  ( k  e.  B  ->  -.  k  e.  A
) )
4645imp 435 . . . . . . . 8  |-  ( (
ph  /\  k  e.  B )  ->  -.  k  e.  A )
4746iffalsed 3904 . . . . . . 7  |-  ( (
ph  /\  k  e.  B )  ->  if ( k  e.  A ,  C ,  0 )  =  0 )
48 iftrue 3899 . . . . . . . 8  |-  ( k  e.  B  ->  if ( k  e.  B ,  C ,  0 )  =  C )
4948adantl 472 . . . . . . 7  |-  ( (
ph  /\  k  e.  B )  ->  if ( k  e.  B ,  C ,  0 )  =  C )
5047, 49oveq12d 6333 . . . . . 6  |-  ( (
ph  /\  k  e.  B )  ->  ( if ( k  e.  A ,  C ,  0 )  +  if ( k  e.  B ,  C ,  0 ) )  =  ( 0  +  C ) )
5115addid2d 9860 . . . . . 6  |-  ( (
ph  /\  k  e.  B )  ->  (
0  +  C )  =  C )
5250, 51eqtrd 2496 . . . . 5  |-  ( (
ph  /\  k  e.  B )  ->  ( if ( k  e.  A ,  C ,  0 )  +  if ( k  e.  B ,  C ,  0 ) )  =  C )
5344, 52jaodan 799 . . . 4  |-  ( (
ph  /\  ( k  e.  A  \/  k  e.  B ) )  -> 
( if ( k  e.  A ,  C ,  0 )  +  if ( k  e.  B ,  C , 
0 ) )  =  C )
5429, 53syldan 477 . . 3  |-  ( (
ph  /\  k  e.  U )  ->  ( if ( k  e.  A ,  C ,  0 )  +  if ( k  e.  B ,  C ,  0 ) )  =  C )
5554sumeq2dv 13818 . 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 2503 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 374    /\ wa 375    = wceq 1455    e. wcel 1898   A.wral 2749    u. cun 3414    i^i cin 3415    C_ wss 3416   (/)c0 3743   ifcif 3893   ` cfv 5601  (class class class)co 6315   Fincfn 7595   CCcc 9563   0cc0 9565    + caddc 9568   ZZ>=cuz 11188   sum_csu 13801
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-inf2 8172  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642  ax-pre-sup 9643
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-fal 1461  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-se 4813  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-1st 6820  df-2nd 6821  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-1o 7208  df-oadd 7212  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599  df-sup 7982  df-oi 8051  df-card 8399  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-div 10298  df-nn 10638  df-2 10696  df-3 10697  df-n0 10899  df-z 10967  df-uz 11189  df-rp 11332  df-fz 11814  df-fzo 11947  df-seq 12246  df-exp 12305  df-hash 12548  df-cj 13211  df-re 13212  df-im 13213  df-sqrt 13347  df-abs 13348  df-clim 13601  df-sum 13802
This theorem is referenced by:  sumpr  13858  sumtp  13859  fsumm1  13861  fsum1p  13863  fsumsplitsnun  13865  fsum2dlem  13880  fsumless  13905  fsumabs  13910  fsumrlim  13920  fsumo1  13921  o1fsum  13922  cvgcmpce  13927  fsumiun  13930  incexclem  13943  incexc  13944  isumltss  13955  climcndslem1  13956  climcndslem2  13957  mertenslem1  13989  bitsinv1  14465  bitsinvp1  14472  sylow2a  17320  fsumcn  21951  ovolfiniun  22503  volfiniun  22549  uniioombllem3  22592  itgfsum  22833  dvmptfsum  22976  vieta1lem2  23313  mtest  23408  birthdaylem2  23927  fsumharmonic  23986  ftalem5  24050  ftalem5OLD  24052  chtprm  24129  chtdif  24134  perfectlem2  24207  lgsquadlem2  24332  dchrisumlem1  24376  dchrisumlem2  24377  rpvmasum2  24399  dchrisum0lem1b  24402  dchrisum0lem3  24406  pntrsumbnd2  24454  pntrlog2bndlem6  24470  pntpbnd2  24474  pntlemf  24492  axlowdimlem16  25036  axlowdimlem17  25037  signsplypnf  29488  jm2.22  35895  jm2.23  35896  sumpair  37396  fsumsplitf  37684  sumnnodd  37748  stoweidlem11  37909  stoweidlem26  37924  stoweidlem44  37943  sge0resplit  38286  sge0split  38289  perfectALTVlem2  38882  fsumsplitsndif  39138
  Copyright terms: Public domain W3C validator