Theorem remulcld 11214

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

Syntax hints:   → wi 4   ∈ wcel 2144  (class class class)co 7398  ℝcr 11074   · cmul 11080

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

This theorem depends on definitions:  df-bi 209  df-an 400

This theorem is referenced by:  mulge0  11707  msqge0  11710  redivcl  11912  prodgt0  12040  ltmul1a  12042  ltmul1  12043  ltmuldiv  12067  lt2msq1  12078  lt2msq  12079  le2msq  12094  msq11  12095  supmul1  12163  supmullem2  12165  supmul  12166  div4p1lem1div2  12478  mul2lt0rlt0  13099  mul2lt0bi  13103  prodge0rd  13104  ge2halflem1  13112  qbtwnre  13204  xmulneg1  13274  xmulf  13277  lincmb01cmp  13501  iccf1o  13502  flmulnn0  13839  flhalf  13842  modcl  13885  mod0  13888  modge0  13891  modmulnn  13901  mulp1mod1  13926  muladdmod  13927  2txmodxeq0  13946  modaddmulmod  13953  moddi  13954  modsubdir  13955  modirr  13957  addmodlteq  13961  bernneq  14244  bernneq3  14246  expnbnd  14247  expmulnbnd  14250  discr1  14254  discr  14255  faclbnd  14305  faclbnd6  14314  remullem  15157  01sqrexlem7  15277  sqrtmul  15288  abstri  15360  sqreulem  15389  bhmafibid1  15497  mulcn2  15625  reccn2  15626  o1rlimmul  15648  lo1mul  15657  iseraltlem2  15712  iseraltlem3  15713  iseralt  15714  o1fsum  15843  cvgcmpce  15848  climcndslem1  15881  climcndslem2  15882  climcnds  15883  geomulcvg  15908  cvgrat  15915  mertenslem1  15916  fprodge1  16027  eftlub  16143  sin02gt0  16226  eirrlem  16238  bitsp1o  16469  2mulprm  16729  isprm5  16744  modprm0  16843  prmreclem3  16956  prmreclem4  16957  prmreclem5  16958  2expltfac  17130  metss2lem  24573  nlmvscnlem2  24747  nrginvrcnlem  24753  nmoco  24799  nmotri  24801  nghmcn  24807  icopnfhmeo  25007  nmoleub2lem3  25179  ipcau2  25298  tcphcphlem1  25299  ipcnlem2  25308  rrxcph  25456  csbren  25463  trirn  25464  pjthlem1  25501  opnmbllem  25665  vitalilem4  25675  itg1val2  25748  itg1cl  25749  itg1ge0  25750  itg1addlem4  25763  itg1mulc  25768  itg1ge0a  25775  itg1climres  25778  mbfi1fseqlem1  25779  mbfi1fseqlem3  25781  mbfi1fseqlem4  25782  mbfi1fseqlem5  25783  mbfi1fseqlem6  25784  itg2const2  25805  itg2mulclem  25810  itg2mulc  25811  itg2monolem1  25814  itg2monolem3  25816  itg2cnlem2  25826  iblconst  25882  iblmulc2  25895  itgmulc2lem1  25896  itgmulc2lem2  25897  bddmulibl  25903  bddiblnc  25906  dveflem  26043  cmvth  26055  dvlip  26057  dvlipcn  26058  dvivthlem1  26072  lhop1lem  26077  dvcvx  26084  dvfsumlem2  26091  dvfsumlem3  26092  dvfsumlem4  26093  dvfsum2  26098  ftc1lem4  26103  plyeq0lem  26272  plyn0mulidp  26347  aalioulem3  26400  aalioulem4  26401  aaliou3lem9  26416  ulmdvlem1  26465  itgulm  26473  radcnvlem1  26478  radcnvlem2  26479  dvradcnv  26486  abelthlem2  26497  abelthlem7  26503  tangtx  26572  tanregt0  26606  logdivlti  26687  logcnlem3  26711  logcnlem4  26712  logccv  26730  recxpcl  26742  cxpmul  26755  cxplt  26761  cxple2  26764  abscxpbnd  26820  lawcoslem1  26882  heron  26905  atans2  26998  efrlim  27036  o1cxp  27041  scvxcvx  27052  jensenlem2  27054  amgmlem  27056  fsumharmonic  27078  lgamgulmlem2  27096  lgamgulmlem3  27097  lgamgulmlem4  27098  lgamgulmlem5  27099  lgamgulmlem6  27100  relgamcl  27128  ftalem1  27139  ftalem2  27140  ftalem5  27143  basellem3  27149  basellem8  27154  chpub  27286  logfacubnd  27287  logfaclbnd  27288  logfacbnd3  27289  logexprlim  27291  perfectlem2  27296  bclbnd  27346  efexple  27347  bposlem1  27350  bposlem2  27351  bposlem6  27355  bposlem9  27358  lgsdilem  27390  gausslemma2dlem0c  27424  gausslemma2dlem2  27433  gausslemma2dlem3  27434  gausslemma2dlem6  27438  lgseisenlem4  27444  lgseisen  27445  lgsquadlem1  27446  lgsquadlem2  27447  2lgslem1a1  27455  2sqmod  27502  chebbnd1lem1  27535  chebbnd1lem3  27537  chtppilimlem1  27539  chpchtlim  27545  vmadivsum  27548  rplogsumlem1  27550  rpvmasumlem  27553  dchrisumlem2  27556  dchrisumlem3  27557  dchrmusum2  27560  dchrvmasumlem2  27564  dchrvmasumiflem1  27567  dchrisum0re  27579  dchrisum0lem1  27582  dirith2  27594  mulogsumlem  27597  mulogsum  27598  mulog2sumlem2  27601  vmalogdivsum2  27604  vmalogdivsum  27605  2vmadivsumlem  27606  logsqvma  27608  logsqvma2  27609  log2sumbnd  27610  selberglem2  27612  selberg  27614  selbergb  27615  selberg2lem  27616  selberg2b  27618  chpdifbndlem1  27619  chpdifbndlem2  27620  selberg3lem1  27623  selberg3lem2  27624  selberg3  27625  selberg4lem1  27626  selberg4  27627  pntrsumbnd2  27633  selberg3r  27635  selberg4r  27636  selberg34r  27637  pntsf  27639  pntsval2  27642  pntrlog2bndlem1  27643  pntrlog2bndlem2  27644  pntrlog2bndlem3  27645  pntrlog2bndlem4  27646  pntrlog2bndlem5  27647  pntrlog2bndlem6  27649  pntrlog2bnd  27650  pntpbnd1a  27651  pntpbnd1  27652  pntpbnd2  27653  pntibndlem2a  27656  pntibndlem2  27657  pntlemb  27663  pntlemr  27668  pntlemj  27669  pntlemf  27671  pntlemk  27672  pntlemo  27673  pntlem3  27675  ostth2lem1  27684  ostth2lem2  27700  ostth2lem3  27701  ostth2lem4  27702  ostth3  27704  ttgcontlem1  29087  brbtwn2  29108  colinearalglem4  29112  axsegconlem8  29127  axsegconlem9  29128  axsegconlem10  29129  ax5seglem3  29134  axpaschlem  29143  axpasch  29144  axeuclidlem  29165  numclwwlk5  30592  numclwwlk7  30595  smcnlem  30902  ubthlem2  31076  htthlem  31122  pjhthlem1  31596  cnlnadjlem7  32278  nmopcoadji  32306  branmfn  32310  leopnmid  32343  nexple  33037  constrremulcl  34066  constrmulcl  34070  cos9thpiminplylem1  34081  cos9thpinconstrlem1  34088  rmulccn  34227  xrge0iifhom  34236  dya2icoseg  34576  eulerpartlems  34659  eulerpartlemgc  34661  eulerpartlemb  34667  signsvtp  34879  reprgt  34917  breprexplemc  34928  circlemethhgt  34939  hgt750lemd  34944  logdivsqrle  34946  hgt750lem  34947  hgt750lemf  34949  hgt750lemb  34952  hgt750lema  34953  hgt750leme  34954  tgoldbachgtde  34956  resconn  35601  knoppcnlem2  36937  knoppcnlem4  36939  knoppcnlem10  36945  unbdqndv2lem1  36952  unbdqndv2lem2  36953  knoppndvlem1  36955  knoppndvlem11  36965  knoppndvlem12  36966  knoppndvlem14  36968  knoppndvlem15  36969  knoppndvlem17  36971  knoppndvlem18  36972  knoppndvlem19  36973  knoppndvlem20  36974  knoppndvlem21  36975  opnmbllem0  38160  itg2addnclem2  38176  itg2addnclem3  38177  iblmulc2nc  38189  itgmulc2nclem1  38190  ftc1cnnclem  38195  ftc1anclem3  38199  areacirclem4  38215  geomcau  38263  equivbnd  38294  bfplem1  38326  bfplem2  38327  bfp  38328  rrnequiv  38339  rrntotbnd  38340  lcmineqlem19  42669  lcmineqlem20  42670  lcmineqlem21  42671  lcmineqlem22  42672  3lexlogpow2ineq2  42681  dvrelogpow2b  42690  aks4d1p1p2  42692  aks4d1p1p4  42693  aks4d1p1p6  42695  aks4d1p1p7  42696  aks4d1p1p5  42697  aks4d1p1  42698  aks4d1p8d2  42707  aks4d1p8  42709  posbezout  42722  aks6d1c2lem4  42749  2np3bcnp1  42766  2ap1caineq  42767  aks6d1c6lem4  42795  aks6d1c7lem1  42802  aks6d1c7lem2  42803  resubdi  43010  remul02  43019  remul01  43021  remulinvcom  43047  rediveud  43057  redivcan3d  43062  redivrec2d  43074  rediv23d  43075  sn-0tie0  43078  renegmulnnass  43092  mulgt0con1d  43097  mulgt0con2d  43098  mulgt0b1d  43099  sn-ltmul2d  43100  mulgt0b2d  43105  sn-mulgt1d  43106  mulltgt0d  43109  mullt0b1d  43110  mullt0b2d  43111  sn-mullt0d  43112  sn-itrere  43115  sn-retire  43116  fltnltalem  43249  fltnlta  43250  3cubeslem2  43271  3cubeslem3r  43273  3cubeslem4  43275  irrapxlem1  43404  irrapxlem2  43405  irrapxlem3  43406  irrapxlem4  43407  irrapxlem5  43408  pellexlem2  43412  pellexlem6  43416  pell14qrgt0  43441  pell1qrge1  43452  pell1qrgaplem  43455  pellqrexplicit  43459  pellqrex  43461  rmspecsqrtnq  43488  rmxycomplete  43499  rmxypos  43529  ltrmynn0  43530  ltrmxnn0  43531  jm2.24nn  43541  jm2.17a  43542  jm2.17b  43543  jm2.17c  43544  jm2.27c  43589  jm3.1lem2  43600  areaquad  43798  sqrtcval  44222  resqrtval  44224  imsqrtval  44225  imo72b2lem0  44746  cvgdvgrat  44894  nzprmdif  44900  lt3addmuld  45885  fperiodmullem  45887  fperiodmul  45888  lt4addmuld  45890  xralrple2  45935  xralrple3  45954  ltmulneg  45972  fmul01  46161  fmuldfeqlem1  46163  fmul01lt1lem1  46165  sumnnodd  46211  ltmod  46217  0ellimcdiv  46228  limclner  46230  dvdivbd  46502  dvbdfbdioolem2  46508  dvbdfbdioo  46509  ioodvbdlimc1lem1  46510  ioodvbdlimc1lem2  46511  ioodvbdlimc2lem  46513  stoweidlem1  46580  stoweidlem11  46590  stoweidlem13  46592  stoweidlem14  46593  stoweidlem16  46595  stoweidlem17  46596  stoweidlem22  46601  stoweidlem24  46603  stoweidlem25  46604  stoweidlem26  46605  stoweidlem30  46609  stoweidlem34  46613  stoweidlem36  46615  stoweidlem49  46628  stoweidlem59  46638  stoweidlem60  46639  wallispilem4  46647  wallispilem5  46648  wallispi  46649  wallispi2lem1  46650  wallispi2  46652  stirlinglem1  46653  stirlinglem3  46655  stirlinglem5  46657  stirlinglem6  46658  stirlinglem7  46659  stirlinglem10  46662  stirlinglem11  46663  stirlinglem12  46664  stirlinglem15  46667  stirlingr  46669  dirker2re  46671  dirkerval2  46673  dirkerre  46674  dirkertrigeqlem1  46677  dirkertrigeqlem2  46678  dirkeritg  46681  dirkercncflem2  46683  dirkercncflem4  46685  fourierdlem4  46690  fourierdlem5  46691  fourierdlem6  46692  fourierdlem7  46693  fourierdlem16  46702  fourierdlem18  46704  fourierdlem19  46705  fourierdlem21  46707  fourierdlem22  46708  fourierdlem26  46712  fourierdlem35  46721  fourierdlem39  46725  fourierdlem41  46727  fourierdlem42  46728  fourierdlem43  46729  fourierdlem48  46733  fourierdlem49  46734  fourierdlem51  46736  fourierdlem55  46740  fourierdlem56  46741  fourierdlem57  46742  fourierdlem58  46743  fourierdlem62  46747  fourierdlem63  46748  fourierdlem64  46749  fourierdlem65  46750  fourierdlem66  46751  fourierdlem67  46752  fourierdlem68  46753  fourierdlem71  46756  fourierdlem72  46757  fourierdlem73  46758  fourierdlem76  46761  fourierdlem77  46762  fourierdlem78  46763  fourierdlem83  46768  fourierdlem84  46769  fourierdlem87  46772  fourierdlem88  46773  fourierdlem89  46774  fourierdlem90  46775  fourierdlem91  46776  fourierdlem94  46779  fourierdlem95  46780  fourierdlem97  46782  fourierdlem103  46788  fourierdlem104  46789  fourierdlem112  46797  fourierdlem113  46798  sqwvfoura  46807  sqwvfourb  46808  fouriersw  46810  etransclem23  46836  etransclem48  46861  rrndistlt  46869  hoidmvlelem1  47174  hoidmvlelem2  47175  hoidmvlelem4  47177  smfmullem1  47370  smfmullem2  47371  smfmullem3  47372  smfmul  47374  2timesltsqm1  47978  fmtno4prmfac  48186  lighneallem4a  48222  requad01  48248  requad1  48249  requad2  48250  perfectALTVlem2  48349  gpg3kgrtriexlem1  48710  gpg3kgrtriexlem4  48713  gpg3kgrtriexlem6  48715  ply1mulgsumlem2  49014  digvalnn0  49226  dignn0fr  49228  dig2nn0  49238  affinecomb1  49329  rrx2linest2  49371  line2  49379  itsclc0lem1  49383  itsclc0lem2  49384  itsclc0lem3  49385  itscnhlc0yqe  49386  itsclc0yqsollem2  49390  itsclc0yqsol  49391  itscnhlc0xyqsol  49392  itsclc0xyqsolr  49396  itsclinecirc0  49400  itsclinecirc0b  49401  itsclinecirc0in  49402  itsclquadb  49403  itsclquadeu  49404  2itscp  49408  itscnhlinecirc02plem1  49409  itscnhlinecirc02p  49412  inlinecirc02plem  49413  amgmwlem  50428