Theorem remulcld 11241

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 11187	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 595	1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2149  (class class class)co 7413  ℝcr 11101   · cmul 11107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 11165

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

This theorem is referenced by:  mulge0  11734  msqge0  11737  redivcl  11936  prodgt0  12064  ltmul1a  12066  ltmul1  12067  ltmuldiv  12090  lt2msq1  12101  lt2msq  12102  le2msq  12117  msq11  12118  supmul1  12186  supmullem2  12188  supmul  12189  div4p1lem1div2  12501  mul2lt0rlt0  13122  mul2lt0bi  13126  prodge0rd  13127  ge2halflem1  13135  qbtwnre  13227  xmulneg1  13297  xmulf  13300  lincmb01cmp  13524  iccf1o  13525  flmulnn0  13862  flhalf  13865  modcl  13908  mod0  13911  modge0  13914  modmulnn  13924  mulp1mod1  13949  muladdmod  13950  2txmodxeq0  13969  modaddmulmod  13976  moddi  13977  modsubdir  13978  modirr  13980  addmodlteq  13984  bernneq  14267  bernneq3  14269  expnbnd  14270  expmulnbnd  14273  discr1  14277  discr  14278  faclbnd  14328  faclbnd6  14337  remullem  15181  01sqrexlem7  15301  sqrtmul  15312  abstri  15384  sqreulem  15413  bhmafibid1  15521  mulcn2  15649  reccn2  15650  o1rlimmul  15672  lo1mul  15681  iseraltlem2  15736  iseraltlem3  15737  iseralt  15738  o1fsum  15867  cvgcmpce  15872  climcndslem1  15905  climcndslem2  15906  climcnds  15907  geomulcvg  15932  cvgrat  15939  mertenslem1  15940  fprodge1  16051  eftlub  16167  sin02gt0  16250  eirrlem  16262  bitsp1o  16493  2mulprm  16753  isprm5  16768  modprm0  16867  prmreclem3  16980  prmreclem4  16981  prmreclem5  16982  2expltfac  17154  metss2lem  24639  nlmvscnlem2  24813  nrginvrcnlem  24819  nmoco  24865  nmotri  24867  nghmcn  24873  icopnfhmeo  25073  nmoleub2lem3  25245  ipcau2  25364  tcphcphlem1  25365  ipcnlem2  25374  rrxcph  25522  csbren  25529  trirn  25530  pjthlem1  25567  opnmbllem  25731  vitalilem4  25741  itg1val2  25814  itg1cl  25815  itg1ge0  25816  itg1addlem4  25829  itg1mulc  25834  itg1ge0a  25841  itg1climres  25844  mbfi1fseqlem1  25845  mbfi1fseqlem3  25847  mbfi1fseqlem4  25848  mbfi1fseqlem5  25849  mbfi1fseqlem6  25850  itg2const2  25871  itg2mulclem  25876  itg2mulc  25877  itg2monolem1  25880  itg2monolem3  25882  itg2cnlem2  25892  iblconst  25948  iblmulc2  25961  itgmulc2lem1  25962  itgmulc2lem2  25963  bddmulibl  25969  bddiblnc  25972  dveflem  26109  cmvth  26121  dvlip  26123  dvlipcn  26124  dvivthlem1  26138  lhop1lem  26143  dvcvx  26150  dvfsumlem2  26157  dvfsumlem3  26158  dvfsumlem4  26159  dvfsum2  26164  ftc1lem4  26169  plyeq0lem  26338  plyn0mulidp  26413  aalioulem3  26466  aalioulem4  26467  aaliou3lem9  26482  ulmdvlem1  26531  itgulm  26539  radcnvlem1  26544  radcnvlem2  26545  dvradcnv  26552  abelthlem2  26563  abelthlem7  26569  tangtx  26638  tanregt0  26672  logdivlti  26753  logcnlem3  26777  logcnlem4  26778  logccv  26796  recxpcl  26808  cxpmul  26821  cxplt  26827  cxple2  26830  abscxpbnd  26886  lawcoslem1  26948  heron  26971  atans2  27064  efrlim  27102  o1cxp  27107  scvxcvx  27118  jensenlem2  27120  amgmlem  27122  fsumharmonic  27144  lgamgulmlem2  27162  lgamgulmlem3  27163  lgamgulmlem4  27164  lgamgulmlem5  27165  lgamgulmlem6  27166  relgamcl  27194  ftalem1  27205  ftalem2  27206  ftalem5  27209  basellem3  27215  basellem8  27220  chpub  27352  logfacubnd  27353  logfaclbnd  27354  logfacbnd3  27355  logexprlim  27357  perfectlem2  27362  bclbnd  27412  efexple  27413  bposlem1  27416  bposlem2  27417  bposlem6  27421  bposlem9  27424  lgsdilem  27456  gausslemma2dlem0c  27490  gausslemma2dlem2  27499  gausslemma2dlem3  27500  gausslemma2dlem6  27504  lgseisenlem4  27510  lgseisen  27511  lgsquadlem1  27512  lgsquadlem2  27513  2lgslem1a1  27521  2sqmod  27568  chebbnd1lem1  27601  chebbnd1lem3  27603  chtppilimlem1  27605  chpchtlim  27611  vmadivsum  27614  rplogsumlem1  27616  rpvmasumlem  27619  dchrisumlem2  27622  dchrisumlem3  27623  dchrmusum2  27626  dchrvmasumlem2  27630  dchrvmasumiflem1  27633  dchrisum0re  27645  dchrisum0lem1  27648  dirith2  27660  mulogsumlem  27663  mulogsum  27664  mulog2sumlem2  27667  vmalogdivsum2  27670  vmalogdivsum  27671  2vmadivsumlem  27672  logsqvma  27674  logsqvma2  27675  log2sumbnd  27676  selberglem2  27678  selberg  27680  selbergb  27681  selberg2lem  27682  selberg2b  27684  chpdifbndlem1  27685  chpdifbndlem2  27686  selberg3lem1  27689  selberg3lem2  27690  selberg3  27691  selberg4lem1  27692  selberg4  27693  pntrsumbnd2  27699  selberg3r  27701  selberg4r  27702  selberg34r  27703  pntsf  27705  pntsval2  27708  pntrlog2bndlem1  27709  pntrlog2bndlem2  27710  pntrlog2bndlem3  27711  pntrlog2bndlem4  27712  pntrlog2bndlem5  27713  pntrlog2bndlem6  27715  pntrlog2bnd  27716  pntpbnd1a  27717  pntpbnd1  27718  pntpbnd2  27719  pntibndlem2a  27722  pntibndlem2  27723  pntlemb  27729  pntlemr  27734  pntlemj  27735  pntlemf  27737  pntlemk  27738  pntlemo  27739  pntlem3  27741  ostth2lem1  27750  ostth2lem2  27766  ostth2lem3  27767  ostth2lem4  27768  ostth3  27770  ttgcontlem1  29177  brbtwn2  29198  colinearalglem4  29202  axsegconlem8  29217  axsegconlem9  29218  axsegconlem10  29219  ax5seglem3  29224  axpaschlem  29233  axpasch  29234  axeuclidlem  29255  numclwwlk5  30682  numclwwlk7  30685  smcnlem  30992  ubthlem2  31166  htthlem  31212  pjhthlem1  31686  cnlnadjlem7  32368  nmopcoadji  32396  branmfn  32400  leopnmid  32433  nexple  33120  constrremulcl  34104  constrmulcl  34108  cos9thpiminplylem1  34119  cos9thpinconstrlem1  34126  rmulccn  34265  xrge0iifhom  34274  dya2icoseg  34614  eulerpartlems  34697  eulerpartlemgc  34699  eulerpartlemb  34705  signsvtp  34917  reprgt  34955  breprexplemc  34966  circlemethhgt  34977  hgt750lemd  34982  logdivsqrle  34984  hgt750lem  34985  hgt750lemf  34987  hgt750lemb  34990  hgt750lema  34991  hgt750leme  34992  tgoldbachgtde  34994  resconn  35673  knoppcnlem2  37008  knoppcnlem4  37010  knoppcnlem10  37016  unbdqndv2lem1  37023  unbdqndv2lem2  37024  knoppndvlem1  37026  knoppndvlem11  37036  knoppndvlem12  37037  knoppndvlem14  37039  knoppndvlem15  37040  knoppndvlem17  37042  knoppndvlem18  37043  knoppndvlem19  37044  knoppndvlem20  37045  knoppndvlem21  37046  opnmbllem0  38232  itg2addnclem2  38248  itg2addnclem3  38249  iblmulc2nc  38261  itgmulc2nclem1  38262  ftc1cnnclem  38267  ftc1anclem3  38271  areacirclem4  38287  geomcau  38335  equivbnd  38366  bfplem1  38398  bfplem2  38399  bfp  38400  rrnequiv  38411  rrntotbnd  38412  lcmineqlem19  42741  lcmineqlem20  42742  lcmineqlem21  42743  lcmineqlem22  42744  3lexlogpow2ineq2  42753  dvrelogpow2b  42762  aks4d1p1p2  42764  aks4d1p1p4  42765  aks4d1p1p6  42767  aks4d1p1p7  42768  aks4d1p1p5  42769  aks4d1p1  42770  aks4d1p8d2  42779  aks4d1p8  42781  posbezout  42794  aks6d1c2lem4  42821  2np3bcnp1  42838  2ap1caineq  42839  aks6d1c6lem4  42867  aks6d1c7lem1  42874  aks6d1c7lem2  42875  resubdi  43084  remul02  43093  remul01  43095  remulinvcom  43121  rediveud  43131  redivcan3d  43136  redivrec2d  43148  rediv23d  43149  sn-0tie0  43152  renegmulnnass  43166  mulgt0con1d  43171  mulgt0con2d  43172  mulgt0b1d  43173  sn-ltmul2d  43174  mulgt0b2d  43179  sn-mulgt1d  43180  mulltgt0d  43183  mullt0b1d  43184  mullt0b2d  43185  sn-mullt0d  43186  sn-itrere  43189  sn-retire  43190  fltnltalem  43323  fltnlta  43324  3cubeslem2  43345  3cubeslem3r  43347  3cubeslem4  43349  irrapxlem1  43478  irrapxlem2  43479  irrapxlem3  43480  irrapxlem4  43481  irrapxlem5  43482  pellexlem2  43486  pellexlem6  43490  pell14qrgt0  43515  pell1qrge1  43526  pell1qrgaplem  43529  pellqrexplicit  43533  pellqrex  43535  rmspecsqrtnq  43562  rmxycomplete  43573  rmxypos  43603  ltrmynn0  43604  ltrmxnn0  43605  jm2.24nn  43615  jm2.17a  43616  jm2.17b  43617  jm2.17c  43618  jm2.27c  43663  jm3.1lem2  43674  areaquad  43872  sqrtcval  44296  resqrtval  44298  imsqrtval  44299  imo72b2lem0  44820  cvgdvgrat  44952  nzprmdif  44958  lt3addmuld  45949  fperiodmullem  45951  fperiodmul  45952  lt4addmuld  45954  xralrple2  45999  xralrple3  46018  ltmulneg  46036  fmul01  46225  fmuldfeqlem1  46227  fmul01lt1lem1  46229  sumnnodd  46275  ltmod  46281  0ellimcdiv  46292  limclner  46294  dvdivbd  46566  dvbdfbdioolem2  46572  dvbdfbdioo  46573  ioodvbdlimc1lem1  46574  ioodvbdlimc1lem2  46575  ioodvbdlimc2lem  46577  stoweidlem1  46644  stoweidlem11  46654  stoweidlem13  46656  stoweidlem14  46657  stoweidlem16  46659  stoweidlem17  46660  stoweidlem22  46665  stoweidlem24  46667  stoweidlem25  46668  stoweidlem26  46669  stoweidlem30  46673  stoweidlem34  46677  stoweidlem36  46679  stoweidlem49  46692  stoweidlem59  46702  stoweidlem60  46703  wallispilem4  46711  wallispilem5  46712  wallispi  46713  wallispi2lem1  46714  wallispi2  46716  stirlinglem1  46717  stirlinglem3  46719  stirlinglem5  46721  stirlinglem6  46722  stirlinglem7  46723  stirlinglem10  46726  stirlinglem11  46727  stirlinglem12  46728  stirlinglem15  46731  stirlingr  46733  dirker2re  46735  dirkerval2  46737  dirkerre  46738  dirkertrigeqlem1  46741  dirkertrigeqlem2  46742  dirkeritg  46745  dirkercncflem2  46747  dirkercncflem4  46749  fourierdlem4  46754  fourierdlem5  46755  fourierdlem6  46756  fourierdlem7  46757  fourierdlem16  46766  fourierdlem18  46768  fourierdlem19  46769  fourierdlem21  46771  fourierdlem22  46772  fourierdlem26  46776  fourierdlem35  46785  fourierdlem39  46789  fourierdlem41  46791  fourierdlem42  46792  fourierdlem43  46793  fourierdlem48  46797  fourierdlem49  46798  fourierdlem51  46800  fourierdlem55  46804  fourierdlem56  46805  fourierdlem57  46806  fourierdlem58  46807  fourierdlem62  46811  fourierdlem63  46812  fourierdlem64  46813  fourierdlem65  46814  fourierdlem66  46815  fourierdlem67  46816  fourierdlem68  46817  fourierdlem71  46820  fourierdlem72  46821  fourierdlem73  46822  fourierdlem76  46825  fourierdlem77  46826  fourierdlem78  46827  fourierdlem83  46832  fourierdlem84  46833  fourierdlem87  46836  fourierdlem88  46837  fourierdlem89  46838  fourierdlem90  46839  fourierdlem91  46840  fourierdlem94  46843  fourierdlem95  46844  fourierdlem97  46846  fourierdlem103  46852  fourierdlem104  46853  fourierdlem112  46861  fourierdlem113  46862  sqwvfoura  46871  sqwvfourb  46872  fouriersw  46874  etransclem23  46900  etransclem48  46925  rrndistlt  46933  hoidmvlelem1  47238  hoidmvlelem2  47239  hoidmvlelem4  47241  smfmullem1  47434  smfmullem2  47435  smfmullem3  47436  smfmul  47438  2timesltsqm1  48042  fmtno4prmfac  48250  lighneallem4a  48286  requad01  48312  requad1  48313  requad2  48314  perfectALTVlem2  48413  gpg3kgrtriexlem1  48774  gpg3kgrtriexlem4  48777  gpg3kgrtriexlem6  48779  ply1mulgsumlem2  49089  digvalnn0  49301  dignn0fr  49303  dig2nn0  49313  affinecomb1  49404  rrx2linest2  49446  line2  49454  itsclc0lem1  49458  itsclc0lem2  49459  itsclc0lem3  49460  itscnhlc0yqe  49461  itsclc0yqsollem2  49465  itsclc0yqsol  49466  itscnhlc0xyqsol  49467  itsclc0xyqsolr  49471  itsclinecirc0  49475  itsclinecirc0b  49476  itsclinecirc0in  49477  itsclquadb  49478  itsclquadeu  49479  2itscp  49483  itscnhlinecirc02plem1  49484  itscnhlinecirc02p  49487  inlinecirc02plem  49488  amgmwlem  50513