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

Theorem readdcld 9669
Description: Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
recnd.1  |-  ( ph  ->  A  e.  RR )
readdcld.2  |-  ( ph  ->  B  e.  RR )
Assertion
Ref Expression
readdcld  |-  ( ph  ->  ( A  +  B
)  e.  RR )

Proof of Theorem readdcld
StepHypRef Expression
1 recnd.1 . 2  |-  ( ph  ->  A  e.  RR )
2 readdcld.2 . 2  |-  ( ph  ->  B  e.  RR )
3 readdcl 9621 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )
41, 2, 3syl2anc 665 1  |-  ( ph  ->  ( A  +  B
)  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870  (class class class)co 6305   RRcr 9537    + caddc 9541
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 9599
This theorem depends on definitions:  df-bi 188  df-an 372
This theorem is referenced by:  ltadd2  9737  readdcan  9806  addid1  9812  leadd1  10081  le2add  10095  lesub2  10108  lesub3d  10230  supaddc  10574  supadd  10575  cju  10605  rpnnen1lem5  11294  xralrple  11498  xov1plusxeqvd  11776  elincfzoext  11969  fladdz  12055  flhalf  12059  fldiv  12084  modaddmodup  12150  modaddmodlo  12151  discr1  12405  discr  12406  2cshw  12897  remim  13159  remullem  13170  sqrlem7  13291  absrele  13350  abstri  13372  abs3lem  13380  amgm2  13411  mulcn2  13637  o1add  13655  o1sub  13657  lo1add  13668  caucvgrlem  13714  caucvgrlemOLD  13715  iseraltlem2  13727  iseraltlem3  13728  fsumabs  13839  o1fsum  13851  climcndslem2  13886  tanhlt1  14192  eirrlem  14234  ruclem1  14261  ruclem2  14262  ruclem3  14263  bitscmp  14386  sadcaddlem  14405  sadasslem  14418  smuval2  14430  prmreclem4  14826  4sqlem5  14849  4sqlem6  14850  4sqlem12  14863  4sqlem15OLD  14866  4sqlem16OLD  14867  4sqlem15  14872  4sqlem16  14873  prmgaplem7  14990  prmgaplem8  14991  2expltfac  15026  cshwshashlem2  15030  chfacfscmul0  19813  chfacfscmulgsum  19815  chfacfpmmul0  19817  chfacfpmmulgsum  19819  prdsxmetlem  21314  xblss2ps  21347  metustexhalf  21502  nrmmetd  21520  ngptgp  21575  nlmvscnlem2  21619  nlmvscnlem1  21620  nmotri  21671  nghmplusg  21672  blcvx  21727  iccntr  21750  icccmplem2  21752  reconnlem2  21756  metdcnlem  21765  metnrmlem3  21789  cnllycmp  21880  lebnumii  21890  tchcphlem1  22102  ipcnlem2  22108  ipcnlem1  22109  csbren  22246  trirn  22247  minveclem2  22261  minveclem3b  22263  minveclem4  22267  ivthlem2  22284  ovolgelb  22311  ovollb2lem  22319  ovolunlem1a  22327  ovolunlem1  22328  ovolfiniun  22332  ovoliunlem1  22333  ovoliunlem2  22334  ovolshftlem1  22340  ovolscalem1  22344  ovolicopnf  22355  ismbl2  22358  nulmbl2  22367  unmbl  22368  voliunlem2  22381  ioombl1lem2  22389  ioombl1lem4  22391  ioombl1  22392  ioorcl2  22401  uniioombllem1  22415  uniioombllem3  22420  uniioombllem4  22421  uniioombllem5  22422  uniioombl  22424  opnmbllem  22436  volcn  22441  itg1addlem4  22534  mbfi1fseqlem4  22553  mbfi1fseqlem6  22555  itg2splitlem  22583  itg2split  22584  itg2monolem3  22587  itg2addlem  22593  ibladdlem  22654  itgaddlem1  22657  itgaddlem2  22658  iblabslem  22662  iblabs  22663  dvferm1lem  22813  dvferm2lem  22815  dvlip2  22824  lhop1lem  22842  lhop1  22843  lhop  22845  dvcnvrelem1  22846  dvcnvrelem2  22847  dvcnvre  22848  dvcvx  22849  dvfsumlem3  22857  dvfsumlem4  22858  dvfsum2  22863  ftc1lem4  22868  coemullem  23072  ulmbdd  23218  ulmcn  23219  ulmdvlem1  23220  radcnvle  23240  pserdvlem1  23247  pserdv  23249  abelthlem7  23258  pilem2  23272  pilem2OLD  23273  pilem3  23274  pilem3OLD  23275  cosordlem  23345  abslogle  23432  logccv  23473  cxpaddle  23557  ang180lem2  23604  heron  23629  atanlogaddlem  23704  atans2  23722  cxp2limlem  23766  scvxcvx  23776  jensenlem2  23778  amgmlem  23780  logdiflbnd  23785  harmonicbnd4  23801  fsumharmonic  23802  lgamgulmlem3  23821  lgamgulmlem4  23822  lgamgulmlem5  23823  lgamgulmlem6  23824  lgambdd  23827  lgamucov  23828  regamcl  23851  ftalem5  23866  efnnfsumcl  23892  efchtdvds  23949  chtublem  24002  chtub  24003  logfaclbnd  24013  perfectlem2  24021  bcmono  24068  bposlem7  24081  bposlem9  24083  lgsdirprm  24120  2sqlem8  24163  chpchtlim  24180  vmadivsumb  24184  rplogsumlem1  24185  dchrisumlem2  24191  dchrvmasumlem2  24199  dchrvmasumiflem1  24202  dchrisum0re  24214  dchrisum0lem1b  24216  mulog2sumlem1  24235  mulog2sumlem2  24236  logsqvma2  24244  log2sumbnd  24245  selberglem2  24247  selbergb  24250  selberg2b  24253  chpdifbndlem1  24254  chpdifbndlem2  24255  selberg3lem2  24259  selberg3  24260  selberg4lem1  24261  selberg4  24262  pntrsumbnd2  24268  selberg3r  24270  selberg34r  24272  pntsf  24274  pntrlog2bndlem1  24278  pntrlog2bndlem2  24279  pntrlog2bndlem4  24281  pntrlog2bndlem5  24282  pntrlog2bndlem6  24284  pntrlog2bnd  24285  pntpbnd1a  24286  pntpbnd2  24288  pntibndlem2a  24291  pntibndlem2  24292  pntibndlem3  24293  pntlemg  24299  pntlemr  24303  pntlemk  24307  pntlemo  24308  pntlem3  24310  abvcxp  24316  padicabv  24331  ostth2lem2  24335  ostth3  24339  brbtwn2  24781  axsegconlem8  24800  axsegconlem10  24802  axpaschlem  24816  axpasch  24817  axeuclidlem  24838  axcontlem2  24841  vacn  26175  smcnlem  26178  ubthlem2  26358  minvecolem2  26362  minvecolem3  26363  minvecolem4  26367  minvecolem5  26368  nmoptrii  27582  hstle  27718  staddi  27734  stadd3i  27736  lt2addrd  28169  nndiffz1  28202  bhmafibid1  28243  fsumrp0cl  28296  pmtrto1cl  28451  fzto1st  28455  psgnfzto1st  28457  1smat1  28469  sqsscirc1  28553  cnre2csqlem  28555  tpr2rico  28557  nexple  28670  dya2iocress  28935  dya2iocbrsiga  28936  dya2icobrsiga  28937  dya2icoseg  28938  dya2iocucvr  28945  sxbrsigalem2  28947  omssubaddlem  28960  fibp1  29060  ballotlemfc0  29151  ballotlemfcc  29152  ballotlemsgt1  29169  ballotlemsel1i  29171  eluzmn  29211  plymulx0  29224  rescon  29757  faclim  30169  poimirlem29  31673  heicant  31679  opnmbllem0  31680  mblfinlem3  31683  mblfinlem4  31684  ismblfin  31685  mbfposadd  31692  itg2addnclem  31697  itg2addnclem3  31699  itg2addnc  31700  itg2gt0cn  31701  ibladdnclem  31702  itgaddnclem1  31704  itgaddnclem2  31705  iblabsnclem  31709  iblabsnc  31710  iblmulc2nc  31711  ftc1cnnclem  31719  ftc1anclem4  31724  ftc1anclem7  31727  ftc1anclem8  31728  ftc1anc  31729  areacirclem5  31740  mettrifi  31790  isbnd3  31820  ssbnd  31824  cntotbnd  31832  heibor1lem  31845  bfplem2  31859  rrnequiv  31871  iccbnd  31876  pellexlem2  35384  pell1qrge1  35424  pell14qrgapw  35430  pellqrexplicit  35431  pellqrex  35433  pellfundge  35436  pellfundgt1  35437  rmspecfund  35463  rmxycomplete  35471  ltrmynn0  35504  jm2.24nn  35515  jm2.24  35519  fzmaxdif  35537  jm2.26lem3  35562  jm3.1lem2  35579  areaquad  35800  imo72b2lem0  36245  hashnzfzclim  36308  binomcxplemnotnn0  36342  zltlesub  37104  lt3addmuld  37128  absnpncan2d  37129  fperiodmullem  37130  lt4addmuld  37133  absnpncan3d  37134  leadd12dd  37147  supxrgelem  37169  supxrge  37170  eliooshift  37189  iccshift  37204  iooshift  37208  fsumnncl  37225  climinf  37256  climinfOLD  37257  climsuselem1  37258  sumnnodd  37282  lptre2pt  37292  addlimc  37301  0ellimcdiv  37302  limclner  37304  fperdvper  37362  dvdivbd  37367  dvbdfbdioolem2  37373  dvbdfbdioo  37374  ioodvbdlimc1lem1  37375  ioodvbdlimc1lem2  37376  ioodvbdlimc2lem  37378  dvxpaek  37384  dvnmul  37387  iblsplit  37412  iblspltprt  37419  itgspltprt  37425  itgiccshift  37426  itgperiod  37427  itgsbtaddcnst  37428  stoweidlem1  37430  stoweidlem11  37440  stoweidlem13  37442  stoweidlem14  37443  stoweidlem20  37449  stoweidlem21  37450  stoweidlem26  37455  stoweidlem44  37474  stoweidlem60  37490  wallispilem3  37498  wallispilem4  37499  wallispilem5  37500  wallispi  37501  wallispi2lem1  37502  wallispi2lem2  37503  stirlinglem1  37505  stirlinglem3  37507  stirlinglem5  37509  stirlinglem6  37510  stirlinglem7  37511  stirlinglem10  37514  stirlinglem11  37515  stirlinglem12  37516  dirker2re  37523  dirkerval2  37525  dirkerre  37526  dirkerper  37527  dirkertrigeqlem1  37529  dirkertrigeqlem2  37530  dirkeritg  37533  dirkercncflem1  37534  dirkercncflem2  37535  dirkercncflem4  37537  fourierdlem4  37542  fourierdlem5  37543  fourierdlem6  37544  fourierdlem7  37545  fourierdlem9  37547  fourierdlem10  37548  fourierdlem18  37556  fourierdlem19  37557  fourierdlem20  37558  fourierdlem26  37564  fourierdlem28  37566  fourierdlem30  37568  fourierdlem35  37573  fourierdlem40  37578  fourierdlem41  37579  fourierdlem42  37580  fourierdlem47  37585  fourierdlem48  37586  fourierdlem49  37587  fourierdlem50  37588  fourierdlem51  37589  fourierdlem53  37591  fourierdlem57  37595  fourierdlem59  37597  fourierdlem60  37598  fourierdlem61  37599  fourierdlem63  37601  fourierdlem64  37602  fourierdlem65  37603  fourierdlem66  37604  fourierdlem68  37606  fourierdlem71  37609  fourierdlem72  37610  fourierdlem74  37612  fourierdlem75  37613  fourierdlem76  37614  fourierdlem78  37616  fourierdlem79  37617  fourierdlem80  37618  fourierdlem81  37619  fourierdlem82  37620  fourierdlem83  37621  fourierdlem84  37622  fourierdlem87  37625  fourierdlem88  37626  fourierdlem89  37627  fourierdlem90  37628  fourierdlem91  37629  fourierdlem92  37630  fourierdlem93  37631  fourierdlem94  37632  fourierdlem95  37633  fourierdlem97  37635  fourierdlem101  37639  fourierdlem103  37641  fourierdlem104  37642  fourierdlem111  37649  fourierdlem112  37650  fourierdlem113  37651  sqwvfoura  37660  sqwvfourb  37661  fouriersw  37663  omeiunltfirp  37849  carageniuncllem2  37852  perfectALTVlem2  38234  evengpoap3  38284  nnsum4primesevenALTV  38286  bgoldbtbndlem2  38291  zm1nn  38398  dignn0flhalflem1  39187
  Copyright terms: Public domain W3C validator