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

Theorem remulcld 10660
Description: Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
recnd.1 (𝜑𝐴 ∈ ℝ)
readdcld.2 (𝜑𝐵 ∈ ℝ)
Assertion
Ref Expression
remulcld (𝜑 → (𝐴 · 𝐵) ∈ ℝ)

Proof of Theorem remulcld
StepHypRef Expression
1 recnd.1 . 2 (𝜑𝐴 ∈ ℝ)
2 readdcld.2 . 2 (𝜑𝐵 ∈ ℝ)
3 remulcl 10611 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
41, 2, 3syl2anc 587 1 (𝜑 → (𝐴 · 𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2111  (class class class)co 7135  cr 10525   · cmul 10531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 10589
This theorem depends on definitions:  df-bi 210  df-an 400
This theorem is referenced by:  mulge0  11147  msqge0  11150  redivcl  11348  prodgt0  11476  ltmul1a  11478  ltmul1  11479  ltmuldiv  11502  lt2msq1  11513  lt2msq  11514  le2msq  11529  msq11  11530  supmul1  11597  supmullem2  11599  supmul  11600  div4p1lem1div2  11880  mul2lt0rlt0  12479  mul2lt0bi  12483  prodge0rd  12484  qbtwnre  12580  xmulneg1  12650  xmulf  12653  lincmb01cmp  12873  iccf1o  12874  flmulnn0  13192  flhalf  13195  modcl  13236  mod0  13239  modge0  13242  modmulnn  13252  mulp1mod1  13275  2txmodxeq0  13294  modaddmulmod  13301  moddi  13302  modsubdir  13303  modirr  13305  addmodlteq  13309  bernneq  13586  bernneq3  13588  expnbnd  13589  expmulnbnd  13592  discr1  13596  discr  13597  faclbnd  13646  faclbnd6  13655  remullem  14479  sqrlem7  14600  sqrtmul  14611  abstri  14682  sqreulem  14711  bhmafibid1  14817  mulcn2  14944  reccn2  14945  o1rlimmul  14967  lo1mul  14976  iseraltlem2  15031  iseraltlem3  15032  iseralt  15033  o1fsum  15160  cvgcmpce  15165  climcndslem1  15196  climcndslem2  15197  climcnds  15198  geomulcvg  15224  cvgrat  15231  mertenslem1  15232  fprodge1  15341  eftlub  15454  sin02gt0  15537  eirrlem  15549  bitsp1o  15772  2mulprm  16027  isprm5  16041  modprm0  16132  prmreclem3  16244  prmreclem4  16245  prmreclem5  16246  2expltfac  16418  metss2lem  23118  nlmvscnlem2  23291  nrginvrcnlem  23297  nmoco  23343  nmotri  23345  nghmcn  23351  icopnfhmeo  23548  nmoleub2lem3  23720  ipcau2  23838  tcphcphlem1  23839  ipcnlem2  23848  rrxcph  23996  csbren  24003  trirn  24004  pjthlem1  24041  opnmbllem  24205  vitalilem4  24215  itg1val2  24288  itg1cl  24289  itg1ge0  24290  itg1addlem4  24303  itg1mulc  24308  itg1ge0a  24315  itg1climres  24318  mbfi1fseqlem1  24319  mbfi1fseqlem3  24321  mbfi1fseqlem4  24322  mbfi1fseqlem5  24323  mbfi1fseqlem6  24324  itg2const2  24345  itg2mulclem  24350  itg2mulc  24351  itg2monolem1  24354  itg2monolem3  24356  itg2cnlem2  24366  iblconst  24421  iblmulc2  24434  itgmulc2lem1  24435  itgmulc2lem2  24436  bddmulibl  24442  bddiblnc  24445  dveflem  24582  cmvth  24594  dvlip  24596  dvlipcn  24597  dvivthlem1  24611  lhop1lem  24616  dvcvx  24623  dvfsumlem2  24630  dvfsumlem3  24631  dvfsumlem4  24632  dvfsum2  24637  ftc1lem4  24642  plyeq0lem  24807  aalioulem3  24930  aalioulem4  24931  aaliou3lem9  24946  ulmdvlem1  24995  itgulm  25003  radcnvlem1  25008  radcnvlem2  25009  dvradcnv  25016  abelthlem2  25027  abelthlem7  25033  tangtx  25098  tanregt0  25131  logdivlti  25211  logcnlem3  25235  logcnlem4  25236  logccv  25254  recxpcl  25266  cxpmul  25279  cxplt  25285  cxple2  25288  abscxpbnd  25342  lawcoslem1  25401  heron  25424  atans2  25517  efrlim  25555  o1cxp  25560  scvxcvx  25571  jensenlem2  25573  amgmlem  25575  fsumharmonic  25597  lgamgulmlem2  25615  lgamgulmlem3  25616  lgamgulmlem4  25617  lgamgulmlem5  25618  lgamgulmlem6  25619  relgamcl  25647  ftalem1  25658  ftalem2  25659  ftalem5  25662  basellem3  25668  basellem8  25673  chpub  25804  logfacubnd  25805  logfaclbnd  25806  logfacbnd3  25807  logexprlim  25809  perfectlem2  25814  bclbnd  25864  efexple  25865  bposlem1  25868  bposlem2  25869  bposlem6  25873  bposlem9  25876  lgsdilem  25908  gausslemma2dlem0c  25942  gausslemma2dlem2  25951  gausslemma2dlem3  25952  gausslemma2dlem6  25956  lgseisenlem4  25962  lgseisen  25963  lgsquadlem1  25964  lgsquadlem2  25965  2lgslem1a1  25973  2sqmod  26020  chebbnd1lem1  26053  chebbnd1lem3  26055  chtppilimlem1  26057  chpchtlim  26063  vmadivsum  26066  rplogsumlem1  26068  rpvmasumlem  26071  dchrisumlem2  26074  dchrisumlem3  26075  dchrmusum2  26078  dchrvmasumlem2  26082  dchrvmasumiflem1  26085  dchrisum0re  26097  dchrisum0lem1  26100  dirith2  26112  mulogsumlem  26115  mulogsum  26116  mulog2sumlem2  26119  vmalogdivsum2  26122  vmalogdivsum  26123  2vmadivsumlem  26124  logsqvma  26126  logsqvma2  26127  log2sumbnd  26128  selberglem2  26130  selberg  26132  selbergb  26133  selberg2lem  26134  selberg2b  26136  chpdifbndlem1  26137  chpdifbndlem2  26138  selberg3lem1  26141  selberg3lem2  26142  selberg3  26143  selberg4lem1  26144  selberg4  26145  pntrsumbnd2  26151  selberg3r  26153  selberg4r  26154  selberg34r  26155  pntsf  26157  pntsval2  26160  pntrlog2bndlem1  26161  pntrlog2bndlem2  26162  pntrlog2bndlem3  26163  pntrlog2bndlem4  26164  pntrlog2bndlem5  26165  pntrlog2bndlem6  26167  pntrlog2bnd  26168  pntpbnd1a  26169  pntpbnd1  26170  pntpbnd2  26171  pntibndlem2a  26174  pntibndlem2  26175  pntlemb  26181  pntlemr  26186  pntlemj  26187  pntlemf  26189  pntlemk  26190  pntlemo  26191  pntlem3  26193  ostth2lem1  26202  ostth2lem2  26218  ostth2lem3  26219  ostth2lem4  26220  ostth3  26222  ttgcontlem1  26679  brbtwn2  26699  colinearalglem4  26703  axsegconlem8  26718  axsegconlem9  26719  axsegconlem10  26720  ax5seglem3  26725  axpaschlem  26734  axpasch  26735  axeuclidlem  26756  numclwwlk5  28173  numclwwlk7  28176  smcnlem  28480  ubthlem2  28654  htthlem  28700  pjhthlem1  29174  cnlnadjlem7  29856  nmopcoadji  29884  branmfn  29888  leopnmid  29921  rmulccn  31281  xrge0iifhom  31290  nexple  31378  dya2icoseg  31645  eulerpartlems  31728  eulerpartlemgc  31730  eulerpartlemb  31736  plymulx0  31927  signsvtp  31963  reprgt  32002  breprexplemc  32013  circlemethhgt  32024  hgt750lemd  32029  logdivsqrle  32031  hgt750lem  32032  hgt750lemf  32034  hgt750lemb  32037  hgt750lema  32038  hgt750leme  32039  tgoldbachgtde  32041  resconn  32603  knoppcnlem2  33943  knoppcnlem4  33945  knoppcnlem10  33951  unbdqndv2lem1  33958  unbdqndv2lem2  33959  knoppndvlem1  33961  knoppndvlem11  33971  knoppndvlem12  33972  knoppndvlem14  33974  knoppndvlem15  33975  knoppndvlem17  33977  knoppndvlem18  33978  knoppndvlem19  33979  knoppndvlem20  33980  knoppndvlem21  33981  opnmbllem0  35090  itg2addnclem2  35106  itg2addnclem3  35107  iblmulc2nc  35119  itgmulc2nclem1  35120  ftc1cnnclem  35125  ftc1anclem3  35129  areacirclem4  35145  geomcau  35194  equivbnd  35225  bfplem1  35257  bfplem2  35258  bfp  35259  rrnequiv  35270  rrntotbnd  35271  lcmineqlem19  39332  lcmineqlem20  39333  lcmineqlem21  39334  lcmineqlem22  39335  3lexlogpow5ineq2  39339  2np3bcnp1  39343  2ap1caineq  39344  cxpgt0d  39483  resubdi  39529  remul02  39538  remul01  39540  remulinvcom  39564  sn-0tie0  39571  mulgt0con1d  39578  mulgt0con2d  39579  mulgt0b2d  39580  sn-ltmul2d  39581  sn-inelr  39585  itrere  39586  retire  39587  fltnltalem  39613  fltnlta  39614  3cubeslem2  39621  3cubeslem3r  39623  3cubeslem4  39625  irrapxlem1  39758  irrapxlem2  39759  irrapxlem3  39760  irrapxlem4  39761  irrapxlem5  39762  pellexlem2  39766  pellexlem6  39770  pell14qrgt0  39795  pell1qrge1  39806  pell1qrgaplem  39809  pellqrexplicit  39813  pellqrex  39815  rmspecsqrtnq  39842  rmxycomplete  39853  rmxypos  39883  ltrmynn0  39884  ltrmxnn0  39885  jm2.24nn  39895  jm2.17a  39896  jm2.17b  39897  jm2.17c  39898  jm2.27c  39943  jm3.1lem2  39954  areaquad  40161  sqrtcval  40336  resqrtval  40338  imsqrtval  40339  imo72b2lem0  40864  cvgdvgrat  41012  nzprmdif  41018  lt3addmuld  41928  fperiodmullem  41930  fperiodmul  41931  lt4addmuld  41933  xralrple2  41981  xralrple3  42001  ltmulneg  42023  fmul01  42217  fmuldfeqlem1  42219  fmul01lt1lem1  42221  sumnnodd  42267  ltmod  42275  0ellimcdiv  42286  limclner  42288  dvdivbd  42560  dvbdfbdioolem2  42566  dvbdfbdioo  42567  ioodvbdlimc1lem1  42568  ioodvbdlimc1lem2  42569  ioodvbdlimc2lem  42571  stoweidlem1  42638  stoweidlem11  42648  stoweidlem13  42650  stoweidlem14  42651  stoweidlem16  42653  stoweidlem17  42654  stoweidlem22  42659  stoweidlem24  42661  stoweidlem25  42662  stoweidlem26  42663  stoweidlem30  42667  stoweidlem34  42671  stoweidlem36  42673  stoweidlem49  42686  stoweidlem59  42696  stoweidlem60  42697  wallispilem4  42705  wallispilem5  42706  wallispi  42707  wallispi2lem1  42708  wallispi2  42710  stirlinglem1  42711  stirlinglem3  42713  stirlinglem5  42715  stirlinglem6  42716  stirlinglem7  42717  stirlinglem10  42720  stirlinglem11  42721  stirlinglem12  42722  stirlinglem15  42725  stirlingr  42727  dirker2re  42729  dirkerval2  42731  dirkerre  42732  dirkertrigeqlem1  42735  dirkertrigeqlem2  42736  dirkeritg  42739  dirkercncflem2  42741  dirkercncflem4  42743  fourierdlem4  42748  fourierdlem5  42749  fourierdlem6  42750  fourierdlem7  42751  fourierdlem16  42760  fourierdlem18  42762  fourierdlem19  42763  fourierdlem21  42765  fourierdlem22  42766  fourierdlem26  42770  fourierdlem35  42779  fourierdlem39  42783  fourierdlem41  42785  fourierdlem42  42786  fourierdlem43  42787  fourierdlem48  42791  fourierdlem49  42792  fourierdlem51  42794  fourierdlem55  42798  fourierdlem56  42799  fourierdlem57  42800  fourierdlem58  42801  fourierdlem62  42805  fourierdlem63  42806  fourierdlem64  42807  fourierdlem65  42808  fourierdlem66  42809  fourierdlem67  42810  fourierdlem68  42811  fourierdlem71  42814  fourierdlem72  42815  fourierdlem73  42816  fourierdlem76  42819  fourierdlem77  42820  fourierdlem78  42821  fourierdlem83  42826  fourierdlem84  42827  fourierdlem87  42830  fourierdlem88  42831  fourierdlem89  42832  fourierdlem90  42833  fourierdlem91  42834  fourierdlem94  42837  fourierdlem95  42838  fourierdlem97  42840  fourierdlem103  42846  fourierdlem104  42847  fourierdlem112  42855  fourierdlem113  42856  sqwvfoura  42865  sqwvfourb  42866  fouriersw  42868  etransclem23  42894  etransclem48  42919  rrndistlt  42927  hoidmvlelem1  43229  hoidmvlelem2  43230  hoidmvlelem4  43232  smfmullem1  43418  smfmullem2  43419  smfmullem3  43420  smfmul  43422  fmtno4prmfac  44084  lighneallem4a  44121  requad01  44134  requad1  44135  requad2  44136  perfectALTVlem2  44235  ply1mulgsumlem2  44790  digvalnn0  45008  dignn0fr  45010  dig2nn0  45020  affinecomb1  45111  rrx2linest2  45153  line2  45161  itsclc0lem1  45165  itsclc0lem2  45166  itsclc0lem3  45167  itscnhlc0yqe  45168  itsclc0yqsollem2  45172  itsclc0yqsol  45173  itscnhlc0xyqsol  45174  itsclc0xyqsolr  45178  itsclinecirc0  45182  itsclinecirc0b  45183  itsclinecirc0in  45184  itsclquadb  45185  itsclquadeu  45186  2itscp  45190  itscnhlinecirc02plem1  45191  itscnhlinecirc02p  45194  inlinecirc02plem  45195  amgmwlem  45325
  Copyright terms: Public domain W3C validator