Theorem fsumrecl 15686

Description: Closure of a finite sum of reals. (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.)

Hypotheses

Ref	Expression
fsumcl.1	⊢ (𝜑 → 𝐴 ∈ Fin)
fsumrecl.2	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)

Assertion

Ref	Expression
fsumrecl	⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℝ)

Distinct variable groups:   𝐴,𝑘   𝜑,𝑘

Allowed substitution hint:   𝐵(𝑘)

Proof of Theorem fsumrecl

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-resscn 11169	. . 3 ⊢ ℝ ⊆ ℂ
2	1	a1i 11	. 2 ⊢ (𝜑 → ℝ ⊆ ℂ)
3		readdcl 11195	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ)
4	3	adantl 481	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 + 𝑦) ∈ ℝ)
5		fsumcl.1	. 2 ⊢ (𝜑 → 𝐴 ∈ Fin)
6		fsumrecl.2	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)
7		0red 11221	. 2 ⊢ (𝜑 → 0 ∈ ℝ)
8	2, 4, 5, 6, 7	fsumcllem 15684	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2098   ⊆ wss 3943  (class class class)co 7405  Fincfn 8941  ℂcc 11110  ℝcr 11111   + caddc 11115  Σcsu 15638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7853  df-1st 7974  df-2nd 7975  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-oi 9507  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-n0 12477  df-z 12563  df-uz 12827  df-rp 12981  df-fz 13491  df-fzo 13634  df-seq 13973  df-exp 14033  df-hash 14296  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-clim 15438  df-sum 15639

This theorem is referenced by:  fsumless  15748  fsumle  15751  fsumlt  15752  fsumabs  15753  o1fsum  15765  isumltss  15800  climcndslem1  15801  climcndslem2  15802  mertenslem1  15836  rpnnen2lem10  16173  prmreclem4  16861  prmreclem5  16862  lebnumlem1  24842  csbren  25282  trirn  25283  rrxmet  25291  rrxdstprj1  25292  ovolfiniun  25385  ovoliunlem1  25386  ovolscalem1  25397  ovolicc2lem4  25404  volfiniun  25431  uniioombllem3a  25468  uniioombllem4  25470  i1fd  25565  itg1cl  25569  i1fadd  25579  i1fmul  25580  dvfsumge  25911  dvfsumabs  25912  dvfsumrlimf  25914  dvfsumlem2  25916  dvfsumlem2OLD  25917  dvfsumlem3  25918  dvfsumlem4  25919  dvfsum2  25924  aaliou3lem5  26237  mtest  26295  mtestbdd  26296  abelthlem7  26330  abelthlem8  26331  log2ublem2  26834  log2ub  26836  birthdaylem3  26840  emcllem1  26883  emcllem2  26884  emcllem3  26885  harmoniclbnd  26896  harmonicubnd  26897  harmonicbnd4  26898  fsumharmonic  26899  ftalem1  26960  ftalem4  26963  ftalem5  26964  chtf  26995  chpf  27010  chpub  27108  logfaclbnd  27110  logexprlim  27113  chtppilimlem1  27361  vmadivsum  27370  vmadivsumb  27371  rplogsumlem1  27372  rplogsumlem2  27373  rpvmasumlem  27375  dchrisumlem2  27378  dchrmusum2  27382  dchrvmasumlem2  27386  dchrvmasumlem3  27387  dchrvmasumiflem1  27389  dchrisum0ff  27395  dchrisum0flblem1  27396  dchrisum0fno1  27399  dchrisum0re  27401  dchrisum0lem1  27404  dchrisum0lem2a  27405  rplogsum  27415  dirith2  27416  mudivsum  27418  mulogsumlem  27419  mulog2sumlem1  27422  mulog2sumlem2  27423  vmalogdivsum2  27426  vmalogdivsum  27427  2vmadivsumlem  27428  logsqvma2  27431  log2sumbnd  27432  selberglem2  27434  selberg  27436  selbergb  27437  selberg2b  27440  chpdifbndlem1  27441  logdivbnd  27444  selberg3lem1  27445  selberg3lem2  27446  selberg3  27447  selberg4lem1  27448  selberg4  27449  pntrsumo1  27453  pntrsumbnd  27454  pntrsumbnd2  27455  selberg3r  27457  selberg4r  27458  selberg34r  27459  pntsf  27461  pntsval2  27464  pntrlog2bndlem1  27465  pntrlog2bndlem2  27466  pntrlog2bndlem3  27467  pntrlog2bndlem4  27468  pntrlog2bndlem5  27469  pntrlog2bndlem6  27471  pntrlog2bnd  27472  pntpbnd1  27474  pntpbnd2  27475  pntlemj  27491  pntlemf  27493  pntlemk  27494  pntlemo  27495  axsegconlem2  28684  ax5seglem3  28697  ax5seg  28704  esumpcvgval  33606  esumcvg  33614  sibfof  33869  reprlt  34160  reprgt  34162  reprinfz1  34163  hgt750lemd  34189  hgt750lemb  34197  hgt750lema  34198  hgt750leme  34199  tgoldbachgtde  34201  knoppndvlem5  35900  knoppndvlem11  35906  knoppndvlem14  35909  mettrifi  37138  geomcau  37140  rrnmet  37210  rrndstprj1  37211  rrndstprj2  37212  aks4d1p1p2  41451  sticksstones6  41528  sumcubes  41769  fltnltalem  41982  refsumcn  44290  fsumge0cl  44861  fsumreclf  44864  stoweidlem11  45299  stoweidlem17  45305  stoweidlem20  45308  stoweidlem26  45314  stoweidlem30  45318  stoweidlem32  45320  stoweidlem38  45326  stoweidlem44  45332  stirlinglem12  45373  dirkeritg  45390  fourierdlem73  45467  fourierdlem83  45477  fourierdlem112  45506  etransclem23  45545  etransclem35  45557  etransclem48  45570  sge0rnre  45652  sge0cl  45669  sge0fsum  45675  sge0ltfirp  45688  sge0le  45695  sge0split  45697  sge0iunmptlemfi  45701  sge0iunmptlemre  45703  sge0xaddlem1  45721  sge0xaddlem2  45722  sge0seq  45734  omeiunltfirp  45807  carageniuncllem2  45810  hoidmvlelem2  45884  hoidmvlelem3  45885  hoiqssbllem2  45911  fsummsndifre  46612  fsummmodsndifre  46614