Theorem readdcld 10749

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 10699	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 587	1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2113  (class class class)co 7171  ℝcr 10615   + caddc 10619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 10677

This theorem depends on definitions:  df-bi 210  df-an 400

This theorem is referenced by:  ltadd2  10823  readdcan  10893  addid1  10899  leadd1  11187  le2add  11201  lesub2  11214  lesub3d  11337  supaddc  11686  supadd  11687  cju  11713  nnne0  11751  div4p1lem1div2  11972  difgtsumgt  12030  eluzmn  12332  rpnnen1lem5  12464  addlelt  12587  xralrple  12682  xov1plusxeqvd  12973  zltaddlt1le  12980  elincfzoext  13187  fladdz  13287  2tnp1ge0ge0  13291  flhalf  13292  fldiv  13320  modaddmodup  13394  modaddmodlo  13395  addmodlteq  13406  discr1  13693  discr  13694  ccatalpha  14037  2cshw  14265  remim  14567  remullem  14578  sqrlem7  14699  absrele  14759  abstri  14781  abs3lem  14789  amgm2  14820  bhmafibid1  14916  mulcn2  15044  o1add  15062  o1sub  15064  lo1add  15075  caucvgrlem  15123  iseraltlem2  15133  iseraltlem3  15134  fsumabs  15250  o1fsum  15262  climcndslem2  15299  tanhlt1  15606  eirrlem  15650  ruclem1  15677  ruclem2  15678  ruclem3  15679  ltoddhalfle  15807  bitscmp  15882  sadcaddlem  15901  sadasslem  15914  smuval2  15926  iserodd  16273  prmreclem4  16356  4sqlem5  16379  4sqlem6  16380  4sqlem12  16393  4sqlem15  16396  4sqlem16  16397  prmgaplem7  16494  prmgaplem8  16495  2expltfac  16530  cshwshashlem2  16534  chfacfscmul0  21610  chfacfscmulgsum  21612  chfacfpmmul0  21614  chfacfpmmulgsum  21616  prdsxmetlem  23122  xblss2ps  23155  metustexhalf  23310  nrmmetd  23328  ngptgp  23390  nlmvscnlem2  23439  nlmvscnlem1  23440  nmotri  23493  nghmplusg  23494  blcvx  23551  iccntr  23574  icccmplem2  23576  reconnlem2  23580  metdcnlem  23589  metnrmlem3  23614  cnllycmp  23709  lebnumii  23719  tcphcphlem1  23988  ipcnlem2  23997  ipcnlem1  23998  csbren  24152  trirn  24153  minveclem2  24179  minveclem3b  24181  minveclem4  24185  ivthlem2  24205  ovolgelb  24233  ovollb2lem  24241  ovolunlem1a  24249  ovolunlem1  24250  ovolfiniun  24254  ovoliunlem1  24255  ovoliunlem2  24256  ovolshftlem1  24262  ovolscalem1  24266  ovolicopnf  24277  ismbl2  24280  nulmbl2  24289  unmbl  24290  voliunlem2  24304  ioombl1lem2  24312  ioombl1lem4  24314  ioombl1  24315  ioorcl2  24325  uniioombllem1  24334  uniioombllem3  24338  uniioombllem4  24339  uniioombllem5  24340  uniioombl  24342  opnmbllem  24354  volcn  24359  itg1addlem4  24452  mbfi1fseqlem4  24471  mbfi1fseqlem6  24473  itg2splitlem  24501  itg2split  24502  itg2monolem3  24505  itg2addlem  24511  ibladdlem  24572  itgaddlem1  24575  itgaddlem2  24576  iblabslem  24580  iblabs  24581  dvferm1lem  24736  dvferm2lem  24738  dvlip2  24747  lhop1lem  24765  lhop1  24766  lhop  24768  dvcnvrelem1  24769  dvcnvrelem2  24770  dvcnvre  24771  dvcvx  24772  dvfsumlem3  24780  dvfsumlem4  24781  dvfsum2  24786  ftc1lem4  24791  coemullem  24999  ulmbdd  25145  ulmcn  25146  ulmdvlem1  25147  radcnvle  25167  pserdvlem1  25174  pserdv  25176  abelthlem7  25185  pilem2  25199  pilem3  25200  cosordlem  25274  abslogle  25361  logccv  25406  cxpaddle  25493  ang180lem2  25548  heron  25576  atanlogaddlem  25651  atans2  25669  cxp2limlem  25713  scvxcvx  25723  jensenlem2  25725  amgmlem  25727  logdiflbnd  25732  harmonicbnd4  25748  fsumharmonic  25749  lgamgulmlem3  25768  lgamgulmlem4  25769  lgamgulmlem5  25770  lgamgulmlem6  25771  lgambdd  25774  lgamucov  25775  regamcl  25798  ftalem5  25814  efnnfsumcl  25840  efchtdvds  25896  chtublem  25947  chtub  25948  logfaclbnd  25958  perfectlem2  25966  bposlem7  26026  bposlem9  26028  lgsdirprm  26067  gausslemma2dlem1a  26101  2sqlem8  26162  chpchtlim  26215  vmadivsumb  26219  rplogsumlem1  26220  dchrisumlem2  26226  dchrvmasumlem2  26234  dchrvmasumiflem1  26237  dchrisum0re  26249  dchrisum0lem1b  26251  mulog2sumlem1  26270  mulog2sumlem2  26271  logsqvma2  26279  log2sumbnd  26280  selberglem2  26282  selbergb  26285  selberg2b  26288  chpdifbndlem1  26289  chpdifbndlem2  26290  selberg3lem2  26294  selberg3  26295  selberg4lem1  26296  selberg4  26297  pntrsumbnd2  26303  selberg3r  26305  selberg34r  26307  pntsf  26309  pntrlog2bndlem1  26313  pntrlog2bndlem2  26314  pntrlog2bndlem4  26316  pntrlog2bndlem5  26317  pntrlog2bndlem6  26319  pntrlog2bnd  26320  pntpbnd1a  26321  pntpbnd2  26323  pntibndlem2a  26326  pntibndlem2  26327  pntibndlem3  26328  pntlemg  26334  pntlemr  26338  pntlemk  26342  pntlemo  26343  pntlem3  26345  abvcxp  26351  padicabv  26366  ostth2lem2  26370  ostth3  26374  brbtwn2  26851  axsegconlem8  26870  axsegconlem10  26872  axpaschlem  26886  axpasch  26887  axeuclidlem  26908  axcontlem2  26911  crctcshwlkn0lem3  27750  crctcshwlkn0lem5  27752  vacn  28629  smcnlem  28632  ubthlem2  28806  minvecolem2  28810  minvecolem3  28811  minvecolem4  28815  minvecolem5  28816  nmoptrii  30029  hstle  30165  staddi  30181  stadd3i  30183  lt2addrd  30649  nndiffz1  30682  wrdt2ind  30800  cshwrnid  30808  fsumrp0cl  30881  pmtrto1cl  30943  fzto1st  30947  psgnfzto1st  30949  1smat1  31326  sqsscirc1  31430  cnre2csqlem  31432  tpr2rico  31434  nexple  31547  dya2iocress  31811  dya2iocbrsiga  31812  dya2icobrsiga  31813  dya2icoseg  31814  dya2iocucvr  31821  sxbrsigalem2  31823  omssubaddlem  31836  fibp1  31938  ballotlemfc0  32029  ballotlemfcc  32030  ballotlemsgt1  32047  ballotlemsel1i  32049  plymulx0  32096  breprexplemc  32182  breprexp  32183  logdivsqrle  32200  resconn  32779  faclim  33283  dnizphlfeqhlf  34294  dnibndlem4  34299  dnibndlem6  34301  dnibndlem8  34303  dnibndlem9  34304  dnibndlem10  34305  dnibndlem11  34306  dnibndlem13  34308  dnibnd  34309  knoppcnlem4  34314  unblimceq0lem  34324  unblimceq0  34325  unbdqndv2lem1  34327  poimirlem29  35426  heicant  35432  opnmbllem0  35433  mblfinlem3  35436  mblfinlem4  35437  ismblfin  35438  mbfposadd  35444  itg2addnclem  35448  itg2addnclem3  35450  itg2addnc  35451  itg2gt0cn  35452  ibladdnclem  35453  itgaddnclem1  35455  itgaddnclem2  35456  iblabsnclem  35460  iblabsnc  35461  iblmulc2nc  35462  ftc1cnnclem  35468  ftc1anclem4  35473  ftc1anclem7  35476  ftc1anclem8  35477  ftc1anc  35478  areacirclem5  35489  mettrifi  35535  isbnd3  35562  ssbnd  35566  cntotbnd  35574  heibor1lem  35587  bfplem2  35601  rrnequiv  35613  iccbnd  35618  lcmineqlem18  39671  lcmineqlem20  39673  aks4d1p1p3  39693  aks4d1p1p2  39694  aks4d1p1p4  39695  aks4d1p1p6  39697  aks4d1p1p7  39698  aks4d1p1p5  39699  aks4d1p1  39700  2np3bcnp1  39703  2ap1caineq  39704  sticksstones6  39710  sticksstones7  39711  metakunt29  39741  2xp3dxp2ge1d  39750  factwoffsmonot  39751  readdid1addid2d  39862  resubeulem1  39927  resubeulem2  39928  resubeu  39929  readdsub  39936  reladdrsub  39937  resubidaddid1lem  39946  renegid2  39965  sn-it0e0  39966  sn-0tie0  39990  cnreeu  40007  dffltz  40035  fltnltalem  40063  fltnlta  40064  3cubeslem1  40070  pellexlem2  40216  pell1qrge1  40256  pell14qrgapw  40262  pellqrexplicit  40263  pellqrex  40265  pellfundge  40268  pellfundgt1  40269  rmspecfund  40295  rmxycomplete  40303  ltrmynn0  40334  jm2.24nn  40345  jm2.24  40349  fzmaxdif  40367  jm2.26lem3  40387  jm3.1lem2  40404  areaquad  40611  sqrtcvallem4  40784  sqrtcvallem5  40785  sqrtcval  40786  imo72b2lem0  41314  hashnzfzclim  41470  binomcxplemnotnn0  41504  zltlesub  42353  lt3addmuld  42370  absnpncan2d  42371  fperiodmullem  42372  lt4addmuld  42375  absnpncan3d  42376  leadd12dd  42385  supxrgelem  42406  supxrge  42407  ltadd12dd  42412  xralrple2  42423  infxr  42436  infleinflem2  42440  xralrple4  42442  xralrple3  42443  xrralrecnnle  42452  eliooshift  42576  iccshift  42588  iooshift  42592  iooiinicc  42612  iooiinioc  42626  fsumnncl  42646  climinf  42681  climsuselem1  42682  sumnnodd  42705  lptre2pt  42715  addlimc  42723  0ellimcdiv  42724  limclner  42726  climleltrp  42751  liminfltlem  42879  fperdvper  42994  dvdivbd  42998  dvbdfbdioolem2  43004  dvbdfbdioo  43005  ioodvbdlimc1lem1  43006  ioodvbdlimc1lem2  43007  ioodvbdlimc2lem  43009  dvxpaek  43015  dvnmul  43018  iblsplit  43041  iblspltprt  43048  itgspltprt  43054  itgiccshift  43055  itgperiod  43056  itgsbtaddcnst  43057  stoweidlem1  43076  stoweidlem11  43086  stoweidlem13  43088  stoweidlem14  43089  stoweidlem20  43095  stoweidlem21  43096  stoweidlem26  43101  stoweidlem44  43119  stoweidlem60  43135  wallispilem3  43142  wallispilem4  43143  wallispilem5  43144  wallispi  43145  wallispi2lem1  43146  wallispi2lem2  43147  stirlinglem1  43149  stirlinglem3  43151  stirlinglem5  43153  stirlinglem6  43154  stirlinglem7  43155  stirlinglem10  43158  stirlinglem11  43159  stirlinglem12  43160  dirker2re  43167  dirkerval2  43169  dirkerre  43170  dirkerper  43171  dirkertrigeqlem1  43173  dirkertrigeqlem2  43174  dirkeritg  43177  dirkercncflem1  43178  dirkercncflem2  43179  dirkercncflem4  43181  fourierdlem4  43186  fourierdlem5  43187  fourierdlem6  43188  fourierdlem7  43189  fourierdlem9  43191  fourierdlem10  43192  fourierdlem18  43200  fourierdlem19  43201  fourierdlem20  43202  fourierdlem26  43208  fourierdlem28  43210  fourierdlem30  43212  fourierdlem35  43217  fourierdlem40  43222  fourierdlem41  43223  fourierdlem42  43224  fourierdlem47  43228  fourierdlem48  43229  fourierdlem49  43230  fourierdlem50  43231  fourierdlem51  43232  fourierdlem53  43234  fourierdlem57  43238  fourierdlem59  43240  fourierdlem60  43241  fourierdlem61  43242  fourierdlem63  43244  fourierdlem64  43245  fourierdlem65  43246  fourierdlem66  43247  fourierdlem68  43249  fourierdlem71  43252  fourierdlem72  43253  fourierdlem74  43255  fourierdlem75  43256  fourierdlem76  43257  fourierdlem78  43259  fourierdlem79  43260  fourierdlem80  43261  fourierdlem81  43262  fourierdlem82  43263  fourierdlem83  43264  fourierdlem84  43265  fourierdlem87  43268  fourierdlem88  43269  fourierdlem89  43270  fourierdlem90  43271  fourierdlem91  43272  fourierdlem92  43273  fourierdlem93  43274  fourierdlem94  43275  fourierdlem95  43276  fourierdlem97  43278  fourierdlem101  43282  fourierdlem103  43284  fourierdlem104  43285  fourierdlem111  43292  fourierdlem112  43293  fourierdlem113  43294  sqwvfoura  43303  sqwvfourb  43304  fouriersw  43306  qndenserrnbllem  43369  ioorrnopnlem  43379  ioorrnopnxrlem  43381  sge0xaddlem1  43505  sge0xaddlem2  43506  omeiunltfirp  43591  carageniuncllem2  43594  hoidmv1lelem1  43663  hoidmv1lelem2  43664  hoidmvlelem1  43667  hoidmvlelem2  43668  hoidmvlelem3  43669  hoidmvlelem4  43670  hoiqssbllem1  43694  hoiqssbllem2  43695  hoiqssbllem3  43696  hspmbllem2  43699  hspmbllem3  43700  ovolval5lem1  43724  iinhoiicclem  43745  iinhoiicc  43746  iunhoiioolem  43747  iccvonmbllem  43750  vonioolem1  43752  vonioolem2  43753  vonicclem1  43755  vonicclem2  43756  preimaleiinlt  43789  salpreimaltle  43793  smfaddlem1  43829  smfadd  43831  smflimlem3  43839  smflimlem4  43840  smflimlem6  43842  smfmullem1  43856  smfmullem2  43857  smfmullem3  43858  zm1nn  44320  requad01  44599  requad1  44600  requad2  44601  perfectALTVlem2  44700  nnsum4primesevenALTV  44779  bgoldbtbndlem2  44784  dignn0flhalflem1  45487  affinecomb1  45574  resum2sqcl  45578  2sphere  45621  line2  45624  itsclc0lem1  45628  itscnhlc0yqe  45631  itsclquadb  45648  2itscp  45653  itscnhlinecirc02plem1  45654  itscnhlinecirc02plem3  45656  itscnhlinecirc02p  45657  inlinecirc02plem  45658  amgmwlem  45951