Theorem remulcld 11175

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7367  ℝcr 11037   · cmul 11043

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

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

This theorem is referenced by:  mulge0  11668  msqge0  11671  redivcl  11874  prodgt0  12002  ltmul1a  12004  ltmul1  12005  ltmuldiv  12029  lt2msq1  12040  lt2msq  12041  le2msq  12056  msq11  12057  supmul1  12125  supmullem2  12127  supmul  12128  div4p1lem1div2  12432  mul2lt0rlt0  13046  mul2lt0bi  13050  prodge0rd  13051  ge2halflem1  13059  qbtwnre  13151  xmulneg1  13221  xmulf  13224  lincmb01cmp  13448  iccf1o  13449  flmulnn0  13786  flhalf  13789  modcl  13832  mod0  13835  modge0  13838  modmulnn  13848  mulp1mod1  13873  muladdmod  13874  2txmodxeq0  13893  modaddmulmod  13900  moddi  13901  modsubdir  13902  modirr  13904  addmodlteq  13908  bernneq  14191  bernneq3  14193  expnbnd  14194  expmulnbnd  14197  discr1  14201  discr  14202  faclbnd  14252  faclbnd6  14261  remullem  15090  01sqrexlem7  15210  sqrtmul  15221  abstri  15293  sqreulem  15322  bhmafibid1  15430  mulcn2  15558  reccn2  15559  o1rlimmul  15581  lo1mul  15590  iseraltlem2  15645  iseraltlem3  15646  iseralt  15647  o1fsum  15776  cvgcmpce  15781  climcndslem1  15814  climcndslem2  15815  climcnds  15816  geomulcvg  15841  cvgrat  15848  mertenslem1  15849  fprodge1  15960  eftlub  16076  sin02gt0  16159  eirrlem  16171  bitsp1o  16402  2mulprm  16662  isprm5  16677  modprm0  16776  prmreclem3  16889  prmreclem4  16890  prmreclem5  16891  2expltfac  17063  metss2lem  24476  nlmvscnlem2  24650  nrginvrcnlem  24656  nmoco  24702  nmotri  24704  nghmcn  24710  icopnfhmeo  24910  nmoleub2lem3  25082  ipcau2  25201  tcphcphlem1  25202  ipcnlem2  25211  rrxcph  25359  csbren  25366  trirn  25367  pjthlem1  25404  opnmbllem  25568  vitalilem4  25578  itg1val2  25651  itg1cl  25652  itg1ge0  25653  itg1addlem4  25666  itg1mulc  25671  itg1ge0a  25678  itg1climres  25681  mbfi1fseqlem1  25682  mbfi1fseqlem3  25684  mbfi1fseqlem4  25685  mbfi1fseqlem5  25686  mbfi1fseqlem6  25687  itg2const2  25708  itg2mulclem  25713  itg2mulc  25714  itg2monolem1  25717  itg2monolem3  25719  itg2cnlem2  25729  iblconst  25785  iblmulc2  25798  itgmulc2lem1  25799  itgmulc2lem2  25800  bddmulibl  25806  bddiblnc  25809  dveflem  25946  cmvth  25958  dvlip  25960  dvlipcn  25961  dvivthlem1  25975  lhop1lem  25980  dvcvx  25987  dvfsumlem2  25994  dvfsumlem3  25995  dvfsumlem4  25996  dvfsum2  26001  ftc1lem4  26006  plyeq0lem  26175  aalioulem3  26300  aalioulem4  26301  aaliou3lem9  26316  ulmdvlem1  26365  itgulm  26373  radcnvlem1  26378  radcnvlem2  26379  dvradcnv  26386  abelthlem2  26397  abelthlem7  26403  tangtx  26469  tanregt0  26503  logdivlti  26584  logcnlem3  26608  logcnlem4  26609  logccv  26627  recxpcl  26639  cxpmul  26652  cxplt  26658  cxple2  26661  abscxpbnd  26717  lawcoslem1  26779  heron  26802  atans2  26895  efrlim  26933  o1cxp  26938  scvxcvx  26949  jensenlem2  26951  amgmlem  26953  fsumharmonic  26975  lgamgulmlem2  26993  lgamgulmlem3  26994  lgamgulmlem4  26995  lgamgulmlem5  26996  lgamgulmlem6  26997  relgamcl  27025  ftalem1  27036  ftalem2  27037  ftalem5  27040  basellem3  27046  basellem8  27051  chpub  27183  logfacubnd  27184  logfaclbnd  27185  logfacbnd3  27186  logexprlim  27188  perfectlem2  27193  bclbnd  27243  efexple  27244  bposlem1  27247  bposlem2  27248  bposlem6  27252  bposlem9  27255  lgsdilem  27287  gausslemma2dlem0c  27321  gausslemma2dlem2  27330  gausslemma2dlem3  27331  gausslemma2dlem6  27335  lgseisenlem4  27341  lgseisen  27342  lgsquadlem1  27343  lgsquadlem2  27344  2lgslem1a1  27352  2sqmod  27399  chebbnd1lem1  27432  chebbnd1lem3  27434  chtppilimlem1  27436  chpchtlim  27442  vmadivsum  27445  rplogsumlem1  27447  rpvmasumlem  27450  dchrisumlem2  27453  dchrisumlem3  27454  dchrmusum2  27457  dchrvmasumlem2  27461  dchrvmasumiflem1  27464  dchrisum0re  27476  dchrisum0lem1  27479  dirith2  27491  mulogsumlem  27494  mulogsum  27495  mulog2sumlem2  27498  vmalogdivsum2  27501  vmalogdivsum  27502  2vmadivsumlem  27503  logsqvma  27505  logsqvma2  27506  log2sumbnd  27507  selberglem2  27509  selberg  27511  selbergb  27512  selberg2lem  27513  selberg2b  27515  chpdifbndlem1  27516  chpdifbndlem2  27517  selberg3lem1  27520  selberg3lem2  27521  selberg3  27522  selberg4lem1  27523  selberg4  27524  pntrsumbnd2  27530  selberg3r  27532  selberg4r  27533  selberg34r  27534  pntsf  27536  pntsval2  27539  pntrlog2bndlem1  27540  pntrlog2bndlem2  27541  pntrlog2bndlem3  27542  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntrlog2bndlem6  27546  pntrlog2bnd  27547  pntpbnd1a  27548  pntpbnd1  27549  pntpbnd2  27550  pntibndlem2a  27553  pntibndlem2  27554  pntlemb  27560  pntlemr  27565  pntlemj  27566  pntlemf  27568  pntlemk  27569  pntlemo  27570  pntlem3  27572  ostth2lem1  27581  ostth2lem2  27597  ostth2lem3  27598  ostth2lem4  27599  ostth3  27601  ttgcontlem1  28953  brbtwn2  28974  colinearalglem4  28978  axsegconlem8  28993  axsegconlem9  28994  axsegconlem10  28995  ax5seglem3  29000  axpaschlem  29009  axpasch  29010  axeuclidlem  29031  numclwwlk5  30458  numclwwlk7  30461  smcnlem  30768  ubthlem2  30942  htthlem  30988  pjhthlem1  31462  cnlnadjlem7  32144  nmopcoadji  32172  branmfn  32176  leopnmid  32209  nexple  32917  constrremulcl  33911  constrmulcl  33915  cos9thpiminplylem1  33926  cos9thpinconstrlem1  33933  rmulccn  34072  xrge0iifhom  34081  dya2icoseg  34421  eulerpartlems  34504  eulerpartlemgc  34506  eulerpartlemb  34512  plymulx0  34691  signsvtp  34727  reprgt  34765  breprexplemc  34776  circlemethhgt  34787  hgt750lemd  34792  logdivsqrle  34794  hgt750lem  34795  hgt750lemf  34797  hgt750lemb  34800  hgt750lema  34801  hgt750leme  34802  tgoldbachgtde  34804  resconn  35428  knoppcnlem2  36754  knoppcnlem4  36756  knoppcnlem10  36762  unbdqndv2lem1  36769  unbdqndv2lem2  36770  knoppndvlem1  36772  knoppndvlem11  36782  knoppndvlem12  36783  knoppndvlem14  36785  knoppndvlem15  36786  knoppndvlem17  36788  knoppndvlem18  36789  knoppndvlem19  36790  knoppndvlem20  36791  knoppndvlem21  36792  opnmbllem0  37977  itg2addnclem2  37993  itg2addnclem3  37994  iblmulc2nc  38006  itgmulc2nclem1  38007  ftc1cnnclem  38012  ftc1anclem3  38016  areacirclem4  38032  geomcau  38080  equivbnd  38111  bfplem1  38143  bfplem2  38144  bfp  38145  rrnequiv  38156  rrntotbnd  38157  lcmineqlem19  42486  lcmineqlem20  42487  lcmineqlem21  42488  lcmineqlem22  42489  3lexlogpow2ineq2  42498  dvrelogpow2b  42507  aks4d1p1p2  42509  aks4d1p1p4  42510  aks4d1p1p6  42512  aks4d1p1p7  42513  aks4d1p1p5  42514  aks4d1p1  42515  aks4d1p8d2  42524  aks4d1p8  42526  posbezout  42539  aks6d1c2lem4  42566  2np3bcnp1  42583  2ap1caineq  42584  aks6d1c6lem4  42612  aks6d1c7lem1  42619  aks6d1c7lem2  42620  resubdi  42828  remul02  42837  remul01  42839  remulinvcom  42865  rediveud  42875  redivcan3d  42880  redivrec2d  42892  rediv23d  42893  sn-0tie0  42896  renegmulnnass  42910  mulgt0con1d  42915  mulgt0con2d  42916  mulgt0b1d  42917  sn-ltmul2d  42918  mulgt0b2d  42923  sn-mulgt1d  42924  mulltgt0d  42927  mullt0b1d  42928  mullt0b2d  42929  sn-mullt0d  42930  sn-itrere  42933  sn-retire  42934  fltnltalem  43095  fltnlta  43096  3cubeslem2  43117  3cubeslem3r  43119  3cubeslem4  43121  irrapxlem1  43250  irrapxlem2  43251  irrapxlem3  43252  irrapxlem4  43253  irrapxlem5  43254  pellexlem2  43258  pellexlem6  43262  pell14qrgt0  43287  pell1qrge1  43298  pell1qrgaplem  43301  pellqrexplicit  43305  pellqrex  43307  rmspecsqrtnq  43334  rmxycomplete  43345  rmxypos  43375  ltrmynn0  43376  ltrmxnn0  43377  jm2.24nn  43387  jm2.17a  43388  jm2.17b  43389  jm2.17c  43390  jm2.27c  43435  jm3.1lem2  43446  areaquad  43644  sqrtcval  44068  resqrtval  44070  imsqrtval  44071  imo72b2lem0  44592  cvgdvgrat  44740  nzprmdif  44746  lt3addmuld  45734  fperiodmullem  45736  fperiodmul  45737  lt4addmuld  45739  xralrple2  45784  xralrple3  45803  ltmulneg  45821  fmul01  46010  fmuldfeqlem1  46012  fmul01lt1lem1  46014  sumnnodd  46060  ltmod  46066  0ellimcdiv  46077  limclner  46079  dvdivbd  46351  dvbdfbdioolem2  46357  dvbdfbdioo  46358  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  stoweidlem1  46429  stoweidlem11  46439  stoweidlem13  46441  stoweidlem14  46442  stoweidlem16  46444  stoweidlem17  46445  stoweidlem22  46450  stoweidlem24  46452  stoweidlem25  46453  stoweidlem26  46454  stoweidlem30  46458  stoweidlem34  46462  stoweidlem36  46464  stoweidlem49  46477  stoweidlem59  46487  stoweidlem60  46488  wallispilem4  46496  wallispilem5  46497  wallispi  46498  wallispi2lem1  46499  wallispi2  46501  stirlinglem1  46502  stirlinglem3  46504  stirlinglem5  46506  stirlinglem6  46507  stirlinglem7  46508  stirlinglem10  46511  stirlinglem11  46512  stirlinglem12  46513  stirlinglem15  46516  stirlingr  46518  dirker2re  46520  dirkerval2  46522  dirkerre  46523  dirkertrigeqlem1  46526  dirkertrigeqlem2  46527  dirkeritg  46530  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem4  46539  fourierdlem5  46540  fourierdlem6  46541  fourierdlem7  46542  fourierdlem16  46551  fourierdlem18  46553  fourierdlem19  46554  fourierdlem21  46556  fourierdlem22  46557  fourierdlem26  46561  fourierdlem35  46570  fourierdlem39  46574  fourierdlem41  46576  fourierdlem42  46577  fourierdlem43  46578  fourierdlem48  46582  fourierdlem49  46583  fourierdlem51  46585  fourierdlem55  46589  fourierdlem56  46590  fourierdlem57  46591  fourierdlem58  46592  fourierdlem62  46596  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  fourierdlem66  46600  fourierdlem67  46601  fourierdlem68  46602  fourierdlem71  46605  fourierdlem72  46606  fourierdlem73  46607  fourierdlem76  46610  fourierdlem77  46611  fourierdlem78  46612  fourierdlem83  46617  fourierdlem84  46618  fourierdlem87  46621  fourierdlem88  46622  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem94  46628  fourierdlem95  46629  fourierdlem97  46631  fourierdlem103  46637  fourierdlem104  46638  fourierdlem112  46646  fourierdlem113  46647  sqwvfoura  46656  sqwvfourb  46657  fouriersw  46659  etransclem23  46685  etransclem48  46710  rrndistlt  46718  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem4  47026  smfmullem1  47219  smfmullem2  47220  smfmullem3  47221  smfmul  47223  2timesltsqm1  47827  fmtno4prmfac  48035  lighneallem4a  48071  requad01  48097  requad1  48098  requad2  48099  perfectALTVlem2  48198  gpg3kgrtriexlem1  48559  gpg3kgrtriexlem4  48562  gpg3kgrtriexlem6  48564  ply1mulgsumlem2  48863  digvalnn0  49075  dignn0fr  49077  dig2nn0  49087  affinecomb1  49178  rrx2linest2  49220  line2  49228  itsclc0lem1  49232  itsclc0lem2  49233  itsclc0lem3  49234  itscnhlc0yqe  49235  itsclc0yqsollem2  49239  itsclc0yqsol  49240  itscnhlc0xyqsol  49241  itsclc0xyqsolr  49245  itsclinecirc0  49249  itsclinecirc0b  49250  itsclinecirc0in  49251  itsclquadb  49252  itsclquadeu  49253  2itscp  49257  itscnhlinecirc02plem1  49258  itscnhlinecirc02p  49261  inlinecirc02plem  49262  amgmwlem  50277