Theorem remulcld 10989

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7268  ℝcr 10854   · cmul 10860

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

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

This theorem is referenced by:  mulge0  11476  msqge0  11479  redivcl  11677  prodgt0  11805  ltmul1a  11807  ltmul1  11808  ltmuldiv  11831  lt2msq1  11842  lt2msq  11843  le2msq  11858  msq11  11859  supmul1  11927  supmullem2  11929  supmul  11930  div4p1lem1div2  12211  mul2lt0rlt0  12814  mul2lt0bi  12818  prodge0rd  12819  qbtwnre  12915  xmulneg1  12985  xmulf  12988  lincmb01cmp  13209  iccf1o  13210  flmulnn0  13528  flhalf  13531  modcl  13574  mod0  13577  modge0  13580  modmulnn  13590  mulp1mod1  13613  2txmodxeq0  13632  modaddmulmod  13639  moddi  13640  modsubdir  13641  modirr  13643  addmodlteq  13647  bernneq  13925  bernneq3  13927  expnbnd  13928  expmulnbnd  13931  discr1  13935  discr  13936  faclbnd  13985  faclbnd6  13994  remullem  14820  sqrlem7  14941  sqrtmul  14952  abstri  15023  sqreulem  15052  bhmafibid1  15158  mulcn2  15286  reccn2  15287  o1rlimmul  15309  lo1mul  15318  iseraltlem2  15375  iseraltlem3  15376  iseralt  15377  o1fsum  15506  cvgcmpce  15511  climcndslem1  15542  climcndslem2  15543  climcnds  15544  geomulcvg  15569  cvgrat  15576  mertenslem1  15577  fprodge1  15686  eftlub  15799  sin02gt0  15882  eirrlem  15894  bitsp1o  16121  2mulprm  16379  isprm5  16393  modprm0  16487  prmreclem3  16600  prmreclem4  16601  prmreclem5  16602  2expltfac  16775  metss2lem  23648  nlmvscnlem2  23830  nrginvrcnlem  23836  nmoco  23882  nmotri  23884  nghmcn  23890  icopnfhmeo  24087  nmoleub2lem3  24259  ipcau2  24379  tcphcphlem1  24380  ipcnlem2  24389  rrxcph  24537  csbren  24544  trirn  24545  pjthlem1  24582  opnmbllem  24746  vitalilem4  24756  itg1val2  24829  itg1cl  24830  itg1ge0  24831  itg1addlem4  24844  itg1addlem4OLD  24845  itg1mulc  24850  itg1ge0a  24857  itg1climres  24860  mbfi1fseqlem1  24861  mbfi1fseqlem3  24863  mbfi1fseqlem4  24864  mbfi1fseqlem5  24865  mbfi1fseqlem6  24866  itg2const2  24887  itg2mulclem  24892  itg2mulc  24893  itg2monolem1  24896  itg2monolem3  24898  itg2cnlem2  24908  iblconst  24963  iblmulc2  24976  itgmulc2lem1  24977  itgmulc2lem2  24978  bddmulibl  24984  bddiblnc  24987  dveflem  25124  cmvth  25136  dvlip  25138  dvlipcn  25139  dvivthlem1  25153  lhop1lem  25158  dvcvx  25165  dvfsumlem2  25172  dvfsumlem3  25173  dvfsumlem4  25174  dvfsum2  25179  ftc1lem4  25184  plyeq0lem  25352  aalioulem3  25475  aalioulem4  25476  aaliou3lem9  25491  ulmdvlem1  25540  itgulm  25548  radcnvlem1  25553  radcnvlem2  25554  dvradcnv  25561  abelthlem2  25572  abelthlem7  25578  tangtx  25643  tanregt0  25676  logdivlti  25756  logcnlem3  25780  logcnlem4  25781  logccv  25799  recxpcl  25811  cxpmul  25824  cxplt  25830  cxple2  25833  abscxpbnd  25887  lawcoslem1  25946  heron  25969  atans2  26062  efrlim  26100  o1cxp  26105  scvxcvx  26116  jensenlem2  26118  amgmlem  26120  fsumharmonic  26142  lgamgulmlem2  26160  lgamgulmlem3  26161  lgamgulmlem4  26162  lgamgulmlem5  26163  lgamgulmlem6  26164  relgamcl  26192  ftalem1  26203  ftalem2  26204  ftalem5  26207  basellem3  26213  basellem8  26218  chpub  26349  logfacubnd  26350  logfaclbnd  26351  logfacbnd3  26352  logexprlim  26354  perfectlem2  26359  bclbnd  26409  efexple  26410  bposlem1  26413  bposlem2  26414  bposlem6  26418  bposlem9  26421  lgsdilem  26453  gausslemma2dlem0c  26487  gausslemma2dlem2  26496  gausslemma2dlem3  26497  gausslemma2dlem6  26501  lgseisenlem4  26507  lgseisen  26508  lgsquadlem1  26509  lgsquadlem2  26510  2lgslem1a1  26518  2sqmod  26565  chebbnd1lem1  26598  chebbnd1lem3  26600  chtppilimlem1  26602  chpchtlim  26608  vmadivsum  26611  rplogsumlem1  26613  rpvmasumlem  26616  dchrisumlem2  26619  dchrisumlem3  26620  dchrmusum2  26623  dchrvmasumlem2  26627  dchrvmasumiflem1  26630  dchrisum0re  26642  dchrisum0lem1  26645  dirith2  26657  mulogsumlem  26660  mulogsum  26661  mulog2sumlem2  26664  vmalogdivsum2  26667  vmalogdivsum  26668  2vmadivsumlem  26669  logsqvma  26671  logsqvma2  26672  log2sumbnd  26673  selberglem2  26675  selberg  26677  selbergb  26678  selberg2lem  26679  selberg2b  26681  chpdifbndlem1  26682  chpdifbndlem2  26683  selberg3lem1  26686  selberg3lem2  26687  selberg3  26688  selberg4lem1  26689  selberg4  26690  pntrsumbnd2  26696  selberg3r  26698  selberg4r  26699  selberg34r  26700  pntsf  26702  pntsval2  26705  pntrlog2bndlem1  26706  pntrlog2bndlem2  26707  pntrlog2bndlem3  26708  pntrlog2bndlem4  26709  pntrlog2bndlem5  26710  pntrlog2bndlem6  26712  pntrlog2bnd  26713  pntpbnd1a  26714  pntpbnd1  26715  pntpbnd2  26716  pntibndlem2a  26719  pntibndlem2  26720  pntlemb  26726  pntlemr  26731  pntlemj  26732  pntlemf  26734  pntlemk  26735  pntlemo  26736  pntlem3  26738  ostth2lem1  26747  ostth2lem2  26763  ostth2lem3  26764  ostth2lem4  26765  ostth3  26767  ttgcontlem1  27233  brbtwn2  27254  colinearalglem4  27258  axsegconlem8  27273  axsegconlem9  27274  axsegconlem10  27275  ax5seglem3  27280  axpaschlem  27289  axpasch  27290  axeuclidlem  27311  numclwwlk5  28731  numclwwlk7  28734  smcnlem  29038  ubthlem2  29212  htthlem  29258  pjhthlem1  29732  cnlnadjlem7  30414  nmopcoadji  30442  branmfn  30446  leopnmid  30479  rmulccn  31857  xrge0iifhom  31866  nexple  31956  dya2icoseg  32223  eulerpartlems  32306  eulerpartlemgc  32308  eulerpartlemb  32314  plymulx0  32505  signsvtp  32541  reprgt  32580  breprexplemc  32591  circlemethhgt  32602  hgt750lemd  32607  logdivsqrle  32609  hgt750lem  32610  hgt750lemf  32612  hgt750lemb  32615  hgt750lema  32616  hgt750leme  32617  tgoldbachgtde  32619  resconn  33187  knoppcnlem2  34653  knoppcnlem4  34655  knoppcnlem10  34661  unbdqndv2lem1  34668  unbdqndv2lem2  34669  knoppndvlem1  34671  knoppndvlem11  34681  knoppndvlem12  34682  knoppndvlem14  34684  knoppndvlem15  34685  knoppndvlem17  34687  knoppndvlem18  34688  knoppndvlem19  34689  knoppndvlem20  34690  knoppndvlem21  34691  opnmbllem0  35792  itg2addnclem2  35808  itg2addnclem3  35809  iblmulc2nc  35821  itgmulc2nclem1  35822  ftc1cnnclem  35827  ftc1anclem3  35831  areacirclem4  35847  geomcau  35896  equivbnd  35927  bfplem1  35959  bfplem2  35960  bfp  35961  rrnequiv  35972  rrntotbnd  35973  lcmineqlem19  40035  lcmineqlem20  40036  lcmineqlem21  40037  lcmineqlem22  40038  3lexlogpow2ineq2  40047  dvrelogpow2b  40056  aks4d1p1p2  40058  aks4d1p1p4  40059  aks4d1p1p6  40061  aks4d1p1p7  40062  aks4d1p1p5  40063  aks4d1p1  40064  aks4d1p8d2  40073  aks4d1p8  40075  2np3bcnp1  40080  2ap1caineq  40081  resubdi  40359  remul02  40368  remul01  40370  remulinvcom  40394  sn-0tie0  40401  mulgt0con1d  40408  mulgt0con2d  40409  mulgt0b2d  40410  sn-ltmul2d  40411  sn-inelr  40415  itrere  40416  retire  40417  fltnltalem  40479  fltnlta  40480  3cubeslem2  40487  3cubeslem3r  40489  3cubeslem4  40491  irrapxlem1  40624  irrapxlem2  40625  irrapxlem3  40626  irrapxlem4  40627  irrapxlem5  40628  pellexlem2  40632  pellexlem6  40636  pell14qrgt0  40661  pell1qrge1  40672  pell1qrgaplem  40675  pellqrexplicit  40679  pellqrex  40681  rmspecsqrtnq  40708  rmxycomplete  40719  rmxypos  40749  ltrmynn0  40750  ltrmxnn0  40751  jm2.24nn  40761  jm2.17a  40762  jm2.17b  40763  jm2.17c  40764  jm2.27c  40809  jm3.1lem2  40820  areaquad  41027  sqrtcval  41202  resqrtval  41204  imsqrtval  41205  imo72b2lem0  41729  cvgdvgrat  41884  nzprmdif  41890  lt3addmuld  42794  fperiodmullem  42796  fperiodmul  42797  lt4addmuld  42799  xralrple2  42847  xralrple3  42867  ltmulneg  42886  fmul01  43075  fmuldfeqlem1  43077  fmul01lt1lem1  43079  sumnnodd  43125  ltmod  43133  0ellimcdiv  43144  limclner  43146  dvdivbd  43418  dvbdfbdioolem2  43424  dvbdfbdioo  43425  ioodvbdlimc1lem1  43426  ioodvbdlimc1lem2  43427  ioodvbdlimc2lem  43429  stoweidlem1  43496  stoweidlem11  43506  stoweidlem13  43508  stoweidlem14  43509  stoweidlem16  43511  stoweidlem17  43512  stoweidlem22  43517  stoweidlem24  43519  stoweidlem25  43520  stoweidlem26  43521  stoweidlem30  43525  stoweidlem34  43529  stoweidlem36  43531  stoweidlem49  43544  stoweidlem59  43554  stoweidlem60  43555  wallispilem4  43563  wallispilem5  43564  wallispi  43565  wallispi2lem1  43566  wallispi2  43568  stirlinglem1  43569  stirlinglem3  43571  stirlinglem5  43573  stirlinglem6  43574  stirlinglem7  43575  stirlinglem10  43578  stirlinglem11  43579  stirlinglem12  43580  stirlinglem15  43583  stirlingr  43585  dirker2re  43587  dirkerval2  43589  dirkerre  43590  dirkertrigeqlem1  43593  dirkertrigeqlem2  43594  dirkeritg  43597  dirkercncflem2  43599  dirkercncflem4  43601  fourierdlem4  43606  fourierdlem5  43607  fourierdlem6  43608  fourierdlem7  43609  fourierdlem16  43618  fourierdlem18  43620  fourierdlem19  43621  fourierdlem21  43623  fourierdlem22  43624  fourierdlem26  43628  fourierdlem35  43637  fourierdlem39  43641  fourierdlem41  43643  fourierdlem42  43644  fourierdlem43  43645  fourierdlem48  43649  fourierdlem49  43650  fourierdlem51  43652  fourierdlem55  43656  fourierdlem56  43657  fourierdlem57  43658  fourierdlem58  43659  fourierdlem62  43663  fourierdlem63  43664  fourierdlem64  43665  fourierdlem65  43666  fourierdlem66  43667  fourierdlem67  43668  fourierdlem68  43669  fourierdlem71  43672  fourierdlem72  43673  fourierdlem73  43674  fourierdlem76  43677  fourierdlem77  43678  fourierdlem78  43679  fourierdlem83  43684  fourierdlem84  43685  fourierdlem87  43688  fourierdlem88  43689  fourierdlem89  43690  fourierdlem90  43691  fourierdlem91  43692  fourierdlem94  43695  fourierdlem95  43696  fourierdlem97  43698  fourierdlem103  43704  fourierdlem104  43705  fourierdlem112  43713  fourierdlem113  43714  sqwvfoura  43723  sqwvfourb  43724  fouriersw  43726  etransclem23  43752  etransclem48  43777  rrndistlt  43785  hoidmvlelem1  44087  hoidmvlelem2  44088  hoidmvlelem4  44090  smfmullem1  44276  smfmullem2  44277  smfmullem3  44278  smfmul  44280  fmtno4prmfac  44976  lighneallem4a  45012  requad01  45025  requad1  45026  requad2  45027  perfectALTVlem2  45126  ply1mulgsumlem2  45680  digvalnn0  45897  dignn0fr  45899  dig2nn0  45909  affinecomb1  46000  rrx2linest2  46042  line2  46050  itsclc0lem1  46054  itsclc0lem2  46055  itsclc0lem3  46056  itscnhlc0yqe  46057  itsclc0yqsollem2  46061  itsclc0yqsol  46062  itscnhlc0xyqsol  46063  itsclc0xyqsolr  46067  itsclinecirc0  46071  itsclinecirc0b  46072  itsclinecirc0in  46073  itsclquadb  46074  itsclquadeu  46075  2itscp  46079  itscnhlinecirc02plem1  46080  itscnhlinecirc02p  46083  inlinecirc02plem  46084  amgmwlem  46458