Theorem fsumcl 15820

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 3954	. 2 ⊢ (𝜑 → ℂ ⊆ ℂ)
2		addcl 11207	. . 3 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ)
3	2	adantl 487	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 + 𝑦) ∈ ℂ)
4		fsumcl.1	. 2 ⊢ (𝜑 → 𝐴 ∈ Fin)
5		fsumcl.2	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
6		0cnd 11224	. 2 ⊢ (𝜑 → 0 ∈ ℂ)
7	1, 3, 4, 5, 6	fsumcllem 15819	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  (class class class)co 7414  Fincfn 8953  ℂcc 11123   + caddc 11128  Σcsu 15774

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-inf2 9621  ax-cnex 11181  ax-resscn 11182  ax-1cn 11183  ax-icn 11184  ax-addcl 11185  ax-addrcl 11186  ax-mulcl 11187  ax-mulrcl 11188  ax-mulcom 11189  ax-addass 11190  ax-mulass 11191  ax-distr 11192  ax-i2m1 11193  ax-1ne0 11194  ax-1rid 11195  ax-rnegex 11196  ax-rrecex 11197  ax-cnre 11198  ax-pre-lttri 11199  ax-pre-lttrn 11200  ax-pre-ltadd 11201  ax-pre-mulgt0 11202  ax-pre-sup 11203

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7371  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7864  df-1st 7987  df-2nd 7988  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-1o 8456  df-er 8697  df-en 8954  df-dom 8955  df-sdom 8956  df-fin 8957  df-sup 9413  df-oi 9483  df-card 9945  df-pnf 11270  df-mnf 11271  df-xr 11272  df-ltxr 11273  df-le 11274  df-sub 11468  df-neg 11469  df-div 11897  df-nn 12259  df-2 12328  df-3 12329  df-n0 12530  df-z 12617  df-uz 12889  df-rp 13044  df-fz 13563  df-fzo 13711  df-seq 14067  df-exp 14127  df-hash 14396  df-cj 15187  df-re 15188  df-im 15189  df-sqrt 15323  df-abs 15324  df-clim 15576  df-sum 15775

This theorem is used by:  fsumclf  15825  fsum2dlem  15857  fsum0diag2  15870  fsummulc1  15872  fsumdivc  15873  fsumneg  15874  fsumsub  15875  fsum2mul  15876  fsumabs  15889  telfsumo  15890  fsumparts  15894  o1fsum  15901  cvgcmpce  15906  climfsum  15908  fsumiun  15909  binom1dif  15923  incexclem  15926  incexc  15927  isumsplit  15930  arisum2  15951  geoserg  15956  pwdif  15958  mertenslem1  15974  mertens  15976  binomfallfaclem2  16127  bpolycl  16139  bpolysum  16140  bpolydiflem  16141  fsumkthpow  16143  fprodefsum  16182  eirrlem  16293  pwp1fsum  16482  pcfac  16992  sylow2a  19747  itg1addlem5  25929  itgcl  26012  dvmptfsum  26203  dvfsumabs  26251  dvfsumlem1  26254  plyf  26424  plymullem1  26441  coeeulem  26451  coemullem  26477  plycjlem  26503  taylpf  26603  mtest  26641  mtestbdd  26642  pserdvlem2  26665  abelthlem6  26673  abelthlem7  26675  advlogexp  26893  log2tlbnd  27183  birthdaylem2  27190  fsumharmonic  27249  lgamcvg2  27292  ftalem1  27310  ftalem5  27314  sgmf  27382  chtdif  27395  fsumdvdscom  27422  fsumdvdsmul  27432  logexprlim  27462  dchrsum2  27505  sumdchr2  27507  rpvmasumlem  27724  dchrisumlem1  27726  dchrisumlem2  27727  dchrisum  27729  dchrmusum2  27731  dchrvmasum2if  27734  dchrvmasumlem3  27736  dchrvmasumiflem1  27738  dchrvmasumiflem2  27739  rpvmasum2  27749  dchrisum0lem1b  27752  dchrisum0lem1  27753  dchrisum0lem2a  27754  dchrisum0lem2  27755  dchrisum0lem3  27756  dchrmusumlem  27759  dchrvmasumlem  27760  mudivsum  27767  mulogsumlem  27768  mulogsum  27769  mulog2sumlem1  27771  mulog2sumlem2  27772  mulog2sumlem3  27773  vmalogdivsum  27776  logsqvma  27779  selberglem1  27782  selberglem2  27783  selberg2lem  27787  selberg2  27788  selberg3lem1  27794  pntrsumo1  27802  pntrsumbnd  27803  selbergr  27805  selberg4r  27807  pntrlog2bndlem2  27815  pntrlog2bndlem4  27817  pntrlog2bndlem5  27818  pntlemo  27844  ax5seglem6  29392  axlowdimlem16  29415  finsumvtxdg2ssteplem4  30009  dipcl  31194  indsumin  33308  elrgspnlem2  33684  esumcvg  34597  fsum2dsub  35116  reprsuc  35124  breprexplemc  35141  breprexp  35142  breprexpnat  35143  vtscl  35147  circlemeth  35149  hgt750lemd  35157  tgoldbachgtde  35169  subfacval2  35767  subfaclim  35768  fwddifnp1  36746  knoppndvlem11  37220  aks4d1p1p1  42930  sticksstones12a  43024  unitscyglem2  43063  sumcubes  43189  fltnltalem  43509  jm2.23  43838  fsumsermpt  46410  sumnnodd  46461  dvnmul  46772  dvnprodlem1  46775  dvnprodlem2  46776  stoweidlem26  46855  dirkertrigeqlem2  46928  dirkeritg  46931  fourierdlem73  47008  fourierdlem83  47018  elaa2lem  47062  etransclem23  47086  etransclem27  47090  etransclem31  47094  etransclem33  47096  etransclem39  47102  etransclem46  47109  etransclem47  47110  etransclem48  47111  altgsumbcALT  49284  nn0sumshdiglemA  49550  amgmlemALT  50822