Theorem remulcld 11243

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

Step	Hyp	Ref	Expression
1		recnd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		readdcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		remulcl 11189	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 595	1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2143  (class class class)co 7410  ℝcr 11103   · cmul 11109

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 11167

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  mulge0  11736  msqge0  11739  redivcl  11938  prodgt0  12066  ltmul1a  12068  ltmul1  12069  ltmuldiv  12092  lt2msq1  12103  lt2msq  12104  le2msq  12119  msq11  12120  supmul1  12188  supmullem2  12190  supmul  12191  div4p1lem1div2  12503  mul2lt0rlt0  13124  mul2lt0bi  13128  prodge0rd  13129  ge2halflem1  13137  qbtwnre  13229  xmulneg1  13299  xmulf  13302  lincmb01cmp  13526  iccf1o  13527  flmulnn0  13865  flhalf  13868  modcl  13911  mod0  13914  modge0  13917  modmulnn  13927  mulp1mod1  13952  muladdmod  13953  2txmodxeq0  13972  modaddmulmod  13979  moddi  13980  modsubdir  13981  modirr  13983  addmodlteq  13987  bernneq  14270  bernneq3  14272  expnbnd  14273  expmulnbnd  14276  discr1  14280  discr  14281  faclbnd  14331  faclbnd6  14340  remullem  15184  01sqrexlem7  15304  sqrtmul  15315  abstri  15387  sqreulem  15416  bhmafibid1  15524  mulcn2  15652  reccn2  15653  o1rlimmul  15675  lo1mul  15684  iseraltlem2  15739  iseraltlem3  15740  iseralt  15741  o1fsum  15870  cvgcmpce  15875  climcndslem1  15908  climcndslem2  15909  climcnds  15910  geomulcvg  15935  cvgrat  15942  mertenslem1  15943  fprodge1  16054  eftlub  16169  sin02gt0  16252  eirrlem  16264  bitsp1o  16495  2mulprm  16755  isprm5  16770  modprm0  16869  prmreclem3  16982  prmreclem4  16983  prmreclem5  16984  2expltfac  17156  metss2lem  24677  nlmvscnlem2  24851  nrginvrcnlem  24857  nmoco  24903  nmotri  24905  nghmcn  24911  icopnfhmeo  25111  nmoleub2lem3  25283  ipcau2  25402  tcphcphlem1  25403  ipcnlem2  25412  rrxcph  25560  csbren  25567  trirn  25568  pjthlem1  25605  opnmbllem  25769  vitalilem4  25779  itg1val2  25852  itg1cl  25853  itg1ge0  25854  itg1addlem4  25867  itg1mulc  25872  itg1ge0a  25879  itg1climres  25882  mbfi1fseqlem1  25883  mbfi1fseqlem3  25885  mbfi1fseqlem4  25886  mbfi1fseqlem5  25887  mbfi1fseqlem6  25888  itg2const2  25909  itg2mulclem  25914  itg2mulc  25915  itg2monolem1  25918  itg2monolem3  25920  itg2cnlem2  25930  iblconst  25986  iblmulc2  25999  itgmulc2lem1  26000  itgmulc2lem2  26001  bddmulibl  26007  bddiblnc  26010  dveflem  26147  cmvth  26159  dvlip  26161  dvlipcn  26162  dvivthlem1  26176  lhop1lem  26181  dvcvx  26188  dvfsumlem2  26195  dvfsumlem3  26196  dvfsumlem4  26197  dvfsum2  26202  ftc1lem4  26207  plyeq0lem  26376  plyn0mulidp  26451  aalioulem3  26506  aalioulem4  26507  aaliou3lem9  26522  ulmdvlem1  26572  itgulm  26580  radcnvlem1  26585  radcnvlem2  26586  dvradcnv  26593  abelthlem2  26604  abelthlem7  26610  tangtx  26679  tanregt0  26713  logdivlti  26794  logcnlem3  26818  logcnlem4  26819  logccv  26837  recxpcl  26849  cxpmul  26862  cxplt  26868  cxple2  26871  abscxpbnd  26927  lawcoslem1  26989  heron  27012  atans2  27105  efrlim  27143  o1cxp  27148  scvxcvx  27159  jensenlem2  27161  amgmlem  27163  fsumharmonic  27185  lgamgulmlem2  27203  lgamgulmlem3  27204  lgamgulmlem4  27205  lgamgulmlem5  27206  lgamgulmlem6  27207  relgamcl  27235  ftalem1  27246  ftalem2  27247  ftalem5  27250  basellem3  27256  basellem8  27261  chpub  27393  logfacubnd  27394  logfaclbnd  27395  logfacbnd3  27396  logexprlim  27398  perfectlem2  27403  bclbnd  27453  efexple  27454  bposlem1  27457  bposlem2  27458  bposlem6  27462  bposlem9  27465  lgsdilem  27497  gausslemma2dlem0c  27531  gausslemma2dlem2  27540  gausslemma2dlem3  27541  gausslemma2dlem6  27545  lgseisenlem4  27551  lgseisen  27552  lgsquadlem1  27553  lgsquadlem2  27554  2lgslem1a1  27562  2sqmod  27609  chebbnd1lem1  27642  chebbnd1lem3  27644  chtppilimlem1  27646  chpchtlim  27652  vmadivsum  27655  rplogsumlem1  27657  rpvmasumlem  27660  dchrisumlem2  27663  dchrisumlem3  27664  dchrmusum2  27667  dchrvmasumlem2  27671  dchrvmasumiflem1  27674  dchrisum0re  27686  dchrisum0lem1  27689  dirith2  27701  mulogsumlem  27704  mulogsum  27705  mulog2sumlem2  27708  vmalogdivsum2  27711  vmalogdivsum  27712  2vmadivsumlem  27713  logsqvma  27715  logsqvma2  27716  log2sumbnd  27717  selberglem2  27719  selberg  27721  selbergb  27722  selberg2lem  27723  selberg2b  27725  chpdifbndlem1  27726  chpdifbndlem2  27727  selberg3lem1  27730  selberg3lem2  27731  selberg3  27732  selberg4lem1  27733  selberg4  27734  pntrsumbnd2  27740  selberg3r  27742  selberg4r  27743  selberg34r  27744  pntsf  27746  pntsval2  27749  pntrlog2bndlem1  27750  pntrlog2bndlem2  27751  pntrlog2bndlem3  27752  pntrlog2bndlem4  27753  pntrlog2bndlem5  27754  pntrlog2bndlem6  27756  pntrlog2bnd  27757  pntpbnd1a  27758  pntpbnd1  27759  pntpbnd2  27760  pntibndlem2a  27763  pntibndlem2  27764  pntlemb  27770  pntlemr  27775  pntlemj  27776  pntlemf  27778  pntlemk  27779  pntlemo  27780  pntlem3  27782  ostth2lem1  27791  ostth2lem2  27807  ostth2lem3  27808  ostth2lem4  27809  ostth3  27811  ttgcontlem1  29243  brbtwn2  29264  colinearalglem4  29268  axsegconlem8  29283  axsegconlem9  29284  axsegconlem10  29285  ax5seglem3  29290  axpaschlem  29299  axpasch  29300  axeuclidlem  29321  numclwwlk5  30748  numclwwlk7  30751  smcnlem  31058  ubthlem2  31232  htthlem  31278  pjhthlem1  31752  cnlnadjlem7  32434  nmopcoadji  32462  branmfn  32466  leopnmid  32499  nexple  33186  constrremulcl  34166  constrmulcl  34170  cos9thpiminplylem1  34181  cos9thpinconstrlem1  34188  rmulccn  34327  xrge0iifhom  34336  dya2icoseg  34676  eulerpartlems  34759  eulerpartlemgc  34761  eulerpartlemb  34767  signsvtp  34979  reprgt  35017  breprexplemc  35028  circlemethhgt  35039  hgt750lemd  35044  logdivsqrle  35046  hgt750lem  35047  hgt750lemf  35049  hgt750lemb  35052  hgt750lema  35053  hgt750leme  35054  tgoldbachgtde  35056  resconn  35746  knoppcnlem2  37111  knoppcnlem4  37113  knoppcnlem10  37119  unbdqndv2lem1  37126  unbdqndv2lem2  37127  knoppndvlem1  37129  knoppndvlem11  37139  knoppndvlem12  37140  knoppndvlem14  37142  knoppndvlem15  37143  knoppndvlem17  37145  knoppndvlem18  37146  knoppndvlem19  37147  knoppndvlem20  37148  knoppndvlem21  37149  opnmbllem0  38335  itg2addnclem2  38351  itg2addnclem3  38352  iblmulc2nc  38364  itgmulc2nclem1  38365  ftc1cnnclem  38370  ftc1anclem3  38374  areacirclem4  38390  geomcau  38438  equivbnd  38469  bfplem1  38501  bfplem2  38502  bfp  38503  rrnequiv  38514  rrntotbnd  38515  lcmineqlem19  42842  lcmineqlem20  42843  lcmineqlem21  42844  lcmineqlem22  42845  3lexlogpow2ineq2  42854  dvrelogpow2b  42863  aks4d1p1p2  42865  aks4d1p1p4  42866  aks4d1p1p6  42868  aks4d1p1p7  42869  aks4d1p1p5  42870  aks4d1p1  42871  aks4d1p8d2  42880  aks4d1p8  42882  posbezout  42895  aks6d1c2lem4  42922  2np3bcnp1  42939  2ap1caineq  42940  aks6d1c6lem4  42968  aks6d1c7lem1  42975  aks6d1c7lem2  42976  resubdi  43185  remul02  43194  remul01  43196  remulinvcom  43222  rediveud  43232  redivcan3d  43237  redivrec2d  43249  rediv23d  43250  sn-0tie0  43253  renegmulnnass  43267  mulgt0con1d  43272  mulgt0con2d  43273  mulgt0b1d  43274  sn-ltmul2d  43275  mulgt0b2d  43280  sn-mulgt1d  43281  mulltgt0d  43284  mullt0b1d  43285  mullt0b2d  43286  sn-mullt0d  43287  sn-itrere  43290  sn-retire  43291  fltnltalem  43422  fltnlta  43423  3cubeslem2  43444  3cubeslem3r  43446  3cubeslem4  43448  irrapxlem1  43577  irrapxlem2  43578  irrapxlem3  43579  irrapxlem4  43580  irrapxlem5  43581  pellexlem2  43585  pellexlem6  43589  pell14qrgt0  43614  pell1qrge1  43625  pell1qrgaplem  43628  pellqrexplicit  43632  pellqrex  43634  rmspecsqrtnq  43661  rmxycomplete  43672  rmxypos  43702  ltrmynn0  43703  ltrmxnn0  43704  jm2.24nn  43714  jm2.17a  43715  jm2.17b  43716  jm2.17c  43717  jm2.27c  43762  jm3.1lem2  43773  areaquad  43971  sqrtcval  44395  resqrtval  44397  imsqrtval  44398  imo72b2lem0  44919  cvgdvgrat  45051  nzprmdif  45057  lt3addmuld  46048  fperiodmullem  46050  fperiodmul  46051  lt4addmuld  46053  xralrple2  46098  xralrple3  46117  ltmulneg  46135  fmul01  46324  fmuldfeqlem1  46326  fmul01lt1lem1  46328  sumnnodd  46374  ltmod  46380  0ellimcdiv  46391  limclner  46393  dvdivbd  46665  dvbdfbdioolem2  46671  dvbdfbdioo  46672  ioodvbdlimc1lem1  46673  ioodvbdlimc1lem2  46674  ioodvbdlimc2lem  46676  stoweidlem1  46743  stoweidlem11  46753  stoweidlem13  46755  stoweidlem14  46756  stoweidlem16  46758  stoweidlem17  46759  stoweidlem22  46764  stoweidlem24  46766  stoweidlem25  46767  stoweidlem26  46768  stoweidlem30  46772  stoweidlem34  46776  stoweidlem36  46778  stoweidlem49  46791  stoweidlem59  46801  stoweidlem60  46802  wallispilem4  46810  wallispilem5  46811  wallispi  46812  wallispi2lem1  46813  wallispi2  46815  stirlinglem1  46816  stirlinglem3  46818  stirlinglem5  46820  stirlinglem6  46821  stirlinglem7  46822  stirlinglem10  46825  stirlinglem11  46826  stirlinglem12  46827  stirlinglem15  46830  stirlingr  46832  dirker2re  46834  dirkerval2  46836  dirkerre  46837  dirkertrigeqlem1  46840  dirkertrigeqlem2  46841  dirkeritg  46844  dirkercncflem2  46846  dirkercncflem4  46848  fourierdlem4  46853  fourierdlem5  46854  fourierdlem6  46855  fourierdlem7  46856  fourierdlem16  46865  fourierdlem18  46867  fourierdlem19  46868  fourierdlem21  46870  fourierdlem22  46871  fourierdlem26  46875  fourierdlem35  46884  fourierdlem39  46888  fourierdlem41  46890  fourierdlem42  46891  fourierdlem43  46892  fourierdlem48  46896  fourierdlem49  46897  fourierdlem51  46899  fourierdlem55  46903  fourierdlem56  46904  fourierdlem57  46905  fourierdlem58  46906  fourierdlem62  46910  fourierdlem63  46911  fourierdlem64  46912  fourierdlem65  46913  fourierdlem66  46914  fourierdlem67  46915  fourierdlem68  46916  fourierdlem71  46919  fourierdlem72  46920  fourierdlem73  46921  fourierdlem76  46924  fourierdlem77  46925  fourierdlem78  46926  fourierdlem83  46931  fourierdlem84  46932  fourierdlem87  46935  fourierdlem88  46936  fourierdlem89  46937  fourierdlem90  46938  fourierdlem91  46939  fourierdlem94  46942  fourierdlem95  46943  fourierdlem97  46945  fourierdlem103  46951  fourierdlem104  46952  fourierdlem112  46960  fourierdlem113  46961  sqwvfoura  46970  sqwvfourb  46971  fouriersw  46973  etransclem23  46999  etransclem48  47024  rrndistlt  47032  hoidmvlelem1  47337  hoidmvlelem2  47338  hoidmvlelem4  47340  smfmullem1  47533  smfmullem2  47534  smfmullem3  47535  smfmul  47537  2timesltsqm1  48144  fmtno4prmfac  48352  lighneallem4a  48388  requad01  48414  requad1  48415  requad2  48416  perfectALTVlem2  48515  gpg3kgrtriexlem1  48876  gpg3kgrtriexlem4  48879  gpg3kgrtriexlem6  48881  ply1mulgsumlem2  49195  digvalnn0  49407  dignn0fr  49409  dig2nn0  49419  affinecomb1  49510  rrx2linest2  49552  line2  49560  itsclc0lem1  49564  itsclc0lem2  49565  itsclc0lem3  49566  itscnhlc0yqe  49567  itsclc0yqsollem2  49571  itsclc0yqsol  49572  itscnhlc0xyqsol  49573  itsclc0xyqsolr  49577  itsclinecirc0  49581  itsclinecirc0b  49582  itsclinecirc0in  49583  itsclquadb  49584  itsclquadeu  49585  2itscp  49589  itscnhlinecirc02plem1  49590  itscnhlinecirc02p  49593  inlinecirc02plem  49594  crosspdotsumi  50673  crossp3i  50676  amgmwlem  50677