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

Theorem sumz 13565
Description: Any sum of zero over a summable set is zero. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Mario Carneiro, 20-Apr-2014.)
Assertion
Ref Expression
sumz  |-  ( ( A  C_  ( ZZ>= `  M )  \/  A  e.  Fin )  ->  sum_ k  e.  A  0  = 
0 )
Distinct variable groups:    A, k    k, M

Proof of Theorem sumz
Dummy variables  f  n are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2392 . . . . 5  |-  ( ZZ>= `  M )  =  (
ZZ>= `  M )
2 simpr 459 . . . . 5  |-  ( ( A  C_  ( ZZ>= `  M )  /\  M  e.  ZZ )  ->  M  e.  ZZ )
3 simpl 455 . . . . 5  |-  ( ( A  C_  ( ZZ>= `  M )  /\  M  e.  ZZ )  ->  A  C_  ( ZZ>= `  M )
)
4 c0ex 9519 . . . . . . . 8  |-  0  e.  _V
54fvconst2 6043 . . . . . . 7  |-  ( k  e.  ( ZZ>= `  M
)  ->  ( (
( ZZ>= `  M )  X.  { 0 } ) `
 k )  =  0 )
6 ifid 3907 . . . . . . 7  |-  if ( k  e.  A , 
0 ,  0 )  =  0
75, 6syl6eqr 2451 . . . . . 6  |-  ( k  e.  ( ZZ>= `  M
)  ->  ( (
( ZZ>= `  M )  X.  { 0 } ) `
 k )  =  if ( k  e.  A ,  0 ,  0 ) )
87adantl 464 . . . . 5  |-  ( ( ( A  C_  ( ZZ>=
`  M )  /\  M  e.  ZZ )  /\  k  e.  ( ZZ>=
`  M ) )  ->  ( ( (
ZZ>= `  M )  X. 
{ 0 } ) `
 k )  =  if ( k  e.  A ,  0 ,  0 ) )
9 0cnd 9518 . . . . 5  |-  ( ( ( A  C_  ( ZZ>=
`  M )  /\  M  e.  ZZ )  /\  k  e.  A
)  ->  0  e.  CC )
101, 2, 3, 8, 9zsum 13561 . . . 4  |-  ( ( A  C_  ( ZZ>= `  M )  /\  M  e.  ZZ )  ->  sum_ k  e.  A  0  =  ( 
~~>  `  seq M (  +  ,  ( (
ZZ>= `  M )  X. 
{ 0 } ) ) ) )
11 fclim 13397 . . . . . 6  |-  ~~>  : dom  ~~>  --> CC
12 ffun 5654 . . . . . 6  |-  (  ~~>  : dom  ~~>  --> CC 
->  Fun  ~~>  )
1311, 12ax-mp 5 . . . . 5  |-  Fun  ~~>
14 serclim0 13421 . . . . . 6  |-  ( M  e.  ZZ  ->  seq M (  +  , 
( ( ZZ>= `  M
)  X.  { 0 } ) )  ~~>  0 )
1514adantl 464 . . . . 5  |-  ( ( A  C_  ( ZZ>= `  M )  /\  M  e.  ZZ )  ->  seq M (  +  , 
( ( ZZ>= `  M
)  X.  { 0 } ) )  ~~>  0 )
16 funbrfv 5825 . . . . 5  |-  ( Fun  ~~>  ->  (  seq M (  +  ,  ( (
ZZ>= `  M )  X. 
{ 0 } ) )  ~~>  0  ->  (  ~~>  ` 
seq M (  +  ,  ( ( ZZ>= `  M )  X.  {
0 } ) ) )  =  0 ) )
1713, 15, 16mpsyl 63 . . . 4  |-  ( ( A  C_  ( ZZ>= `  M )  /\  M  e.  ZZ )  ->  (  ~~>  ` 
seq M (  +  ,  ( ( ZZ>= `  M )  X.  {
0 } ) ) )  =  0 )
1810, 17eqtrd 2433 . . 3  |-  ( ( A  C_  ( ZZ>= `  M )  /\  M  e.  ZZ )  ->  sum_ k  e.  A  0  = 
0 )
19 uzf 11022 . . . . . . . . 9  |-  ZZ>= : ZZ --> ~P ZZ
2019fdmi 5657 . . . . . . . 8  |-  dom  ZZ>=  =  ZZ
2120eleq2i 2470 . . . . . . 7  |-  ( M  e.  dom  ZZ>=  <->  M  e.  ZZ )
22 ndmfv 5811 . . . . . . 7  |-  ( -.  M  e.  dom  ZZ>=  -> 
( ZZ>= `  M )  =  (/) )
2321, 22sylnbir 305 . . . . . 6  |-  ( -.  M  e.  ZZ  ->  (
ZZ>= `  M )  =  (/) )
2423sseq2d 3458 . . . . 5  |-  ( -.  M  e.  ZZ  ->  ( A  C_  ( ZZ>= `  M )  <->  A  C_  (/) ) )
2524biimpac 484 . . . 4  |-  ( ( A  C_  ( ZZ>= `  M )  /\  -.  M  e.  ZZ )  ->  A  C_  (/) )
26 ss0 3756 . . . 4  |-  ( A 
C_  (/)  ->  A  =  (/) )
27 sumeq1 13532 . . . . 5  |-  ( A  =  (/)  ->  sum_ k  e.  A  0  =  sum_ k  e.  (/)  0 )
28 sum0 13564 . . . . 5  |-  sum_ k  e.  (/)  0  =  0
2927, 28syl6eq 2449 . . . 4  |-  ( A  =  (/)  ->  sum_ k  e.  A  0  = 
0 )
3025, 26, 293syl 20 . . 3  |-  ( ( A  C_  ( ZZ>= `  M )  /\  -.  M  e.  ZZ )  -> 
sum_ k  e.  A 
0  =  0 )
3118, 30pm2.61dan 789 . 2  |-  ( A 
C_  ( ZZ>= `  M
)  ->  sum_ k  e.  A  0  =  0 )
32 fz1f1o 13553 . . 3  |-  ( A  e.  Fin  ->  ( A  =  (/)  \/  (
( # `  A )  e.  NN  /\  E. f  f : ( 1 ... ( # `  A ) ) -1-1-onto-> A ) ) )
33 eqidd 2393 . . . . . . . . 9  |-  ( k  =  ( f `  n )  ->  0  =  0 )
34 simpl 455 . . . . . . . . 9  |-  ( ( ( # `  A
)  e.  NN  /\  f : ( 1 ... ( # `  A
) ) -1-1-onto-> A )  ->  ( # `
 A )  e.  NN )
35 simpr 459 . . . . . . . . 9  |-  ( ( ( # `  A
)  e.  NN  /\  f : ( 1 ... ( # `  A
) ) -1-1-onto-> A )  ->  f : ( 1 ... ( # `  A
) ) -1-1-onto-> A )
36 0cnd 9518 . . . . . . . . 9  |-  ( ( ( ( # `  A
)  e.  NN  /\  f : ( 1 ... ( # `  A
) ) -1-1-onto-> A )  /\  k  e.  A )  ->  0  e.  CC )
37 elfznn 11653 . . . . . . . . . . 11  |-  ( n  e.  ( 1 ... ( # `  A
) )  ->  n  e.  NN )
384fvconst2 6043 . . . . . . . . . . 11  |-  ( n  e.  NN  ->  (
( NN  X.  {
0 } ) `  n )  =  0 )
3937, 38syl 16 . . . . . . . . . 10  |-  ( n  e.  ( 1 ... ( # `  A
) )  ->  (
( NN  X.  {
0 } ) `  n )  =  0 )
4039adantl 464 . . . . . . . . 9  |-  ( ( ( ( # `  A
)  e.  NN  /\  f : ( 1 ... ( # `  A
) ) -1-1-onto-> A )  /\  n  e.  ( 1 ... ( # `
 A ) ) )  ->  ( ( NN  X.  { 0 } ) `  n )  =  0 )
4133, 34, 35, 36, 40fsum 13563 . . . . . . . 8  |-  ( ( ( # `  A
)  e.  NN  /\  f : ( 1 ... ( # `  A
) ) -1-1-onto-> A )  ->  sum_ k  e.  A  0  =  (  seq 1 (  +  ,  ( NN  X.  { 0 } ) ) `  ( # `  A ) ) )
42 nnuz 11054 . . . . . . . . . 10  |-  NN  =  ( ZZ>= `  1 )
4342ser0 12081 . . . . . . . . 9  |-  ( (
# `  A )  e.  NN  ->  (  seq 1 (  +  , 
( NN  X.  {
0 } ) ) `
 ( # `  A
) )  =  0 )
4443adantr 463 . . . . . . . 8  |-  ( ( ( # `  A
)  e.  NN  /\  f : ( 1 ... ( # `  A
) ) -1-1-onto-> A )  ->  (  seq 1 (  +  , 
( NN  X.  {
0 } ) ) `
 ( # `  A
) )  =  0 )
4541, 44eqtrd 2433 . . . . . . 7  |-  ( ( ( # `  A
)  e.  NN  /\  f : ( 1 ... ( # `  A
) ) -1-1-onto-> A )  ->  sum_ k  e.  A  0  = 
0 )
4645ex 432 . . . . . 6  |-  ( (
# `  A )  e.  NN  ->  ( f : ( 1 ... ( # `  A
) ) -1-1-onto-> A  ->  sum_ k  e.  A  0  =  0 ) )
4746exlimdv 1739 . . . . 5  |-  ( (
# `  A )  e.  NN  ->  ( E. f  f : ( 1 ... ( # `  A ) ) -1-1-onto-> A  ->  sum_ k  e.  A  0  =  0 ) )
4847imp 427 . . . 4  |-  ( ( ( # `  A
)  e.  NN  /\  E. f  f : ( 1 ... ( # `  A ) ) -1-1-onto-> A )  ->  sum_ k  e.  A 
0  =  0 )
4929, 48jaoi 377 . . 3  |-  ( ( A  =  (/)  \/  (
( # `  A )  e.  NN  /\  E. f  f : ( 1 ... ( # `  A ) ) -1-1-onto-> A ) )  ->  sum_ k  e.  A  0  =  0 )
5032, 49syl 16 . 2  |-  ( A  e.  Fin  ->  sum_ k  e.  A  0  = 
0 )
5131, 50jaoi 377 1  |-  ( ( A  C_  ( ZZ>= `  M )  \/  A  e.  Fin )  ->  sum_ k  e.  A  0  = 
0 )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 366    /\ wa 367    = wceq 1399   E.wex 1627    e. wcel 1836    C_ wss 3402   (/)c0 3724   ifcif 3870   ~Pcpw 3940   {csn 3957   class class class wbr 4380    X. cxp 4924   dom cdm 4926   Fun wfun 5503   -->wf 5505   -1-1-onto->wf1o 5508   ` cfv 5509  (class class class)co 6214   Fincfn 7453   CCcc 9419   0cc0 9421   1c1 9422    + caddc 9424   NNcn 10470   ZZcz 10799   ZZ>=cuz 11019   ...cfz 11611    seqcseq 12029   #chash 12326    ~~> cli 13328   sum_csu 13529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-rep 4491  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509  ax-inf2 7990  ax-cnex 9477  ax-resscn 9478  ax-1cn 9479  ax-icn 9480  ax-addcl 9481  ax-addrcl 9482  ax-mulcl 9483  ax-mulrcl 9484  ax-mulcom 9485  ax-addass 9486  ax-mulass 9487  ax-distr 9488  ax-i2m1 9489  ax-1ne0 9490  ax-1rid 9491  ax-rnegex 9492  ax-rrecex 9493  ax-cnre 9494  ax-pre-lttri 9495  ax-pre-lttrn 9496  ax-pre-ltadd 9497  ax-pre-mulgt0 9498  ax-pre-sup 9499
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-nel 2590  df-ral 2747  df-rex 2748  df-reu 2749  df-rmo 2750  df-rab 2751  df-v 3049  df-sbc 3266  df-csb 3362  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-pss 3418  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-tp 3962  df-op 3964  df-uni 4177  df-int 4213  df-iun 4258  df-br 4381  df-opab 4439  df-mpt 4440  df-tr 4474  df-eprel 4718  df-id 4722  df-po 4727  df-so 4728  df-fr 4765  df-se 4766  df-we 4767  df-ord 4808  df-on 4809  df-lim 4810  df-suc 4811  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-fv 5517  df-isom 5518  df-riota 6176  df-ov 6217  df-oprab 6218  df-mpt2 6219  df-om 6618  df-1st 6717  df-2nd 6718  df-recs 6978  df-rdg 7012  df-1o 7066  df-oadd 7070  df-er 7247  df-en 7454  df-dom 7455  df-sdom 7456  df-fin 7457  df-sup 7834  df-oi 7868  df-card 8251  df-pnf 9559  df-mnf 9560  df-xr 9561  df-ltxr 9562  df-le 9563  df-sub 9738  df-neg 9739  df-div 10142  df-nn 10471  df-2 10529  df-3 10530  df-n0 10731  df-z 10800  df-uz 11020  df-rp 11158  df-fz 11612  df-fzo 11736  df-seq 12030  df-exp 12089  df-hash 12327  df-cj 12953  df-re 12954  df-im 12955  df-sqrt 13089  df-abs 13090  df-clim 13332  df-sum 13530
This theorem is referenced by:  fsum00  13633  fsumdvds  14050  pcfac  14439  ovoliunnul  22022  vitalilem5  22125  itg1addlem5  22211  itg10a  22221  itg0  22290  itgz  22291  plymullem1  22715  coemullem  22751  logtayl  23147  ftalem5  23486  chp1  23577  logexprlim  23636  bposlem2  23696  rpvmasumlem  23808  axcgrid  24361  axlowdimlem16  24402  plymulx0  28723  signsplypnf  28726  volsupnfl  30260  binomcxplemnn0  31458  binomcxplemnotnn0  31465  sumnnodd  31837  stoweidlem37  32020  fourierdlem103  32193  fourierdlem104  32194  etransclem24  32242  etransclem32  32250  etransclem35  32253  aacllem  33585
  Copyright terms: Public domain W3C validator