MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fsumcl Structured version   Visualization version   GIF version

Theorem fsumcl 14801
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.
StepHypRef Expression
1 ssidd 3818 . 2 (𝜑 → ℂ ⊆ ℂ)
2 addcl 10304 . . 3 ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ)
32adantl 474 . 2 ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 + 𝑦) ∈ ℂ)
4 fsumcl.1 . 2 (𝜑𝐴 ∈ Fin)
5 fsumcl.2 . 2 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
6 0cnd 10319 . 2 (𝜑 → 0 ∈ ℂ)
71, 3, 4, 5, 6fsumcllem 14800 1 (𝜑 → Σ𝑘𝐴 𝐵 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  wcel 2157  (class class class)co 6876  Fincfn 8193  cc 10220   + caddc 10225  Σcsu 14753
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2375  ax-ext 2775  ax-rep 4962  ax-sep 4973  ax-nul 4981  ax-pow 5033  ax-pr 5095  ax-un 7181  ax-inf2 8786  ax-cnex 10278  ax-resscn 10279  ax-1cn 10280  ax-icn 10281  ax-addcl 10282  ax-addrcl 10283  ax-mulcl 10284  ax-mulrcl 10285  ax-mulcom 10286  ax-addass 10287  ax-mulass 10288  ax-distr 10289  ax-i2m1 10290  ax-1ne0 10291  ax-1rid 10292  ax-rnegex 10293  ax-rrecex 10294  ax-cnre 10295  ax-pre-lttri 10296  ax-pre-lttrn 10297  ax-pre-ltadd 10298  ax-pre-mulgt0 10299  ax-pre-sup 10300
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3or 1109  df-3an 1110  df-tru 1657  df-fal 1667  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2590  df-eu 2607  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-ne 2970  df-nel 3073  df-ral 3092  df-rex 3093  df-reu 3094  df-rmo 3095  df-rab 3096  df-v 3385  df-sbc 3632  df-csb 3727  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-pss 3783  df-nul 4114  df-if 4276  df-pw 4349  df-sn 4367  df-pr 4369  df-tp 4371  df-op 4373  df-uni 4627  df-int 4666  df-iun 4710  df-br 4842  df-opab 4904  df-mpt 4921  df-tr 4944  df-id 5218  df-eprel 5223  df-po 5231  df-so 5232  df-fr 5269  df-se 5270  df-we 5271  df-xp 5316  df-rel 5317  df-cnv 5318  df-co 5319  df-dm 5320  df-rn 5321  df-res 5322  df-ima 5323  df-pred 5896  df-ord 5942  df-on 5943  df-lim 5944  df-suc 5945  df-iota 6062  df-fun 6101  df-fn 6102  df-f 6103  df-f1 6104  df-fo 6105  df-f1o 6106  df-fv 6107  df-isom 6108  df-riota 6837  df-ov 6879  df-oprab 6880  df-mpt2 6881  df-om 7298  df-1st 7399  df-2nd 7400  df-wrecs 7643  df-recs 7705  df-rdg 7743  df-1o 7797  df-oadd 7801  df-er 7980  df-en 8194  df-dom 8195  df-sdom 8196  df-fin 8197  df-sup 8588  df-oi 8655  df-card 9049  df-pnf 10363  df-mnf 10364  df-xr 10365  df-ltxr 10366  df-le 10367  df-sub 10556  df-neg 10557  df-div 10975  df-nn 11311  df-2 11372  df-3 11373  df-n0 11577  df-z 11663  df-uz 11927  df-rp 12071  df-fz 12577  df-fzo 12717  df-seq 13052  df-exp 13111  df-hash 13367  df-cj 14176  df-re 14177  df-im 14178  df-sqrt 14312  df-abs 14313  df-clim 14556  df-sum 14754
This theorem is referenced by:  fsum2dlem  14836  fsum0diag2  14849  fsummulc1  14851  fsumdivc  14852  fsumneg  14853  fsumsub  14854  fsum2mul  14855  fsumabs  14867  telfsumo  14868  fsumparts  14872  o1fsum  14879  cvgcmpce  14884  climfsum  14886  fsumiun  14887  binom1dif  14899  incexclem  14902  incexc  14903  isumsplit  14906  arisum2  14927  geoserg  14932  pwm1geoser  14934  mertenslem1  14949  mertens  14951  binomfallfaclem2  15103  bpolycl  15115  bpolysum  15116  bpolydiflem  15117  fsumkthpow  15119  fprodefsum  15157  eirrlem  15264  pwp1fsum  15446  pcfac  15932  sylow2a  18343  itg1addlem5  23804  itgcl  23887  dvmptfsum  24075  dvfsumabs  24123  dvfsumlem1  24126  plyf  24291  plymullem1  24307  coeeulem  24317  coemullem  24343  plycjlem  24369  taylpf  24457  mtest  24495  mtestbdd  24496  pserdvlem2  24519  abelthlem6  24527  abelthlem7  24529  advlogexp  24738  log2tlbnd  25020  birthdaylem2  25027  fsumharmonic  25086  lgamcvg2  25129  ftalem1  25147  ftalem5  25151  sgmf  25219  chtdif  25232  fsumdvdscom  25259  fsumdvdsmul  25269  logexprlim  25298  dchrsum2  25341  sumdchr2  25343  rpvmasumlem  25524  dchrisumlem1  25526  dchrisumlem2  25527  dchrisum  25529  dchrmusum2  25531  dchrvmasum2if  25534  dchrvmasumlem3  25536  dchrvmasumiflem1  25538  dchrvmasumiflem2  25539  rpvmasum2  25549  dchrisum0lem1b  25552  dchrisum0lem1  25553  dchrisum0lem2a  25554  dchrisum0lem2  25555  dchrisum0lem3  25556  dchrmusumlem  25559  dchrvmasumlem  25560  mudivsum  25567  mulogsumlem  25568  mulogsum  25569  mulog2sumlem1  25571  mulog2sumlem2  25572  mulog2sumlem3  25573  vmalogdivsum  25576  logsqvma  25579  selberglem1  25582  selberglem2  25583  selberg2lem  25587  selberg2  25588  selberg3lem1  25594  pntrsumo1  25602  pntrsumbnd  25603  selbergr  25605  selberg4r  25607  pntrlog2bndlem2  25615  pntrlog2bndlem4  25617  pntrlog2bndlem5  25618  pntlemo  25644  ax5seglem6  26162  axlowdimlem16  26185  finsumvtxdg2ssteplem4  26789  dipcl  28083  indsumin  30591  esumcvg  30655  fsum2dsub  31196  reprsuc  31204  breprexplemc  31221  breprexp  31222  breprexpnat  31223  vtscl  31227  circlemeth  31229  hgt750lemd  31237  tgoldbachgtde  31249  subfacval2  31677  subfaclim  31678  fwddifnp1  32776  knoppndvlem11  33012  jm2.23  38335  fsumclf  40532  fsumsermpt  40542  sumnnodd  40593  dvnmul  40889  dvnprodlem1  40892  dvnprodlem2  40893  stoweidlem26  40973  dirkertrigeqlem2  41046  dirkeritg  41049  fourierdlem73  41126  fourierdlem83  41136  elaa2lem  41180  etransclem23  41204  etransclem27  41208  etransclem31  41212  etransclem33  41214  etransclem39  41220  etransclem46  41227  etransclem47  41228  etransclem48  41229  pwdif  42270  altgsumbcALT  42917  nn0sumshdiglemA  43199  amgmlemALT  43338
  Copyright terms: Public domain W3C validator