Theorem fsumcl 13329

Description: Closure of a finite sum of complex numbers A ( k ). (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.)

Hypotheses

Ref	Expression
fsumcl.1	|- ( ph -> A e. Fin )
fsumcl.2	|- ( ( ph /\ k e. A ) -> B e. CC )

Assertion

Ref	Expression
fsumcl	|- ( ph -> sum_ k e. A B e. CC )

Distinct variable groups:   A, k   ph, k

Allowed substitution hint:   B( k)

Proof of Theorem fsumcl

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssid 3484	. . 3 |- CC C_ CC
2	1	a1i 11	. 2 |- ( ph -> CC C_ CC )
3		addcl 9476	. . 3 |- ( ( x e. CC /\ y e. CC ) -> ( x + y ) e. CC )
4	3	adantl 466	. 2 |- ( ( ph /\ ( x e. CC /\ y e. CC ) ) -> ( x + y ) e. CC )
5		fsumcl.1	. 2 |- ( ph -> A e. Fin )
6		fsumcl.2	. 2 |- ( ( ph /\ k e. A ) -> B e. CC )
7		0cnd 9491	. 2 |- ( ph -> 0 e. CC )
8	2, 4, 5, 6, 7	fsumcllem 13328	1 |- ( ph -> sum_ k e. A B e. CC )

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1758   C_ wss 3437  (class class class)co 6201   Fincfn 7421   CCcc 9392   + caddc 9397   sum_csu 13282

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4512  ax-sep 4522  ax-nul 4530  ax-pow 4579  ax-pr 4640  ax-un 6483  ax-inf2 7959  ax-cnex 9450  ax-resscn 9451  ax-1cn 9452  ax-icn 9453  ax-addcl 9454  ax-addrcl 9455  ax-mulcl 9456  ax-mulrcl 9457  ax-mulcom 9458  ax-addass 9459  ax-mulass 9460  ax-distr 9461  ax-i2m1 9462  ax-1ne0 9463  ax-1rid 9464  ax-rnegex 9465  ax-rrecex 9466  ax-cnre 9467  ax-pre-lttri 9468  ax-pre-lttrn 9469  ax-pre-ltadd 9470  ax-pre-mulgt0 9471  ax-pre-sup 9472

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-fal 1376  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-nel 2651  df-ral 2804  df-rex 2805  df-reu 2806  df-rmo 2807  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3747  df-if 3901  df-pw 3971  df-sn 3987  df-pr 3989  df-tp 3991  df-op 3993  df-uni 4201  df-int 4238  df-iun 4282  df-br 4402  df-opab 4460  df-mpt 4461  df-tr 4495  df-eprel 4741  df-id 4745  df-po 4750  df-so 4751  df-fr 4788  df-se 4789  df-we 4790  df-ord 4831  df-on 4832  df-lim 4833  df-suc 4834  df-xp 4955  df-rel 4956  df-cnv 4957  df-co 4958  df-dm 4959  df-rn 4960  df-res 4961  df-ima 4962  df-iota 5490  df-fun 5529  df-fn 5530  df-f 5531  df-f1 5532  df-fo 5533  df-f1o 5534  df-fv 5535  df-isom 5536  df-riota 6162  df-ov 6204  df-oprab 6205  df-mpt2 6206  df-om 6588  df-1st 6688  df-2nd 6689  df-recs 6943  df-rdg 6977  df-1o 7031  df-oadd 7035  df-er 7212  df-en 7422  df-dom 7423  df-sdom 7424  df-fin 7425  df-sup 7803  df-oi 7836  df-card 8221  df-pnf 9532  df-mnf 9533  df-xr 9534  df-ltxr 9535  df-le 9536  df-sub 9709  df-neg 9710  df-div 10106  df-nn 10435  df-2 10492  df-3 10493  df-n0 10692  df-z 10759  df-uz 10974  df-rp 11104  df-fz 11556  df-fzo 11667  df-seq 11925  df-exp 11984  df-hash 12222  df-cj 12707  df-re 12708  df-im 12709  df-sqr 12843  df-abs 12844  df-clim 13085  df-sum 13283

This theorem is referenced by:  fsum2dlem  13356  fsum0diag2  13369  fsummulc1  13371  fsumdivc  13372  fsumneg  13373  fsumsub  13374  fsum2mul  13375  fsumabs  13383  fsumtscopo  13384  fsumparts  13388  o1fsum  13395  cvgcmpce  13400  climfsum  13402  fsumiun  13403  binom1dif  13415  incexclem  13418  incexc  13419  isumsplit  13422  arisum2  13442  geoserg  13447  mertenslem1  13463  mertens  13465  eirrlem  13605  pcfac  14080  sylow2a  16240  itg1addlem5  21312  itgcl  21395  dvmptfsum  21581  dvfsumabs  21629  dvfsumlem1  21632  plyf  21800  plymullem1  21816  coeeulem  21826  coemullem  21851  plycjlem  21877  taylpf  21965  mtest  22003  mtestbdd  22004  pserdvlem2  22027  abelthlem6  22035  abelthlem7  22037  advlogexp  22234  log2tlbnd  22474  birthdaylem2  22480  fsumharmonic  22539  ftalem1  22544  ftalem5  22548  sgmf  22617  chtdif  22630  fsumdvdscom  22659  fsumdvdsmul  22669  logexprlim  22698  dchrsum2  22741  sumdchr2  22743  rpvmasumlem  22870  dchrisumlem1  22872  dchrisumlem2  22873  dchrisum  22875  dchrmusum2  22877  dchrvmasum2if  22880  dchrvmasumlem3  22882  dchrvmasumiflem1  22884  dchrvmasumiflem2  22885  rpvmasum2  22895  dchrisum0lem1b  22898  dchrisum0lem1  22899  dchrisum0lem2a  22900  dchrisum0lem2  22901  dchrisum0lem3  22902  dchrmusumlem  22905  dchrvmasumlem  22906  mudivsum  22913  mulogsumlem  22914  mulogsum  22915  mulog2sumlem1  22917  mulog2sumlem2  22918  mulog2sumlem3  22919  vmalogdivsum  22922  logsqvma  22925  selberglem1  22928  selberglem2  22929  selberg2lem  22933  selberg2  22934  selberg3lem1  22940  pntrsumo1  22948  pntrsumbnd  22949  selbergr  22951  selberg4r  22953  pntrlog2bndlem2  22961  pntrlog2bndlem4  22963  pntrlog2bndlem5  22964  pntlemo  22990  ax5seglem6  23333  axlowdimlem16  23356  dipcl  24263  esumcvg  26681  lgamcvg2  27186  subfacval2  27220  subfaclim  27221  fprodefsum  27630  binomfallfaclem2  27688  bpolycl  28340  bpolysum  28341  bpolydiflem  28342  fsumkthpow  28344  jm2.23  29494  stoweidlem26  29970  altgsumbcALT  30899