Theorem fsumcl 15784

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

Hypotheses

Ref	Expression
fsumcl.1	⊢ (𝜑 → 𝐴 ∈ Fin)
fsumcl.2	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
fsumcl	⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℂ)

Distinct variable groups:   𝐴,𝑘   𝜑,𝑘

Allowed substitution hint:   𝐵(𝑘)

Proof of Theorem fsumcl

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssidd 3968	. 2 ⊢ (𝜑 → ℂ ⊆ ℂ)
2		addcl 11182	. . 3 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ)
3	2	adantl 486	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 + 𝑦) ∈ ℂ)
4		fsumcl.1	. 2 ⊢ (𝜑 → 𝐴 ∈ Fin)
5		fsumcl.2	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
6		0cnd 11199	. 2 ⊢ (𝜑 → 0 ∈ ℂ)
7	1, 3, 4, 5, 6	fsumcllem 15783	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℂ)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  (class class class)co 7411  Fincfn 8943  ℂcc 11098   + caddc 11103  Σcsu 15737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-inf2 9610  ax-cnex 11156  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-addrcl 11161  ax-mulcl 11162  ax-mulrcl 11163  ax-mulcom 11164  ax-addass 11165  ax-mulass 11166  ax-distr 11167  ax-i2m1 11168  ax-1ne0 11169  ax-1rid 11170  ax-rnegex 11171  ax-rrecex 11172  ax-cnre 11173  ax-pre-lttri 11174  ax-pre-lttrn 11175  ax-pre-ltadd 11176  ax-pre-mulgt0 11177  ax-pre-sup 11178

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-int 4917  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-se 5616  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7863  df-1st 7986  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8358  df-rdg 8397  df-1o 8453  df-er 8694  df-en 8944  df-dom 8945  df-sdom 8946  df-fin 8947  df-sup 9402  df-oi 9472  df-card 9925  df-pnf 11245  df-mnf 11246  df-xr 11247  df-ltxr 11248  df-le 11249  df-sub 11443  df-neg 11444  df-div 11872  df-nn 12234  df-2 12303  df-3 12304  df-n0 12505  df-z 12592  df-uz 12863  df-rp 13017  df-fz 13536  df-fzo 13683  df-seq 14038  df-exp 14098  df-hash 14367  df-cj 15150  df-re 15151  df-im 15152  df-sqrt 15286  df-abs 15287  df-clim 15539  df-sum 15738

This theorem is referenced by:  fsumclf  15789  fsum2dlem  15821  fsum0diag2  15834  fsummulc1  15836  fsumdivc  15837  fsumneg  15838  fsumsub  15839  fsum2mul  15840  fsumabs  15853  telfsumo  15854  fsumparts  15858  o1fsum  15865  cvgcmpce  15870  climfsum  15872  fsumiun  15873  binom1dif  15887  incexclem  15890  incexc  15891  isumsplit  15894  arisum2  15915  geoserg  15920  pwdif  15922  mertenslem1  15938  mertens  15940  binomfallfaclem2  16094  bpolycl  16106  bpolysum  16107  bpolydiflem  16108  fsumkthpow  16110  fprodefsum  16149  eirrlem  16260  pwp1fsum  16449  pcfac  16959  sylow2a  19689  itg1addlem5  25828  itgcl  25912  dvmptfsum  26103  dvfsumabs  26151  dvfsumlem1  26154  plyf  26324  plymullem1  26340  coeeulem  26350  coemullem  26376  plycjlem  26402  taylpf  26495  mtest  26533  mtestbdd  26534  pserdvlem2  26557  abelthlem6  26565  abelthlem7  26567  advlogexp  26786  log2tlbnd  27076  birthdaylem2  27083  fsumharmonic  27142  lgamcvg2  27185  ftalem1  27203  ftalem5  27207  sgmf  27275  chtdif  27288  fsumdvdscom  27315  fsumdvdsmul  27325  logexprlim  27355  dchrsum2  27398  sumdchr2  27400  rpvmasumlem  27617  dchrisumlem1  27619  dchrisumlem2  27620  dchrisum  27622  dchrmusum2  27624  dchrvmasum2if  27627  dchrvmasumlem3  27629  dchrvmasumiflem1  27631  dchrvmasumiflem2  27632  rpvmasum2  27642  dchrisum0lem1b  27645  dchrisum0lem1  27646  dchrisum0lem2a  27647  dchrisum0lem2  27648  dchrisum0lem3  27649  dchrmusumlem  27652  dchrvmasumlem  27653  mudivsum  27660  mulogsumlem  27661  mulogsum  27662  mulog2sumlem1  27664  mulog2sumlem2  27665  mulog2sumlem3  27666  vmalogdivsum  27669  logsqvma  27672  selberglem1  27675  selberglem2  27676  selberg2lem  27680  selberg2  27681  selberg3lem1  27687  pntrsumo1  27695  pntrsumbnd  27696  selbergr  27698  selberg4r  27700  pntrlog2bndlem2  27708  pntrlog2bndlem4  27710  pntrlog2bndlem5  27711  pntlemo  27737  ax5seglem6  29225  axlowdimlem16  29248  finsumvtxdg2ssteplem4  29839  dipcl  31005  indsumin  33122  elrgspnlem2  33504  esumcvg  34421  fsum2dsub  34939  reprsuc  34947  breprexplemc  34964  breprexp  34965  breprexpnat  34966  vtscl  34970  circlemeth  34972  hgt750lemd  34980  tgoldbachgtde  34992  subfacval2  35578  subfaclim  35579  fwddifnp1  36556  knoppndvlem11  37000  aks4d1p1p1  42720  sticksstones12a  42814  unitscyglem2  42853  sumcubes  42964  fltnltalem  43286  jm2.23  43615  fsumsermpt  46187  sumnnodd  46238  dvnmul  46549  dvnprodlem1  46552  dvnprodlem2  46553  stoweidlem26  46632  dirkertrigeqlem2  46705  dirkeritg  46708  fourierdlem73  46785  fourierdlem83  46795  elaa2lem  46839  etransclem23  46863  etransclem27  46867  etransclem31  46871  etransclem33  46873  etransclem39  46879  etransclem46  46886  etransclem47  46887  etransclem48  46888  altgsumbcALT  49018  nn0sumshdiglemA  49284  amgmlemALT  50477