Theorem fsumcl 15128

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 3916	. 2 ⊢ (𝜑 → ℂ ⊆ ℂ)
2		addcl 10647	. . 3 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ)
3	2	adantl 486	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 + 𝑦) ∈ ℂ)
4		fsumcl.1	. 2 ⊢ (𝜑 → 𝐴 ∈ Fin)
5		fsumcl.2	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
6		0cnd 10662	. 2 ⊢ (𝜑 → 0 ∈ ℂ)
7	1, 3, 4, 5, 6	fsumcllem 15127	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℂ)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2112  (class class class)co 7148  Fincfn 8525  ℂcc 10563   + caddc 10568  Σcsu 15080

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7457  ax-inf2 9127  ax-cnex 10621  ax-resscn 10622  ax-1cn 10623  ax-icn 10624  ax-addcl 10625  ax-addrcl 10626  ax-mulcl 10627  ax-mulrcl 10628  ax-mulcom 10629  ax-addass 10630  ax-mulass 10631  ax-distr 10632  ax-i2m1 10633  ax-1ne0 10634  ax-1rid 10635  ax-rnegex 10636  ax-rrecex 10637  ax-cnre 10638  ax-pre-lttri 10639  ax-pre-lttrn 10640  ax-pre-ltadd 10641  ax-pre-mulgt0 10642  ax-pre-sup 10643

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4419  df-pw 4494  df-sn 4521  df-pr 4523  df-tp 4525  df-op 4527  df-uni 4797  df-int 4837  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5428  df-eprel 5433  df-po 5441  df-so 5442  df-fr 5481  df-se 5482  df-we 5483  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-res 5534  df-ima 5535  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6292  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-isom 6342  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7578  df-1st 7691  df-2nd 7692  df-wrecs 7955  df-recs 8016  df-rdg 8054  df-1o 8110  df-oadd 8114  df-er 8297  df-en 8526  df-dom 8527  df-sdom 8528  df-fin 8529  df-sup 8929  df-oi 8997  df-card 9391  df-pnf 10705  df-mnf 10706  df-xr 10707  df-ltxr 10708  df-le 10709  df-sub 10900  df-neg 10901  df-div 11326  df-nn 11665  df-2 11727  df-3 11728  df-n0 11925  df-z 12011  df-uz 12273  df-rp 12421  df-fz 12930  df-fzo 13073  df-seq 13409  df-exp 13470  df-hash 13731  df-cj 14496  df-re 14497  df-im 14498  df-sqrt 14632  df-abs 14633  df-clim 14883  df-sum 15081

This theorem is referenced by:  fsum2dlem  15163  fsum0diag2  15176  fsummulc1  15178  fsumdivc  15179  fsumneg  15180  fsumsub  15181  fsum2mul  15182  fsumabs  15194  telfsumo  15195  fsumparts  15199  o1fsum  15206  cvgcmpce  15211  climfsum  15213  fsumiun  15214  binom1dif  15226  incexclem  15229  incexc  15230  isumsplit  15233  arisum2  15254  geoserg  15259  pwdif  15261  pwm1geoserOLD  15263  mertenslem1  15278  mertens  15280  binomfallfaclem2  15432  bpolycl  15444  bpolysum  15445  bpolydiflem  15446  fsumkthpow  15448  fprodefsum  15486  eirrlem  15595  pwp1fsum  15782  pcfac  16280  sylow2a  18801  itg1addlem5  24390  itgcl  24473  dvmptfsum  24664  dvfsumabs  24712  dvfsumlem1  24715  plyf  24884  plymullem1  24900  coeeulem  24910  coemullem  24936  plycjlem  24962  taylpf  25050  mtest  25088  mtestbdd  25089  pserdvlem2  25112  abelthlem6  25120  abelthlem7  25122  advlogexp  25335  log2tlbnd  25620  birthdaylem2  25627  fsumharmonic  25686  lgamcvg2  25729  ftalem1  25747  ftalem5  25751  sgmf  25819  chtdif  25832  fsumdvdscom  25859  fsumdvdsmul  25869  logexprlim  25898  dchrsum2  25941  sumdchr2  25943  rpvmasumlem  26160  dchrisumlem1  26162  dchrisumlem2  26163  dchrisum  26165  dchrmusum2  26167  dchrvmasum2if  26170  dchrvmasumlem3  26172  dchrvmasumiflem1  26174  dchrvmasumiflem2  26175  rpvmasum2  26185  dchrisum0lem1b  26188  dchrisum0lem1  26189  dchrisum0lem2a  26190  dchrisum0lem2  26191  dchrisum0lem3  26192  dchrmusumlem  26195  dchrvmasumlem  26196  mudivsum  26203  mulogsumlem  26204  mulogsum  26205  mulog2sumlem1  26207  mulog2sumlem2  26208  mulog2sumlem3  26209  vmalogdivsum  26212  logsqvma  26215  selberglem1  26218  selberglem2  26219  selberg2lem  26223  selberg2  26224  selberg3lem1  26230  pntrsumo1  26238  pntrsumbnd  26239  selbergr  26241  selberg4r  26243  pntrlog2bndlem2  26251  pntrlog2bndlem4  26253  pntrlog2bndlem5  26254  pntlemo  26280  ax5seglem6  26817  axlowdimlem16  26840  finsumvtxdg2ssteplem4  27427  dipcl  28584  indsumin  31499  esumcvg  31563  fsum2dsub  32096  reprsuc  32104  breprexplemc  32121  breprexp  32122  breprexpnat  32123  vtscl  32127  circlemeth  32129  hgt750lemd  32137  tgoldbachgtde  32149  subfacval2  32655  subfaclim  32656  fwddifnp1  34006  knoppndvlem11  34241  aks4d1p1p1  39619  fltnltalem  39981  jm2.23  40300  fsumclf  42567  fsumsermpt  42577  sumnnodd  42628  dvnmul  42941  dvnprodlem1  42944  dvnprodlem2  42945  stoweidlem26  43024  dirkertrigeqlem2  43097  dirkeritg  43100  fourierdlem73  43177  fourierdlem83  43187  elaa2lem  43231  etransclem23  43255  etransclem27  43259  etransclem31  43263  etransclem33  43265  etransclem39  43271  etransclem46  43278  etransclem47  43279  etransclem48  43280  altgsumbcALT  45112  nn0sumshdiglemA  45388  amgmlemALT  45686