Theorem readdcld 11319

Description: Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
recnd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
readdcld.2	⊢ (𝜑 → 𝐵 ∈ ℝ)

Assertion

Ref	Expression
readdcld	⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)

Proof of Theorem readdcld

Step	Hyp	Ref	Expression
1		recnd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		readdcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		readdcl 11264	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 596	1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7412  ℝcr 11180   + caddc 11184

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 11242

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ltadd2  11395  readdcan  11465  addrid  11471  leadd1  11765  le2add  11779  lesub2  11792  lesub3d  11915  le2addd  11916  supaddc  12265  supadd  12266  cju  12297  nnne0  12353  div4p1lem1div2  12582  difgtsumgt  12640  eluzmn  12953  rpnnen1lem5  13090  addlelt  13217  xralrple  13316  xov1plusxeqvd  13610  zltaddlt1le  13617  elincfzoext  13838  fladdz  13945  2tnp1ge0ge0  13949  flhalf  13950  fldiv  13980  modaddb  14029  modaddmodup  14057  modaddmodlo  14058  addmodlteq  14069  discr1  14363  discr  14364  ccatalpha  14720  2cshw  14944  remim  15264  remullem  15275  01sqrexlem7  15395  absrele  15455  abstri  15478  abs3lem  15486  amgm2  15517  bhmafibid1  15615  mulcn2  15743  o1add  15761  o1sub  15763  lo1add  15774  caucvgrlem  15820  iseraltlem2  15830  iseraltlem3  15831  fsumabs  15948  o1fsum  15960  climcndslem2  15999  tanhlt1  16308  eirrlem  16352  ruclem1  16379  ruclem2  16380  ruclem3  16381  ltoddhalfle  16511  bitscmp  16588  sadcaddlem  16607  sadasslem  16620  smuval2  16632  iserodd  16993  prmreclem4  17077  4sqlem5  17100  4sqlem6  17101  4sqlem12  17114  4sqlem15  17117  4sqlem16  17118  prmgaplem7  17215  prmgaplem8  17216  2expltfac  17250  cshwshashlem2  17254  chfacfscmul0  23156  chfacfscmulgsum  23158  chfacfpmmul0  23160  chfacfpmmulgsum  23162  prdsxmetlem  24667  xblss2ps  24700  metustexhalf  24855  nrmmetd  24873  ngptgp  24935  nlmvscnlem2  24984  nlmvscnlem1  24985  nmotri  25038  nghmplusg  25039  blcvx  25097  iccntr  25121  icccmplem2  25123  reconnlem2  25127  metdcnlem  25136  metnrmlem3  25161  cnllycmp  25257  lebnumii  25267  tcphcphlem1  25536  ipcnlem2  25545  ipcnlem1  25546  csbren  25700  trirn  25701  minveclem2  25727  minveclem3b  25729  minveclem4  25733  ivthlem2  25753  ovolgelb  25781  ovollb2lem  25789  ovolunlem1a  25797  ovolunlem1  25798  ovolfiniun  25802  ovoliunlem1  25803  ovoliunlem2  25804  ovolshftlem1  25810  ovolscalem1  25814  ovolicopnf  25825  ismbl2  25828  nulmbl2  25837  unmbl  25838  voliunlem2  25852  ioombl1lem2  25860  ioombl1lem4  25862  ioombl1  25863  ioorcl2  25873  uniioombllem1  25882  uniioombllem3  25886  uniioombllem4  25887  uniioombllem5  25888  uniioombl  25890  opnmbllem  25902  volcn  25907  itg1addlem4  26000  mbfi1fseqlem4  26019  mbfi1fseqlem6  26021  itg2splitlem  26049  itg2split  26050  itg2monolem3  26053  itg2addlem  26059  ibladdlem  26120  itgaddlem1  26123  itgaddlem2  26124  iblabslem  26128  iblabs  26129  dvferm1lem  26284  dvferm2lem  26286  dvlip2  26295  lhop1lem  26313  lhop1  26314  lhop  26316  dvcnvrelem1  26317  dvcnvrelem2  26318  dvcnvre  26319  dvcvx  26320  dvfsumlem3  26328  dvfsumlem4  26329  dvfsum2  26334  ftc1lem4  26339  coemullem  26549  plyn0mulidp  26584  ulmbdd  26707  ulmcn  26708  ulmdvlem1  26709  radcnvle  26729  pserdvlem1  26736  pserdv  26738  abelthlem7  26747  pilem2  26761  pilem3  26762  cosordlem  26840  abslogle  26928  logccv  26973  cxpaddle  27062  ang180lem2  27120  heron  27148  atanlogaddlem  27223  atans2  27241  cxp2limlem  27285  scvxcvx  27295  jensenlem2  27297  amgmlem  27299  logdiflbnd  27304  harmonicbnd4  27320  fsumharmonic  27321  lgamgulmlem3  27340  lgamgulmlem4  27341  lgamgulmlem5  27342  lgamgulmlem6  27343  lgambdd  27346  lgamucov  27347  regamcl  27370  ftalem5  27386  efnnfsumcl  27412  efchtdvds  27468  chtublem  27520  chtub  27521  logfaclbnd  27531  perfectlem2  27539  bposlem7  27599  bposlem9  27601  lgsdirprm  27640  gausslemma2dlem1a  27674  2sqlem8  27735  chpchtlim  27788  vmadivsumb  27792  rplogsumlem1  27793  dchrisumlem2  27799  dchrvmasumlem2  27807  dchrvmasumiflem1  27810  dchrisum0re  27822  dchrisum0lem1b  27824  mulog2sumlem1  27843  mulog2sumlem2  27844  logsqvma2  27852  log2sumbnd  27853  selberglem2  27855  selbergb  27858  selberg2b  27861  chpdifbndlem1  27862  chpdifbndlem2  27863  selberg3lem2  27867  selberg3  27868  selberg4lem1  27869  selberg4  27870  pntrsumbnd2  27876  selberg3r  27878  selberg34r  27880  pntsf  27882  pntrlog2bndlem1  27886  pntrlog2bndlem2  27887  pntrlog2bndlem4  27889  pntrlog2bndlem5  27890  pntrlog2bndlem6  27892  pntrlog2bnd  27893  pntpbnd1a  27894  pntpbnd2  27896  pntibndlem2a  27899  pntibndlem2  27900  pntibndlem3  27901  pntlemg  27907  pntlemr  27911  pntlemk  27915  pntlemo  27916  pntlem3  27918  abvcxp  27924  padicabv  27939  ostth2lem2  27943  ostth3  27947  brbtwn2  29465  axsegconlem8  29484  axsegconlem10  29486  axpaschlem  29500  axpasch  29501  axeuclidlem  29522  axcontlem2  29525  crctcshwlkn0lem3  30383  crctcshwlkn0lem5  30385  vacn  31278  smcnlem  31281  ubthlem2  31455  minvecolem2  31459  minvecolem3  31460  minvecolem4  31464  minvecolem5  31465  nmoptrii  32678  hstle  32814  staddi  32830  stadd3i  32832  lt2addrd  33324  nndiffz1  33360  nexple  33406  wrdt2ind  33498  cshwrnid  33504  fsumrp0cl  33564  pmtrto1cl  33642  fzto1st  33646  psgnfzto1st  33648  constrresqrtcl  34391  cos9thpiminplylem1  34396  1smat1  34418  sqsscirc1  34522  cnre2csqlem  34524  tpr2rico  34526  dya2iocress  34889  dya2iocbrsiga  34890  dya2icobrsiga  34891  dya2icoseg  34892  dya2iocucvr  34899  sxbrsigalem2  34901  omssubaddlem  34914  fibp1  35016  ballotlemfc0  35108  ballotlemfcc  35109  ballotlemsgt1  35126  ballotlemsel1i  35128  breprexplemc  35244  breprexp  35245  logdivsqrle  35262  resconn  35980  faclim  36480  dnizphlfeqhlf  37312  dnibndlem4  37317  dnibndlem6  37319  dnibndlem8  37321  dnibndlem9  37322  dnibndlem10  37323  dnibndlem11  37324  dnibndlem13  37326  dnibnd  37327  knoppcnlem4  37332  unblimceq0lem  37342  unblimceq0  37343  unbdqndv2lem1  37345  poimirlem29  38535  heicant  38541  opnmbllem0  38542  mblfinlem3  38545  mblfinlem4  38546  ismblfin  38547  mbfposadd  38553  itg2addnclem  38557  itg2addnclem3  38559  itg2addnc  38560  itg2gt0cn  38561  ibladdnclem  38562  itgaddnclem1  38564  itgaddnclem2  38565  iblabsnclem  38569  iblabsnc  38570  iblmulc2nc  38571  ftc1cnnclem  38577  ftc1anclem4  38582  ftc1anclem7  38585  ftc1anclem8  38586  ftc1anc  38587  areacirclem5  38598  mettrifi  38659  isbnd3  38686  ssbnd  38690  cntotbnd  38698  heibor1lem  38711  bfplem2  38725  rrnequiv  38737  iccbnd  38742  lcmineqlem18  43064  lcmineqlem20  43066  aks4d1p1p3  43087  aks4d1p1p2  43088  aks4d1p1p4  43089  aks4d1p1p6  43091  aks4d1p1p7  43092  aks4d1p1p5  43093  aks4d1p1  43094  posbezout  43118  aks6d1c1  43134  aks6d1c2  43148  2np3bcnp1  43162  2ap1caineq  43163  sticksstones6  43169  sticksstones7  43170  sticksstones10  43173  sticksstones12a  43175  sticksstones12  43176  sticksstones22  43186  bcle2d  43197  aks6d1c7lem1  43198  readdridaddlidd  43276  resubeulem1  43394  resubeulem2  43395  resubeu  43396  readdsub  43403  reladdrsub  43404  resubidaddlidlem  43413  renegid2  43433  sn-it0e0  43435  redivdird  43481  sn-0tie0  43483  sn-addlt0d  43490  sn-addgt0d  43491  cnreeu  43522  dffltz  43624  fltnltalem  43627  fltnlta  43628  3cubeslem1  43648  pellexlem2  43790  pell1qrge1  43830  pell14qrgapw  43836  pellqrexplicit  43837  pellqrex  43839  pellfundge  43842  pellfundgt1  43843  rmspecfund  43869  rmxycomplete  43877  ltrmynn0  43908  jm2.24nn  43919  jm2.24  43923  fzmaxdif  43941  jm2.26lem3  43961  jm3.1lem2  43978  areaquad  44176  sqrtcvallem4  44598  sqrtcvallem5  44599  sqrtcval  44600  imo72b2lem0  45124  hashnzfzclim  45265  binomcxplemnotnn0  45299  zltlesub  46244  lt3addmuld  46260  absnpncan2d  46261  fperiodmullem  46262  lt4addmuld  46265  absnpncan3d  46266  supxrgelem  46293  supxrge  46294  ltadd12dd  46299  xralrple2  46310  infxr  46322  infleinflem2  46326  xralrple4  46328  xralrple3  46329  xrralrecnnle  46338  eliooshift  46462  iccshift  46474  iooshift  46478  iooiinicc  46498  iooiinioc  46512  fsumnncl  46528  climinf  46562  climsuselem1  46563  sumnnodd  46586  lptre2pt  46594  addlimc  46602  0ellimcdiv  46603  limclner  46605  climleltrp  46630  liminfltlem  46758  fperdvper  46873  dvdivbd  46877  dvbdfbdioolem2  46883  dvbdfbdioo  46884  ioodvbdlimc1lem1  46885  ioodvbdlimc1lem2  46886  ioodvbdlimc2lem  46888  dvxpaek  46894  dvnmul  46897  iblsplit  46920  iblspltprt  46927  itgspltprt  46933  itgiccshift  46934  itgperiod  46935  itgsbtaddcnst  46936  stoweidlem1  46955  stoweidlem11  46965  stoweidlem13  46967  stoweidlem14  46968  stoweidlem20  46974  stoweidlem21  46975  stoweidlem26  46980  stoweidlem44  46998  stoweidlem60  47014  wallispilem3  47021  wallispilem4  47022  wallispilem5  47023  wallispi  47024  wallispi2lem1  47025  wallispi2lem2  47026  stirlinglem1  47028  stirlinglem3  47030  stirlinglem5  47032  stirlinglem6  47033  stirlinglem7  47034  stirlinglem10  47037  stirlinglem11  47038  stirlinglem12  47039  dirker2re  47046  dirkerval2  47048  dirkerre  47049  dirkerper  47050  dirkertrigeqlem1  47052  dirkertrigeqlem2  47053  dirkeritg  47056  dirkercncflem1  47057  dirkercncflem2  47058  dirkercncflem4  47060  fourierdlem4  47065  fourierdlem5  47066  fourierdlem6  47067  fourierdlem7  47068  fourierdlem9  47070  fourierdlem10  47071  fourierdlem18  47079  fourierdlem19  47080  fourierdlem20  47081  fourierdlem26  47087  fourierdlem28  47089  fourierdlem30  47091  fourierdlem35  47096  fourierdlem40  47101  fourierdlem41  47102  fourierdlem42  47103  fourierdlem47  47107  fourierdlem48  47108  fourierdlem49  47109  fourierdlem50  47110  fourierdlem51  47111  fourierdlem53  47113  fourierdlem57  47117  fourierdlem59  47119  fourierdlem60  47120  fourierdlem61  47121  fourierdlem63  47123  fourierdlem64  47124  fourierdlem65  47125  fourierdlem66  47126  fourierdlem68  47128  fourierdlem71  47131  fourierdlem72  47132  fourierdlem74  47134  fourierdlem75  47135  fourierdlem76  47136  fourierdlem78  47138  fourierdlem79  47139  fourierdlem80  47140  fourierdlem81  47141  fourierdlem82  47142  fourierdlem83  47143  fourierdlem84  47144  fourierdlem87  47147  fourierdlem88  47148  fourierdlem89  47149  fourierdlem90  47150  fourierdlem91  47151  fourierdlem92  47152  fourierdlem93  47153  fourierdlem94  47154  fourierdlem95  47155  fourierdlem97  47157  fourierdlem101  47161  fourierdlem103  47163  fourierdlem104  47164  fourierdlem111  47171  fourierdlem112  47172  fourierdlem113  47173  sqwvfoura  47182  sqwvfourb  47183  fouriersw  47185  qndenserrnbllem  47248  ioorrnopnlem  47258  ioorrnopnxrlem  47260  sge0xaddlem1  47387  sge0xaddlem2  47388  omeiunltfirp  47473  carageniuncllem2  47476  hoidmv1lelem1  47545  hoidmv1lelem2  47546  hoidmvlelem1  47549  hoidmvlelem2  47550  hoidmvlelem3  47551  hoidmvlelem4  47552  hoiqssbllem1  47576  hoiqssbllem2  47577  hoiqssbllem3  47578  hspmbllem2  47581  hspmbllem3  47582  ovolval5lem1  47606  iinhoiicclem  47627  iinhoiicc  47628  iunhoiioolem  47629  iccvonmbllem  47632  vonioolem1  47634  vonioolem2  47635  vonicclem1  47637  vonicclem2  47638  preimaleiinlt  47675  salpreimaltle  47680  smfaddlem1  47717  smfadd  47719  smflimlem3  47727  smflimlem4  47728  smflimlem6  47730  smfmullem1  47745  smfmullem2  47746  smfmullem3  47747  ormkglobd  47831  zm1nn  48316  requad01  48663  requad1  48664  requad2  48665  perfectALTVlem2  48764  nnsum4primesevenALTV  48843  bgoldbtbndlem2  48848  gpgvtxedg0  49105  gpgvtxedg1  49106  gpg5nbgrvtx03starlem2  49111  gpg5nbgrvtx13starlem2  49114  dignn0flhalflem1  49671  affinecomb1  49758  resum2sqcl  49762  2sphere  49805  line2  49808  itsclc0lem1  49812  itscnhlc0yqe  49815  itsclquadb  49832  2itscp  49837  itscnhlinecirc02plem1  49838  itscnhlinecirc02plem3  49840  itscnhlinecirc02p  49841  inlinecirc02plem  49842  crossp3d  50911  veronesefvcl  50916  veronesev1lem  50917  veronesev2lem  50918  veronesev3lem  50919  veronesev4lem  50920  veronesev5lem  50921  veronesev6lem  50922  amgmwlem  50931