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

Theorem remulcld 9072
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 9031 . 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 6040   RRcr 8945    x. cmul 8951
This theorem is referenced by:  mulge0  9501  msqge0  9505  redivcl  9689  prodgt0  9811  prodge0  9813  ltmul1a  9815  ltmul1  9816  ltmuldiv  9836  lt2msq1  9849  lt2msq  9850  le2msq  9866  msq11  9867  supmul1  9929  supmullem2  9931  supmul  9932  qbtwnre  10741  xmulneg1  10804  xmulf  10807  lincmb01cmp  10994  iccf1o  10995  flmulnn0  11184  flhalf  11186  modcl  11208  mod0  11210  modge0  11212  modmulnn  11220  moddi  11239  modsubdir  11240  modirr  11241  bernneq  11460  bernneq3  11462  expnbnd  11463  expmulnbnd  11466  discr1  11470  discr  11471  faclbnd  11536  faclbnd6  11545  remullem  11888  sqrlem7  12009  sqrmul  12020  abstri  12089  sqreulem  12118  mulcn2  12344  reccn2  12345  o1rlimmul  12367  lo1mul  12376  iseraltlem2  12431  iseraltlem3  12432  iseralt  12433  o1fsum  12547  cvgcmpce  12552  climcndslem1  12584  climcndslem2  12585  climcnds  12586  geomulcvg  12608  cvgrat  12615  mertenslem1  12616  eftlub  12665  sin02gt0  12748  eirrlem  12758  bitsp1o  12900  isprm5  13067  prmreclem3  13241  prmreclem4  13242  prmreclem5  13243  2expltfac  13381  metss2lem  18494  nlmvscnlem2  18674  nrginvrcnlem  18679  nmoco  18724  nmotri  18726  nghmcn  18732  icopnfhmeo  18921  nmoleub2lem3  19076  ipcau2  19144  tchcphlem1  19145  ipcnlem2  19151  pjthlem1  19291  opnmbllem  19446  vitalilem4  19456  itg1val2  19529  itg1cl  19530  itg1ge0  19531  itg1addlem4  19544  itg1mulc  19549  itg1ge0a  19556  itg1climres  19559  mbfi1fseqlem1  19560  mbfi1fseqlem3  19562  mbfi1fseqlem4  19563  mbfi1fseqlem5  19564  mbfi1fseqlem6  19565  itg2const2  19586  itg2mulclem  19591  itg2mulc  19592  itg2monolem1  19595  itg2monolem3  19597  itg2cnlem2  19607  iblconst  19662  iblmulc2  19675  itgmulc2lem1  19676  itgmulc2lem2  19677  bddmulibl  19683  dveflem  19816  cmvth  19828  dvlip  19830  dvlipcn  19831  dvivthlem1  19845  lhop1lem  19850  dvcvx  19857  dvfsumlem2  19864  dvfsumlem3  19865  dvfsumlem4  19866  dvfsum2  19871  ftc1lem4  19876  plyeq0lem  20082  aalioulem3  20204  aalioulem4  20205  aaliou3lem9  20220  ulmdvlem1  20269  itgulm  20277  radcnvlem1  20282  radcnvlem2  20283  dvradcnv  20290  abelthlem2  20301  abelthlem7  20307  tangtx  20366  tanregt0  20394  logdivlti  20468  logcnlem3  20488  logcnlem4  20489  logccv  20507  recxpcl  20519  cxpmul  20532  cxplt  20538  cxple2  20541  abscxpbnd  20590  lawcoslem1  20610  atans2  20724  efrlim  20761  o1cxp  20766  scvxcvx  20777  jensenlem2  20779  amgmlem  20781  fsumharmonic  20803  ftalem1  20808  ftalem2  20809  ftalem5  20812  basellem3  20818  basellem8  20823  chpub  20957  logfacubnd  20958  logfaclbnd  20959  logfacbnd3  20960  logexprlim  20962  perfectlem2  20967  bclbnd  21017  efexple  21018  bposlem1  21021  bposlem2  21022  bposlem6  21026  bposlem9  21029  lgsdilem  21059  lgseisenlem4  21089  lgseisen  21090  lgsquadlem1  21091  lgsquadlem2  21092  chebbnd1lem1  21116  chebbnd1lem3  21118  chtppilimlem1  21120  chpchtlim  21126  vmadivsum  21129  rplogsumlem1  21131  rpvmasumlem  21134  dchrisumlem2  21137  dchrisumlem3  21138  dchrmusum2  21141  dchrvmasumlem2  21145  dchrvmasumiflem1  21148  dchrisum0re  21160  dchrisum0lem1  21163  dirith2  21175  mulogsumlem  21178  mulogsum  21179  mulog2sumlem2  21182  vmalogdivsum2  21185  vmalogdivsum  21186  2vmadivsumlem  21187  logsqvma  21189  logsqvma2  21190  log2sumbnd  21191  selberglem2  21193  selberg  21195  selbergb  21196  selberg2lem  21197  selberg2b  21199  chpdifbndlem1  21200  chpdifbndlem2  21201  selberg3lem1  21204  selberg3lem2  21205  selberg3  21206  selberg4lem1  21207  selberg4  21208  pntrsumbnd2  21214  selberg3r  21216  selberg4r  21217  selberg34r  21218  pntsf  21220  pntsval2  21223  pntrlog2bndlem1  21224  pntrlog2bndlem2  21225  pntrlog2bndlem3  21226  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  pntrlog2bndlem6  21230  pntrlog2bnd  21231  pntpbnd1a  21232  pntpbnd1  21233  pntpbnd2  21234  pntibndlem2a  21237  pntibndlem2  21238  pntlemb  21244  pntlemr  21249  pntlemj  21250  pntlemf  21252  pntlemk  21253  pntlemo  21254  pntlem3  21256  ostth2lem1  21265  ostth2lem2  21281  ostth2lem3  21282  ostth2lem4  21283  ostth3  21285  smcnlem  22146  ubthlem2  22326  htthlem  22373  pjhthlem1  22846  cnlnadjlem7  23529  nmopcoadji  23557  branmfn  23561  leopnmid  23594  rmulccn  24267  xrge0iifhom  24276  dya2icoseg  24580  lgamgulmlem2  24767  lgamgulmlem3  24768  lgamgulmlem4  24769  lgamgulmlem5  24770  lgamgulmlem6  24771  relgamcl  24799  rescon  24886  brbtwn2  25748  colinearalglem4  25752  axsegconlem8  25767  axsegconlem9  25768  axsegconlem10  25769  ax5seglem3  25774  axpaschlem  25783  axpasch  25784  axeuclidlem  25805  mblfinlem  26143  itg2addnclem2  26156  itg2addnclem3  26157  iblmulc2nc  26169  itgmulc2nclem1  26170  bddiblnc  26174  ftc1cnnclem  26177  areacirclem5  26185  csbrn  26346  trirn  26347  geomcau  26355  equivbnd  26389  bfplem1  26421  bfplem2  26422  bfp  26423  rrnequiv  26434  rrntotbnd  26435  irrapxlem1  26775  irrapxlem2  26776  irrapxlem3  26777  irrapxlem4  26778  irrapxlem5  26779  pellexlem2  26783  pellexlem6  26787  pell14qrgt0  26812  pell1qrge1  26823  pell1qrgaplem  26826  pellqrexplicit  26830  pellqrex  26832  rmxycomplete  26870  rmxypos  26902  ltrmynn0  26903  ltrmxnn0  26904  jm2.24nn  26914  jm2.17a  26915  jm2.17b  26916  jm2.17c  26917  jm2.27c  26968  jm3.1lem2  26979  fmul01  27577  fmuldfeqlem1  27579  fmul01lt1lem1  27581  stoweidlem1  27617  stoweidlem11  27627  stoweidlem13  27629  stoweidlem14  27630  stoweidlem16  27632  stoweidlem17  27633  stoweidlem22  27638  stoweidlem24  27640  stoweidlem25  27641  stoweidlem26  27642  stoweidlem30  27646  stoweidlem34  27650  stoweidlem36  27652  stoweidlem49  27665  stoweidlem59  27675  stoweidlem60  27676  wallispilem4  27684  wallispilem5  27685  wallispi  27686  wallispi2lem1  27687  wallispi2  27689  stirlinglem1  27690  stirlinglem3  27692  stirlinglem5  27694  stirlinglem6  27695  stirlinglem7  27696  stirlinglem10  27699  stirlinglem11  27700  stirlinglem12  27701  stirlinglem15  27704  stirlingr  27706
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulrcl 9009
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator