MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  readdcld Structured version   Visualization version   GIF version

Theorem readdcld 10659
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
StepHypRef Expression
1 recnd.1 . 2 (𝜑𝐴 ∈ ℝ)
2 readdcld.2 . 2 (𝜑𝐵 ∈ ℝ)
3 readdcl 10609 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
41, 2, 3syl2anc 584 1 (𝜑 → (𝐴 + 𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  (class class class)co 7145  cr 10525   + caddc 10529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 10587
This theorem depends on definitions:  df-bi 208  df-an 397
This theorem is referenced by:  ltadd2  10733  readdcan  10803  addid1  10809  leadd1  11097  le2add  11111  lesub2  11124  lesub3d  11247  supaddc  11597  supadd  11598  cju  11623  nnne0  11660  div4p1lem1div2  11881  difgtsumgt  11939  eluzmn  12239  rpnnen1lem5  12370  addlelt  12493  xralrple  12588  xov1plusxeqvd  12874  zltaddlt1le  12880  elincfzoext  13085  fladdz  13185  2tnp1ge0ge0  13189  flhalf  13190  fldiv  13218  modaddmodup  13292  modaddmodlo  13293  addmodlteq  13304  discr1  13590  discr  13591  ccatalpha  13937  2cshw  14165  remim  14466  remullem  14477  sqrlem7  14598  absrele  14658  abstri  14680  abs3lem  14688  amgm2  14719  bhmafibid1  14815  mulcn2  14942  o1add  14960  o1sub  14962  lo1add  14973  caucvgrlem  15019  iseraltlem2  15029  iseraltlem3  15030  fsumabs  15146  o1fsum  15158  climcndslem2  15195  tanhlt1  15503  eirrlem  15547  ruclem1  15574  ruclem2  15575  ruclem3  15576  ltoddhalfle  15700  bitscmp  15777  sadcaddlem  15796  sadasslem  15809  smuval2  15821  iserodd  16162  prmreclem4  16245  4sqlem5  16268  4sqlem6  16269  4sqlem12  16282  4sqlem15  16285  4sqlem16  16286  prmgaplem7  16383  prmgaplem8  16384  2expltfac  16416  cshwshashlem2  16420  chfacfscmul0  21396  chfacfscmulgsum  21398  chfacfpmmul0  21400  chfacfpmmulgsum  21402  prdsxmetlem  22907  xblss2ps  22940  metustexhalf  23095  nrmmetd  23113  ngptgp  23174  nlmvscnlem2  23223  nlmvscnlem1  23224  nmotri  23277  nghmplusg  23278  blcvx  23335  iccntr  23358  icccmplem2  23360  reconnlem2  23364  metdcnlem  23373  metnrmlem3  23398  cnllycmp  23489  lebnumii  23499  tcphcphlem1  23767  ipcnlem2  23776  ipcnlem1  23777  csbren  23931  trirn  23932  minveclem2  23958  minveclem3b  23960  minveclem4  23964  ivthlem2  23982  ovolgelb  24010  ovollb2lem  24018  ovolunlem1a  24026  ovolunlem1  24027  ovolfiniun  24031  ovoliunlem1  24032  ovoliunlem2  24033  ovolshftlem1  24039  ovolscalem1  24043  ovolicopnf  24054  ismbl2  24057  nulmbl2  24066  unmbl  24067  voliunlem2  24081  ioombl1lem2  24089  ioombl1lem4  24091  ioombl1  24092  ioorcl2  24102  uniioombllem1  24111  uniioombllem3  24115  uniioombllem4  24116  uniioombllem5  24117  uniioombl  24119  opnmbllem  24131  volcn  24136  itg1addlem4  24229  mbfi1fseqlem4  24248  mbfi1fseqlem6  24250  itg2splitlem  24278  itg2split  24279  itg2monolem3  24282  itg2addlem  24288  ibladdlem  24349  itgaddlem1  24352  itgaddlem2  24353  iblabslem  24357  iblabs  24358  dvferm1lem  24510  dvferm2lem  24512  dvlip2  24521  lhop1lem  24539  lhop1  24540  lhop  24542  dvcnvrelem1  24543  dvcnvrelem2  24544  dvcnvre  24545  dvcvx  24546  dvfsumlem3  24554  dvfsumlem4  24555  dvfsum2  24560  ftc1lem4  24565  coemullem  24769  ulmbdd  24915  ulmcn  24916  ulmdvlem1  24917  radcnvle  24937  pserdvlem1  24944  pserdv  24946  abelthlem7  24955  pilem2  24969  pilem3  24970  cosordlem  25042  abslogle  25128  logccv  25173  cxpaddle  25260  ang180lem2  25315  heron  25343  atanlogaddlem  25418  atans2  25436  cxp2limlem  25481  scvxcvx  25491  jensenlem2  25493  amgmlem  25495  logdiflbnd  25500  harmonicbnd4  25516  fsumharmonic  25517  lgamgulmlem3  25536  lgamgulmlem4  25537  lgamgulmlem5  25538  lgamgulmlem6  25539  lgambdd  25542  lgamucov  25543  regamcl  25566  ftalem5  25582  efnnfsumcl  25608  efchtdvds  25664  chtublem  25715  chtub  25716  logfaclbnd  25726  perfectlem2  25734  bposlem7  25794  bposlem9  25796  lgsdirprm  25835  gausslemma2dlem1a  25869  2sqlem8  25930  chpchtlim  25983  vmadivsumb  25987  rplogsumlem1  25988  dchrisumlem2  25994  dchrvmasumlem2  26002  dchrvmasumiflem1  26005  dchrisum0re  26017  dchrisum0lem1b  26019  mulog2sumlem1  26038  mulog2sumlem2  26039  logsqvma2  26047  log2sumbnd  26048  selberglem2  26050  selbergb  26053  selberg2b  26056  chpdifbndlem1  26057  chpdifbndlem2  26058  selberg3lem2  26062  selberg3  26063  selberg4lem1  26064  selberg4  26065  pntrsumbnd2  26071  selberg3r  26073  selberg34r  26075  pntsf  26077  pntrlog2bndlem1  26081  pntrlog2bndlem2  26082  pntrlog2bndlem4  26084  pntrlog2bndlem5  26085  pntrlog2bndlem6  26087  pntrlog2bnd  26088  pntpbnd1a  26089  pntpbnd2  26091  pntibndlem2a  26094  pntibndlem2  26095  pntibndlem3  26096  pntlemg  26102  pntlemr  26106  pntlemk  26110  pntlemo  26111  pntlem3  26113  abvcxp  26119  padicabv  26134  ostth2lem2  26138  ostth3  26142  brbtwn2  26619  axsegconlem8  26638  axsegconlem10  26640  axpaschlem  26654  axpasch  26655  axeuclidlem  26676  axcontlem2  26679  crctcshwlkn0lem3  27518  crctcshwlkn0lem5  27520  vacn  28399  smcnlem  28402  ubthlem2  28576  minvecolem2  28580  minvecolem3  28581  minvecolem4  28585  minvecolem5  28586  nmoptrii  29799  hstle  29935  staddi  29951  stadd3i  29953  lt2addrd  30402  nndiffz1  30436  wrdt2ind  30555  cshwrnid  30563  fsumrp0cl  30610  pmtrto1cl  30669  fzto1st  30673  psgnfzto1st  30675  1smat1  30969  sqsscirc1  31051  cnre2csqlem  31053  tpr2rico  31055  nexple  31168  dya2iocress  31432  dya2iocbrsiga  31433  dya2icobrsiga  31434  dya2icoseg  31435  dya2iocucvr  31442  sxbrsigalem2  31444  omssubaddlem  31457  fibp1  31559  ballotlemfc0  31650  ballotlemfcc  31651  ballotlemsgt1  31668  ballotlemsel1i  31670  plymulx0  31717  breprexplemc  31803  breprexp  31804  logdivsqrle  31821  resconn  32391  faclim  32876  dnizphlfeqhlf  33713  dnibndlem4  33718  dnibndlem6  33720  dnibndlem8  33722  dnibndlem9  33723  dnibndlem10  33724  dnibndlem11  33725  dnibndlem13  33727  dnibnd  33728  knoppcnlem4  33733  unblimceq0lem  33743  unblimceq0  33744  unbdqndv2lem1  33746  poimirlem29  34803  heicant  34809  opnmbllem0  34810  mblfinlem3  34813  mblfinlem4  34814  ismblfin  34815  mbfposadd  34821  itg2addnclem  34825  itg2addnclem3  34827  itg2addnc  34828  itg2gt0cn  34829  ibladdnclem  34830  itgaddnclem1  34832  itgaddnclem2  34833  iblabsnclem  34837  iblabsnc  34838  iblmulc2nc  34839  ftc1cnnclem  34847  ftc1anclem4  34852  ftc1anclem7  34855  ftc1anclem8  34856  ftc1anc  34857  areacirclem5  34868  mettrifi  34915  isbnd3  34945  ssbnd  34949  cntotbnd  34957  heibor1lem  34970  bfplem2  34984  rrnequiv  34996  iccbnd  35001  readdid1addid2d  39037  resubeulem1  39085  resubeulem2  39086  resubeu  39087  readdsub  39094  reladdrsub  39095  resubidaddid1lem  39104  dffltz  39151  fltnltalem  39154  fltnlta  39155  3cubeslem1  39161  pellexlem2  39307  pell1qrge1  39347  pell14qrgapw  39353  pellqrexplicit  39354  pellqrex  39356  pellfundge  39359  pellfundgt1  39360  rmspecfund  39386  rmxycomplete  39394  ltrmynn0  39425  jm2.24nn  39436  jm2.24  39440  fzmaxdif  39458  jm2.26lem3  39478  jm3.1lem2  39495  areaquad  39703  imo72b2lem0  40396  hashnzfzclim  40534  binomcxplemnotnn0  40568  zltlesub  41431  lt3addmuld  41448  absnpncan2d  41449  fperiodmullem  41450  lt4addmuld  41453  absnpncan3d  41454  leadd12dd  41464  supxrgelem  41485  supxrge  41486  ltadd12dd  41491  xralrple2  41502  infxr  41515  infleinflem2  41519  xralrple4  41521  xralrple3  41522  xrralrecnnle  41533  eliooshift  41662  iccshift  41674  iooshift  41678  iooiinicc  41698  iooiinioc  41712  fsumnncl  41732  climinf  41767  climsuselem1  41768  sumnnodd  41791  lptre2pt  41801  addlimc  41809  0ellimcdiv  41810  limclner  41812  climleltrp  41837  liminfltlem  41965  fperdvper  42083  dvdivbd  42088  dvbdfbdioolem2  42094  dvbdfbdioo  42095  ioodvbdlimc1lem1  42096  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  dvxpaek  42105  dvnmul  42108  iblsplit  42131  iblspltprt  42138  itgspltprt  42144  itgiccshift  42145  itgperiod  42146  itgsbtaddcnst  42147  stoweidlem1  42167  stoweidlem11  42177  stoweidlem13  42179  stoweidlem14  42180  stoweidlem20  42186  stoweidlem21  42187  stoweidlem26  42192  stoweidlem44  42210  stoweidlem60  42226  wallispilem3  42233  wallispilem4  42234  wallispilem5  42235  wallispi  42236  wallispi2lem1  42237  wallispi2lem2  42238  stirlinglem1  42240  stirlinglem3  42242  stirlinglem5  42244  stirlinglem6  42245  stirlinglem7  42246  stirlinglem10  42249  stirlinglem11  42250  stirlinglem12  42251  dirker2re  42258  dirkerval2  42260  dirkerre  42261  dirkerper  42262  dirkertrigeqlem1  42264  dirkertrigeqlem2  42265  dirkeritg  42268  dirkercncflem1  42269  dirkercncflem2  42270  dirkercncflem4  42272  fourierdlem4  42277  fourierdlem5  42278  fourierdlem6  42279  fourierdlem7  42280  fourierdlem9  42282  fourierdlem10  42283  fourierdlem18  42291  fourierdlem19  42292  fourierdlem20  42293  fourierdlem26  42299  fourierdlem28  42301  fourierdlem30  42303  fourierdlem35  42308  fourierdlem40  42313  fourierdlem41  42314  fourierdlem42  42315  fourierdlem47  42319  fourierdlem48  42320  fourierdlem49  42321  fourierdlem50  42322  fourierdlem51  42323  fourierdlem53  42325  fourierdlem57  42329  fourierdlem59  42331  fourierdlem60  42332  fourierdlem61  42333  fourierdlem63  42335  fourierdlem64  42336  fourierdlem65  42337  fourierdlem66  42338  fourierdlem68  42340  fourierdlem71  42343  fourierdlem72  42344  fourierdlem74  42346  fourierdlem75  42347  fourierdlem76  42348  fourierdlem78  42350  fourierdlem79  42351  fourierdlem80  42352  fourierdlem81  42353  fourierdlem82  42354  fourierdlem83  42355  fourierdlem84  42356  fourierdlem87  42359  fourierdlem88  42360  fourierdlem89  42361  fourierdlem90  42362  fourierdlem91  42363  fourierdlem92  42364  fourierdlem93  42365  fourierdlem94  42366  fourierdlem95  42367  fourierdlem97  42369  fourierdlem101  42373  fourierdlem103  42375  fourierdlem104  42376  fourierdlem111  42383  fourierdlem112  42384  fourierdlem113  42385  sqwvfoura  42394  sqwvfourb  42395  fouriersw  42397  qndenserrnbllem  42460  ioorrnopnlem  42470  ioorrnopnxrlem  42472  sge0xaddlem1  42596  sge0xaddlem2  42597  omeiunltfirp  42682  carageniuncllem2  42685  hoidmv1lelem1  42754  hoidmv1lelem2  42755  hoidmvlelem1  42758  hoidmvlelem2  42759  hoidmvlelem3  42760  hoidmvlelem4  42761  hoiqssbllem1  42785  hoiqssbllem2  42786  hoiqssbllem3  42787  hspmbllem2  42790  hspmbllem3  42791  ovolval5lem1  42815  iinhoiicclem  42836  iinhoiicc  42837  iunhoiioolem  42838  iccvonmbllem  42841  vonioolem1  42843  vonioolem2  42844  vonicclem1  42846  vonicclem2  42847  preimaleiinlt  42880  salpreimaltle  42884  smfaddlem1  42920  smfadd  42922  smflimlem3  42930  smflimlem4  42931  smflimlem6  42933  smfmullem1  42947  smfmullem2  42948  smfmullem3  42949  zm1nn  43383  requad01  43633  requad1  43634  requad2  43635  perfectALTVlem2  43734  nnsum4primesevenALTV  43813  bgoldbtbndlem2  43818  dignn0flhalflem1  44573  affinecomb1  44587  resum2sqcl  44591  2sphere  44634  line2  44637  itsclc0lem1  44641  itscnhlc0yqe  44644  itsclquadb  44661  2itscp  44666  itscnhlinecirc02plem1  44667  itscnhlinecirc02plem3  44669  itscnhlinecirc02p  44670  inlinecirc02plem  44671  amgmwlem  44801
  Copyright terms: Public domain W3C validator