Theorem fsumcl 15747

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 3982	. 2 ⊢ (𝜑 → ℂ ⊆ ℂ)
2		addcl 11209	. . 3 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ)
3	2	adantl 481	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 + 𝑦) ∈ ℂ)
4		fsumcl.1	. 2 ⊢ (𝜑 → 𝐴 ∈ Fin)
5		fsumcl.2	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
6		0cnd 11226	. 2 ⊢ (𝜑 → 0 ∈ ℂ)
7	1, 3, 4, 5, 6	fsumcllem 15746	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℂ)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  (class class class)co 7403  Fincfn 8957  ℂcc 11125   + caddc 11130  Σcsu 15700

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-inf2 9653  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204  ax-pre-sup 11205

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-int 4923  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-se 5607  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-isom 6539  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-om 7860  df-1st 7986  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-1o 8478  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-sup 9452  df-oi 9522  df-card 9951  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11466  df-neg 11467  df-div 11893  df-nn 12239  df-2 12301  df-3 12302  df-n0 12500  df-z 12587  df-uz 12851  df-rp 13007  df-fz 13523  df-fzo 13670  df-seq 14018  df-exp 14078  df-hash 14347  df-cj 15116  df-re 15117  df-im 15118  df-sqrt 15252  df-abs 15253  df-clim 15502  df-sum 15701

This theorem is referenced by:  fsumclf  15752  fsum2dlem  15784  fsum0diag2  15797  fsummulc1  15799  fsumdivc  15800  fsumneg  15801  fsumsub  15802  fsum2mul  15803  fsumabs  15815  telfsumo  15816  fsumparts  15820  o1fsum  15827  cvgcmpce  15832  climfsum  15834  fsumiun  15835  binom1dif  15847  incexclem  15850  incexc  15851  isumsplit  15854  arisum2  15875  geoserg  15880  pwdif  15882  mertenslem1  15898  mertens  15900  binomfallfaclem2  16054  bpolycl  16066  bpolysum  16067  bpolydiflem  16068  fsumkthpow  16070  fprodefsum  16109  eirrlem  16220  pwp1fsum  16408  pcfac  16917  sylow2a  19598  itg1addlem5  25651  itgcl  25735  dvmptfsum  25929  dvfsumabs  25979  dvfsumlem1  25982  plyf  26153  plymullem1  26169  coeeulem  26179  coemullem  26205  plycjlem  26232  taylpf  26323  mtest  26363  mtestbdd  26364  pserdvlem2  26388  abelthlem6  26396  abelthlem7  26398  advlogexp  26614  log2tlbnd  26905  birthdaylem2  26912  fsumharmonic  26972  lgamcvg2  27015  ftalem1  27033  ftalem5  27037  sgmf  27105  chtdif  27118  fsumdvdscom  27145  fsumdvdsmul  27155  fsumdvdsmulOLD  27157  logexprlim  27186  dchrsum2  27229  sumdchr2  27231  rpvmasumlem  27448  dchrisumlem1  27450  dchrisumlem2  27451  dchrisum  27453  dchrmusum2  27455  dchrvmasum2if  27458  dchrvmasumlem3  27460  dchrvmasumiflem1  27462  dchrvmasumiflem2  27463  rpvmasum2  27473  dchrisum0lem1b  27476  dchrisum0lem1  27477  dchrisum0lem2a  27478  dchrisum0lem2  27479  dchrisum0lem3  27480  dchrmusumlem  27483  dchrvmasumlem  27484  mudivsum  27491  mulogsumlem  27492  mulogsum  27493  mulog2sumlem1  27495  mulog2sumlem2  27496  mulog2sumlem3  27497  vmalogdivsum  27500  logsqvma  27503  selberglem1  27506  selberglem2  27507  selberg2lem  27511  selberg2  27512  selberg3lem1  27518  pntrsumo1  27526  pntrsumbnd  27527  selbergr  27529  selberg4r  27531  pntrlog2bndlem2  27539  pntrlog2bndlem4  27541  pntrlog2bndlem5  27542  pntlemo  27568  ax5seglem6  28859  axlowdimlem16  28882  finsumvtxdg2ssteplem4  29474  dipcl  30639  indsumin  32785  elrgspnlem2  33184  esumcvg  34063  fsum2dsub  34585  reprsuc  34593  breprexplemc  34610  breprexp  34611  breprexpnat  34612  vtscl  34616  circlemeth  34618  hgt750lemd  34626  tgoldbachgtde  34638  subfacval2  35155  subfaclim  35156  fwddifnp1  36129  knoppndvlem11  36486  aks4d1p1p1  42022  sticksstones12a  42116  unitscyglem2  42155  sumcubes  42309  fltnltalem  42632  jm2.23  42967  fsumsermpt  45556  sumnnodd  45607  dvnmul  45920  dvnprodlem1  45923  dvnprodlem2  45924  stoweidlem26  46003  dirkertrigeqlem2  46076  dirkeritg  46079  fourierdlem73  46156  fourierdlem83  46166  elaa2lem  46210  etransclem23  46234  etransclem27  46238  etransclem31  46242  etransclem33  46244  etransclem39  46250  etransclem46  46257  etransclem47  46258  etransclem48  46259  altgsumbcALT  48276  nn0sumshdiglemA  48547  amgmlemALT  49615