Theorem remulcld 11142

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

Syntax hints:   → wi 4   ∈ wcel 2111  (class class class)co 7346  ℝcr 11005   · cmul 11011

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

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

This theorem is referenced by:  mulge0  11635  msqge0  11638  redivcl  11840  prodgt0  11968  ltmul1a  11970  ltmul1  11971  ltmuldiv  11995  lt2msq1  12006  lt2msq  12007  le2msq  12022  msq11  12023  supmul1  12091  supmullem2  12093  supmul  12094  div4p1lem1div2  12376  mul2lt0rlt0  12994  mul2lt0bi  12998  prodge0rd  12999  ge2halflem1  13007  qbtwnre  13098  xmulneg1  13168  xmulf  13171  lincmb01cmp  13395  iccf1o  13396  flmulnn0  13731  flhalf  13734  modcl  13777  mod0  13780  modge0  13783  modmulnn  13793  mulp1mod1  13818  muladdmod  13819  2txmodxeq0  13838  modaddmulmod  13845  moddi  13846  modsubdir  13847  modirr  13849  addmodlteq  13853  bernneq  14136  bernneq3  14138  expnbnd  14139  expmulnbnd  14142  discr1  14146  discr  14147  faclbnd  14197  faclbnd6  14206  remullem  15035  01sqrexlem7  15155  sqrtmul  15166  abstri  15238  sqreulem  15267  bhmafibid1  15375  mulcn2  15503  reccn2  15504  o1rlimmul  15526  lo1mul  15535  iseraltlem2  15590  iseraltlem3  15591  iseralt  15592  o1fsum  15720  cvgcmpce  15725  climcndslem1  15756  climcndslem2  15757  climcnds  15758  geomulcvg  15783  cvgrat  15790  mertenslem1  15791  fprodge1  15902  eftlub  16018  sin02gt0  16101  eirrlem  16113  bitsp1o  16344  2mulprm  16604  isprm5  16618  modprm0  16717  prmreclem3  16830  prmreclem4  16831  prmreclem5  16832  2expltfac  17004  metss2lem  24426  nlmvscnlem2  24600  nrginvrcnlem  24606  nmoco  24652  nmotri  24654  nghmcn  24660  icopnfhmeo  24868  nmoleub2lem3  25042  ipcau2  25161  tcphcphlem1  25162  ipcnlem2  25171  rrxcph  25319  csbren  25326  trirn  25327  pjthlem1  25364  opnmbllem  25529  vitalilem4  25539  itg1val2  25612  itg1cl  25613  itg1ge0  25614  itg1addlem4  25627  itg1mulc  25632  itg1ge0a  25639  itg1climres  25642  mbfi1fseqlem1  25643  mbfi1fseqlem3  25645  mbfi1fseqlem4  25646  mbfi1fseqlem5  25647  mbfi1fseqlem6  25648  itg2const2  25669  itg2mulclem  25674  itg2mulc  25675  itg2monolem1  25678  itg2monolem3  25680  itg2cnlem2  25690  iblconst  25746  iblmulc2  25759  itgmulc2lem1  25760  itgmulc2lem2  25761  bddmulibl  25767  bddiblnc  25770  dveflem  25910  cmvth  25922  cmvthOLD  25923  dvlip  25925  dvlipcn  25926  dvivthlem1  25940  lhop1lem  25945  dvcvx  25952  dvfsumlem2  25960  dvfsumlem2OLD  25961  dvfsumlem3  25962  dvfsumlem4  25963  dvfsum2  25968  ftc1lem4  25973  plyeq0lem  26142  aalioulem3  26269  aalioulem4  26270  aaliou3lem9  26285  ulmdvlem1  26336  itgulm  26344  radcnvlem1  26349  radcnvlem2  26350  dvradcnv  26357  abelthlem2  26369  abelthlem7  26375  tangtx  26441  tanregt0  26475  logdivlti  26556  logcnlem3  26580  logcnlem4  26581  logccv  26599  recxpcl  26611  cxpmul  26624  cxplt  26630  cxple2  26633  abscxpbnd  26690  lawcoslem1  26752  heron  26775  atans2  26868  efrlim  26906  efrlimOLD  26907  o1cxp  26912  scvxcvx  26923  jensenlem2  26925  amgmlem  26927  fsumharmonic  26949  lgamgulmlem2  26967  lgamgulmlem3  26968  lgamgulmlem4  26969  lgamgulmlem5  26970  lgamgulmlem6  26971  relgamcl  26999  ftalem1  27010  ftalem2  27011  ftalem5  27014  basellem3  27020  basellem8  27025  chpub  27158  logfacubnd  27159  logfaclbnd  27160  logfacbnd3  27161  logexprlim  27163  perfectlem2  27168  bclbnd  27218  efexple  27219  bposlem1  27222  bposlem2  27223  bposlem6  27227  bposlem9  27230  lgsdilem  27262  gausslemma2dlem0c  27296  gausslemma2dlem2  27305  gausslemma2dlem3  27306  gausslemma2dlem6  27310  lgseisenlem4  27316  lgseisen  27317  lgsquadlem1  27318  lgsquadlem2  27319  2lgslem1a1  27327  2sqmod  27374  chebbnd1lem1  27407  chebbnd1lem3  27409  chtppilimlem1  27411  chpchtlim  27417  vmadivsum  27420  rplogsumlem1  27422  rpvmasumlem  27425  dchrisumlem2  27428  dchrisumlem3  27429  dchrmusum2  27432  dchrvmasumlem2  27436  dchrvmasumiflem1  27439  dchrisum0re  27451  dchrisum0lem1  27454  dirith2  27466  mulogsumlem  27469  mulogsum  27470  mulog2sumlem2  27473  vmalogdivsum2  27476  vmalogdivsum  27477  2vmadivsumlem  27478  logsqvma  27480  logsqvma2  27481  log2sumbnd  27482  selberglem2  27484  selberg  27486  selbergb  27487  selberg2lem  27488  selberg2b  27490  chpdifbndlem1  27491  chpdifbndlem2  27492  selberg3lem1  27495  selberg3lem2  27496  selberg3  27497  selberg4lem1  27498  selberg4  27499  pntrsumbnd2  27505  selberg3r  27507  selberg4r  27508  selberg34r  27509  pntsf  27511  pntsval2  27514  pntrlog2bndlem1  27515  pntrlog2bndlem2  27516  pntrlog2bndlem3  27517  pntrlog2bndlem4  27518  pntrlog2bndlem5  27519  pntrlog2bndlem6  27521  pntrlog2bnd  27522  pntpbnd1a  27523  pntpbnd1  27524  pntpbnd2  27525  pntibndlem2a  27528  pntibndlem2  27529  pntlemb  27535  pntlemr  27540  pntlemj  27541  pntlemf  27543  pntlemk  27544  pntlemo  27545  pntlem3  27547  ostth2lem1  27556  ostth2lem2  27572  ostth2lem3  27573  ostth2lem4  27574  ostth3  27576  ttgcontlem1  28863  brbtwn2  28883  colinearalglem4  28887  axsegconlem8  28902  axsegconlem9  28903  axsegconlem10  28904  ax5seglem3  28909  axpaschlem  28918  axpasch  28919  axeuclidlem  28940  numclwwlk5  30368  numclwwlk7  30371  smcnlem  30677  ubthlem2  30851  htthlem  30897  pjhthlem1  31371  cnlnadjlem7  32053  nmopcoadji  32081  branmfn  32085  leopnmid  32118  nexple  32827  constrremulcl  33780  constrmulcl  33784  cos9thpiminplylem1  33795  cos9thpinconstrlem1  33802  rmulccn  33941  xrge0iifhom  33950  dya2icoseg  34290  eulerpartlems  34373  eulerpartlemgc  34375  eulerpartlemb  34381  plymulx0  34560  signsvtp  34596  reprgt  34634  breprexplemc  34645  circlemethhgt  34656  hgt750lemd  34661  logdivsqrle  34663  hgt750lem  34664  hgt750lemf  34666  hgt750lemb  34669  hgt750lema  34670  hgt750leme  34671  tgoldbachgtde  34673  resconn  35290  knoppcnlem2  36538  knoppcnlem4  36540  knoppcnlem10  36546  unbdqndv2lem1  36553  unbdqndv2lem2  36554  knoppndvlem1  36556  knoppndvlem11  36566  knoppndvlem12  36567  knoppndvlem14  36569  knoppndvlem15  36570  knoppndvlem17  36572  knoppndvlem18  36573  knoppndvlem19  36574  knoppndvlem20  36575  knoppndvlem21  36576  opnmbllem0  37695  itg2addnclem2  37711  itg2addnclem3  37712  iblmulc2nc  37724  itgmulc2nclem1  37725  ftc1cnnclem  37730  ftc1anclem3  37734  areacirclem4  37750  geomcau  37798  equivbnd  37829  bfplem1  37861  bfplem2  37862  bfp  37863  rrnequiv  37874  rrntotbnd  37875  lcmineqlem19  42139  lcmineqlem20  42140  lcmineqlem21  42141  lcmineqlem22  42142  3lexlogpow2ineq2  42151  dvrelogpow2b  42160  aks4d1p1p2  42162  aks4d1p1p4  42163  aks4d1p1p6  42165  aks4d1p1p7  42166  aks4d1p1p5  42167  aks4d1p1  42168  aks4d1p8d2  42177  aks4d1p8  42179  posbezout  42192  aks6d1c2lem4  42219  2np3bcnp1  42236  2ap1caineq  42237  aks6d1c6lem4  42265  aks6d1c7lem1  42272  aks6d1c7lem2  42273  resubdi  42488  remul02  42497  remul01  42499  remulinvcom  42525  rediveud  42535  redivcan3d  42539  sn-0tie0  42543  renegmulnnass  42557  mulgt0con1d  42562  mulgt0con2d  42563  mulgt0b1d  42564  sn-ltmul2d  42565  mulgt0b2d  42570  sn-mulgt1d  42571  mulltgt0d  42574  mullt0b1d  42575  mullt0b2d  42576  sn-mullt0d  42577  sn-itrere  42580  sn-retire  42581  fltnltalem  42754  fltnlta  42755  3cubeslem2  42777  3cubeslem3r  42779  3cubeslem4  42781  irrapxlem1  42914  irrapxlem2  42915  irrapxlem3  42916  irrapxlem4  42917  irrapxlem5  42918  pellexlem2  42922  pellexlem6  42926  pell14qrgt0  42951  pell1qrge1  42962  pell1qrgaplem  42965  pellqrexplicit  42969  pellqrex  42971  rmspecsqrtnq  42998  rmxycomplete  43009  rmxypos  43039  ltrmynn0  43040  ltrmxnn0  43041  jm2.24nn  43051  jm2.17a  43052  jm2.17b  43053  jm2.17c  43054  jm2.27c  43099  jm3.1lem2  43110  areaquad  43308  sqrtcval  43733  resqrtval  43735  imsqrtval  43736  imo72b2lem0  44257  cvgdvgrat  44405  nzprmdif  44411  lt3addmuld  45401  fperiodmullem  45403  fperiodmul  45404  lt4addmuld  45406  xralrple2  45452  xralrple3  45471  ltmulneg  45489  fmul01  45679  fmuldfeqlem1  45681  fmul01lt1lem1  45683  sumnnodd  45729  ltmod  45735  0ellimcdiv  45746  limclner  45748  dvdivbd  46020  dvbdfbdioolem2  46026  dvbdfbdioo  46027  ioodvbdlimc1lem1  46028  ioodvbdlimc1lem2  46029  ioodvbdlimc2lem  46031  stoweidlem1  46098  stoweidlem11  46108  stoweidlem13  46110  stoweidlem14  46111  stoweidlem16  46113  stoweidlem17  46114  stoweidlem22  46119  stoweidlem24  46121  stoweidlem25  46122  stoweidlem26  46123  stoweidlem30  46127  stoweidlem34  46131  stoweidlem36  46133  stoweidlem49  46146  stoweidlem59  46156  stoweidlem60  46157  wallispilem4  46165  wallispilem5  46166  wallispi  46167  wallispi2lem1  46168  wallispi2  46170  stirlinglem1  46171  stirlinglem3  46173  stirlinglem5  46175  stirlinglem6  46176  stirlinglem7  46177  stirlinglem10  46180  stirlinglem11  46181  stirlinglem12  46182  stirlinglem15  46185  stirlingr  46187  dirker2re  46189  dirkerval2  46191  dirkerre  46192  dirkertrigeqlem1  46195  dirkertrigeqlem2  46196  dirkeritg  46199  dirkercncflem2  46201  dirkercncflem4  46203  fourierdlem4  46208  fourierdlem5  46209  fourierdlem6  46210  fourierdlem7  46211  fourierdlem16  46220  fourierdlem18  46222  fourierdlem19  46223  fourierdlem21  46225  fourierdlem22  46226  fourierdlem26  46230  fourierdlem35  46239  fourierdlem39  46243  fourierdlem41  46245  fourierdlem42  46246  fourierdlem43  46247  fourierdlem48  46251  fourierdlem49  46252  fourierdlem51  46254  fourierdlem55  46258  fourierdlem56  46259  fourierdlem57  46260  fourierdlem58  46261  fourierdlem62  46265  fourierdlem63  46266  fourierdlem64  46267  fourierdlem65  46268  fourierdlem66  46269  fourierdlem67  46270  fourierdlem68  46271  fourierdlem71  46274  fourierdlem72  46275  fourierdlem73  46276  fourierdlem76  46279  fourierdlem77  46280  fourierdlem78  46281  fourierdlem83  46286  fourierdlem84  46287  fourierdlem87  46290  fourierdlem88  46291  fourierdlem89  46292  fourierdlem90  46293  fourierdlem91  46294  fourierdlem94  46297  fourierdlem95  46298  fourierdlem97  46300  fourierdlem103  46306  fourierdlem104  46307  fourierdlem112  46315  fourierdlem113  46316  sqwvfoura  46325  sqwvfourb  46326  fouriersw  46328  etransclem23  46354  etransclem48  46379  rrndistlt  46387  hoidmvlelem1  46692  hoidmvlelem2  46693  hoidmvlelem4  46695  smfmullem1  46888  smfmullem2  46889  smfmullem3  46890  smfmul  46892  fmtno4prmfac  47671  lighneallem4a  47707  requad01  47720  requad1  47721  requad2  47722  perfectALTVlem2  47821  gpg3kgrtriexlem1  48182  gpg3kgrtriexlem4  48185  gpg3kgrtriexlem6  48187  ply1mulgsumlem2  48487  digvalnn0  48699  dignn0fr  48701  dig2nn0  48711  affinecomb1  48802  rrx2linest2  48844  line2  48852  itsclc0lem1  48856  itsclc0lem2  48857  itsclc0lem3  48858  itscnhlc0yqe  48859  itsclc0yqsollem2  48863  itsclc0yqsol  48864  itscnhlc0xyqsol  48865  itsclc0xyqsolr  48869  itsclinecirc0  48873  itsclinecirc0b  48874  itsclinecirc0in  48875  itsclquadb  48876  itsclquadeu  48877  2itscp  48881  itscnhlinecirc02plem1  48882  itscnhlinecirc02p  48885  inlinecirc02plem  48886  amgmwlem  49902