Theorem remulcld 11145

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7349  ℝcr 11008   · cmul 11014

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

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

This theorem is referenced by:  mulge0  11638  msqge0  11641  redivcl  11843  prodgt0  11971  ltmul1a  11973  ltmul1  11974  ltmuldiv  11998  lt2msq1  12009  lt2msq  12010  le2msq  12025  msq11  12026  supmul1  12094  supmullem2  12096  supmul  12097  div4p1lem1div2  12379  mul2lt0rlt0  12997  mul2lt0bi  13001  prodge0rd  13002  ge2halflem1  13010  qbtwnre  13101  xmulneg1  13171  xmulf  13174  lincmb01cmp  13398  iccf1o  13399  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  24397  nlmvscnlem2  24571  nrginvrcnlem  24577  nmoco  24623  nmotri  24625  nghmcn  24631  icopnfhmeo  24839  nmoleub2lem3  25013  ipcau2  25132  tcphcphlem1  25133  ipcnlem2  25142  rrxcph  25290  csbren  25297  trirn  25298  pjthlem1  25335  opnmbllem  25500  vitalilem4  25510  itg1val2  25583  itg1cl  25584  itg1ge0  25585  itg1addlem4  25598  itg1mulc  25603  itg1ge0a  25610  itg1climres  25613  mbfi1fseqlem1  25614  mbfi1fseqlem3  25616  mbfi1fseqlem4  25617  mbfi1fseqlem5  25618  mbfi1fseqlem6  25619  itg2const2  25640  itg2mulclem  25645  itg2mulc  25646  itg2monolem1  25649  itg2monolem3  25651  itg2cnlem2  25661  iblconst  25717  iblmulc2  25730  itgmulc2lem1  25731  itgmulc2lem2  25732  bddmulibl  25738  bddiblnc  25741  dveflem  25881  cmvth  25893  cmvthOLD  25894  dvlip  25896  dvlipcn  25897  dvivthlem1  25911  lhop1lem  25916  dvcvx  25923  dvfsumlem2  25931  dvfsumlem2OLD  25932  dvfsumlem3  25933  dvfsumlem4  25934  dvfsum2  25939  ftc1lem4  25944  plyeq0lem  26113  aalioulem3  26240  aalioulem4  26241  aaliou3lem9  26256  ulmdvlem1  26307  itgulm  26315  radcnvlem1  26320  radcnvlem2  26321  dvradcnv  26328  abelthlem2  26340  abelthlem7  26346  tangtx  26412  tanregt0  26446  logdivlti  26527  logcnlem3  26551  logcnlem4  26552  logccv  26570  recxpcl  26582  cxpmul  26595  cxplt  26601  cxple2  26604  abscxpbnd  26661  lawcoslem1  26723  heron  26746  atans2  26839  efrlim  26877  efrlimOLD  26878  o1cxp  26883  scvxcvx  26894  jensenlem2  26896  amgmlem  26898  fsumharmonic  26920  lgamgulmlem2  26938  lgamgulmlem3  26939  lgamgulmlem4  26940  lgamgulmlem5  26941  lgamgulmlem6  26942  relgamcl  26970  ftalem1  26981  ftalem2  26982  ftalem5  26985  basellem3  26991  basellem8  26996  chpub  27129  logfacubnd  27130  logfaclbnd  27131  logfacbnd3  27132  logexprlim  27134  perfectlem2  27139  bclbnd  27189  efexple  27190  bposlem1  27193  bposlem2  27194  bposlem6  27198  bposlem9  27201  lgsdilem  27233  gausslemma2dlem0c  27267  gausslemma2dlem2  27276  gausslemma2dlem3  27277  gausslemma2dlem6  27281  lgseisenlem4  27287  lgseisen  27288  lgsquadlem1  27289  lgsquadlem2  27290  2lgslem1a1  27298  2sqmod  27345  chebbnd1lem1  27378  chebbnd1lem3  27380  chtppilimlem1  27382  chpchtlim  27388  vmadivsum  27391  rplogsumlem1  27393  rpvmasumlem  27396  dchrisumlem2  27399  dchrisumlem3  27400  dchrmusum2  27403  dchrvmasumlem2  27407  dchrvmasumiflem1  27410  dchrisum0re  27422  dchrisum0lem1  27425  dirith2  27437  mulogsumlem  27440  mulogsum  27441  mulog2sumlem2  27444  vmalogdivsum2  27447  vmalogdivsum  27448  2vmadivsumlem  27449  logsqvma  27451  logsqvma2  27452  log2sumbnd  27453  selberglem2  27455  selberg  27457  selbergb  27458  selberg2lem  27459  selberg2b  27461  chpdifbndlem1  27462  chpdifbndlem2  27463  selberg3lem1  27466  selberg3lem2  27467  selberg3  27468  selberg4lem1  27469  selberg4  27470  pntrsumbnd2  27476  selberg3r  27478  selberg4r  27479  selberg34r  27480  pntsf  27482  pntsval2  27485  pntrlog2bndlem1  27486  pntrlog2bndlem2  27487  pntrlog2bndlem3  27488  pntrlog2bndlem4  27489  pntrlog2bndlem5  27490  pntrlog2bndlem6  27492  pntrlog2bnd  27493  pntpbnd1a  27494  pntpbnd1  27495  pntpbnd2  27496  pntibndlem2a  27499  pntibndlem2  27500  pntlemb  27506  pntlemr  27511  pntlemj  27512  pntlemf  27514  pntlemk  27515  pntlemo  27516  pntlem3  27518  ostth2lem1  27527  ostth2lem2  27543  ostth2lem3  27544  ostth2lem4  27545  ostth3  27547  ttgcontlem1  28830  brbtwn2  28850  colinearalglem4  28854  axsegconlem8  28869  axsegconlem9  28870  axsegconlem10  28871  ax5seglem3  28876  axpaschlem  28885  axpasch  28886  axeuclidlem  28907  numclwwlk5  30332  numclwwlk7  30335  smcnlem  30641  ubthlem2  30815  htthlem  30861  pjhthlem1  31335  cnlnadjlem7  32017  nmopcoadji  32045  branmfn  32049  leopnmid  32082  nexple  32790  constrremulcl  33740  constrmulcl  33744  cos9thpiminplylem1  33755  cos9thpinconstrlem1  33762  rmulccn  33901  xrge0iifhom  33910  dya2icoseg  34251  eulerpartlems  34334  eulerpartlemgc  34336  eulerpartlemb  34342  plymulx0  34521  signsvtp  34557  reprgt  34595  breprexplemc  34606  circlemethhgt  34617  hgt750lemd  34622  logdivsqrle  34624  hgt750lem  34625  hgt750lemf  34627  hgt750lemb  34630  hgt750lema  34631  hgt750leme  34632  tgoldbachgtde  34634  resconn  35229  knoppcnlem2  36478  knoppcnlem4  36480  knoppcnlem10  36486  unbdqndv2lem1  36493  unbdqndv2lem2  36494  knoppndvlem1  36496  knoppndvlem11  36506  knoppndvlem12  36507  knoppndvlem14  36509  knoppndvlem15  36510  knoppndvlem17  36512  knoppndvlem18  36513  knoppndvlem19  36514  knoppndvlem20  36515  knoppndvlem21  36516  opnmbllem0  37646  itg2addnclem2  37662  itg2addnclem3  37663  iblmulc2nc  37675  itgmulc2nclem1  37676  ftc1cnnclem  37681  ftc1anclem3  37685  areacirclem4  37701  geomcau  37749  equivbnd  37780  bfplem1  37812  bfplem2  37813  bfp  37814  rrnequiv  37825  rrntotbnd  37826  lcmineqlem19  42030  lcmineqlem20  42031  lcmineqlem21  42032  lcmineqlem22  42033  3lexlogpow2ineq2  42042  dvrelogpow2b  42051  aks4d1p1p2  42053  aks4d1p1p4  42054  aks4d1p1p6  42056  aks4d1p1p7  42057  aks4d1p1p5  42058  aks4d1p1  42059  aks4d1p8d2  42068  aks4d1p8  42070  posbezout  42083  aks6d1c2lem4  42110  2np3bcnp1  42127  2ap1caineq  42128  aks6d1c6lem4  42156  aks6d1c7lem1  42163  aks6d1c7lem2  42164  resubdi  42379  remul02  42388  remul01  42390  remulinvcom  42416  rediveud  42426  redivcan3d  42430  sn-0tie0  42434  renegmulnnass  42448  mulgt0con1d  42453  mulgt0con2d  42454  mulgt0b1d  42455  sn-ltmul2d  42456  mulgt0b2d  42461  sn-mulgt1d  42462  mulltgt0d  42465  mullt0b1d  42466  mullt0b2d  42467  sn-mullt0d  42468  sn-itrere  42471  sn-retire  42472  fltnltalem  42645  fltnlta  42646  3cubeslem2  42668  3cubeslem3r  42670  3cubeslem4  42672  irrapxlem1  42805  irrapxlem2  42806  irrapxlem3  42807  irrapxlem4  42808  irrapxlem5  42809  pellexlem2  42813  pellexlem6  42817  pell14qrgt0  42842  pell1qrge1  42853  pell1qrgaplem  42856  pellqrexplicit  42860  pellqrex  42862  rmspecsqrtnq  42889  rmxycomplete  42900  rmxypos  42930  ltrmynn0  42931  ltrmxnn0  42932  jm2.24nn  42942  jm2.17a  42943  jm2.17b  42944  jm2.17c  42945  jm2.27c  42990  jm3.1lem2  43001  areaquad  43199  sqrtcval  43624  resqrtval  43626  imsqrtval  43627  imo72b2lem0  44148  cvgdvgrat  44296  nzprmdif  44302  lt3addmuld  45293  fperiodmullem  45295  fperiodmul  45296  lt4addmuld  45298  xralrple2  45344  xralrple3  45363  ltmulneg  45381  fmul01  45571  fmuldfeqlem1  45573  fmul01lt1lem1  45575  sumnnodd  45621  ltmod  45629  0ellimcdiv  45640  limclner  45642  dvdivbd  45914  dvbdfbdioolem2  45920  dvbdfbdioo  45921  ioodvbdlimc1lem1  45922  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  stoweidlem1  45992  stoweidlem11  46002  stoweidlem13  46004  stoweidlem14  46005  stoweidlem16  46007  stoweidlem17  46008  stoweidlem22  46013  stoweidlem24  46015  stoweidlem25  46016  stoweidlem26  46017  stoweidlem30  46021  stoweidlem34  46025  stoweidlem36  46027  stoweidlem49  46040  stoweidlem59  46050  stoweidlem60  46051  wallispilem4  46059  wallispilem5  46060  wallispi  46061  wallispi2lem1  46062  wallispi2  46064  stirlinglem1  46065  stirlinglem3  46067  stirlinglem5  46069  stirlinglem6  46070  stirlinglem7  46071  stirlinglem10  46074  stirlinglem11  46075  stirlinglem12  46076  stirlinglem15  46079  stirlingr  46081  dirker2re  46083  dirkerval2  46085  dirkerre  46086  dirkertrigeqlem1  46089  dirkertrigeqlem2  46090  dirkeritg  46093  dirkercncflem2  46095  dirkercncflem4  46097  fourierdlem4  46102  fourierdlem5  46103  fourierdlem6  46104  fourierdlem7  46105  fourierdlem16  46114  fourierdlem18  46116  fourierdlem19  46117  fourierdlem21  46119  fourierdlem22  46120  fourierdlem26  46124  fourierdlem35  46133  fourierdlem39  46137  fourierdlem41  46139  fourierdlem42  46140  fourierdlem43  46141  fourierdlem48  46145  fourierdlem49  46146  fourierdlem51  46148  fourierdlem55  46152  fourierdlem56  46153  fourierdlem57  46154  fourierdlem58  46155  fourierdlem62  46159  fourierdlem63  46160  fourierdlem64  46161  fourierdlem65  46162  fourierdlem66  46163  fourierdlem67  46164  fourierdlem68  46165  fourierdlem71  46168  fourierdlem72  46169  fourierdlem73  46170  fourierdlem76  46173  fourierdlem77  46174  fourierdlem78  46175  fourierdlem83  46180  fourierdlem84  46181  fourierdlem87  46184  fourierdlem88  46185  fourierdlem89  46186  fourierdlem90  46187  fourierdlem91  46188  fourierdlem94  46191  fourierdlem95  46192  fourierdlem97  46194  fourierdlem103  46200  fourierdlem104  46201  fourierdlem112  46209  fourierdlem113  46210  sqwvfoura  46219  sqwvfourb  46220  fouriersw  46222  etransclem23  46248  etransclem48  46273  rrndistlt  46281  hoidmvlelem1  46586  hoidmvlelem2  46587  hoidmvlelem4  46589  smfmullem1  46782  smfmullem2  46783  smfmullem3  46784  smfmul  46786  fmtno4prmfac  47566  lighneallem4a  47602  requad01  47615  requad1  47616  requad2  47617  perfectALTVlem2  47716  gpg3kgrtriexlem1  48077  gpg3kgrtriexlem4  48080  gpg3kgrtriexlem6  48082  ply1mulgsumlem2  48382  digvalnn0  48594  dignn0fr  48596  dig2nn0  48606  affinecomb1  48697  rrx2linest2  48739  line2  48747  itsclc0lem1  48751  itsclc0lem2  48752  itsclc0lem3  48753  itscnhlc0yqe  48754  itsclc0yqsollem2  48758  itsclc0yqsol  48759  itscnhlc0xyqsol  48760  itsclc0xyqsolr  48764  itsclinecirc0  48768  itsclinecirc0b  48769  itsclinecirc0in  48770  itsclquadb  48771  itsclquadeu  48772  2itscp  48776  itscnhlinecirc02plem1  48777  itscnhlinecirc02p  48780  inlinecirc02plem  48781  amgmwlem  49797