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

Theorem remulcld 10030
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 9981 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
41, 2, 3syl2anc 692 1 (𝜑 → (𝐴 · 𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  (class class class)co 6615  cr 9895   · cmul 9901
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 9959
This theorem depends on definitions:  df-bi 197  df-an 386
This theorem is referenced by:  mulge0  10506  msqge0  10509  redivcl  10704  prodgt0  10828  prodge0  10830  ltmul1a  10832  ltmul1  10833  ltmuldiv  10856  lt2msq1  10867  lt2msq  10868  le2msq  10883  msq11  10884  supmul1  10952  supmullem2  10954  supmul  10955  div4p1lem1div2  11247  mul2lt0rlt0  11892  mul2lt0bi  11896  qbtwnre  11989  xmulneg1  12058  xmulf  12061  lincmb01cmp  12273  iccf1o  12274  flmulnn0  12584  flhalf  12587  modcl  12628  mod0  12631  modge0  12634  modmulnn  12644  mulp1mod1  12667  2txmodxeq0  12686  modaddmulmod  12693  moddi  12694  modsubdir  12695  modirr  12697  addmodlteq  12701  bernneq  12946  bernneq3  12948  expnbnd  12949  expmulnbnd  12952  discr1  12956  discr  12957  faclbnd  13033  faclbnd6  13042  remullem  13818  sqrlem7  13939  sqrtmul  13950  abstri  14020  sqreulem  14049  mulcn2  14276  reccn2  14277  o1rlimmul  14299  lo1mul  14308  iseraltlem2  14363  iseraltlem3  14364  iseralt  14365  o1fsum  14491  cvgcmpce  14496  climcndslem1  14525  climcndslem2  14526  climcnds  14527  geomulcvg  14551  cvgrat  14559  mertenslem1  14560  fprodge1  14670  eftlub  14783  sin02gt0  14866  eirrlem  14876  bitsp1o  15098  isprm5  15362  modprm0  15453  prmreclem3  15565  prmreclem4  15566  prmreclem5  15567  2expltfac  15742  metss2lem  22256  nlmvscnlem2  22429  nrginvrcnlem  22435  nmoco  22481  nmotri  22483  nghmcn  22489  icopnfhmeo  22682  nmoleub2lem3  22855  ipcau2  22973  tchcphlem1  22974  ipcnlem2  22983  rrxcph  23120  csbren  23122  trirn  23123  pjthlem1  23148  opnmbllem  23309  vitalilem4  23320  itg1val2  23391  itg1cl  23392  itg1ge0  23393  itg1addlem4  23406  itg1mulc  23411  itg1ge0a  23418  itg1climres  23421  mbfi1fseqlem1  23422  mbfi1fseqlem3  23424  mbfi1fseqlem4  23425  mbfi1fseqlem5  23426  mbfi1fseqlem6  23427  itg2const2  23448  itg2mulclem  23453  itg2mulc  23454  itg2monolem1  23457  itg2monolem3  23459  itg2cnlem2  23469  iblconst  23524  iblmulc2  23537  itgmulc2lem1  23538  itgmulc2lem2  23539  bddmulibl  23545  dveflem  23680  cmvth  23692  dvlip  23694  dvlipcn  23695  dvivthlem1  23709  lhop1lem  23714  dvcvx  23721  dvfsumlem2  23728  dvfsumlem3  23729  dvfsumlem4  23730  dvfsum2  23735  ftc1lem4  23740  plyeq0lem  23904  aalioulem3  24027  aalioulem4  24028  aaliou3lem9  24043  ulmdvlem1  24092  itgulm  24100  radcnvlem1  24105  radcnvlem2  24106  dvradcnv  24113  abelthlem2  24124  abelthlem7  24130  tangtx  24195  tanregt0  24223  logdivlti  24304  logcnlem3  24324  logcnlem4  24325  logccv  24343  recxpcl  24355  cxpmul  24368  cxplt  24374  cxple2  24377  abscxpbnd  24428  lawcoslem1  24479  heron  24499  atans2  24592  efrlim  24630  o1cxp  24635  scvxcvx  24646  jensenlem2  24648  amgmlem  24650  fsumharmonic  24672  lgamgulmlem2  24690  lgamgulmlem3  24691  lgamgulmlem4  24692  lgamgulmlem5  24693  lgamgulmlem6  24694  relgamcl  24722  ftalem1  24733  ftalem2  24734  ftalem5  24737  basellem3  24743  basellem8  24748  chpub  24879  logfacubnd  24880  logfaclbnd  24881  logfacbnd3  24882  logexprlim  24884  perfectlem2  24889  bclbnd  24939  efexple  24940  bposlem1  24943  bposlem2  24944  bposlem6  24948  bposlem9  24951  lgsdilem  24983  gausslemma2dlem0c  25017  gausslemma2dlem2  25026  gausslemma2dlem3  25027  gausslemma2dlem6  25031  lgseisenlem4  25037  lgseisen  25038  lgsquadlem1  25039  lgsquadlem2  25040  2lgslem1a1  25048  chebbnd1lem1  25092  chebbnd1lem3  25094  chtppilimlem1  25096  chpchtlim  25102  vmadivsum  25105  rplogsumlem1  25107  rpvmasumlem  25110  dchrisumlem2  25113  dchrisumlem3  25114  dchrmusum2  25117  dchrvmasumlem2  25121  dchrvmasumiflem1  25124  dchrisum0re  25136  dchrisum0lem1  25139  dirith2  25151  mulogsumlem  25154  mulogsum  25155  mulog2sumlem2  25158  vmalogdivsum2  25161  vmalogdivsum  25162  2vmadivsumlem  25163  logsqvma  25165  logsqvma2  25166  log2sumbnd  25167  selberglem2  25169  selberg  25171  selbergb  25172  selberg2lem  25173  selberg2b  25175  chpdifbndlem1  25176  chpdifbndlem2  25177  selberg3lem1  25180  selberg3lem2  25181  selberg3  25182  selberg4lem1  25183  selberg4  25184  pntrsumbnd2  25190  selberg3r  25192  selberg4r  25193  selberg34r  25194  pntsf  25196  pntsval2  25199  pntrlog2bndlem1  25200  pntrlog2bndlem2  25201  pntrlog2bndlem3  25202  pntrlog2bndlem4  25203  pntrlog2bndlem5  25204  pntrlog2bndlem6  25206  pntrlog2bnd  25207  pntpbnd1a  25208  pntpbnd1  25209  pntpbnd2  25210  pntibndlem2a  25213  pntibndlem2  25214  pntlemb  25220  pntlemr  25225  pntlemj  25226  pntlemf  25228  pntlemk  25229  pntlemo  25230  pntlem3  25232  ostth2lem1  25241  ostth2lem2  25257  ostth2lem3  25258  ostth2lem4  25259  ostth3  25261  ttgcontlem1  25699  brbtwn2  25719  colinearalglem4  25723  axsegconlem8  25738  axsegconlem9  25739  axsegconlem10  25740  ax5seglem3  25745  axpaschlem  25754  axpasch  25755  axeuclidlem  25776  numclwwlk5  27134  numclwwlk7  27137  smcnlem  27440  ubthlem2  27615  htthlem  27662  pjhthlem1  28138  cnlnadjlem7  28820  nmopcoadji  28848  branmfn  28852  leopnmid  28885  bhmafibid1  29471  2sqmod  29475  rmulccn  29798  xrge0iifhom  29807  nexple  29895  dya2icoseg  30162  eulerpartlems  30245  eulerpartlemgc  30247  eulerpartlemb  30253  plymulx0  30446  signsvtp  30482  resconn  30989  knoppcnlem2  32179  knoppcnlem4  32181  knoppcnlem10  32187  unbdqndv2lem1  32195  unbdqndv2lem2  32196  knoppndvlem1  32198  knoppndvlem11  32208  knoppndvlem12  32209  knoppndvlem14  32211  knoppndvlem15  32212  knoppndvlem17  32214  knoppndvlem18  32215  knoppndvlem19  32216  knoppndvlem20  32217  knoppndvlem21  32218  opnmbllem0  33116  itg2addnclem2  33133  itg2addnclem3  33134  iblmulc2nc  33146  itgmulc2nclem1  33147  bddiblnc  33151  ftc1cnnclem  33154  ftc1anclem3  33158  areacirclem4  33174  geomcau  33226  equivbnd  33260  bfplem1  33292  bfplem2  33293  bfp  33294  rrnequiv  33305  rrntotbnd  33306  irrapxlem1  36905  irrapxlem2  36906  irrapxlem3  36907  irrapxlem4  36908  irrapxlem5  36909  pellexlem2  36913  pellexlem6  36917  pell14qrgt0  36942  pell1qrge1  36953  pell1qrgaplem  36956  pellqrexplicit  36960  pellqrex  36962  rmspecsqrtnq  36989  rmxycomplete  37001  rmxypos  37033  ltrmynn0  37034  ltrmxnn0  37035  jm2.24nn  37045  jm2.17a  37046  jm2.17b  37047  jm2.17c  37048  jm2.27c  37093  jm3.1lem2  37104  areaquad  37322  imo72b2lem0  37986  cvgdvgrat  38033  nzprmdif  38039  lt3addmuld  39014  fperiodmullem  39016  fperiodmul  39017  lt4addmuld  39019  xralrple2  39069  xralrple3  39089  ltmulneg  39114  fmul01  39248  fmuldfeqlem1  39250  fmul01lt1lem1  39252  sumnnodd  39298  ltmod  39306  0ellimcdiv  39317  limclner  39319  dvdivbd  39475  dvbdfbdioolem2  39481  dvbdfbdioo  39482  ioodvbdlimc1lem1  39483  ioodvbdlimc1lem2  39484  ioodvbdlimc2lem  39486  stoweidlem1  39555  stoweidlem11  39565  stoweidlem13  39567  stoweidlem14  39568  stoweidlem16  39570  stoweidlem17  39571  stoweidlem22  39576  stoweidlem24  39578  stoweidlem25  39579  stoweidlem26  39580  stoweidlem30  39584  stoweidlem34  39588  stoweidlem36  39590  stoweidlem49  39603  stoweidlem59  39613  stoweidlem60  39614  wallispilem4  39622  wallispilem5  39623  wallispi  39624  wallispi2lem1  39625  wallispi2  39627  stirlinglem1  39628  stirlinglem3  39630  stirlinglem5  39632  stirlinglem6  39633  stirlinglem7  39634  stirlinglem10  39637  stirlinglem11  39638  stirlinglem12  39639  stirlinglem15  39642  stirlingr  39644  dirker2re  39646  dirkerval2  39648  dirkerre  39649  dirkertrigeqlem1  39652  dirkertrigeqlem2  39653  dirkeritg  39656  dirkercncflem2  39658  dirkercncflem4  39660  fourierdlem4  39665  fourierdlem5  39666  fourierdlem6  39667  fourierdlem7  39668  fourierdlem16  39677  fourierdlem18  39679  fourierdlem19  39680  fourierdlem21  39682  fourierdlem22  39683  fourierdlem26  39687  fourierdlem35  39696  fourierdlem39  39700  fourierdlem41  39702  fourierdlem42  39703  fourierdlem43  39704  fourierdlem48  39708  fourierdlem49  39709  fourierdlem51  39711  fourierdlem55  39715  fourierdlem56  39716  fourierdlem57  39717  fourierdlem58  39718  fourierdlem62  39722  fourierdlem63  39723  fourierdlem64  39724  fourierdlem65  39725  fourierdlem66  39726  fourierdlem67  39727  fourierdlem68  39728  fourierdlem71  39731  fourierdlem72  39732  fourierdlem73  39733  fourierdlem76  39736  fourierdlem77  39737  fourierdlem78  39738  fourierdlem83  39743  fourierdlem84  39744  fourierdlem87  39747  fourierdlem88  39748  fourierdlem89  39749  fourierdlem90  39750  fourierdlem91  39751  fourierdlem94  39754  fourierdlem95  39755  fourierdlem97  39757  fourierdlem103  39763  fourierdlem104  39764  fourierdlem112  39772  fourierdlem113  39773  sqwvfoura  39782  sqwvfourb  39783  fouriersw  39785  etransclem23  39811  etransclem48  39836  rrndistlt  39847  hoidmvlelem1  40146  hoidmvlelem2  40147  hoidmvlelem4  40149  smfmullem1  40335  smfmullem2  40336  smfmullem3  40337  smfmul  40339  fmtno4prmfac  40813  lighneallem4a  40854  perfectALTVlem2  40956  ply1mulgsumlem2  41493  digvalnn0  41715  dignn0fr  41717  dig2nn0  41727  amgmwlem  41881
  Copyright terms: Public domain W3C validator