Theorem fsumrecl 15770

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   ⊆ wss 3951  (class class class)co 7431  Fincfn 8985  ℂcc 11153  ℝcr 11154   + caddc 11158  Σcsu 15722

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-z 12614  df-uz 12879  df-rp 13035  df-fz 13548  df-fzo 13695  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-sum 15723

This theorem is referenced by:  fsumless  15832  fsumle  15835  fsumlt  15836  fsumabs  15837  o1fsum  15849  isumltss  15884  climcndslem1  15885  climcndslem2  15886  mertenslem1  15920  rpnnen2lem10  16259  prmreclem4  16957  prmreclem5  16958  lebnumlem1  24993  csbren  25433  trirn  25434  rrxmet  25442  rrxdstprj1  25443  ovolfiniun  25536  ovoliunlem1  25537  ovolscalem1  25548  ovolicc2lem4  25555  volfiniun  25582  uniioombllem3a  25619  uniioombllem4  25621  i1fd  25716  itg1cl  25720  i1fadd  25730  i1fmul  25731  dvfsumge  26062  dvfsumabs  26063  dvfsumrlimf  26065  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumlem3  26069  dvfsumlem4  26070  dvfsum2  26075  aaliou3lem5  26389  mtest  26447  mtestbdd  26448  abelthlem7  26482  abelthlem8  26483  log2ublem2  26990  log2ub  26992  birthdaylem3  26996  emcllem1  27039  emcllem2  27040  emcllem3  27041  harmoniclbnd  27052  harmonicubnd  27053  harmonicbnd4  27054  fsumharmonic  27055  ftalem1  27116  ftalem4  27119  ftalem5  27120  chtf  27151  chpf  27166  chpub  27264  logfaclbnd  27266  logexprlim  27269  chtppilimlem1  27517  vmadivsum  27526  vmadivsumb  27527  rplogsumlem1  27528  rplogsumlem2  27529  rpvmasumlem  27531  dchrisumlem2  27534  dchrmusum2  27538  dchrvmasumlem2  27542  dchrvmasumlem3  27543  dchrvmasumiflem1  27545  dchrisum0ff  27551  dchrisum0flblem1  27552  dchrisum0fno1  27555  dchrisum0re  27557  dchrisum0lem1  27560  dchrisum0lem2a  27561  rplogsum  27571  dirith2  27572  mudivsum  27574  mulogsumlem  27575  mulog2sumlem1  27578  mulog2sumlem2  27579  vmalogdivsum2  27582  vmalogdivsum  27583  2vmadivsumlem  27584  logsqvma2  27587  log2sumbnd  27588  selberglem2  27590  selberg  27592  selbergb  27593  selberg2b  27596  chpdifbndlem1  27597  logdivbnd  27600  selberg3lem1  27601  selberg3lem2  27602  selberg3  27603  selberg4lem1  27604  selberg4  27605  pntrsumo1  27609  pntrsumbnd  27610  pntrsumbnd2  27611  selberg3r  27613  selberg4r  27614  selberg34r  27615  pntsf  27617  pntsval2  27620  pntrlog2bndlem1  27621  pntrlog2bndlem2  27622  pntrlog2bndlem3  27623  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  pntrlog2bndlem6  27627  pntrlog2bnd  27628  pntpbnd1  27630  pntpbnd2  27631  pntlemj  27647  pntlemf  27649  pntlemk  27650  pntlemo  27651  axsegconlem2  28933  ax5seglem3  28946  ax5seg  28953  esumpcvgval  34079  esumcvg  34087  sibfof  34342  reprlt  34634  reprgt  34636  reprinfz1  34637  hgt750lemd  34663  hgt750lemb  34671  hgt750lema  34672  hgt750leme  34673  tgoldbachgtde  34675  knoppndvlem5  36517  knoppndvlem11  36523  knoppndvlem14  36526  mettrifi  37764  geomcau  37766  rrnmet  37836  rrndstprj1  37837  rrndstprj2  37838  aks4d1p1p2  42071  sticksstones6  42152  unitscyglem4  42199  sumcubes  42347  fltnltalem  42672  refsumcn  45035  fsumge0cl  45588  fsumreclf  45591  stoweidlem11  46026  stoweidlem17  46032  stoweidlem20  46035  stoweidlem26  46041  stoweidlem30  46045  stoweidlem32  46047  stoweidlem38  46053  stoweidlem44  46059  stirlinglem12  46100  dirkeritg  46117  fourierdlem73  46194  fourierdlem83  46204  fourierdlem112  46233  etransclem23  46272  etransclem35  46284  etransclem48  46297  sge0rnre  46379  sge0cl  46396  sge0fsum  46402  sge0ltfirp  46415  sge0le  46422  sge0split  46424  sge0iunmptlemfi  46428  sge0iunmptlemre  46430  sge0xaddlem1  46448  sge0xaddlem2  46449  sge0seq  46461  omeiunltfirp  46534  carageniuncllem2  46537  hoidmvlelem2  46611  hoidmvlelem3  46612  hoiqssbllem2  46638  fsummsndifre  47359  fsummmodsndifre  47361