Theorem remulcld 11266

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7414  ℝcr 11126   · cmul 11132

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 11190

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mulge0  11759  msqge0  11762  redivcl  11961  prodgt0  12089  ltmul1a  12091  ltmul1  12092  ltmuldiv  12115  lt2msq1  12126  lt2msq  12127  le2msq  12142  msq11  12143  supmul1  12211  supmullem2  12213  supmul  12214  div4p1lem1div2  12526  mul2lt0rlt0  13149  mul2lt0bi  13153  prodge0rd  13154  ge2halflem1  13162  qbtwnre  13254  xmulneg1  13324  xmulf  13327  lincmb01cmp  13551  iccf1o  13552  flmulnn0  13891  flhalf  13894  modcl  13937  mod0  13940  modge0  13943  modmulnn  13953  mulp1mod1  13978  muladdmod  13979  2txmodxeq0  13998  modaddmulmod  14005  moddi  14006  modsubdir  14007  modirr  14009  addmodlteq  14013  bernneq  14296  bernneq3  14298  expnbnd  14299  expmulnbnd  14302  discr1  14306  discr  14307  faclbnd  14357  faclbnd6  14366  remullem  15218  01sqrexlem7  15338  sqrtmul  15349  abstri  15421  sqreulem  15450  bhmafibid1  15558  mulcn2  15686  reccn2  15687  o1rlimmul  15709  lo1mul  15718  iseraltlem2  15773  iseraltlem3  15774  iseralt  15775  o1fsum  15903  cvgcmpce  15908  climcndslem1  15941  climcndslem2  15942  climcnds  15943  geomulcvg  15968  cvgrat  15975  mertenslem1  15976  fprodge1  16085  eftlub  16200  sin02gt0  16283  eirrlem  16295  bitsp1o  16526  2mulprm  16786  isprm5  16801  modprm0  16900  prmreclem3  17013  prmreclem4  17014  prmreclem5  17015  2expltfac  17187  metss2lem  24740  nlmvscnlem2  24914  nrginvrcnlem  24920  nmoco  24966  nmotri  24968  nghmcn  24974  icopnfhmeo  25174  nmoleub2lem3  25346  ipcau2  25465  tcphcphlem1  25466  ipcnlem2  25475  rrxcph  25623  csbren  25630  trirn  25631  pjthlem1  25668  opnmbllem  25832  vitalilem4  25842  itg1val2  25915  itg1cl  25916  itg1ge0  25917  itg1addlem4  25930  itg1mulc  25935  itg1ge0a  25942  itg1climres  25945  mbfi1fseqlem1  25946  mbfi1fseqlem3  25948  mbfi1fseqlem4  25949  mbfi1fseqlem5  25950  mbfi1fseqlem6  25951  itg2const2  25972  itg2mulclem  25977  itg2mulc  25978  itg2monolem1  25981  itg2monolem3  25983  itg2cnlem2  25993  iblconst  26048  iblmulc2  26061  itgmulc2lem1  26062  itgmulc2lem2  26063  bddmulibl  26069  bddiblnc  26072  dveflem  26209  cmvth  26221  dvlip  26223  dvlipcn  26224  dvivthlem1  26238  lhop1lem  26243  dvcvx  26250  dvfsumlem2  26257  dvfsumlem3  26258  dvfsumlem4  26259  dvfsum2  26264  ftc1lem4  26269  plyeq0lem  26439  plyn0mulidp  26514  aalioulem3  26573  aalioulem4  26574  aaliou3lem9  26589  ulmdvlem1  26639  itgulm  26647  radcnvlem1  26652  radcnvlem2  26653  dvradcnv  26660  abelthlem2  26671  abelthlem7  26677  tangtx  26746  tanregt0  26779  logdivlti  26860  logcnlem3  26884  logcnlem4  26885  logccv  26903  recxpcl  26915  cxpmul  26928  cxplt  26934  cxple2  26937  abscxpbnd  26993  lawcoslem1  27055  heron  27078  atans2  27171  efrlim  27209  o1cxp  27214  scvxcvx  27225  jensenlem2  27227  amgmlem  27229  fsumharmonic  27251  lgamgulmlem2  27269  lgamgulmlem3  27270  lgamgulmlem4  27271  lgamgulmlem5  27272  lgamgulmlem6  27273  relgamcl  27301  ftalem1  27312  ftalem2  27313  ftalem5  27316  basellem3  27322  basellem8  27327  chpub  27459  logfacubnd  27460  logfaclbnd  27461  logfacbnd3  27462  logexprlim  27464  perfectlem2  27469  bclbnd  27519  efexple  27520  bposlem1  27523  bposlem2  27524  bposlem6  27528  bposlem9  27531  lgsdilem  27563  gausslemma2dlem0c  27597  gausslemma2dlem2  27606  gausslemma2dlem3  27607  gausslemma2dlem6  27611  lgseisenlem4  27617  lgseisen  27618  lgsquadlem1  27619  lgsquadlem2  27620  2lgslem1a1  27628  2sqmod  27675  chebbnd1lem1  27708  chebbnd1lem3  27710  chtppilimlem1  27712  chpchtlim  27718  vmadivsum  27721  rplogsumlem1  27723  rpvmasumlem  27726  dchrisumlem2  27729  dchrisumlem3  27730  dchrmusum2  27733  dchrvmasumlem2  27737  dchrvmasumiflem1  27740  dchrisum0re  27752  dchrisum0lem1  27755  dirith2  27767  mulogsumlem  27770  mulogsum  27771  mulog2sumlem2  27774  vmalogdivsum2  27777  vmalogdivsum  27778  2vmadivsumlem  27779  logsqvma  27781  logsqvma2  27782  log2sumbnd  27783  selberglem2  27785  selberg  27787  selbergb  27788  selberg2lem  27789  selberg2b  27791  chpdifbndlem1  27792  chpdifbndlem2  27793  selberg3lem1  27796  selberg3lem2  27797  selberg3  27798  selberg4lem1  27799  selberg4  27800  pntrsumbnd2  27806  selberg3r  27808  selberg4r  27809  selberg34r  27810  pntsf  27812  pntsval2  27815  pntrlog2bndlem1  27816  pntrlog2bndlem2  27817  pntrlog2bndlem3  27818  pntrlog2bndlem4  27819  pntrlog2bndlem5  27820  pntrlog2bndlem6  27822  pntrlog2bnd  27823  pntpbnd1a  27824  pntpbnd1  27825  pntpbnd2  27826  pntibndlem2a  27829  pntibndlem2  27830  pntlemb  27836  pntlemr  27841  pntlemj  27842  pntlemf  27844  pntlemk  27845  pntlemo  27846  pntlem3  27848  ostth2lem1  27857  ostth2lem2  27873  ostth2lem3  27874  ostth2lem4  27875  ostth3  27877  ttgcontlem1  29344  brbtwn2  29365  colinearalglem4  29369  axsegconlem8  29384  axsegconlem9  29385  axsegconlem10  29386  ax5seglem3  29391  axpaschlem  29400  axpasch  29401  axeuclidlem  29422  numclwwlk5  30871  numclwwlk7  30874  smcnlem  31181  ubthlem2  31355  htthlem  31401  pjhthlem1  31875  cnlnadjlem7  32557  nmopcoadji  32585  branmfn  32589  leopnmid  32622  nexple  33306  constrremulcl  34280  constrmulcl  34284  cos9thpiminplylem1  34295  cos9thpinconstrlem1  34302  rmulccn  34441  xrge0iifhom  34450  dya2icoseg  34791  eulerpartlems  34874  eulerpartlemgc  34876  eulerpartlemb  34882  signsvtp  35094  reprgt  35132  breprexplemc  35143  circlemethhgt  35154  hgt750lemd  35159  logdivsqrle  35161  hgt750lem  35162  hgt750lemf  35164  hgt750lemb  35167  hgt750lema  35168  hgt750leme  35169  tgoldbachgtde  35171  resconn  35828  knoppcnlem2  37194  knoppcnlem4  37196  knoppcnlem10  37202  unbdqndv2lem1  37209  unbdqndv2lem2  37210  knoppndvlem1  37212  knoppndvlem11  37222  knoppndvlem12  37223  knoppndvlem14  37225  knoppndvlem15  37226  knoppndvlem17  37228  knoppndvlem18  37229  knoppndvlem19  37230  knoppndvlem20  37231  knoppndvlem21  37232  opnmbllem0  38408  itg2addnclem2  38424  itg2addnclem3  38425  iblmulc2nc  38437  itgmulc2nclem1  38438  ftc1cnnclem  38443  ftc1anclem3  38447  areacirclem4  38463  geomcau  38512  equivbnd  38543  bfplem1  38575  bfplem2  38576  bfp  38577  rrnequiv  38588  rrntotbnd  38589  lcmineqlem19  42916  lcmineqlem20  42917  lcmineqlem21  42918  lcmineqlem22  42919  3lexlogpow2ineq2  42928  dvrelogpow2b  42937  aks4d1p1p2  42939  aks4d1p1p4  42940  aks4d1p1p6  42942  aks4d1p1p7  42943  aks4d1p1p5  42944  aks4d1p1  42945  aks4d1p8d2  42954  aks4d1p8  42956  posbezout  42969  aks6d1c2lem4  42996  2np3bcnp1  43013  2ap1caineq  43014  aks6d1c6lem4  43042  aks6d1c7lem1  43049  aks6d1c7lem2  43050  resubdi  43274  remul02  43283  remul01  43285  remulinvcom  43311  rediveud  43321  redivcan3d  43326  redivrec2d  43338  rediv23d  43339  sn-0tie0  43342  renegmulnnass  43356  mulgt0con1d  43361  mulgt0con2d  43362  mulgt0b1d  43363  sn-ltmul2d  43364  mulgt0b2d  43369  sn-mulgt1d  43370  mulltgt0d  43373  mullt0b1d  43374  mullt0b2d  43375  sn-mullt0d  43376  sn-itrere  43379  sn-retire  43380  fltnltalem  43511  fltnlta  43512  3cubeslem2  43533  3cubeslem3r  43535  3cubeslem4  43537  irrapxlem1  43666  irrapxlem2  43667  irrapxlem3  43668  irrapxlem4  43669  irrapxlem5  43670  pellexlem2  43674  pellexlem6  43678  pell14qrgt0  43703  pell1qrge1  43714  pell1qrgaplem  43717  pellqrexplicit  43721  pellqrex  43723  rmspecsqrtnq  43750  rmxycomplete  43761  rmxypos  43791  ltrmynn0  43792  ltrmxnn0  43793  jm2.24nn  43803  jm2.17a  43804  jm2.17b  43805  jm2.17c  43806  jm2.27c  43851  jm3.1lem2  43862  areaquad  44060  sqrtcval  44484  resqrtval  44486  imsqrtval  44487  imo72b2lem0  45008  cvgdvgrat  45140  nzprmdif  45146  lt3addmuld  46137  fperiodmullem  46139  fperiodmul  46140  lt4addmuld  46142  xralrple2  46187  xralrple3  46206  ltmulneg  46224  fmul01  46413  fmuldfeqlem1  46415  fmul01lt1lem1  46417  sumnnodd  46463  ltmod  46469  0ellimcdiv  46480  limclner  46482  dvdivbd  46754  dvbdfbdioolem2  46760  dvbdfbdioo  46761  ioodvbdlimc1lem1  46762  ioodvbdlimc1lem2  46763  ioodvbdlimc2lem  46765  stoweidlem1  46832  stoweidlem11  46842  stoweidlem13  46844  stoweidlem14  46845  stoweidlem16  46847  stoweidlem17  46848  stoweidlem22  46853  stoweidlem24  46855  stoweidlem25  46856  stoweidlem26  46857  stoweidlem30  46861  stoweidlem34  46865  stoweidlem36  46867  stoweidlem49  46880  stoweidlem59  46890  stoweidlem60  46891  wallispilem4  46899  wallispilem5  46900  wallispi  46901  wallispi2lem1  46902  wallispi2  46904  stirlinglem1  46905  stirlinglem3  46907  stirlinglem5  46909  stirlinglem6  46910  stirlinglem7  46911  stirlinglem10  46914  stirlinglem11  46915  stirlinglem12  46916  stirlinglem15  46919  stirlingr  46921  dirker2re  46923  dirkerval2  46925  dirkerre  46926  dirkertrigeqlem1  46929  dirkertrigeqlem2  46930  dirkeritg  46933  dirkercncflem2  46935  dirkercncflem4  46937  fourierdlem4  46942  fourierdlem5  46943  fourierdlem6  46944  fourierdlem7  46945  fourierdlem16  46954  fourierdlem18  46956  fourierdlem19  46957  fourierdlem21  46959  fourierdlem22  46960  fourierdlem26  46964  fourierdlem35  46973  fourierdlem39  46977  fourierdlem41  46979  fourierdlem42  46980  fourierdlem43  46981  fourierdlem48  46985  fourierdlem49  46986  fourierdlem51  46988  fourierdlem55  46992  fourierdlem56  46993  fourierdlem57  46994  fourierdlem58  46995  fourierdlem62  46999  fourierdlem63  47000  fourierdlem64  47001  fourierdlem65  47002  fourierdlem66  47003  fourierdlem67  47004  fourierdlem68  47005  fourierdlem71  47008  fourierdlem72  47009  fourierdlem73  47010  fourierdlem76  47013  fourierdlem77  47014  fourierdlem78  47015  fourierdlem83  47020  fourierdlem84  47021  fourierdlem87  47024  fourierdlem88  47025  fourierdlem89  47026  fourierdlem90  47027  fourierdlem91  47028  fourierdlem94  47031  fourierdlem95  47032  fourierdlem97  47034  fourierdlem103  47040  fourierdlem104  47041  fourierdlem112  47049  fourierdlem113  47050  sqwvfoura  47059  sqwvfourb  47060  fouriersw  47062  etransclem23  47088  etransclem48  47113  rrndistlt  47121  hoidmvlelem1  47426  hoidmvlelem2  47427  hoidmvlelem4  47429  smfmullem1  47622  smfmullem2  47623  smfmullem3  47624  smfmul  47626  2timesltsqm1  48270  fmtno4prmfac  48478  lighneallem4a  48514  requad01  48540  requad1  48541  requad2  48542  perfectALTVlem2  48641  gpg3kgrtriexlem1  49002  gpg3kgrtriexlem4  49005  gpg3kgrtriexlem6  49007  ply1mulgsumlem2  49320  digvalnn0  49532  dignn0fr  49534  dig2nn0  49544  affinecomb1  49635  rrx2linest2  49677  line2  49685  itsclc0lem1  49689  itsclc0lem2  49690  itsclc0lem3  49691  itscnhlc0yqe  49692  itsclc0yqsollem2  49696  itsclc0yqsol  49697  itscnhlc0xyqsol  49698  itsclc0xyqsolr  49702  itsclinecirc0  49706  itsclinecirc0b  49707  itsclinecirc0in  49708  itsclquadb  49709  itsclquadeu  49710  2itscp  49714  itscnhlinecirc02plem1  49715  itscnhlinecirc02p  49718  inlinecirc02plem  49719  crosspcle1d  50791  crosspcle2d  50792  crosspcle3d  50793  crosspdotsumlem  50800  crosspdotd  50801  crosspaltd  50802  crossp3d  50803  veronesefvcl  50808  veronesev4lem  50812  veronesev5lem  50813  veronesev6lem  50814  veroquadgsumlem  50819  veroquadmodzerod  50820  amgmwlem  50823