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

Theorem remulcld 11143
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 11094 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
41, 2, 3syl2anc 584 1 (𝜑 → (𝐴 · 𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  (class class class)co 7351  cr 11008   · cmul 11014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 11072
This theorem depends on definitions:  df-bi 206  df-an 397
This theorem is referenced by:  mulge0  11631  msqge0  11634  redivcl  11832  prodgt0  11960  ltmul1a  11962  ltmul1  11963  ltmuldiv  11986  lt2msq1  11997  lt2msq  11998  le2msq  12013  msq11  12014  supmul1  12082  supmullem2  12084  supmul  12085  div4p1lem1div2  12366  mul2lt0rlt0  12971  mul2lt0bi  12975  prodge0rd  12976  qbtwnre  13072  xmulneg1  13142  xmulf  13145  lincmb01cmp  13366  iccf1o  13367  flmulnn0  13686  flhalf  13689  modcl  13732  mod0  13735  modge0  13738  modmulnn  13748  mulp1mod1  13771  2txmodxeq0  13790  modaddmulmod  13797  moddi  13798  modsubdir  13799  modirr  13801  addmodlteq  13805  bernneq  14086  bernneq3  14088  expnbnd  14089  expmulnbnd  14092  discr1  14096  discr  14097  faclbnd  14144  faclbnd6  14153  remullem  14973  01sqrexlem7  15093  sqrtmul  15104  abstri  15175  sqreulem  15204  bhmafibid1  15310  mulcn2  15438  reccn2  15439  o1rlimmul  15461  lo1mul  15470  iseraltlem2  15527  iseraltlem3  15528  iseralt  15529  o1fsum  15658  cvgcmpce  15663  climcndslem1  15694  climcndslem2  15695  climcnds  15696  geomulcvg  15721  cvgrat  15728  mertenslem1  15729  fprodge1  15838  eftlub  15951  sin02gt0  16034  eirrlem  16046  bitsp1o  16273  2mulprm  16529  isprm5  16543  modprm0  16637  prmreclem3  16750  prmreclem4  16751  prmreclem5  16752  2expltfac  16925  metss2lem  23819  nlmvscnlem2  24001  nrginvrcnlem  24007  nmoco  24053  nmotri  24055  nghmcn  24061  icopnfhmeo  24258  nmoleub2lem3  24430  ipcau2  24550  tcphcphlem1  24551  ipcnlem2  24560  rrxcph  24708  csbren  24715  trirn  24716  pjthlem1  24753  opnmbllem  24917  vitalilem4  24927  itg1val2  25000  itg1cl  25001  itg1ge0  25002  itg1addlem4  25015  itg1addlem4OLD  25016  itg1mulc  25021  itg1ge0a  25028  itg1climres  25031  mbfi1fseqlem1  25032  mbfi1fseqlem3  25034  mbfi1fseqlem4  25035  mbfi1fseqlem5  25036  mbfi1fseqlem6  25037  itg2const2  25058  itg2mulclem  25063  itg2mulc  25064  itg2monolem1  25067  itg2monolem3  25069  itg2cnlem2  25079  iblconst  25134  iblmulc2  25147  itgmulc2lem1  25148  itgmulc2lem2  25149  bddmulibl  25155  bddiblnc  25158  dveflem  25295  cmvth  25307  dvlip  25309  dvlipcn  25310  dvivthlem1  25324  lhop1lem  25329  dvcvx  25336  dvfsumlem2  25343  dvfsumlem3  25344  dvfsumlem4  25345  dvfsum2  25350  ftc1lem4  25355  plyeq0lem  25523  aalioulem3  25646  aalioulem4  25647  aaliou3lem9  25662  ulmdvlem1  25711  itgulm  25719  radcnvlem1  25724  radcnvlem2  25725  dvradcnv  25732  abelthlem2  25743  abelthlem7  25749  tangtx  25814  tanregt0  25847  logdivlti  25927  logcnlem3  25951  logcnlem4  25952  logccv  25970  recxpcl  25982  cxpmul  25995  cxplt  26001  cxple2  26004  abscxpbnd  26058  lawcoslem1  26117  heron  26140  atans2  26233  efrlim  26271  o1cxp  26276  scvxcvx  26287  jensenlem2  26289  amgmlem  26291  fsumharmonic  26313  lgamgulmlem2  26331  lgamgulmlem3  26332  lgamgulmlem4  26333  lgamgulmlem5  26334  lgamgulmlem6  26335  relgamcl  26363  ftalem1  26374  ftalem2  26375  ftalem5  26378  basellem3  26384  basellem8  26389  chpub  26520  logfacubnd  26521  logfaclbnd  26522  logfacbnd3  26523  logexprlim  26525  perfectlem2  26530  bclbnd  26580  efexple  26581  bposlem1  26584  bposlem2  26585  bposlem6  26589  bposlem9  26592  lgsdilem  26624  gausslemma2dlem0c  26658  gausslemma2dlem2  26667  gausslemma2dlem3  26668  gausslemma2dlem6  26672  lgseisenlem4  26678  lgseisen  26679  lgsquadlem1  26680  lgsquadlem2  26681  2lgslem1a1  26689  2sqmod  26736  chebbnd1lem1  26769  chebbnd1lem3  26771  chtppilimlem1  26773  chpchtlim  26779  vmadivsum  26782  rplogsumlem1  26784  rpvmasumlem  26787  dchrisumlem2  26790  dchrisumlem3  26791  dchrmusum2  26794  dchrvmasumlem2  26798  dchrvmasumiflem1  26801  dchrisum0re  26813  dchrisum0lem1  26816  dirith2  26828  mulogsumlem  26831  mulogsum  26832  mulog2sumlem2  26835  vmalogdivsum2  26838  vmalogdivsum  26839  2vmadivsumlem  26840  logsqvma  26842  logsqvma2  26843  log2sumbnd  26844  selberglem2  26846  selberg  26848  selbergb  26849  selberg2lem  26850  selberg2b  26852  chpdifbndlem1  26853  chpdifbndlem2  26854  selberg3lem1  26857  selberg3lem2  26858  selberg3  26859  selberg4lem1  26860  selberg4  26861  pntrsumbnd2  26867  selberg3r  26869  selberg4r  26870  selberg34r  26871  pntsf  26873  pntsval2  26876  pntrlog2bndlem1  26877  pntrlog2bndlem2  26878  pntrlog2bndlem3  26879  pntrlog2bndlem4  26880  pntrlog2bndlem5  26881  pntrlog2bndlem6  26883  pntrlog2bnd  26884  pntpbnd1a  26885  pntpbnd1  26886  pntpbnd2  26887  pntibndlem2a  26890  pntibndlem2  26891  pntlemb  26897  pntlemr  26902  pntlemj  26903  pntlemf  26905  pntlemk  26906  pntlemo  26907  pntlem3  26909  ostth2lem1  26918  ostth2lem2  26934  ostth2lem3  26935  ostth2lem4  26936  ostth3  26938  ttgcontlem1  27662  brbtwn2  27683  colinearalglem4  27687  axsegconlem8  27702  axsegconlem9  27703  axsegconlem10  27704  ax5seglem3  27709  axpaschlem  27718  axpasch  27719  axeuclidlem  27740  numclwwlk5  29161  numclwwlk7  29164  smcnlem  29468  ubthlem2  29642  htthlem  29688  pjhthlem1  30162  cnlnadjlem7  30844  nmopcoadji  30872  branmfn  30876  leopnmid  30909  rmulccn  32321  xrge0iifhom  32330  nexple  32420  dya2icoseg  32689  eulerpartlems  32772  eulerpartlemgc  32774  eulerpartlemb  32780  plymulx0  32971  signsvtp  33007  reprgt  33046  breprexplemc  33057  circlemethhgt  33068  hgt750lemd  33073  logdivsqrle  33075  hgt750lem  33076  hgt750lemf  33078  hgt750lemb  33081  hgt750lema  33082  hgt750leme  33083  tgoldbachgtde  33085  resconn  33652  knoppcnlem2  34895  knoppcnlem4  34897  knoppcnlem10  34903  unbdqndv2lem1  34910  unbdqndv2lem2  34911  knoppndvlem1  34913  knoppndvlem11  34923  knoppndvlem12  34924  knoppndvlem14  34926  knoppndvlem15  34927  knoppndvlem17  34929  knoppndvlem18  34930  knoppndvlem19  34931  knoppndvlem20  34932  knoppndvlem21  34933  opnmbllem0  36052  itg2addnclem2  36068  itg2addnclem3  36069  iblmulc2nc  36081  itgmulc2nclem1  36082  ftc1cnnclem  36087  ftc1anclem3  36091  areacirclem4  36107  geomcau  36156  equivbnd  36187  bfplem1  36219  bfplem2  36220  bfp  36221  rrnequiv  36232  rrntotbnd  36233  lcmineqlem19  40442  lcmineqlem20  40443  lcmineqlem21  40444  lcmineqlem22  40445  3lexlogpow2ineq2  40454  dvrelogpow2b  40463  aks4d1p1p2  40465  aks4d1p1p4  40466  aks4d1p1p6  40468  aks4d1p1p7  40469  aks4d1p1p5  40470  aks4d1p1  40471  aks4d1p8d2  40480  aks4d1p8  40482  2np3bcnp1  40490  2ap1caineq  40491  resubdi  40774  remul02  40783  remul01  40785  remulinvcom  40810  sn-0tie0  40817  renegmulnnass  40831  mulgt0con1d  40836  mulgt0con2d  40837  mulgt0b2d  40838  sn-ltmul2d  40839  sn-inelr  40843  itrere  40844  retire  40845  fltnltalem  40909  fltnlta  40910  3cubeslem2  40917  3cubeslem3r  40919  3cubeslem4  40921  irrapxlem1  41054  irrapxlem2  41055  irrapxlem3  41056  irrapxlem4  41057  irrapxlem5  41058  pellexlem2  41062  pellexlem6  41066  pell14qrgt0  41091  pell1qrge1  41102  pell1qrgaplem  41105  pellqrexplicit  41109  pellqrex  41111  rmspecsqrtnq  41138  rmxycomplete  41150  rmxypos  41180  ltrmynn0  41181  ltrmxnn0  41182  jm2.24nn  41192  jm2.17a  41193  jm2.17b  41194  jm2.17c  41195  jm2.27c  41240  jm3.1lem2  41251  areaquad  41459  sqrtcval  41824  resqrtval  41826  imsqrtval  41827  imo72b2lem0  42349  cvgdvgrat  42504  nzprmdif  42510  lt3addmuld  43440  fperiodmullem  43442  fperiodmul  43443  lt4addmuld  43445  xralrple2  43493  xralrple3  43513  ltmulneg  43532  fmul01  43722  fmuldfeqlem1  43724  fmul01lt1lem1  43726  sumnnodd  43772  ltmod  43780  0ellimcdiv  43791  limclner  43793  dvdivbd  44065  dvbdfbdioolem2  44071  dvbdfbdioo  44072  ioodvbdlimc1lem1  44073  ioodvbdlimc1lem2  44074  ioodvbdlimc2lem  44076  stoweidlem1  44143  stoweidlem11  44153  stoweidlem13  44155  stoweidlem14  44156  stoweidlem16  44158  stoweidlem17  44159  stoweidlem22  44164  stoweidlem24  44166  stoweidlem25  44167  stoweidlem26  44168  stoweidlem30  44172  stoweidlem34  44176  stoweidlem36  44178  stoweidlem49  44191  stoweidlem59  44201  stoweidlem60  44202  wallispilem4  44210  wallispilem5  44211  wallispi  44212  wallispi2lem1  44213  wallispi2  44215  stirlinglem1  44216  stirlinglem3  44218  stirlinglem5  44220  stirlinglem6  44221  stirlinglem7  44222  stirlinglem10  44225  stirlinglem11  44226  stirlinglem12  44227  stirlinglem15  44230  stirlingr  44232  dirker2re  44234  dirkerval2  44236  dirkerre  44237  dirkertrigeqlem1  44240  dirkertrigeqlem2  44241  dirkeritg  44244  dirkercncflem2  44246  dirkercncflem4  44248  fourierdlem4  44253  fourierdlem5  44254  fourierdlem6  44255  fourierdlem7  44256  fourierdlem16  44265  fourierdlem18  44267  fourierdlem19  44268  fourierdlem21  44270  fourierdlem22  44271  fourierdlem26  44275  fourierdlem35  44284  fourierdlem39  44288  fourierdlem41  44290  fourierdlem42  44291  fourierdlem43  44292  fourierdlem48  44296  fourierdlem49  44297  fourierdlem51  44299  fourierdlem55  44303  fourierdlem56  44304  fourierdlem57  44305  fourierdlem58  44306  fourierdlem62  44310  fourierdlem63  44311  fourierdlem64  44312  fourierdlem65  44313  fourierdlem66  44314  fourierdlem67  44315  fourierdlem68  44316  fourierdlem71  44319  fourierdlem72  44320  fourierdlem73  44321  fourierdlem76  44324  fourierdlem77  44325  fourierdlem78  44326  fourierdlem83  44331  fourierdlem84  44332  fourierdlem87  44335  fourierdlem88  44336  fourierdlem89  44337  fourierdlem90  44338  fourierdlem91  44339  fourierdlem94  44342  fourierdlem95  44343  fourierdlem97  44345  fourierdlem103  44351  fourierdlem104  44352  fourierdlem112  44360  fourierdlem113  44361  sqwvfoura  44370  sqwvfourb  44371  fouriersw  44373  etransclem23  44399  etransclem48  44424  rrndistlt  44432  hoidmvlelem1  44737  hoidmvlelem2  44738  hoidmvlelem4  44740  smfmullem1  44933  smfmullem2  44934  smfmullem3  44935  smfmul  44937  fmtno4prmfac  45665  lighneallem4a  45701  requad01  45714  requad1  45715  requad2  45716  perfectALTVlem2  45815  ply1mulgsumlem2  46369  digvalnn0  46586  dignn0fr  46588  dig2nn0  46598  affinecomb1  46689  rrx2linest2  46731  line2  46739  itsclc0lem1  46743  itsclc0lem2  46744  itsclc0lem3  46745  itscnhlc0yqe  46746  itsclc0yqsollem2  46750  itsclc0yqsol  46751  itscnhlc0xyqsol  46752  itsclc0xyqsolr  46756  itsclinecirc0  46760  itsclinecirc0b  46761  itsclinecirc0in  46762  itsclquadb  46763  itsclquadeu  46764  2itscp  46768  itscnhlinecirc02plem1  46769  itscnhlinecirc02p  46772  inlinecirc02plem  46773  amgmwlem  47150
  Copyright terms: Public domain W3C validator