Theorem remulcld 11170

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7362  ℝcr 11032   · cmul 11038

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

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

This theorem is referenced by:  mulge0  11663  msqge0  11666  redivcl  11869  prodgt0  11997  ltmul1a  11999  ltmul1  12000  ltmuldiv  12024  lt2msq1  12035  lt2msq  12036  le2msq  12051  msq11  12052  supmul1  12120  supmullem2  12122  supmul  12123  div4p1lem1div2  12427  mul2lt0rlt0  13041  mul2lt0bi  13045  prodge0rd  13046  ge2halflem1  13054  qbtwnre  13146  xmulneg1  13216  xmulf  13219  lincmb01cmp  13443  iccf1o  13444  flmulnn0  13781  flhalf  13784  modcl  13827  mod0  13830  modge0  13833  modmulnn  13843  mulp1mod1  13868  muladdmod  13869  2txmodxeq0  13888  modaddmulmod  13895  moddi  13896  modsubdir  13897  modirr  13899  addmodlteq  13903  bernneq  14186  bernneq3  14188  expnbnd  14189  expmulnbnd  14192  discr1  14196  discr  14197  faclbnd  14247  faclbnd6  14256  remullem  15085  01sqrexlem7  15205  sqrtmul  15216  abstri  15288  sqreulem  15317  bhmafibid1  15425  mulcn2  15553  reccn2  15554  o1rlimmul  15576  lo1mul  15585  iseraltlem2  15640  iseraltlem3  15641  iseralt  15642  o1fsum  15771  cvgcmpce  15776  climcndslem1  15809  climcndslem2  15810  climcnds  15811  geomulcvg  15836  cvgrat  15843  mertenslem1  15844  fprodge1  15955  eftlub  16071  sin02gt0  16154  eirrlem  16166  bitsp1o  16397  2mulprm  16657  isprm5  16672  modprm0  16771  prmreclem3  16884  prmreclem4  16885  prmreclem5  16886  2expltfac  17058  metss2lem  24490  nlmvscnlem2  24664  nrginvrcnlem  24670  nmoco  24716  nmotri  24718  nghmcn  24724  icopnfhmeo  24924  nmoleub2lem3  25096  ipcau2  25215  tcphcphlem1  25216  ipcnlem2  25225  rrxcph  25373  csbren  25380  trirn  25381  pjthlem1  25418  opnmbllem  25582  vitalilem4  25592  itg1val2  25665  itg1cl  25666  itg1ge0  25667  itg1addlem4  25680  itg1mulc  25685  itg1ge0a  25692  itg1climres  25695  mbfi1fseqlem1  25696  mbfi1fseqlem3  25698  mbfi1fseqlem4  25699  mbfi1fseqlem5  25700  mbfi1fseqlem6  25701  itg2const2  25722  itg2mulclem  25727  itg2mulc  25728  itg2monolem1  25731  itg2monolem3  25733  itg2cnlem2  25743  iblconst  25799  iblmulc2  25812  itgmulc2lem1  25813  itgmulc2lem2  25814  bddmulibl  25820  bddiblnc  25823  dveflem  25960  cmvth  25972  dvlip  25974  dvlipcn  25975  dvivthlem1  25989  lhop1lem  25994  dvcvx  26001  dvfsumlem2  26008  dvfsumlem3  26009  dvfsumlem4  26010  dvfsum2  26015  ftc1lem4  26020  plyeq0lem  26189  aalioulem3  26315  aalioulem4  26316  aaliou3lem9  26331  ulmdvlem1  26382  itgulm  26390  radcnvlem1  26395  radcnvlem2  26396  dvradcnv  26403  abelthlem2  26414  abelthlem7  26420  tangtx  26486  tanregt0  26520  logdivlti  26601  logcnlem3  26625  logcnlem4  26626  logccv  26644  recxpcl  26656  cxpmul  26669  cxplt  26675  cxple2  26678  abscxpbnd  26734  lawcoslem1  26796  heron  26819  atans2  26912  efrlim  26950  efrlimOLD  26951  o1cxp  26956  scvxcvx  26967  jensenlem2  26969  amgmlem  26971  fsumharmonic  26993  lgamgulmlem2  27011  lgamgulmlem3  27012  lgamgulmlem4  27013  lgamgulmlem5  27014  lgamgulmlem6  27015  relgamcl  27043  ftalem1  27054  ftalem2  27055  ftalem5  27058  basellem3  27064  basellem8  27069  chpub  27201  logfacubnd  27202  logfaclbnd  27203  logfacbnd3  27204  logexprlim  27206  perfectlem2  27211  bclbnd  27261  efexple  27262  bposlem1  27265  bposlem2  27266  bposlem6  27270  bposlem9  27273  lgsdilem  27305  gausslemma2dlem0c  27339  gausslemma2dlem2  27348  gausslemma2dlem3  27349  gausslemma2dlem6  27353  lgseisenlem4  27359  lgseisen  27360  lgsquadlem1  27361  lgsquadlem2  27362  2lgslem1a1  27370  2sqmod  27417  chebbnd1lem1  27450  chebbnd1lem3  27452  chtppilimlem1  27454  chpchtlim  27460  vmadivsum  27463  rplogsumlem1  27465  rpvmasumlem  27468  dchrisumlem2  27471  dchrisumlem3  27472  dchrmusum2  27475  dchrvmasumlem2  27479  dchrvmasumiflem1  27482  dchrisum0re  27494  dchrisum0lem1  27497  dirith2  27509  mulogsumlem  27512  mulogsum  27513  mulog2sumlem2  27516  vmalogdivsum2  27519  vmalogdivsum  27520  2vmadivsumlem  27521  logsqvma  27523  logsqvma2  27524  log2sumbnd  27525  selberglem2  27527  selberg  27529  selbergb  27530  selberg2lem  27531  selberg2b  27533  chpdifbndlem1  27534  chpdifbndlem2  27535  selberg3lem1  27538  selberg3lem2  27539  selberg3  27540  selberg4lem1  27541  selberg4  27542  pntrsumbnd2  27548  selberg3r  27550  selberg4r  27551  selberg34r  27552  pntsf  27554  pntsval2  27557  pntrlog2bndlem1  27558  pntrlog2bndlem2  27559  pntrlog2bndlem3  27560  pntrlog2bndlem4  27561  pntrlog2bndlem5  27562  pntrlog2bndlem6  27564  pntrlog2bnd  27565  pntpbnd1a  27566  pntpbnd1  27567  pntpbnd2  27568  pntibndlem2a  27571  pntibndlem2  27572  pntlemb  27578  pntlemr  27583  pntlemj  27584  pntlemf  27586  pntlemk  27587  pntlemo  27588  pntlem3  27590  ostth2lem1  27599  ostth2lem2  27615  ostth2lem3  27616  ostth2lem4  27617  ostth3  27619  ttgcontlem1  28971  brbtwn2  28992  colinearalglem4  28996  axsegconlem8  29011  axsegconlem9  29012  axsegconlem10  29013  ax5seglem3  29018  axpaschlem  29027  axpasch  29028  axeuclidlem  29049  numclwwlk5  30477  numclwwlk7  30480  smcnlem  30787  ubthlem2  30961  htthlem  31007  pjhthlem1  31481  cnlnadjlem7  32163  nmopcoadji  32191  branmfn  32195  leopnmid  32228  nexple  32936  constrremulcl  33931  constrmulcl  33935  cos9thpiminplylem1  33946  cos9thpinconstrlem1  33953  rmulccn  34092  xrge0iifhom  34101  dya2icoseg  34441  eulerpartlems  34524  eulerpartlemgc  34526  eulerpartlemb  34532  plymulx0  34711  signsvtp  34747  reprgt  34785  breprexplemc  34796  circlemethhgt  34807  hgt750lemd  34812  logdivsqrle  34814  hgt750lem  34815  hgt750lemf  34817  hgt750lemb  34820  hgt750lema  34821  hgt750leme  34822  tgoldbachgtde  34824  resconn  35448  knoppcnlem2  36774  knoppcnlem4  36776  knoppcnlem10  36782  unbdqndv2lem1  36789  unbdqndv2lem2  36790  knoppndvlem1  36792  knoppndvlem11  36802  knoppndvlem12  36803  knoppndvlem14  36805  knoppndvlem15  36806  knoppndvlem17  36808  knoppndvlem18  36809  knoppndvlem19  36810  knoppndvlem20  36811  knoppndvlem21  36812  opnmbllem0  37995  itg2addnclem2  38011  itg2addnclem3  38012  iblmulc2nc  38024  itgmulc2nclem1  38025  ftc1cnnclem  38030  ftc1anclem3  38034  areacirclem4  38050  geomcau  38098  equivbnd  38129  bfplem1  38161  bfplem2  38162  bfp  38163  rrnequiv  38174  rrntotbnd  38175  lcmineqlem19  42504  lcmineqlem20  42505  lcmineqlem21  42506  lcmineqlem22  42507  3lexlogpow2ineq2  42516  dvrelogpow2b  42525  aks4d1p1p2  42527  aks4d1p1p4  42528  aks4d1p1p6  42530  aks4d1p1p7  42531  aks4d1p1p5  42532  aks4d1p1  42533  aks4d1p8d2  42542  aks4d1p8  42544  posbezout  42557  aks6d1c2lem4  42584  2np3bcnp1  42601  2ap1caineq  42602  aks6d1c6lem4  42630  aks6d1c7lem1  42637  aks6d1c7lem2  42638  resubdi  42846  remul02  42855  remul01  42857  remulinvcom  42883  rediveud  42893  redivcan3d  42898  redivrec2d  42910  rediv23d  42911  sn-0tie0  42914  renegmulnnass  42928  mulgt0con1d  42933  mulgt0con2d  42934  mulgt0b1d  42935  sn-ltmul2d  42936  mulgt0b2d  42941  sn-mulgt1d  42942  mulltgt0d  42945  mullt0b1d  42946  mullt0b2d  42947  sn-mullt0d  42948  sn-itrere  42951  sn-retire  42952  fltnltalem  43113  fltnlta  43114  3cubeslem2  43135  3cubeslem3r  43137  3cubeslem4  43139  irrapxlem1  43272  irrapxlem2  43273  irrapxlem3  43274  irrapxlem4  43275  irrapxlem5  43276  pellexlem2  43280  pellexlem6  43284  pell14qrgt0  43309  pell1qrge1  43320  pell1qrgaplem  43323  pellqrexplicit  43327  pellqrex  43329  rmspecsqrtnq  43356  rmxycomplete  43367  rmxypos  43397  ltrmynn0  43398  ltrmxnn0  43399  jm2.24nn  43409  jm2.17a  43410  jm2.17b  43411  jm2.17c  43412  jm2.27c  43457  jm3.1lem2  43468  areaquad  43666  sqrtcval  44090  resqrtval  44092  imsqrtval  44093  imo72b2lem0  44614  cvgdvgrat  44762  nzprmdif  44768  lt3addmuld  45756  fperiodmullem  45758  fperiodmul  45759  lt4addmuld  45761  xralrple2  45806  xralrple3  45825  ltmulneg  45843  fmul01  46032  fmuldfeqlem1  46034  fmul01lt1lem1  46036  sumnnodd  46082  ltmod  46088  0ellimcdiv  46099  limclner  46101  dvdivbd  46373  dvbdfbdioolem2  46379  dvbdfbdioo  46380  ioodvbdlimc1lem1  46381  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  stoweidlem1  46451  stoweidlem11  46461  stoweidlem13  46463  stoweidlem14  46464  stoweidlem16  46466  stoweidlem17  46467  stoweidlem22  46472  stoweidlem24  46474  stoweidlem25  46475  stoweidlem26  46476  stoweidlem30  46480  stoweidlem34  46484  stoweidlem36  46486  stoweidlem49  46499  stoweidlem59  46509  stoweidlem60  46510  wallispilem4  46518  wallispilem5  46519  wallispi  46520  wallispi2lem1  46521  wallispi2  46523  stirlinglem1  46524  stirlinglem3  46526  stirlinglem5  46528  stirlinglem6  46529  stirlinglem7  46530  stirlinglem10  46533  stirlinglem11  46534  stirlinglem12  46535  stirlinglem15  46538  stirlingr  46540  dirker2re  46542  dirkerval2  46544  dirkerre  46545  dirkertrigeqlem1  46548  dirkertrigeqlem2  46549  dirkeritg  46552  dirkercncflem2  46554  dirkercncflem4  46556  fourierdlem4  46561  fourierdlem5  46562  fourierdlem6  46563  fourierdlem7  46564  fourierdlem16  46573  fourierdlem18  46575  fourierdlem19  46576  fourierdlem21  46578  fourierdlem22  46579  fourierdlem26  46583  fourierdlem35  46592  fourierdlem39  46596  fourierdlem41  46598  fourierdlem42  46599  fourierdlem43  46600  fourierdlem48  46604  fourierdlem49  46605  fourierdlem51  46607  fourierdlem55  46611  fourierdlem56  46612  fourierdlem57  46613  fourierdlem58  46614  fourierdlem62  46618  fourierdlem63  46619  fourierdlem64  46620  fourierdlem65  46621  fourierdlem66  46622  fourierdlem67  46623  fourierdlem68  46624  fourierdlem71  46627  fourierdlem72  46628  fourierdlem73  46629  fourierdlem76  46632  fourierdlem77  46633  fourierdlem78  46634  fourierdlem83  46639  fourierdlem84  46640  fourierdlem87  46643  fourierdlem88  46644  fourierdlem89  46645  fourierdlem90  46646  fourierdlem91  46647  fourierdlem94  46650  fourierdlem95  46651  fourierdlem97  46653  fourierdlem103  46659  fourierdlem104  46660  fourierdlem112  46668  fourierdlem113  46669  sqwvfoura  46678  sqwvfourb  46679  fouriersw  46681  etransclem23  46707  etransclem48  46732  rrndistlt  46740  hoidmvlelem1  47045  hoidmvlelem2  47046  hoidmvlelem4  47048  smfmullem1  47241  smfmullem2  47242  smfmullem3  47243  smfmul  47245  2timesltsqm1  47843  fmtno4prmfac  48051  lighneallem4a  48087  requad01  48113  requad1  48114  requad2  48115  perfectALTVlem2  48214  gpg3kgrtriexlem1  48575  gpg3kgrtriexlem4  48578  gpg3kgrtriexlem6  48580  ply1mulgsumlem2  48879  digvalnn0  49091  dignn0fr  49093  dig2nn0  49103  affinecomb1  49194  rrx2linest2  49236  line2  49244  itsclc0lem1  49248  itsclc0lem2  49249  itsclc0lem3  49250  itscnhlc0yqe  49251  itsclc0yqsollem2  49255  itsclc0yqsol  49256  itscnhlc0xyqsol  49257  itsclc0xyqsolr  49261  itsclinecirc0  49265  itsclinecirc0b  49266  itsclinecirc0in  49267  itsclquadb  49268  itsclquadeu  49269  2itscp  49273  itscnhlinecirc02plem1  49274  itscnhlinecirc02p  49277  inlinecirc02plem  49278  amgmwlem  50293