Theorem remulcld 11320

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7448  ℝcr 11183   · cmul 11189

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

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  mulge0  11808  msqge0  11811  redivcl  12013  prodgt0  12141  ltmul1a  12143  ltmul1  12144  ltmuldiv  12168  lt2msq1  12179  lt2msq  12180  le2msq  12195  msq11  12196  supmul1  12264  supmullem2  12266  supmul  12267  div4p1lem1div2  12548  mul2lt0rlt0  13159  mul2lt0bi  13163  prodge0rd  13164  qbtwnre  13261  xmulneg1  13331  xmulf  13334  lincmb01cmp  13555  iccf1o  13556  flmulnn0  13878  flhalf  13881  modcl  13924  mod0  13927  modge0  13930  modmulnn  13940  mulp1mod1  13963  2txmodxeq0  13982  modaddmulmod  13989  moddi  13990  modsubdir  13991  modirr  13993  addmodlteq  13997  bernneq  14278  bernneq3  14280  expnbnd  14281  expmulnbnd  14284  discr1  14288  discr  14289  faclbnd  14339  faclbnd6  14348  remullem  15177  01sqrexlem7  15297  sqrtmul  15308  abstri  15379  sqreulem  15408  bhmafibid1  15514  mulcn2  15642  reccn2  15643  o1rlimmul  15665  lo1mul  15674  iseraltlem2  15731  iseraltlem3  15732  iseralt  15733  o1fsum  15861  cvgcmpce  15866  climcndslem1  15897  climcndslem2  15898  climcnds  15899  geomulcvg  15924  cvgrat  15931  mertenslem1  15932  fprodge1  16043  eftlub  16157  sin02gt0  16240  eirrlem  16252  bitsp1o  16479  2mulprm  16740  isprm5  16754  modprm0  16852  prmreclem3  16965  prmreclem4  16966  prmreclem5  16967  2expltfac  17140  metss2lem  24545  nlmvscnlem2  24727  nrginvrcnlem  24733  nmoco  24779  nmotri  24781  nghmcn  24787  icopnfhmeo  24993  nmoleub2lem3  25167  ipcau2  25287  tcphcphlem1  25288  ipcnlem2  25297  rrxcph  25445  csbren  25452  trirn  25453  pjthlem1  25490  opnmbllem  25655  vitalilem4  25665  itg1val2  25738  itg1cl  25739  itg1ge0  25740  itg1addlem4  25753  itg1addlem4OLD  25754  itg1mulc  25759  itg1ge0a  25766  itg1climres  25769  mbfi1fseqlem1  25770  mbfi1fseqlem3  25772  mbfi1fseqlem4  25773  mbfi1fseqlem5  25774  mbfi1fseqlem6  25775  itg2const2  25796  itg2mulclem  25801  itg2mulc  25802  itg2monolem1  25805  itg2monolem3  25807  itg2cnlem2  25817  iblconst  25873  iblmulc2  25886  itgmulc2lem1  25887  itgmulc2lem2  25888  bddmulibl  25894  bddiblnc  25897  dveflem  26037  cmvth  26049  cmvthOLD  26050  dvlip  26052  dvlipcn  26053  dvivthlem1  26067  lhop1lem  26072  dvcvx  26079  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsumlem3  26089  dvfsumlem4  26090  dvfsum2  26095  ftc1lem4  26100  plyeq0lem  26269  aalioulem3  26394  aalioulem4  26395  aaliou3lem9  26410  ulmdvlem1  26461  itgulm  26469  radcnvlem1  26474  radcnvlem2  26475  dvradcnv  26482  abelthlem2  26494  abelthlem7  26500  tangtx  26565  tanregt0  26599  logdivlti  26680  logcnlem3  26704  logcnlem4  26705  logccv  26723  recxpcl  26735  cxpmul  26748  cxplt  26754  cxple2  26757  abscxpbnd  26814  lawcoslem1  26876  heron  26899  atans2  26992  efrlim  27030  efrlimOLD  27031  o1cxp  27036  scvxcvx  27047  jensenlem2  27049  amgmlem  27051  fsumharmonic  27073  lgamgulmlem2  27091  lgamgulmlem3  27092  lgamgulmlem4  27093  lgamgulmlem5  27094  lgamgulmlem6  27095  relgamcl  27123  ftalem1  27134  ftalem2  27135  ftalem5  27138  basellem3  27144  basellem8  27149  chpub  27282  logfacubnd  27283  logfaclbnd  27284  logfacbnd3  27285  logexprlim  27287  perfectlem2  27292  bclbnd  27342  efexple  27343  bposlem1  27346  bposlem2  27347  bposlem6  27351  bposlem9  27354  lgsdilem  27386  gausslemma2dlem0c  27420  gausslemma2dlem2  27429  gausslemma2dlem3  27430  gausslemma2dlem6  27434  lgseisenlem4  27440  lgseisen  27441  lgsquadlem1  27442  lgsquadlem2  27443  2lgslem1a1  27451  2sqmod  27498  chebbnd1lem1  27531  chebbnd1lem3  27533  chtppilimlem1  27535  chpchtlim  27541  vmadivsum  27544  rplogsumlem1  27546  rpvmasumlem  27549  dchrisumlem2  27552  dchrisumlem3  27553  dchrmusum2  27556  dchrvmasumlem2  27560  dchrvmasumiflem1  27563  dchrisum0re  27575  dchrisum0lem1  27578  dirith2  27590  mulogsumlem  27593  mulogsum  27594  mulog2sumlem2  27597  vmalogdivsum2  27600  vmalogdivsum  27601  2vmadivsumlem  27602  logsqvma  27604  logsqvma2  27605  log2sumbnd  27606  selberglem2  27608  selberg  27610  selbergb  27611  selberg2lem  27612  selberg2b  27614  chpdifbndlem1  27615  chpdifbndlem2  27616  selberg3lem1  27619  selberg3lem2  27620  selberg3  27621  selberg4lem1  27622  selberg4  27623  pntrsumbnd2  27629  selberg3r  27631  selberg4r  27632  selberg34r  27633  pntsf  27635  pntsval2  27638  pntrlog2bndlem1  27639  pntrlog2bndlem2  27640  pntrlog2bndlem3  27641  pntrlog2bndlem4  27642  pntrlog2bndlem5  27643  pntrlog2bndlem6  27645  pntrlog2bnd  27646  pntpbnd1a  27647  pntpbnd1  27648  pntpbnd2  27649  pntibndlem2a  27652  pntibndlem2  27653  pntlemb  27659  pntlemr  27664  pntlemj  27665  pntlemf  27667  pntlemk  27668  pntlemo  27669  pntlem3  27671  ostth2lem1  27680  ostth2lem2  27696  ostth2lem3  27697  ostth2lem4  27698  ostth3  27700  ttgcontlem1  28917  brbtwn2  28938  colinearalglem4  28942  axsegconlem8  28957  axsegconlem9  28958  axsegconlem10  28959  ax5seglem3  28964  axpaschlem  28973  axpasch  28974  axeuclidlem  28995  numclwwlk5  30420  numclwwlk7  30423  smcnlem  30729  ubthlem2  30903  htthlem  30949  pjhthlem1  31423  cnlnadjlem7  32105  nmopcoadji  32133  branmfn  32137  leopnmid  32170  rmulccn  33874  xrge0iifhom  33883  nexple  33973  dya2icoseg  34242  eulerpartlems  34325  eulerpartlemgc  34327  eulerpartlemb  34333  plymulx0  34524  signsvtp  34560  reprgt  34598  breprexplemc  34609  circlemethhgt  34620  hgt750lemd  34625  logdivsqrle  34627  hgt750lem  34628  hgt750lemf  34630  hgt750lemb  34633  hgt750lema  34634  hgt750leme  34635  tgoldbachgtde  34637  resconn  35214  knoppcnlem2  36460  knoppcnlem4  36462  knoppcnlem10  36468  unbdqndv2lem1  36475  unbdqndv2lem2  36476  knoppndvlem1  36478  knoppndvlem11  36488  knoppndvlem12  36489  knoppndvlem14  36491  knoppndvlem15  36492  knoppndvlem17  36494  knoppndvlem18  36495  knoppndvlem19  36496  knoppndvlem20  36497  knoppndvlem21  36498  opnmbllem0  37616  itg2addnclem2  37632  itg2addnclem3  37633  iblmulc2nc  37645  itgmulc2nclem1  37646  ftc1cnnclem  37651  ftc1anclem3  37655  areacirclem4  37671  geomcau  37719  equivbnd  37750  bfplem1  37782  bfplem2  37783  bfp  37784  rrnequiv  37795  rrntotbnd  37796  lcmineqlem19  42004  lcmineqlem20  42005  lcmineqlem21  42006  lcmineqlem22  42007  3lexlogpow2ineq2  42016  dvrelogpow2b  42025  aks4d1p1p2  42027  aks4d1p1p4  42028  aks4d1p1p6  42030  aks4d1p1p7  42031  aks4d1p1p5  42032  aks4d1p1  42033  aks4d1p8d2  42042  aks4d1p8  42044  posbezout  42057  aks6d1c2lem4  42084  2np3bcnp1  42101  2ap1caineq  42102  aks6d1c6lem4  42130  aks6d1c7lem1  42137  aks6d1c7lem2  42138  resubdi  42372  remul02  42381  remul01  42383  remulinvcom  42408  sn-0tie0  42415  renegmulnnass  42429  mulgt0con1d  42434  mulgt0con2d  42435  mulgt0b2d  42436  sn-ltmul2d  42437  sn-mulgt1d  42441  sn-inelr  42443  sn-itrere  42444  sn-retire  42445  fltnltalem  42617  fltnlta  42618  3cubeslem2  42641  3cubeslem3r  42643  3cubeslem4  42645  irrapxlem1  42778  irrapxlem2  42779  irrapxlem3  42780  irrapxlem4  42781  irrapxlem5  42782  pellexlem2  42786  pellexlem6  42790  pell14qrgt0  42815  pell1qrge1  42826  pell1qrgaplem  42829  pellqrexplicit  42833  pellqrex  42835  rmspecsqrtnq  42862  rmxycomplete  42874  rmxypos  42904  ltrmynn0  42905  ltrmxnn0  42906  jm2.24nn  42916  jm2.17a  42917  jm2.17b  42918  jm2.17c  42919  jm2.27c  42964  jm3.1lem2  42975  areaquad  43177  sqrtcval  43603  resqrtval  43605  imsqrtval  43606  imo72b2lem0  44127  cvgdvgrat  44282  nzprmdif  44288  lt3addmuld  45216  fperiodmullem  45218  fperiodmul  45219  lt4addmuld  45221  xralrple2  45269  xralrple3  45289  ltmulneg  45307  fmul01  45501  fmuldfeqlem1  45503  fmul01lt1lem1  45505  sumnnodd  45551  ltmod  45559  0ellimcdiv  45570  limclner  45572  dvdivbd  45844  dvbdfbdioolem2  45850  dvbdfbdioo  45851  ioodvbdlimc1lem1  45852  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  stoweidlem1  45922  stoweidlem11  45932  stoweidlem13  45934  stoweidlem14  45935  stoweidlem16  45937  stoweidlem17  45938  stoweidlem22  45943  stoweidlem24  45945  stoweidlem25  45946  stoweidlem26  45947  stoweidlem30  45951  stoweidlem34  45955  stoweidlem36  45957  stoweidlem49  45970  stoweidlem59  45980  stoweidlem60  45981  wallispilem4  45989  wallispilem5  45990  wallispi  45991  wallispi2lem1  45992  wallispi2  45994  stirlinglem1  45995  stirlinglem3  45997  stirlinglem5  45999  stirlinglem6  46000  stirlinglem7  46001  stirlinglem10  46004  stirlinglem11  46005  stirlinglem12  46006  stirlinglem15  46009  stirlingr  46011  dirker2re  46013  dirkerval2  46015  dirkerre  46016  dirkertrigeqlem1  46019  dirkertrigeqlem2  46020  dirkeritg  46023  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem4  46032  fourierdlem5  46033  fourierdlem6  46034  fourierdlem7  46035  fourierdlem16  46044  fourierdlem18  46046  fourierdlem19  46047  fourierdlem21  46049  fourierdlem22  46050  fourierdlem26  46054  fourierdlem35  46063  fourierdlem39  46067  fourierdlem41  46069  fourierdlem42  46070  fourierdlem43  46071  fourierdlem48  46075  fourierdlem49  46076  fourierdlem51  46078  fourierdlem55  46082  fourierdlem56  46083  fourierdlem57  46084  fourierdlem58  46085  fourierdlem62  46089  fourierdlem63  46090  fourierdlem64  46091  fourierdlem65  46092  fourierdlem66  46093  fourierdlem67  46094  fourierdlem68  46095  fourierdlem71  46098  fourierdlem72  46099  fourierdlem73  46100  fourierdlem76  46103  fourierdlem77  46104  fourierdlem78  46105  fourierdlem83  46110  fourierdlem84  46111  fourierdlem87  46114  fourierdlem88  46115  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem94  46121  fourierdlem95  46122  fourierdlem97  46124  fourierdlem103  46130  fourierdlem104  46131  fourierdlem112  46139  fourierdlem113  46140  sqwvfoura  46149  sqwvfourb  46150  fouriersw  46152  etransclem23  46178  etransclem48  46203  rrndistlt  46211  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem4  46519  smfmullem1  46712  smfmullem2  46713  smfmullem3  46714  smfmul  46716  fmtno4prmfac  47446  lighneallem4a  47482  requad01  47495  requad1  47496  requad2  47497  perfectALTVlem2  47596  ply1mulgsumlem2  48116  digvalnn0  48333  dignn0fr  48335  dig2nn0  48345  affinecomb1  48436  rrx2linest2  48478  line2  48486  itsclc0lem1  48490  itsclc0lem2  48491  itsclc0lem3  48492  itscnhlc0yqe  48493  itsclc0yqsollem2  48497  itsclc0yqsol  48498  itscnhlc0xyqsol  48499  itsclc0xyqsolr  48503  itsclinecirc0  48507  itsclinecirc0b  48508  itsclinecirc0in  48509  itsclquadb  48510  itsclquadeu  48511  2itscp  48515  itscnhlinecirc02plem1  48516  itscnhlinecirc02p  48519  inlinecirc02plem  48520  amgmwlem  48896