Theorem fsumrecl 15641

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3903  (class class class)co 7349  Fincfn 8872  ℂcc 11007  ℝcr 11008   + caddc 11012  Σcsu 15593

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 2701  ax-rep 5218  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-inf2 9537  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086  ax-pre-sup 11087

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-int 4897  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-se 5573  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-isom 6491  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-1st 7924  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-1o 8388  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-fin 8876  df-sup 9332  df-oi 9402  df-card 9835  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-div 11778  df-nn 12129  df-2 12191  df-3 12192  df-n0 12385  df-z 12472  df-uz 12736  df-rp 12894  df-fz 13411  df-fzo 13558  df-seq 13909  df-exp 13969  df-hash 14238  df-cj 15006  df-re 15007  df-im 15008  df-sqrt 15142  df-abs 15143  df-clim 15395  df-sum 15594

This theorem is referenced by:  fsumless  15703  fsumle  15706  fsumlt  15707  fsumabs  15708  o1fsum  15720  isumltss  15755  climcndslem1  15756  climcndslem2  15757  mertenslem1  15791  rpnnen2lem10  16132  prmreclem4  16831  prmreclem5  16832  lebnumlem1  24858  csbren  25297  trirn  25298  rrxmet  25306  rrxdstprj1  25307  ovolfiniun  25400  ovoliunlem1  25401  ovolscalem1  25412  ovolicc2lem4  25419  volfiniun  25446  uniioombllem3a  25483  uniioombllem4  25485  i1fd  25580  itg1cl  25584  i1fadd  25594  i1fmul  25595  dvfsumge  25926  dvfsumabs  25927  dvfsumrlimf  25929  dvfsumlem2  25931  dvfsumlem2OLD  25932  dvfsumlem3  25933  dvfsumlem4  25934  dvfsum2  25939  aaliou3lem5  26253  mtest  26311  mtestbdd  26312  abelthlem7  26346  abelthlem8  26347  log2ublem2  26855  log2ub  26857  birthdaylem3  26861  emcllem1  26904  emcllem2  26905  emcllem3  26906  harmoniclbnd  26917  harmonicubnd  26918  harmonicbnd4  26919  fsumharmonic  26920  ftalem1  26981  ftalem4  26984  ftalem5  26985  chtf  27016  chpf  27031  chpub  27129  logfaclbnd  27131  logexprlim  27134  chtppilimlem1  27382  vmadivsum  27391  vmadivsumb  27392  rplogsumlem1  27393  rplogsumlem2  27394  rpvmasumlem  27396  dchrisumlem2  27399  dchrmusum2  27403  dchrvmasumlem2  27407  dchrvmasumlem3  27408  dchrvmasumiflem1  27410  dchrisum0ff  27416  dchrisum0flblem1  27417  dchrisum0fno1  27420  dchrisum0re  27422  dchrisum0lem1  27425  dchrisum0lem2a  27426  rplogsum  27436  dirith2  27437  mudivsum  27439  mulogsumlem  27440  mulog2sumlem1  27443  mulog2sumlem2  27444  vmalogdivsum2  27447  vmalogdivsum  27448  2vmadivsumlem  27449  logsqvma2  27452  log2sumbnd  27453  selberglem2  27455  selberg  27457  selbergb  27458  selberg2b  27461  chpdifbndlem1  27462  logdivbnd  27465  selberg3lem1  27466  selberg3lem2  27467  selberg3  27468  selberg4lem1  27469  selberg4  27470  pntrsumo1  27474  pntrsumbnd  27475  pntrsumbnd2  27476  selberg3r  27478  selberg4r  27479  selberg34r  27480  pntsf  27482  pntsval2  27485  pntrlog2bndlem1  27486  pntrlog2bndlem2  27487  pntrlog2bndlem3  27488  pntrlog2bndlem4  27489  pntrlog2bndlem5  27490  pntrlog2bndlem6  27492  pntrlog2bnd  27493  pntpbnd1  27495  pntpbnd2  27496  pntlemj  27512  pntlemf  27514  pntlemk  27515  pntlemo  27516  axsegconlem2  28867  ax5seglem3  28880  ax5seg  28887  esumpcvgval  34061  esumcvg  34069  sibfof  34324  reprlt  34603  reprgt  34605  reprinfz1  34606  hgt750lemd  34632  hgt750lemb  34640  hgt750lema  34641  hgt750leme  34642  tgoldbachgtde  34644  knoppndvlem5  36510  knoppndvlem11  36516  knoppndvlem14  36519  mettrifi  37757  geomcau  37759  rrnmet  37829  rrndstprj1  37830  rrndstprj2  37831  aks4d1p1p2  42063  sticksstones6  42144  unitscyglem4  42191  sumcubes  42306  fltnltalem  42655  refsumcn  45028  fsumge0cl  45574  fsumreclf  45577  stoweidlem11  46012  stoweidlem17  46018  stoweidlem20  46021  stoweidlem26  46027  stoweidlem30  46031  stoweidlem32  46033  stoweidlem38  46039  stoweidlem44  46045  stirlinglem12  46086  dirkeritg  46103  fourierdlem73  46180  fourierdlem83  46190  fourierdlem112  46219  etransclem23  46258  etransclem35  46270  etransclem48  46283  sge0rnre  46365  sge0cl  46382  sge0fsum  46388  sge0ltfirp  46401  sge0le  46408  sge0split  46410  sge0iunmptlemfi  46414  sge0iunmptlemre  46416  sge0xaddlem1  46434  sge0xaddlem2  46435  sge0seq  46447  omeiunltfirp  46520  carageniuncllem2  46523  hoidmvlelem2  46597  hoidmvlelem3  46598  hoiqssbllem2  46624  fsummsndifre  47376  fsummmodsndifre  47378