Theorem fsumrecl 15763

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2144   ⊆ wss 3906  (class class class)co 7398  Fincfn 8929  ℂcc 11073  ℝcr 11074   + caddc 11078  Σcsu 15715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-rep 5229  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720  ax-inf2 9598  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152  ax-pre-sup 11153

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5544  df-eprel 5549  df-po 5557  df-so 5558  df-fr 5602  df-se 5603  df-we 5604  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-pred 6290  df-ord 6351  df-on 6352  df-lim 6353  df-suc 6354  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-isom 6532  df-riota 7355  df-ov 7401  df-oprab 7402  df-mpo 7403  df-om 7849  df-1st 7972  df-2nd 7973  df-frecs 8264  df-wrecs 8295  df-recs 8344  df-rdg 8383  df-1o 8439  df-er 8680  df-en 8930  df-dom 8931  df-sdom 8932  df-fin 8933  df-sup 9390  df-oi 9460  df-card 9899  df-pnf 11220  df-mnf 11221  df-xr 11222  df-ltxr 11223  df-le 11224  df-sub 11418  df-neg 11419  df-div 11847  df-nn 12213  df-2 12282  df-3 12283  df-n0 12484  df-z 12571  df-uz 12842  df-rp 12996  df-fz 13515  df-fzo 13662  df-seq 14017  df-exp 14077  df-hash 14346  df-cj 15128  df-re 15129  df-im 15130  df-sqrt 15264  df-abs 15265  df-clim 15517  df-sum 15716

This theorem is referenced by:  fsumless  15826  fsumle  15829  fsumlt  15830  fsumabs  15831  o1fsum  15843  isumltss  15880  climcndslem1  15881  climcndslem2  15882  mertenslem1  15916  rpnnen2lem10  16257  prmreclem4  16957  prmreclem5  16958  lebnumlem1  25025  csbren  25463  trirn  25464  rrxmet  25472  rrxdstprj1  25473  ovolfiniun  25565  ovoliunlem1  25566  ovolscalem1  25577  ovolicc2lem4  25584  volfiniun  25611  uniioombllem3a  25648  uniioombllem4  25650  i1fd  25745  itg1cl  25749  i1fadd  25759  i1fmul  25760  dvfsumge  26086  dvfsumabs  26087  dvfsumrlimf  26089  dvfsumlem2  26091  dvfsumlem3  26092  dvfsumlem4  26093  dvfsum2  26098  aaliou3lem5  26413  mtest  26469  mtestbdd  26470  abelthlem7  26503  abelthlem8  26504  log2ublem2  27014  log2ub  27016  birthdaylem3  27020  emcllem1  27062  emcllem2  27063  emcllem3  27064  harmoniclbnd  27075  harmonicubnd  27076  harmonicbnd4  27077  fsumharmonic  27078  ftalem1  27139  ftalem4  27142  ftalem5  27143  chtf  27174  chpf  27189  chpub  27286  logfaclbnd  27288  logexprlim  27291  chtppilimlem1  27539  vmadivsum  27548  vmadivsumb  27549  rplogsumlem1  27550  rplogsumlem2  27551  rpvmasumlem  27553  dchrisumlem2  27556  dchrmusum2  27560  dchrvmasumlem2  27564  dchrvmasumlem3  27565  dchrvmasumiflem1  27567  dchrisum0ff  27573  dchrisum0flblem1  27574  dchrisum0fno1  27577  dchrisum0re  27579  dchrisum0lem1  27582  dchrisum0lem2a  27583  rplogsum  27593  dirith2  27594  mudivsum  27596  mulogsumlem  27597  mulog2sumlem1  27600  mulog2sumlem2  27601  vmalogdivsum2  27604  vmalogdivsum  27605  2vmadivsumlem  27606  logsqvma2  27609  log2sumbnd  27610  selberglem2  27612  selberg  27614  selbergb  27615  selberg2b  27618  chpdifbndlem1  27619  logdivbnd  27622  selberg3lem1  27623  selberg3lem2  27624  selberg3  27625  selberg4lem1  27626  selberg4  27627  pntrsumo1  27631  pntrsumbnd  27632  pntrsumbnd2  27633  selberg3r  27635  selberg4r  27636  selberg34r  27637  pntsf  27639  pntsval2  27642  pntrlog2bndlem1  27643  pntrlog2bndlem2  27644  pntrlog2bndlem3  27645  pntrlog2bndlem4  27646  pntrlog2bndlem5  27647  pntrlog2bndlem6  27649  pntrlog2bnd  27650  pntpbnd1  27652  pntpbnd2  27653  pntlemj  27669  pntlemf  27671  pntlemk  27672  pntlemo  27673  axsegconlem2  29121  ax5seglem3  29134  ax5seg  29141  esumpcvgval  34377  esumcvg  34385  sibfof  34639  reprlt  34915  reprgt  34917  reprinfz1  34918  hgt750lemd  34944  hgt750lemb  34952  hgt750lema  34953  hgt750leme  34954  tgoldbachgtde  34956  knoppndvlem5  36959  knoppndvlem11  36965  knoppndvlem14  36968  mettrifi  38261  geomcau  38263  rrnmet  38333  rrndstprj1  38334  rrndstprj2  38335  aks4d1p1p2  42692  sticksstones6  42773  unitscyglem4  42820  sumcubes  42927  fltnltalem  43249  refsumcn  45615  fsumge0cl  46154  fsumreclf  46157  stoweidlem11  46590  stoweidlem17  46596  stoweidlem20  46599  stoweidlem26  46605  stoweidlem30  46609  stoweidlem32  46611  stoweidlem38  46617  stoweidlem44  46623  stirlinglem12  46664  dirkeritg  46681  fourierdlem73  46758  fourierdlem83  46768  fourierdlem112  46797  etransclem23  46836  etransclem35  46848  etransclem48  46861  sge0rnre  46943  sge0cl  46960  sge0fsum  46966  sge0ltfirp  46979  sge0le  46986  sge0split  46988  sge0iunmptlemfi  46992  sge0iunmptlemre  46994  sge0xaddlem1  47012  sge0xaddlem2  47013  sge0seq  47025  omeiunltfirp  47098  carageniuncllem2  47101  hoidmvlelem2  47175  hoidmvlelem3  47176  hoiqssbllem2  47202  fsummsndifre  47979  fsummmodsndifre  47981