Theorem fsumcl 15760

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 3959	. 2 ⊢ (𝜑 → ℂ ⊆ ℂ)
2		addcl 11155	. . 3 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ)
3	2	adantl 485	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 + 𝑦) ∈ ℂ)
4		fsumcl.1	. 2 ⊢ (𝜑 → 𝐴 ∈ Fin)
5		fsumcl.2	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
6		0cnd 11172	. 2 ⊢ (𝜑 → 0 ∈ ℂ)
7	1, 3, 4, 5, 6	fsumcllem 15759	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℂ)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2142  (class class class)co 7396  Fincfn 8927  ℂcc 11071   + caddc 11076  Σcsu 15713

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5227  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-inf2 9596  ax-cnex 11129  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149  ax-pre-mulgt0 11150  ax-pre-sup 11151

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-int 4906  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-se 5601  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-isom 6530  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7847  df-1st 7970  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-1o 8437  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-fin 8931  df-sup 9388  df-oi 9458  df-card 9897  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222  df-sub 11416  df-neg 11417  df-div 11845  df-nn 12211  df-2 12280  df-3 12281  df-n0 12482  df-z 12569  df-uz 12840  df-rp 12994  df-fz 13513  df-fzo 13660  df-seq 14015  df-exp 14075  df-hash 14344  df-cj 15126  df-re 15127  df-im 15128  df-sqrt 15262  df-abs 15263  df-clim 15515  df-sum 15714

This theorem is referenced by:  fsumclf  15765  fsum2dlem  15797  fsum0diag2  15810  fsummulc1  15812  fsumdivc  15813  fsumneg  15814  fsumsub  15815  fsum2mul  15816  fsumabs  15829  telfsumo  15830  fsumparts  15834  o1fsum  15841  cvgcmpce  15846  climfsum  15848  fsumiun  15849  binom1dif  15863  incexclem  15866  incexc  15867  isumsplit  15870  arisum2  15891  geoserg  15896  pwdif  15898  mertenslem1  15914  mertens  15916  binomfallfaclem2  16070  bpolycl  16082  bpolysum  16083  bpolydiflem  16084  fsumkthpow  16086  fprodefsum  16125  eirrlem  16236  pwp1fsum  16425  pcfac  16935  sylow2a  19659  itg1addlem5  25762  itgcl  25846  dvmptfsum  26037  dvfsumabs  26085  dvfsumlem1  26088  plyf  26258  plymullem1  26274  coeeulem  26284  coemullem  26310  plycjlem  26336  taylpf  26429  mtest  26467  mtestbdd  26468  pserdvlem2  26491  abelthlem6  26499  abelthlem7  26501  advlogexp  26720  log2tlbnd  27010  birthdaylem2  27017  fsumharmonic  27076  lgamcvg2  27119  ftalem1  27137  ftalem5  27141  sgmf  27209  chtdif  27222  fsumdvdscom  27249  fsumdvdsmul  27259  logexprlim  27289  dchrsum2  27332  sumdchr2  27334  rpvmasumlem  27551  dchrisumlem1  27553  dchrisumlem2  27554  dchrisum  27556  dchrmusum2  27558  dchrvmasum2if  27561  dchrvmasumlem3  27563  dchrvmasumiflem1  27565  dchrvmasumiflem2  27566  rpvmasum2  27576  dchrisum0lem1b  27579  dchrisum0lem1  27580  dchrisum0lem2a  27581  dchrisum0lem2  27582  dchrisum0lem3  27583  dchrmusumlem  27586  dchrvmasumlem  27587  mudivsum  27594  mulogsumlem  27595  mulogsum  27596  mulog2sumlem1  27598  mulog2sumlem2  27599  mulog2sumlem3  27600  vmalogdivsum  27603  logsqvma  27606  selberglem1  27609  selberglem2  27610  selberg2lem  27614  selberg2  27615  selberg3lem1  27621  pntrsumo1  27629  pntrsumbnd  27630  selbergr  27632  selberg4r  27634  pntrlog2bndlem2  27642  pntrlog2bndlem4  27644  pntrlog2bndlem5  27645  pntlemo  27671  ax5seglem6  29135  axlowdimlem16  29158  finsumvtxdg2ssteplem4  29749  dipcl  30915  indsumin  33039  elrgspnlem2  33424  esumcvg  34383  fsum2dsub  34901  reprsuc  34909  breprexplemc  34926  breprexp  34927  breprexpnat  34928  vtscl  34932  circlemeth  34934  hgt750lemd  34942  tgoldbachgtde  34954  subfacval2  35537  subfaclim  35538  fwddifnp1  36515  knoppndvlem11  36960  aks4d1p1p1  42680  sticksstones12a  42774  unitscyglem2  42813  sumcubes  42922  fltnltalem  43244  jm2.23  43573  fsumsermpt  46155  sumnnodd  46206  dvnmul  46517  dvnprodlem1  46520  dvnprodlem2  46521  stoweidlem26  46600  dirkertrigeqlem2  46673  dirkeritg  46676  fourierdlem73  46753  fourierdlem83  46763  elaa2lem  46807  etransclem23  46831  etransclem27  46835  etransclem31  46839  etransclem33  46841  etransclem39  46847  etransclem46  46854  etransclem47  46855  etransclem48  46856  altgsumbcALT  48975  nn0sumshdiglemA  49241  amgmlemALT  50424