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

Theorem remulcld 9080
Description: Closure law for multiplication 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
remulcld  |-  ( ph  ->  ( A  x.  B
)  e.  RR )

Proof of Theorem remulcld
StepHypRef Expression
1 recnd.1 . 2  |-  ( ph  ->  A  e.  RR )
2 readdcld.2 . 2  |-  ( ph  ->  B  e.  RR )
3 remulcl 9039 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B
)  e.  RR )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ( A  x.  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721  (class class class)co 6048   RRcr 8953    x. cmul 8959
This theorem is referenced by:  mulge0  9509  msqge0  9513  redivcl  9697  prodgt0  9819  prodge0  9821  ltmul1a  9823  ltmul1  9824  ltmuldiv  9844  lt2msq1  9857  lt2msq  9858  le2msq  9874  msq11  9875  supmul1  9937  supmullem2  9939  supmul  9940  qbtwnre  10749  xmulneg1  10812  xmulf  10815  lincmb01cmp  11002  iccf1o  11003  flmulnn0  11192  flhalf  11194  modcl  11216  mod0  11218  modge0  11220  modmulnn  11228  moddi  11247  modsubdir  11248  modirr  11249  bernneq  11468  bernneq3  11470  expnbnd  11471  expmulnbnd  11474  discr1  11478  discr  11479  faclbnd  11544  faclbnd6  11553  remullem  11896  sqrlem7  12017  sqrmul  12028  abstri  12097  sqreulem  12126  mulcn2  12352  reccn2  12353  o1rlimmul  12375  lo1mul  12384  iseraltlem2  12439  iseraltlem3  12440  iseralt  12441  o1fsum  12555  cvgcmpce  12560  climcndslem1  12592  climcndslem2  12593  climcnds  12594  geomulcvg  12616  cvgrat  12623  mertenslem1  12624  eftlub  12673  sin02gt0  12756  eirrlem  12766  bitsp1o  12908  isprm5  13075  prmreclem3  13249  prmreclem4  13250  prmreclem5  13251  2expltfac  13389  metss2lem  18502  nlmvscnlem2  18682  nrginvrcnlem  18687  nmoco  18732  nmotri  18734  nghmcn  18740  icopnfhmeo  18929  nmoleub2lem3  19084  ipcau2  19152  tchcphlem1  19153  ipcnlem2  19159  pjthlem1  19299  opnmbllem  19454  vitalilem4  19464  itg1val2  19537  itg1cl  19538  itg1ge0  19539  itg1addlem4  19552  itg1mulc  19557  itg1ge0a  19564  itg1climres  19567  mbfi1fseqlem1  19568  mbfi1fseqlem3  19570  mbfi1fseqlem4  19571  mbfi1fseqlem5  19572  mbfi1fseqlem6  19573  itg2const2  19594  itg2mulclem  19599  itg2mulc  19600  itg2monolem1  19603  itg2monolem3  19605  itg2cnlem2  19615  iblconst  19670  iblmulc2  19683  itgmulc2lem1  19684  itgmulc2lem2  19685  bddmulibl  19691  dveflem  19824  cmvth  19836  dvlip  19838  dvlipcn  19839  dvivthlem1  19853  lhop1lem  19858  dvcvx  19865  dvfsumlem2  19872  dvfsumlem3  19873  dvfsumlem4  19874  dvfsum2  19879  ftc1lem4  19884  plyeq0lem  20090  aalioulem3  20212  aalioulem4  20213  aaliou3lem9  20228  ulmdvlem1  20277  itgulm  20285  radcnvlem1  20290  radcnvlem2  20291  dvradcnv  20298  abelthlem2  20309  abelthlem7  20315  tangtx  20374  tanregt0  20402  logdivlti  20476  logcnlem3  20496  logcnlem4  20497  logccv  20515  recxpcl  20527  cxpmul  20540  cxplt  20546  cxple2  20549  abscxpbnd  20598  lawcoslem1  20618  atans2  20732  efrlim  20769  o1cxp  20774  scvxcvx  20785  jensenlem2  20787  amgmlem  20789  fsumharmonic  20811  ftalem1  20816  ftalem2  20817  ftalem5  20820  basellem3  20826  basellem8  20831  chpub  20965  logfacubnd  20966  logfaclbnd  20967  logfacbnd3  20968  logexprlim  20970  perfectlem2  20975  bclbnd  21025  efexple  21026  bposlem1  21029  bposlem2  21030  bposlem6  21034  bposlem9  21037  lgsdilem  21067  lgseisenlem4  21097  lgseisen  21098  lgsquadlem1  21099  lgsquadlem2  21100  chebbnd1lem1  21124  chebbnd1lem3  21126  chtppilimlem1  21128  chpchtlim  21134  vmadivsum  21137  rplogsumlem1  21139  rpvmasumlem  21142  dchrisumlem2  21145  dchrisumlem3  21146  dchrmusum2  21149  dchrvmasumlem2  21153  dchrvmasumiflem1  21156  dchrisum0re  21168  dchrisum0lem1  21171  dirith2  21183  mulogsumlem  21186  mulogsum  21187  mulog2sumlem2  21190  vmalogdivsum2  21193  vmalogdivsum  21194  2vmadivsumlem  21195  logsqvma  21197  logsqvma2  21198  log2sumbnd  21199  selberglem2  21201  selberg  21203  selbergb  21204  selberg2lem  21205  selberg2b  21207  chpdifbndlem1  21208  chpdifbndlem2  21209  selberg3lem1  21212  selberg3lem2  21213  selberg3  21214  selberg4lem1  21215  selberg4  21216  pntrsumbnd2  21222  selberg3r  21224  selberg4r  21225  selberg34r  21226  pntsf  21228  pntsval2  21231  pntrlog2bndlem1  21232  pntrlog2bndlem2  21233  pntrlog2bndlem3  21234  pntrlog2bndlem4  21235  pntrlog2bndlem5  21236  pntrlog2bndlem6  21238  pntrlog2bnd  21239  pntpbnd1a  21240  pntpbnd1  21241  pntpbnd2  21242  pntibndlem2a  21245  pntibndlem2  21246  pntlemb  21252  pntlemr  21257  pntlemj  21258  pntlemf  21260  pntlemk  21261  pntlemo  21262  pntlem3  21264  ostth2lem1  21273  ostth2lem2  21289  ostth2lem3  21290  ostth2lem4  21291  ostth3  21293  smcnlem  22154  ubthlem2  22334  htthlem  22381  pjhthlem1  22854  cnlnadjlem7  23537  nmopcoadji  23565  branmfn  23569  leopnmid  23602  rmulccn  24275  xrge0iifhom  24284  dya2icoseg  24588  lgamgulmlem2  24775  lgamgulmlem3  24776  lgamgulmlem4  24777  lgamgulmlem5  24778  lgamgulmlem6  24779  relgamcl  24807  rescon  24894  brbtwn2  25756  colinearalglem4  25760  axsegconlem8  25775  axsegconlem9  25776  axsegconlem10  25777  ax5seglem3  25782  axpaschlem  25791  axpasch  25792  axeuclidlem  25813  mblfinlem  26151  itg2addnclem2  26164  itg2addnclem3  26165  iblmulc2nc  26177  itgmulc2nclem1  26178  bddiblnc  26182  ftc1cnnclem  26185  areacirclem5  26193  csbrn  26354  trirn  26355  geomcau  26363  equivbnd  26397  bfplem1  26429  bfplem2  26430  bfp  26431  rrnequiv  26442  rrntotbnd  26443  irrapxlem1  26783  irrapxlem2  26784  irrapxlem3  26785  irrapxlem4  26786  irrapxlem5  26787  pellexlem2  26791  pellexlem6  26795  pell14qrgt0  26820  pell1qrge1  26831  pell1qrgaplem  26834  pellqrexplicit  26838  pellqrex  26840  rmxycomplete  26878  rmxypos  26910  ltrmynn0  26911  ltrmxnn0  26912  jm2.24nn  26922  jm2.17a  26923  jm2.17b  26924  jm2.17c  26925  jm2.27c  26976  jm3.1lem2  26987  fmul01  27585  fmuldfeqlem1  27587  fmul01lt1lem1  27589  stoweidlem1  27625  stoweidlem11  27635  stoweidlem13  27637  stoweidlem14  27638  stoweidlem16  27640  stoweidlem17  27641  stoweidlem22  27646  stoweidlem24  27648  stoweidlem25  27649  stoweidlem26  27650  stoweidlem30  27654  stoweidlem34  27658  stoweidlem36  27660  stoweidlem49  27673  stoweidlem59  27683  stoweidlem60  27684  wallispilem4  27692  wallispilem5  27693  wallispi  27694  wallispi2lem1  27695  wallispi2  27697  stirlinglem1  27698  stirlinglem3  27700  stirlinglem5  27702  stirlinglem6  27703  stirlinglem7  27704  stirlinglem10  27707  stirlinglem11  27708  stirlinglem12  27709  stirlinglem15  27712  stirlingr  27714
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulrcl 9017
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator