Theorem fsumrecl 15671

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 11097	. . 3 ⊢ ℝ ⊆ ℂ
2	1	a1i 11	. 2 ⊢ (𝜑 → ℝ ⊆ ℂ)
3		readdcl 11123	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ)
4	3	adantl 481	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 + 𝑦) ∈ ℝ)
5		fsumcl.1	. 2 ⊢ (𝜑 → 𝐴 ∈ Fin)
6		fsumrecl.2	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)
7		0red 11149	. 2 ⊢ (𝜑 → 0 ∈ ℝ)
8	2, 4, 5, 6, 7	fsumcllem 15669	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ⊆ wss 3903  (class class class)co 7370  Fincfn 8897  ℂcc 11038  ℝcr 11039   + caddc 11043  Σcsu 15623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-inf2 9564  ax-cnex 11096  ax-resscn 11097  ax-1cn 11098  ax-icn 11099  ax-addcl 11100  ax-addrcl 11101  ax-mulcl 11102  ax-mulrcl 11103  ax-mulcom 11104  ax-addass 11105  ax-mulass 11106  ax-distr 11107  ax-i2m1 11108  ax-1ne0 11109  ax-1rid 11110  ax-rnegex 11111  ax-rrecex 11112  ax-cnre 11113  ax-pre-lttri 11114  ax-pre-lttrn 11115  ax-pre-ltadd 11116  ax-pre-mulgt0 11117  ax-pre-sup 11118

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-int 4905  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5529  df-eprel 5534  df-po 5542  df-so 5543  df-fr 5587  df-se 5588  df-we 5589  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6269  df-ord 6330  df-on 6331  df-lim 6332  df-suc 6333  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-isom 6511  df-riota 7327  df-ov 7373  df-oprab 7374  df-mpo 7375  df-om 7821  df-1st 7945  df-2nd 7946  df-frecs 8235  df-wrecs 8266  df-recs 8315  df-rdg 8353  df-1o 8409  df-er 8647  df-en 8898  df-dom 8899  df-sdom 8900  df-fin 8901  df-sup 9359  df-oi 9429  df-card 9865  df-pnf 11182  df-mnf 11183  df-xr 11184  df-ltxr 11185  df-le 11186  df-sub 11380  df-neg 11381  df-div 11809  df-nn 12160  df-2 12222  df-3 12223  df-n0 12416  df-z 12503  df-uz 12766  df-rp 12920  df-fz 13438  df-fzo 13585  df-seq 13939  df-exp 13999  df-hash 14268  df-cj 15036  df-re 15037  df-im 15038  df-sqrt 15172  df-abs 15173  df-clim 15425  df-sum 15624

This theorem is referenced by:  fsumless  15733  fsumle  15736  fsumlt  15737  fsumabs  15738  o1fsum  15750  isumltss  15785  climcndslem1  15786  climcndslem2  15787  mertenslem1  15821  rpnnen2lem10  16162  prmreclem4  16861  prmreclem5  16862  lebnumlem1  24933  csbren  25372  trirn  25373  rrxmet  25381  rrxdstprj1  25382  ovolfiniun  25475  ovoliunlem1  25476  ovolscalem1  25487  ovolicc2lem4  25494  volfiniun  25521  uniioombllem3a  25558  uniioombllem4  25560  i1fd  25655  itg1cl  25659  i1fadd  25669  i1fmul  25670  dvfsumge  26001  dvfsumabs  26002  dvfsumrlimf  26004  dvfsumlem2  26006  dvfsumlem2OLD  26007  dvfsumlem3  26008  dvfsumlem4  26009  dvfsum2  26014  aaliou3lem5  26328  mtest  26386  mtestbdd  26387  abelthlem7  26421  abelthlem8  26422  log2ublem2  26930  log2ub  26932  birthdaylem3  26936  emcllem1  26979  emcllem2  26980  emcllem3  26981  harmoniclbnd  26992  harmonicubnd  26993  harmonicbnd4  26994  fsumharmonic  26995  ftalem1  27056  ftalem4  27059  ftalem5  27060  chtf  27091  chpf  27106  chpub  27204  logfaclbnd  27206  logexprlim  27209  chtppilimlem1  27457  vmadivsum  27466  vmadivsumb  27467  rplogsumlem1  27468  rplogsumlem2  27469  rpvmasumlem  27471  dchrisumlem2  27474  dchrmusum2  27478  dchrvmasumlem2  27482  dchrvmasumlem3  27483  dchrvmasumiflem1  27485  dchrisum0ff  27491  dchrisum0flblem1  27492  dchrisum0fno1  27495  dchrisum0re  27497  dchrisum0lem1  27500  dchrisum0lem2a  27501  rplogsum  27511  dirith2  27512  mudivsum  27514  mulogsumlem  27515  mulog2sumlem1  27518  mulog2sumlem2  27519  vmalogdivsum2  27522  vmalogdivsum  27523  2vmadivsumlem  27524  logsqvma2  27527  log2sumbnd  27528  selberglem2  27530  selberg  27532  selbergb  27533  selberg2b  27536  chpdifbndlem1  27537  logdivbnd  27540  selberg3lem1  27541  selberg3lem2  27542  selberg3  27543  selberg4lem1  27544  selberg4  27545  pntrsumo1  27549  pntrsumbnd  27550  pntrsumbnd2  27551  selberg3r  27553  selberg4r  27554  selberg34r  27555  pntsf  27557  pntsval2  27560  pntrlog2bndlem1  27561  pntrlog2bndlem2  27562  pntrlog2bndlem3  27563  pntrlog2bndlem4  27564  pntrlog2bndlem5  27565  pntrlog2bndlem6  27567  pntrlog2bnd  27568  pntpbnd1  27570  pntpbnd2  27571  pntlemj  27587  pntlemf  27589  pntlemk  27590  pntlemo  27591  axsegconlem2  29009  ax5seglem3  29022  ax5seg  29029  esumpcvgval  34262  esumcvg  34270  sibfof  34524  reprlt  34803  reprgt  34805  reprinfz1  34806  hgt750lemd  34832  hgt750lemb  34840  hgt750lema  34841  hgt750leme  34842  tgoldbachgtde  34844  knoppndvlem5  36744  knoppndvlem11  36750  knoppndvlem14  36753  mettrifi  38037  geomcau  38039  rrnmet  38109  rrndstprj1  38110  rrndstprj2  38111  aks4d1p1p2  42469  sticksstones6  42550  unitscyglem4  42597  sumcubes  42712  fltnltalem  43049  refsumcn  45419  fsumge0cl  45962  fsumreclf  45965  stoweidlem11  46398  stoweidlem17  46404  stoweidlem20  46407  stoweidlem26  46413  stoweidlem30  46417  stoweidlem32  46419  stoweidlem38  46425  stoweidlem44  46431  stirlinglem12  46472  dirkeritg  46489  fourierdlem73  46566  fourierdlem83  46576  fourierdlem112  46605  etransclem23  46644  etransclem35  46656  etransclem48  46669  sge0rnre  46751  sge0cl  46768  sge0fsum  46774  sge0ltfirp  46787  sge0le  46794  sge0split  46796  sge0iunmptlemfi  46800  sge0iunmptlemre  46802  sge0xaddlem1  46820  sge0xaddlem2  46821  sge0seq  46833  omeiunltfirp  46906  carageniuncllem2  46909  hoidmvlelem2  46983  hoidmvlelem3  46984  hoiqssbllem2  47010  fsummsndifre  47761  fsummmodsndifre  47763