Theorem remulcld 11339

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  (class class class)co 7420  ℝcr 11199   · cmul 11205

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

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

This theorem is used by:  mulge0  11834  msqge0  11837  redivcl  12036  prodgt0  12164  ltmul1a  12166  ltmul1  12167  ltmuldiv  12190  lt2msq1  12201  lt2msq  12202  le2msq  12217  msq11  12218  supmul1  12286  supmullem2  12288  supmul  12289  div4p1lem1div2  12601  mul2lt0rlt0  13224  mul2lt0bi  13228  prodge0rd  13229  ge2halflem1  13237  qbtwnre  13329  xmulneg1  13399  xmulf  13402  lincmb01cmp  13626  iccf1o  13627  flmulnn0  13967  flhalf  13970  modcl  14013  mod0  14016  modge0  14019  modmulnn  14029  mulp1mod1  14054  muladdmod  14055  2txmodxeq0  14074  modaddmulmod  14081  moddi  14082  modsubdir  14083  modirr  14085  addmodlteq  14089  bernneq  14373  bernneq3  14375  expnbnd  14376  expmulnbnd  14379  discr1  14383  discr  14384  faclbnd  14434  faclbnd6  14443  remullem  15295  01sqrexlem7  15415  sqrtmul  15426  abstri  15498  sqreulem  15527  bhmafibid1  15635  mulcn2  15763  reccn2  15764  o1rlimmul  15786  lo1mul  15795  iseraltlem2  15850  iseraltlem3  15851  iseralt  15852  o1fsum  15980  cvgcmpce  15985  climcndslem1  16018  climcndslem2  16019  climcnds  16020  geomulcvg  16045  cvgrat  16052  mertenslem1  16053  fprodge1  16162  eftlub  16277  sin02gt0  16360  eirrlem  16372  bitsp1o  16603  2mulprm  16868  isprm5  16883  modprm0  16983  prmreclem3  17096  prmreclem4  17097  prmreclem5  17098  2expltfac  17270  metss2lem  24830  nlmvscnlem2  25004  nrginvrcnlem  25010  nmoco  25056  nmotri  25058  nghmcn  25064  icopnfhmeo  25264  nmoleub2lem3  25436  ipcau2  25555  tcphcphlem1  25556  ipcnlem2  25565  rrxcph  25713  csbren  25720  trirn  25721  pjthlem1  25758  opnmbllem  25922  vitalilem4  25932  itg1val2  26005  itg1cl  26006  itg1ge0  26007  itg1addlem4  26020  itg1mulc  26025  itg1ge0a  26032  itg1climres  26035  mbfi1fseqlem1  26036  mbfi1fseqlem3  26038  mbfi1fseqlem4  26039  mbfi1fseqlem5  26040  mbfi1fseqlem6  26041  itg2const2  26062  itg2mulclem  26067  itg2mulc  26068  itg2monolem1  26071  itg2monolem3  26073  itg2cnlem2  26083  iblconst  26138  iblmulc2  26151  itgmulc2lem1  26152  itgmulc2lem2  26153  bddmulibl  26159  bddiblnc  26162  dveflem  26299  cmvth  26311  dvlip  26313  dvlipcn  26314  dvivthlem1  26328  lhop1lem  26333  dvcvx  26340  dvfsumlem2  26347  dvfsumlem3  26348  dvfsumlem4  26349  dvfsum2  26354  ftc1lem4  26359  plyeq0lem  26529  plyn0mulidp  26602  aalioulem3  26661  aalioulem4  26662  aaliou3lem9  26677  ulmdvlem1  26727  itgulm  26735  radcnvlem1  26740  radcnvlem2  26741  dvradcnv  26748  abelthlem2  26759  abelthlem7  26765  tangtx  26834  tanregt0  26867  logdivlti  26948  logcnlem3  26972  logcnlem4  26973  logccv  26991  recxpcl  27003  cxpmul  27016  cxplt  27022  cxple2  27025  abscxpbnd  27081  lawcoslem1  27143  heron  27166  atans2  27259  efrlim  27297  o1cxp  27302  scvxcvx  27313  jensenlem2  27315  amgmlem  27317  fsumharmonic  27339  lgamgulmlem2  27357  lgamgulmlem3  27358  lgamgulmlem4  27359  lgamgulmlem5  27360  lgamgulmlem6  27361  relgamcl  27389  ftalem1  27400  ftalem2  27401  ftalem5  27404  basellem3  27410  basellem8  27415  chpub  27547  logfacubnd  27548  logfaclbnd  27549  logfacbnd3  27550  logexprlim  27552  perfectlem2  27557  bclbnd  27607  efexple  27608  bposlem1  27611  bposlem2  27612  bposlem6  27616  bposlem9  27619  lgsdilem  27651  gausslemma2dlem0c  27685  gausslemma2dlem2  27694  gausslemma2dlem3  27695  gausslemma2dlem6  27699  lgseisenlem4  27705  lgseisen  27706  lgsquadlem1  27707  lgsquadlem2  27708  2lgslem1a1  27716  2sqmod  27763  chebbnd1lem1  27796  chebbnd1lem3  27798  chtppilimlem1  27800  chpchtlim  27806  vmadivsum  27809  rplogsumlem1  27811  rpvmasumlem  27814  dchrisumlem2  27817  dchrisumlem3  27818  dchrmusum2  27821  dchrvmasumlem2  27825  dchrvmasumiflem1  27828  dchrisum0re  27840  dchrisum0lem1  27843  dirith2  27855  mulogsumlem  27858  mulogsum  27859  mulog2sumlem2  27862  vmalogdivsum2  27865  vmalogdivsum  27866  2vmadivsumlem  27867  logsqvma  27869  logsqvma2  27870  log2sumbnd  27871  selberglem2  27873  selberg  27875  selbergb  27876  selberg2lem  27877  selberg2b  27879  chpdifbndlem1  27880  chpdifbndlem2  27881  selberg3lem1  27884  selberg3lem2  27885  selberg3  27886  selberg4lem1  27887  selberg4  27888  pntrsumbnd2  27894  selberg3r  27896  selberg4r  27897  selberg34r  27898  pntsf  27900  pntsval2  27903  pntrlog2bndlem1  27904  pntrlog2bndlem2  27905  pntrlog2bndlem3  27906  pntrlog2bndlem4  27907  pntrlog2bndlem5  27908  pntrlog2bndlem6  27910  pntrlog2bnd  27911  pntpbnd1a  27912  pntpbnd1  27913  pntpbnd2  27914  pntibndlem2a  27917  pntibndlem2  27918  pntlemb  27924  pntlemr  27929  pntlemj  27930  pntlemf  27932  pntlemk  27933  pntlemo  27934  pntlem3  27936  ostth2lem1  27945  ostth2lem2  27961  ostth2lem3  27962  ostth2lem4  27963  ostth3  27965  ttgcontlem1  29462  brbtwn2  29483  colinearalglem4  29487  axsegconlem8  29502  axsegconlem9  29503  axsegconlem10  29504  ax5seglem3  29509  axpaschlem  29518  axpasch  29519  axeuclidlem  29540  numclwwlk5  30989  numclwwlk7  30992  smcnlem  31299  ubthlem2  31473  htthlem  31519  pjhthlem1  31993  cnlnadjlem7  32675  nmopcoadji  32703  branmfn  32707  leopnmid  32740  nexple  33424  constrremulcl  34399  constrmulcl  34403  cos9thpiminplylem1  34414  cos9thpinconstrlem1  34421  rmulccn  34560  xrge0iifhom  34569  dya2icoseg  34909  eulerpartlems  34992  eulerpartlemgc  34994  eulerpartlemb  35000  signsvtp  35212  reprgt  35250  breprexplemc  35261  circlemethhgt  35272  hgt750lemd  35277  logdivsqrle  35279  hgt750lem  35280  hgt750lemf  35282  hgt750lemb  35285  hgt750lema  35286  hgt750leme  35287  tgoldbachgtde  35289  resconn  36011  knoppcnlem2  37360  knoppcnlem4  37362  knoppcnlem10  37368  unbdqndv2lem1  37375  unbdqndv2lem2  37376  knoppndvlem1  37378  knoppndvlem11  37388  knoppndvlem12  37389  knoppndvlem14  37391  knoppndvlem15  37392  knoppndvlem17  37394  knoppndvlem18  37395  knoppndvlem19  37396  knoppndvlem20  37397  knoppndvlem21  37398  opnmbllem0  38575  itg2addnclem2  38591  itg2addnclem3  38592  iblmulc2nc  38604  itgmulc2nclem1  38605  ftc1cnnclem  38610  ftc1anclem3  38614  areacirclem4  38630  geomcau  38694  equivbnd  38725  bfplem1  38757  bfplem2  38758  bfp  38759  rrnequiv  38770  rrntotbnd  38771  lcmineqlem19  43098  lcmineqlem20  43099  lcmineqlem21  43100  lcmineqlem22  43101  3lexlogpow2ineq2  43110  dvrelogpow2b  43119  aks4d1p1p2  43121  aks4d1p1p4  43122  aks4d1p1p6  43124  aks4d1p1p7  43125  aks4d1p1p5  43126  aks4d1p1  43127  aks4d1p8d2  43136  aks4d1p8  43138  posbezout  43151  aks6d1c2lem4  43178  2np3bcnp1  43195  2ap1caineq  43196  aks6d1c6lem4  43224  aks6d1c7lem1  43231  aks6d1c7lem2  43232  resubdi  43448  remul02  43457  remul01  43459  remulinvcom  43485  rediveud  43495  redivcan3d  43500  redivrec2d  43512  rediv23d  43513  sn-0tie0  43516  renegmulnnass  43530  mulgt0con1d  43535  mulgt0con2d  43536  mulgt0b1d  43537  sn-ltmul2d  43538  mulgt0b2d  43543  sn-mulgt1d  43544  mulltgt0d  43547  mullt0b1d  43548  mullt0b2d  43549  sn-mullt0d  43550  sn-itrere  43553  sn-retire  43554  fltnltalem  43674  fltnlta  43675  3cubeslem2  43696  3cubeslem3r  43698  3cubeslem4  43700  irrapxlem1  43829  irrapxlem2  43830  irrapxlem3  43831  irrapxlem4  43832  irrapxlem5  43833  pellexlem2  43837  pellexlem6  43841  pell14qrgt0  43866  pell1qrge1  43877  pell1qrgaplem  43880  pellqrexplicit  43884  pellqrex  43886  rmspecsqrtnq  43913  rmxycomplete  43924  rmxypos  43954  ltrmynn0  43955  ltrmxnn0  43956  jm2.24nn  43966  jm2.17a  43967  jm2.17b  43968  jm2.17c  43969  jm2.27c  44014  jm3.1lem2  44025  areaquad  44218  sqrtcval  44641  resqrtval  44643  imsqrtval  44644  imo72b2lem0  45165  cvgdvgrat  45297  nzprmdif  45303  lt3addmuld  46317  fperiodmullem  46319  fperiodmul  46320  lt4addmuld  46322  xralrple2  46366  xralrple3  46385  ltmulneg  46403  fmul01  46592  fmuldfeqlem1  46594  fmul01lt1lem1  46596  sumnnodd  46642  ltmod  46648  0ellimcdiv  46659  limclner  46661  dvdivbd  46933  dvbdfbdioolem2  46939  dvbdfbdioo  46940  ioodvbdlimc1lem1  46941  ioodvbdlimc1lem2  46942  ioodvbdlimc2lem  46944  stoweidlem1  47011  stoweidlem11  47021  stoweidlem13  47023  stoweidlem14  47024  stoweidlem16  47026  stoweidlem17  47027  stoweidlem22  47032  stoweidlem24  47034  stoweidlem25  47035  stoweidlem26  47036  stoweidlem30  47040  stoweidlem34  47044  stoweidlem36  47046  stoweidlem49  47059  stoweidlem59  47069  stoweidlem60  47070  wallispilem4  47078  wallispilem5  47079  wallispi  47080  wallispi2lem1  47081  wallispi2  47083  stirlinglem1  47084  stirlinglem3  47086  stirlinglem5  47088  stirlinglem6  47089  stirlinglem7  47090  stirlinglem10  47093  stirlinglem11  47094  stirlinglem12  47095  stirlinglem15  47098  stirlingr  47100  dirker2re  47102  dirkerval2  47104  dirkerre  47105  dirkertrigeqlem1  47108  dirkertrigeqlem2  47109  dirkeritg  47112  dirkercncflem2  47114  dirkercncflem4  47116  fourierdlem4  47121  fourierdlem5  47122  fourierdlem6  47123  fourierdlem7  47124  fourierdlem16  47133  fourierdlem18  47135  fourierdlem19  47136  fourierdlem21  47138  fourierdlem22  47139  fourierdlem26  47143  fourierdlem35  47152  fourierdlem39  47156  fourierdlem41  47158  fourierdlem42  47159  fourierdlem43  47160  fourierdlem48  47164  fourierdlem49  47165  fourierdlem51  47167  fourierdlem55  47171  fourierdlem56  47172  fourierdlem57  47173  fourierdlem58  47174  fourierdlem62  47178  fourierdlem63  47179  fourierdlem64  47180  fourierdlem65  47181  fourierdlem66  47182  fourierdlem67  47183  fourierdlem68  47184  fourierdlem71  47187  fourierdlem72  47188  fourierdlem73  47189  fourierdlem76  47192  fourierdlem77  47193  fourierdlem78  47194  fourierdlem83  47199  fourierdlem84  47200  fourierdlem87  47203  fourierdlem88  47204  fourierdlem89  47205  fourierdlem90  47206  fourierdlem91  47207  fourierdlem94  47210  fourierdlem95  47211  fourierdlem97  47213  fourierdlem103  47219  fourierdlem104  47220  fourierdlem112  47228  fourierdlem113  47229  sqwvfoura  47238  sqwvfourb  47239  fouriersw  47241  etransclem23  47267  etransclem48  47292  rrndistlt  47300  hoidmvlelem1  47605  hoidmvlelem2  47606  hoidmvlelem4  47608  smfmullem1  47801  smfmullem2  47802  smfmullem3  47803  smfmul  47805  2timesltsqm1  48449  fmtno4prmfac  48657  lighneallem4a  48693  requad01  48719  requad1  48720  requad2  48721  perfectALTVlem2  48820  gpg3kgrtriexlem1  49181  gpg3kgrtriexlem4  49184  gpg3kgrtriexlem6  49186  ply1mulgsumlem2  49499  digvalnn0  49711  dignn0fr  49713  dig2nn0  49723  affinecomb1  49814  rrx2linest2  49856  line2  49864  itsclc0lem1  49868  itsclc0lem2  49869  itsclc0lem3  49870  itscnhlc0yqe  49871  itsclc0yqsollem2  49875  itsclc0yqsol  49876  itscnhlc0xyqsol  49877  itsclc0xyqsolr  49881  itsclinecirc0  49885  itsclinecirc0b  49886  itsclinecirc0in  49887  itsclquadb  49888  itsclquadeu  49889  2itscp  49893  itscnhlinecirc02plem1  49894  itscnhlinecirc02p  49897  inlinecirc02plem  49898  crosspcle1d  50955  crosspcle2d  50956  crosspcle3d  50957  crosspdotsumlem  50964  crosspdotd  50965  crosspaltd  50966  crossp3d  50967  veronesefvcl  50972  veronesev4lem  50976  veronesev5lem  50977  veronesev6lem  50978  veroquadgsumlem  50983  veroquadmodzerod  50984  amgmwlem  50987