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

Theorem remulcld 9116
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 9075 . 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 1725  (class class class)co 6081   RRcr 8989    x. cmul 8995
This theorem is referenced by:  mulge0  9545  msqge0  9549  redivcl  9733  prodgt0  9855  prodge0  9857  ltmul1a  9859  ltmul1  9860  ltmuldiv  9880  lt2msq1  9893  lt2msq  9894  le2msq  9910  msq11  9911  supmul1  9973  supmullem2  9975  supmul  9976  qbtwnre  10785  xmulneg1  10848  xmulf  10851  lincmb01cmp  11038  iccf1o  11039  flmulnn0  11229  flhalf  11231  modcl  11253  mod0  11255  modge0  11257  modmulnn  11265  moddi  11284  modsubdir  11285  modirr  11286  bernneq  11505  bernneq3  11507  expnbnd  11508  expmulnbnd  11511  discr1  11515  discr  11516  faclbnd  11581  faclbnd6  11590  remullem  11933  sqrlem7  12054  sqrmul  12065  abstri  12134  sqreulem  12163  mulcn2  12389  reccn2  12390  o1rlimmul  12412  lo1mul  12421  iseraltlem2  12476  iseraltlem3  12477  iseralt  12478  o1fsum  12592  cvgcmpce  12597  climcndslem1  12629  climcndslem2  12630  climcnds  12631  geomulcvg  12653  cvgrat  12660  mertenslem1  12661  eftlub  12710  sin02gt0  12793  eirrlem  12803  bitsp1o  12945  isprm5  13112  prmreclem3  13286  prmreclem4  13287  prmreclem5  13288  2expltfac  13426  metss2lem  18541  nlmvscnlem2  18721  nrginvrcnlem  18726  nmoco  18771  nmotri  18773  nghmcn  18779  icopnfhmeo  18968  nmoleub2lem3  19123  ipcau2  19191  tchcphlem1  19192  ipcnlem2  19198  pjthlem1  19338  opnmbllem  19493  vitalilem4  19503  itg1val2  19576  itg1cl  19577  itg1ge0  19578  itg1addlem4  19591  itg1mulc  19596  itg1ge0a  19603  itg1climres  19606  mbfi1fseqlem1  19607  mbfi1fseqlem3  19609  mbfi1fseqlem4  19610  mbfi1fseqlem5  19611  mbfi1fseqlem6  19612  itg2const2  19633  itg2mulclem  19638  itg2mulc  19639  itg2monolem1  19642  itg2monolem3  19644  itg2cnlem2  19654  iblconst  19709  iblmulc2  19722  itgmulc2lem1  19723  itgmulc2lem2  19724  bddmulibl  19730  dveflem  19863  cmvth  19875  dvlip  19877  dvlipcn  19878  dvivthlem1  19892  lhop1lem  19897  dvcvx  19904  dvfsumlem2  19911  dvfsumlem3  19912  dvfsumlem4  19913  dvfsum2  19918  ftc1lem4  19923  plyeq0lem  20129  aalioulem3  20251  aalioulem4  20252  aaliou3lem9  20267  ulmdvlem1  20316  itgulm  20324  radcnvlem1  20329  radcnvlem2  20330  dvradcnv  20337  abelthlem2  20348  abelthlem7  20354  tangtx  20413  tanregt0  20441  logdivlti  20515  logcnlem3  20535  logcnlem4  20536  logccv  20554  recxpcl  20566  cxpmul  20579  cxplt  20585  cxple2  20588  abscxpbnd  20637  lawcoslem1  20657  atans2  20771  efrlim  20808  o1cxp  20813  scvxcvx  20824  jensenlem2  20826  amgmlem  20828  fsumharmonic  20850  ftalem1  20855  ftalem2  20856  ftalem5  20859  basellem3  20865  basellem8  20870  chpub  21004  logfacubnd  21005  logfaclbnd  21006  logfacbnd3  21007  logexprlim  21009  perfectlem2  21014  bclbnd  21064  efexple  21065  bposlem1  21068  bposlem2  21069  bposlem6  21073  bposlem9  21076  lgsdilem  21106  lgseisenlem4  21136  lgseisen  21137  lgsquadlem1  21138  lgsquadlem2  21139  chebbnd1lem1  21163  chebbnd1lem3  21165  chtppilimlem1  21167  chpchtlim  21173  vmadivsum  21176  rplogsumlem1  21178  rpvmasumlem  21181  dchrisumlem2  21184  dchrisumlem3  21185  dchrmusum2  21188  dchrvmasumlem2  21192  dchrvmasumiflem1  21195  dchrisum0re  21207  dchrisum0lem1  21210  dirith2  21222  mulogsumlem  21225  mulogsum  21226  mulog2sumlem2  21229  vmalogdivsum2  21232  vmalogdivsum  21233  2vmadivsumlem  21234  logsqvma  21236  logsqvma2  21237  log2sumbnd  21238  selberglem2  21240  selberg  21242  selbergb  21243  selberg2lem  21244  selberg2b  21246  chpdifbndlem1  21247  chpdifbndlem2  21248  selberg3lem1  21251  selberg3lem2  21252  selberg3  21253  selberg4lem1  21254  selberg4  21255  pntrsumbnd2  21261  selberg3r  21263  selberg4r  21264  selberg34r  21265  pntsf  21267  pntsval2  21270  pntrlog2bndlem1  21271  pntrlog2bndlem2  21272  pntrlog2bndlem3  21273  pntrlog2bndlem4  21274  pntrlog2bndlem5  21275  pntrlog2bndlem6  21277  pntrlog2bnd  21278  pntpbnd1a  21279  pntpbnd1  21280  pntpbnd2  21281  pntibndlem2a  21284  pntibndlem2  21285  pntlemb  21291  pntlemr  21296  pntlemj  21297  pntlemf  21299  pntlemk  21300  pntlemo  21301  pntlem3  21303  ostth2lem1  21312  ostth2lem2  21328  ostth2lem3  21329  ostth2lem4  21330  ostth3  21332  smcnlem  22193  ubthlem2  22373  htthlem  22420  pjhthlem1  22893  cnlnadjlem7  23576  nmopcoadji  23604  branmfn  23608  leopnmid  23641  rmulccn  24314  xrge0iifhom  24323  dya2icoseg  24627  lgamgulmlem2  24814  lgamgulmlem3  24815  lgamgulmlem4  24816  lgamgulmlem5  24817  lgamgulmlem6  24818  relgamcl  24846  rescon  24933  brbtwn2  25844  colinearalglem4  25848  axsegconlem8  25863  axsegconlem9  25864  axsegconlem10  25865  ax5seglem3  25870  axpaschlem  25879  axpasch  25880  axeuclidlem  25901  opnmbllem0  26242  itg2addnclem2  26257  itg2addnclem3  26258  iblmulc2nc  26270  itgmulc2nclem1  26271  bddiblnc  26275  ftc1cnnclem  26278  ftc1anclem3  26282  areacirclem4  26295  csbrn  26456  trirn  26457  geomcau  26465  equivbnd  26499  bfplem1  26531  bfplem2  26532  bfp  26533  rrnequiv  26544  rrntotbnd  26545  irrapxlem1  26885  irrapxlem2  26886  irrapxlem3  26887  irrapxlem4  26888  irrapxlem5  26889  pellexlem2  26893  pellexlem6  26897  pell14qrgt0  26922  pell1qrge1  26933  pell1qrgaplem  26936  pellqrexplicit  26940  pellqrex  26942  rmxycomplete  26980  rmxypos  27012  ltrmynn0  27013  ltrmxnn0  27014  jm2.24nn  27024  jm2.17a  27025  jm2.17b  27026  jm2.17c  27027  jm2.27c  27078  jm3.1lem2  27089  fmul01  27686  fmuldfeqlem1  27688  fmul01lt1lem1  27690  stoweidlem1  27726  stoweidlem11  27736  stoweidlem13  27738  stoweidlem14  27739  stoweidlem16  27741  stoweidlem17  27742  stoweidlem22  27747  stoweidlem24  27749  stoweidlem25  27750  stoweidlem26  27751  stoweidlem30  27755  stoweidlem34  27759  stoweidlem36  27761  stoweidlem49  27774  stoweidlem59  27784  stoweidlem60  27785  wallispilem4  27793  wallispilem5  27794  wallispi  27795  wallispi2lem1  27796  wallispi2  27798  stirlinglem1  27799  stirlinglem3  27801  stirlinglem5  27803  stirlinglem6  27804  stirlinglem7  27805  stirlinglem10  27808  stirlinglem11  27809  stirlinglem12  27810  stirlinglem15  27813  stirlingr  27815  modaddmulmod  28158  2txmodxeq0  28162  modprm0  28228  2cshwmod  28257
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulrcl 9053
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator