Theorem fsumcl 15706

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  (class class class)co 7390  Fincfn 8921  ℂcc 11073   + caddc 11078  Σcsu 15659

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-inf2 9601  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152  ax-pre-sup 11153

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 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-se 5595  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-isom 6523  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7846  df-1st 7971  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-1o 8437  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-sup 9400  df-oi 9470  df-card 9899  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-div 11843  df-nn 12194  df-2 12256  df-3 12257  df-n0 12450  df-z 12537  df-uz 12801  df-rp 12959  df-fz 13476  df-fzo 13623  df-seq 13974  df-exp 14034  df-hash 14303  df-cj 15072  df-re 15073  df-im 15074  df-sqrt 15208  df-abs 15209  df-clim 15461  df-sum 15660

This theorem is referenced by:  fsumclf  15711  fsum2dlem  15743  fsum0diag2  15756  fsummulc1  15758  fsumdivc  15759  fsumneg  15760  fsumsub  15761  fsum2mul  15762  fsumabs  15774  telfsumo  15775  fsumparts  15779  o1fsum  15786  cvgcmpce  15791  climfsum  15793  fsumiun  15794  binom1dif  15806  incexclem  15809  incexc  15810  isumsplit  15813  arisum2  15834  geoserg  15839  pwdif  15841  mertenslem1  15857  mertens  15859  binomfallfaclem2  16013  bpolycl  16025  bpolysum  16026  bpolydiflem  16027  fsumkthpow  16029  fprodefsum  16068  eirrlem  16179  pwp1fsum  16368  pcfac  16877  sylow2a  19556  itg1addlem5  25608  itgcl  25692  dvmptfsum  25886  dvfsumabs  25936  dvfsumlem1  25939  plyf  26110  plymullem1  26126  coeeulem  26136  coemullem  26162  plycjlem  26189  taylpf  26280  mtest  26320  mtestbdd  26321  pserdvlem2  26345  abelthlem6  26353  abelthlem7  26355  advlogexp  26571  log2tlbnd  26862  birthdaylem2  26869  fsumharmonic  26929  lgamcvg2  26972  ftalem1  26990  ftalem5  26994  sgmf  27062  chtdif  27075  fsumdvdscom  27102  fsumdvdsmul  27112  fsumdvdsmulOLD  27114  logexprlim  27143  dchrsum2  27186  sumdchr2  27188  rpvmasumlem  27405  dchrisumlem1  27407  dchrisumlem2  27408  dchrisum  27410  dchrmusum2  27412  dchrvmasum2if  27415  dchrvmasumlem3  27417  dchrvmasumiflem1  27419  dchrvmasumiflem2  27420  rpvmasum2  27430  dchrisum0lem1b  27433  dchrisum0lem1  27434  dchrisum0lem2a  27435  dchrisum0lem2  27436  dchrisum0lem3  27437  dchrmusumlem  27440  dchrvmasumlem  27441  mudivsum  27448  mulogsumlem  27449  mulogsum  27450  mulog2sumlem1  27452  mulog2sumlem2  27453  mulog2sumlem3  27454  vmalogdivsum  27457  logsqvma  27460  selberglem1  27463  selberglem2  27464  selberg2lem  27468  selberg2  27469  selberg3lem1  27475  pntrsumo1  27483  pntrsumbnd  27484  selbergr  27486  selberg4r  27488  pntrlog2bndlem2  27496  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  pntlemo  27525  ax5seglem6  28868  axlowdimlem16  28891  finsumvtxdg2ssteplem4  29483  dipcl  30648  indsumin  32792  elrgspnlem2  33201  esumcvg  34083  fsum2dsub  34605  reprsuc  34613  breprexplemc  34630  breprexp  34631  breprexpnat  34632  vtscl  34636  circlemeth  34638  hgt750lemd  34646  tgoldbachgtde  34658  subfacval2  35181  subfaclim  35182  fwddifnp1  36160  knoppndvlem11  36517  aks4d1p1p1  42058  sticksstones12a  42152  unitscyglem2  42191  sumcubes  42308  fltnltalem  42657  jm2.23  42992  fsumsermpt  45584  sumnnodd  45635  dvnmul  45948  dvnprodlem1  45951  dvnprodlem2  45952  stoweidlem26  46031  dirkertrigeqlem2  46104  dirkeritg  46107  fourierdlem73  46184  fourierdlem83  46194  elaa2lem  46238  etransclem23  46262  etransclem27  46266  etransclem31  46270  etransclem33  46272  etransclem39  46278  etransclem46  46285  etransclem47  46286  etransclem48  46287  altgsumbcALT  48345  nn0sumshdiglemA  48612  amgmlemALT  49796