Theorem remulcld 11291

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7431  ℝcr 11154   · cmul 11160

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

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

This theorem is referenced by:  mulge0  11781  msqge0  11784  redivcl  11986  prodgt0  12114  ltmul1a  12116  ltmul1  12117  ltmuldiv  12141  lt2msq1  12152  lt2msq  12153  le2msq  12168  msq11  12169  supmul1  12237  supmullem2  12239  supmul  12240  div4p1lem1div2  12521  mul2lt0rlt0  13137  mul2lt0bi  13141  prodge0rd  13142  ge2halflem1  13150  qbtwnre  13241  xmulneg1  13311  xmulf  13314  lincmb01cmp  13535  iccf1o  13536  flmulnn0  13867  flhalf  13870  modcl  13913  mod0  13916  modge0  13919  modmulnn  13929  mulp1mod1  13952  muladdmod  13953  2txmodxeq0  13972  modaddmulmod  13979  moddi  13980  modsubdir  13981  modirr  13983  addmodlteq  13987  bernneq  14268  bernneq3  14270  expnbnd  14271  expmulnbnd  14274  discr1  14278  discr  14279  faclbnd  14329  faclbnd6  14338  remullem  15167  01sqrexlem7  15287  sqrtmul  15298  abstri  15369  sqreulem  15398  bhmafibid1  15504  mulcn2  15632  reccn2  15633  o1rlimmul  15655  lo1mul  15664  iseraltlem2  15719  iseraltlem3  15720  iseralt  15721  o1fsum  15849  cvgcmpce  15854  climcndslem1  15885  climcndslem2  15886  climcnds  15887  geomulcvg  15912  cvgrat  15919  mertenslem1  15920  fprodge1  16031  eftlub  16145  sin02gt0  16228  eirrlem  16240  bitsp1o  16470  2mulprm  16730  isprm5  16744  modprm0  16843  prmreclem3  16956  prmreclem4  16957  prmreclem5  16958  2expltfac  17130  metss2lem  24524  nlmvscnlem2  24706  nrginvrcnlem  24712  nmoco  24758  nmotri  24760  nghmcn  24766  icopnfhmeo  24974  nmoleub2lem3  25148  ipcau2  25268  tcphcphlem1  25269  ipcnlem2  25278  rrxcph  25426  csbren  25433  trirn  25434  pjthlem1  25471  opnmbllem  25636  vitalilem4  25646  itg1val2  25719  itg1cl  25720  itg1ge0  25721  itg1addlem4  25734  itg1mulc  25739  itg1ge0a  25746  itg1climres  25749  mbfi1fseqlem1  25750  mbfi1fseqlem3  25752  mbfi1fseqlem4  25753  mbfi1fseqlem5  25754  mbfi1fseqlem6  25755  itg2const2  25776  itg2mulclem  25781  itg2mulc  25782  itg2monolem1  25785  itg2monolem3  25787  itg2cnlem2  25797  iblconst  25853  iblmulc2  25866  itgmulc2lem1  25867  itgmulc2lem2  25868  bddmulibl  25874  bddiblnc  25877  dveflem  26017  cmvth  26029  cmvthOLD  26030  dvlip  26032  dvlipcn  26033  dvivthlem1  26047  lhop1lem  26052  dvcvx  26059  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumlem3  26069  dvfsumlem4  26070  dvfsum2  26075  ftc1lem4  26080  plyeq0lem  26249  aalioulem3  26376  aalioulem4  26377  aaliou3lem9  26392  ulmdvlem1  26443  itgulm  26451  radcnvlem1  26456  radcnvlem2  26457  dvradcnv  26464  abelthlem2  26476  abelthlem7  26482  tangtx  26547  tanregt0  26581  logdivlti  26662  logcnlem3  26686  logcnlem4  26687  logccv  26705  recxpcl  26717  cxpmul  26730  cxplt  26736  cxple2  26739  abscxpbnd  26796  lawcoslem1  26858  heron  26881  atans2  26974  efrlim  27012  efrlimOLD  27013  o1cxp  27018  scvxcvx  27029  jensenlem2  27031  amgmlem  27033  fsumharmonic  27055  lgamgulmlem2  27073  lgamgulmlem3  27074  lgamgulmlem4  27075  lgamgulmlem5  27076  lgamgulmlem6  27077  relgamcl  27105  ftalem1  27116  ftalem2  27117  ftalem5  27120  basellem3  27126  basellem8  27131  chpub  27264  logfacubnd  27265  logfaclbnd  27266  logfacbnd3  27267  logexprlim  27269  perfectlem2  27274  bclbnd  27324  efexple  27325  bposlem1  27328  bposlem2  27329  bposlem6  27333  bposlem9  27336  lgsdilem  27368  gausslemma2dlem0c  27402  gausslemma2dlem2  27411  gausslemma2dlem3  27412  gausslemma2dlem6  27416  lgseisenlem4  27422  lgseisen  27423  lgsquadlem1  27424  lgsquadlem2  27425  2lgslem1a1  27433  2sqmod  27480  chebbnd1lem1  27513  chebbnd1lem3  27515  chtppilimlem1  27517  chpchtlim  27523  vmadivsum  27526  rplogsumlem1  27528  rpvmasumlem  27531  dchrisumlem2  27534  dchrisumlem3  27535  dchrmusum2  27538  dchrvmasumlem2  27542  dchrvmasumiflem1  27545  dchrisum0re  27557  dchrisum0lem1  27560  dirith2  27572  mulogsumlem  27575  mulogsum  27576  mulog2sumlem2  27579  vmalogdivsum2  27582  vmalogdivsum  27583  2vmadivsumlem  27584  logsqvma  27586  logsqvma2  27587  log2sumbnd  27588  selberglem2  27590  selberg  27592  selbergb  27593  selberg2lem  27594  selberg2b  27596  chpdifbndlem1  27597  chpdifbndlem2  27598  selberg3lem1  27601  selberg3lem2  27602  selberg3  27603  selberg4lem1  27604  selberg4  27605  pntrsumbnd2  27611  selberg3r  27613  selberg4r  27614  selberg34r  27615  pntsf  27617  pntsval2  27620  pntrlog2bndlem1  27621  pntrlog2bndlem2  27622  pntrlog2bndlem3  27623  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  pntrlog2bndlem6  27627  pntrlog2bnd  27628  pntpbnd1a  27629  pntpbnd1  27630  pntpbnd2  27631  pntibndlem2a  27634  pntibndlem2  27635  pntlemb  27641  pntlemr  27646  pntlemj  27647  pntlemf  27649  pntlemk  27650  pntlemo  27651  pntlem3  27653  ostth2lem1  27662  ostth2lem2  27678  ostth2lem3  27679  ostth2lem4  27680  ostth3  27682  ttgcontlem1  28899  brbtwn2  28920  colinearalglem4  28924  axsegconlem8  28939  axsegconlem9  28940  axsegconlem10  28941  ax5seglem3  28946  axpaschlem  28955  axpasch  28956  axeuclidlem  28977  numclwwlk5  30407  numclwwlk7  30410  smcnlem  30716  ubthlem2  30890  htthlem  30936  pjhthlem1  31410  cnlnadjlem7  32092  nmopcoadji  32120  branmfn  32124  leopnmid  32157  nexple  32833  rmulccn  33927  xrge0iifhom  33936  dya2icoseg  34279  eulerpartlems  34362  eulerpartlemgc  34364  eulerpartlemb  34370  plymulx0  34562  signsvtp  34598  reprgt  34636  breprexplemc  34647  circlemethhgt  34658  hgt750lemd  34663  logdivsqrle  34665  hgt750lem  34666  hgt750lemf  34668  hgt750lemb  34671  hgt750lema  34672  hgt750leme  34673  tgoldbachgtde  34675  resconn  35251  knoppcnlem2  36495  knoppcnlem4  36497  knoppcnlem10  36503  unbdqndv2lem1  36510  unbdqndv2lem2  36511  knoppndvlem1  36513  knoppndvlem11  36523  knoppndvlem12  36524  knoppndvlem14  36526  knoppndvlem15  36527  knoppndvlem17  36529  knoppndvlem18  36530  knoppndvlem19  36531  knoppndvlem20  36532  knoppndvlem21  36533  opnmbllem0  37663  itg2addnclem2  37679  itg2addnclem3  37680  iblmulc2nc  37692  itgmulc2nclem1  37693  ftc1cnnclem  37698  ftc1anclem3  37702  areacirclem4  37718  geomcau  37766  equivbnd  37797  bfplem1  37829  bfplem2  37830  bfp  37831  rrnequiv  37842  rrntotbnd  37843  lcmineqlem19  42048  lcmineqlem20  42049  lcmineqlem21  42050  lcmineqlem22  42051  3lexlogpow2ineq2  42060  dvrelogpow2b  42069  aks4d1p1p2  42071  aks4d1p1p4  42072  aks4d1p1p6  42074  aks4d1p1p7  42075  aks4d1p1p5  42076  aks4d1p1  42077  aks4d1p8d2  42086  aks4d1p8  42088  posbezout  42101  aks6d1c2lem4  42128  2np3bcnp1  42145  2ap1caineq  42146  aks6d1c6lem4  42174  aks6d1c7lem1  42181  aks6d1c7lem2  42182  resubdi  42426  remul02  42435  remul01  42437  remulinvcom  42462  sn-0tie0  42469  renegmulnnass  42483  mulgt0con1d  42488  mulgt0con2d  42489  mulgt0b2d  42490  sn-ltmul2d  42491  sn-mulgt1d  42495  sn-inelr  42497  sn-itrere  42498  sn-retire  42499  fltnltalem  42672  fltnlta  42673  3cubeslem2  42696  3cubeslem3r  42698  3cubeslem4  42700  irrapxlem1  42833  irrapxlem2  42834  irrapxlem3  42835  irrapxlem4  42836  irrapxlem5  42837  pellexlem2  42841  pellexlem6  42845  pell14qrgt0  42870  pell1qrge1  42881  pell1qrgaplem  42884  pellqrexplicit  42888  pellqrex  42890  rmspecsqrtnq  42917  rmxycomplete  42929  rmxypos  42959  ltrmynn0  42960  ltrmxnn0  42961  jm2.24nn  42971  jm2.17a  42972  jm2.17b  42973  jm2.17c  42974  jm2.27c  43019  jm3.1lem2  43030  areaquad  43228  sqrtcval  43654  resqrtval  43656  imsqrtval  43657  imo72b2lem0  44178  cvgdvgrat  44332  nzprmdif  44338  lt3addmuld  45313  fperiodmullem  45315  fperiodmul  45316  lt4addmuld  45318  xralrple2  45365  xralrple3  45385  ltmulneg  45403  fmul01  45595  fmuldfeqlem1  45597  fmul01lt1lem1  45599  sumnnodd  45645  ltmod  45653  0ellimcdiv  45664  limclner  45666  dvdivbd  45938  dvbdfbdioolem2  45944  dvbdfbdioo  45945  ioodvbdlimc1lem1  45946  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  stoweidlem1  46016  stoweidlem11  46026  stoweidlem13  46028  stoweidlem14  46029  stoweidlem16  46031  stoweidlem17  46032  stoweidlem22  46037  stoweidlem24  46039  stoweidlem25  46040  stoweidlem26  46041  stoweidlem30  46045  stoweidlem34  46049  stoweidlem36  46051  stoweidlem49  46064  stoweidlem59  46074  stoweidlem60  46075  wallispilem4  46083  wallispilem5  46084  wallispi  46085  wallispi2lem1  46086  wallispi2  46088  stirlinglem1  46089  stirlinglem3  46091  stirlinglem5  46093  stirlinglem6  46094  stirlinglem7  46095  stirlinglem10  46098  stirlinglem11  46099  stirlinglem12  46100  stirlinglem15  46103  stirlingr  46105  dirker2re  46107  dirkerval2  46109  dirkerre  46110  dirkertrigeqlem1  46113  dirkertrigeqlem2  46114  dirkeritg  46117  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem4  46126  fourierdlem5  46127  fourierdlem6  46128  fourierdlem7  46129  fourierdlem16  46138  fourierdlem18  46140  fourierdlem19  46141  fourierdlem21  46143  fourierdlem22  46144  fourierdlem26  46148  fourierdlem35  46157  fourierdlem39  46161  fourierdlem41  46163  fourierdlem42  46164  fourierdlem43  46165  fourierdlem48  46169  fourierdlem49  46170  fourierdlem51  46172  fourierdlem55  46176  fourierdlem56  46177  fourierdlem57  46178  fourierdlem58  46179  fourierdlem62  46183  fourierdlem63  46184  fourierdlem64  46185  fourierdlem65  46186  fourierdlem66  46187  fourierdlem67  46188  fourierdlem68  46189  fourierdlem71  46192  fourierdlem72  46193  fourierdlem73  46194  fourierdlem76  46197  fourierdlem77  46198  fourierdlem78  46199  fourierdlem83  46204  fourierdlem84  46205  fourierdlem87  46208  fourierdlem88  46209  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fourierdlem94  46215  fourierdlem95  46216  fourierdlem97  46218  fourierdlem103  46224  fourierdlem104  46225  fourierdlem112  46233  fourierdlem113  46234  sqwvfoura  46243  sqwvfourb  46244  fouriersw  46246  etransclem23  46272  etransclem48  46297  rrndistlt  46305  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem4  46613  smfmullem1  46806  smfmullem2  46807  smfmullem3  46808  smfmul  46810  fmtno4prmfac  47559  lighneallem4a  47595  requad01  47608  requad1  47609  requad2  47610  perfectALTVlem2  47709  gpg3kgrtriexlem1  48039  gpg3kgrtriexlem4  48042  gpg3kgrtriexlem6  48044  ply1mulgsumlem2  48304  digvalnn0  48520  dignn0fr  48522  dig2nn0  48532  affinecomb1  48623  rrx2linest2  48665  line2  48673  itsclc0lem1  48677  itsclc0lem2  48678  itsclc0lem3  48679  itscnhlc0yqe  48680  itsclc0yqsollem2  48684  itsclc0yqsol  48685  itscnhlc0xyqsol  48686  itsclc0xyqsolr  48690  itsclinecirc0  48694  itsclinecirc0b  48695  itsclinecirc0in  48696  itsclquadb  48697  itsclquadeu  48698  2itscp  48702  itscnhlinecirc02plem1  48703  itscnhlinecirc02p  48706  inlinecirc02plem  48707  amgmwlem  49321