Theorem remulcld 10671

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7156  ℝcr 10536   · cmul 10542

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

This theorem depends on definitions:  df-bi 209  df-an 399

This theorem is referenced by:  mulge0  11158  msqge0  11161  redivcl  11359  prodgt0  11487  ltmul1a  11489  ltmul1  11490  ltmuldiv  11513  lt2msq1  11524  lt2msq  11525  le2msq  11540  msq11  11541  supmul1  11610  supmullem2  11612  supmul  11613  div4p1lem1div2  11893  mul2lt0rlt0  12492  mul2lt0bi  12496  prodge0rd  12497  qbtwnre  12593  xmulneg1  12663  xmulf  12666  lincmb01cmp  12882  iccf1o  12883  flmulnn0  13198  flhalf  13201  modcl  13242  mod0  13245  modge0  13248  modmulnn  13258  mulp1mod1  13281  2txmodxeq0  13300  modaddmulmod  13307  moddi  13308  modsubdir  13309  modirr  13311  addmodlteq  13315  bernneq  13591  bernneq3  13593  expnbnd  13594  expmulnbnd  13597  discr1  13601  discr  13602  faclbnd  13651  faclbnd6  13660  remullem  14487  sqrlem7  14608  sqrtmul  14619  abstri  14690  sqreulem  14719  bhmafibid1  14825  mulcn2  14952  reccn2  14953  o1rlimmul  14975  lo1mul  14984  iseraltlem2  15039  iseraltlem3  15040  iseralt  15041  o1fsum  15168  cvgcmpce  15173  climcndslem1  15204  climcndslem2  15205  climcnds  15206  geomulcvg  15232  cvgrat  15239  mertenslem1  15240  fprodge1  15349  eftlub  15462  sin02gt0  15545  eirrlem  15557  bitsp1o  15782  2mulprm  16037  isprm5  16051  modprm0  16142  prmreclem3  16254  prmreclem4  16255  prmreclem5  16256  2expltfac  16426  metss2lem  23121  nlmvscnlem2  23294  nrginvrcnlem  23300  nmoco  23346  nmotri  23348  nghmcn  23354  icopnfhmeo  23547  nmoleub2lem3  23719  ipcau2  23837  tcphcphlem1  23838  ipcnlem2  23847  rrxcph  23995  csbren  24002  trirn  24003  pjthlem1  24040  opnmbllem  24202  vitalilem4  24212  itg1val2  24285  itg1cl  24286  itg1ge0  24287  itg1addlem4  24300  itg1mulc  24305  itg1ge0a  24312  itg1climres  24315  mbfi1fseqlem1  24316  mbfi1fseqlem3  24318  mbfi1fseqlem4  24319  mbfi1fseqlem5  24320  mbfi1fseqlem6  24321  itg2const2  24342  itg2mulclem  24347  itg2mulc  24348  itg2monolem1  24351  itg2monolem3  24353  itg2cnlem2  24363  iblconst  24418  iblmulc2  24431  itgmulc2lem1  24432  itgmulc2lem2  24433  bddmulibl  24439  dveflem  24576  cmvth  24588  dvlip  24590  dvlipcn  24591  dvivthlem1  24605  lhop1lem  24610  dvcvx  24617  dvfsumlem2  24624  dvfsumlem3  24625  dvfsumlem4  24626  dvfsum2  24631  ftc1lem4  24636  plyeq0lem  24800  aalioulem3  24923  aalioulem4  24924  aaliou3lem9  24939  ulmdvlem1  24988  itgulm  24996  radcnvlem1  25001  radcnvlem2  25002  dvradcnv  25009  abelthlem2  25020  abelthlem7  25026  tangtx  25091  tanregt0  25123  logdivlti  25203  logcnlem3  25227  logcnlem4  25228  logccv  25246  recxpcl  25258  cxpmul  25271  cxplt  25277  cxple2  25280  abscxpbnd  25334  lawcoslem1  25393  heron  25416  atans2  25509  efrlim  25547  o1cxp  25552  scvxcvx  25563  jensenlem2  25565  amgmlem  25567  fsumharmonic  25589  lgamgulmlem2  25607  lgamgulmlem3  25608  lgamgulmlem4  25609  lgamgulmlem5  25610  lgamgulmlem6  25611  relgamcl  25639  ftalem1  25650  ftalem2  25651  ftalem5  25654  basellem3  25660  basellem8  25665  chpub  25796  logfacubnd  25797  logfaclbnd  25798  logfacbnd3  25799  logexprlim  25801  perfectlem2  25806  bclbnd  25856  efexple  25857  bposlem1  25860  bposlem2  25861  bposlem6  25865  bposlem9  25868  lgsdilem  25900  gausslemma2dlem0c  25934  gausslemma2dlem2  25943  gausslemma2dlem3  25944  gausslemma2dlem6  25948  lgseisenlem4  25954  lgseisen  25955  lgsquadlem1  25956  lgsquadlem2  25957  2lgslem1a1  25965  2sqmod  26012  chebbnd1lem1  26045  chebbnd1lem3  26047  chtppilimlem1  26049  chpchtlim  26055  vmadivsum  26058  rplogsumlem1  26060  rpvmasumlem  26063  dchrisumlem2  26066  dchrisumlem3  26067  dchrmusum2  26070  dchrvmasumlem2  26074  dchrvmasumiflem1  26077  dchrisum0re  26089  dchrisum0lem1  26092  dirith2  26104  mulogsumlem  26107  mulogsum  26108  mulog2sumlem2  26111  vmalogdivsum2  26114  vmalogdivsum  26115  2vmadivsumlem  26116  logsqvma  26118  logsqvma2  26119  log2sumbnd  26120  selberglem2  26122  selberg  26124  selbergb  26125  selberg2lem  26126  selberg2b  26128  chpdifbndlem1  26129  chpdifbndlem2  26130  selberg3lem1  26133  selberg3lem2  26134  selberg3  26135  selberg4lem1  26136  selberg4  26137  pntrsumbnd2  26143  selberg3r  26145  selberg4r  26146  selberg34r  26147  pntsf  26149  pntsval2  26152  pntrlog2bndlem1  26153  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  pntrlog2bndlem6  26159  pntrlog2bnd  26160  pntpbnd1a  26161  pntpbnd1  26162  pntpbnd2  26163  pntibndlem2a  26166  pntibndlem2  26167  pntlemb  26173  pntlemr  26178  pntlemj  26179  pntlemf  26181  pntlemk  26182  pntlemo  26183  pntlem3  26185  ostth2lem1  26194  ostth2lem2  26210  ostth2lem3  26211  ostth2lem4  26212  ostth3  26214  ttgcontlem1  26671  brbtwn2  26691  colinearalglem4  26695  axsegconlem8  26710  axsegconlem9  26711  axsegconlem10  26712  ax5seglem3  26717  axpaschlem  26726  axpasch  26727  axeuclidlem  26748  numclwwlk5  28167  numclwwlk7  28170  smcnlem  28474  ubthlem2  28648  htthlem  28694  pjhthlem1  29168  cnlnadjlem7  29850  nmopcoadji  29878  branmfn  29882  leopnmid  29915  rmulccn  31171  xrge0iifhom  31180  nexple  31268  dya2icoseg  31535  eulerpartlems  31618  eulerpartlemgc  31620  eulerpartlemb  31626  plymulx0  31817  signsvtp  31853  reprgt  31892  breprexplemc  31903  circlemethhgt  31914  hgt750lemd  31919  logdivsqrle  31921  hgt750lem  31922  hgt750lemf  31924  hgt750lemb  31927  hgt750lema  31928  hgt750leme  31929  tgoldbachgtde  31931  resconn  32493  knoppcnlem2  33833  knoppcnlem4  33835  knoppcnlem10  33841  unbdqndv2lem1  33848  unbdqndv2lem2  33849  knoppndvlem1  33851  knoppndvlem11  33861  knoppndvlem12  33862  knoppndvlem14  33864  knoppndvlem15  33865  knoppndvlem17  33867  knoppndvlem18  33868  knoppndvlem19  33869  knoppndvlem20  33870  knoppndvlem21  33871  opnmbllem0  34943  itg2addnclem2  34959  itg2addnclem3  34960  iblmulc2nc  34972  itgmulc2nclem1  34973  bddiblnc  34977  ftc1cnnclem  34980  ftc1anclem3  34984  areacirclem4  35000  geomcau  35049  equivbnd  35083  bfplem1  35115  bfplem2  35116  bfp  35117  rrnequiv  35128  rrntotbnd  35129  cxpgt0d  39229  resubdi  39275  remul02  39284  remul01  39286  remulinvcom  39297  fltnltalem  39323  fltnlta  39324  3cubeslem2  39331  3cubeslem3r  39333  3cubeslem4  39335  irrapxlem1  39468  irrapxlem2  39469  irrapxlem3  39470  irrapxlem4  39471  irrapxlem5  39472  pellexlem2  39476  pellexlem6  39480  pell14qrgt0  39505  pell1qrge1  39516  pell1qrgaplem  39519  pellqrexplicit  39523  pellqrex  39525  rmspecsqrtnq  39552  rmxycomplete  39563  rmxypos  39593  ltrmynn0  39594  ltrmxnn0  39595  jm2.24nn  39605  jm2.17a  39606  jm2.17b  39607  jm2.17c  39608  jm2.27c  39653  jm3.1lem2  39664  areaquad  39872  imo72b2lem0  40565  cvgdvgrat  40694  nzprmdif  40700  lt3addmuld  41617  fperiodmullem  41619  fperiodmul  41620  lt4addmuld  41622  xralrple2  41671  xralrple3  41691  ltmulneg  41713  fmul01  41910  fmuldfeqlem1  41912  fmul01lt1lem1  41914  sumnnodd  41960  ltmod  41968  0ellimcdiv  41979  limclner  41981  dvdivbd  42257  dvbdfbdioolem2  42263  dvbdfbdioo  42264  ioodvbdlimc1lem1  42265  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  stoweidlem1  42335  stoweidlem11  42345  stoweidlem13  42347  stoweidlem14  42348  stoweidlem16  42350  stoweidlem17  42351  stoweidlem22  42356  stoweidlem24  42358  stoweidlem25  42359  stoweidlem26  42360  stoweidlem30  42364  stoweidlem34  42368  stoweidlem36  42370  stoweidlem49  42383  stoweidlem59  42393  stoweidlem60  42394  wallispilem4  42402  wallispilem5  42403  wallispi  42404  wallispi2lem1  42405  wallispi2  42407  stirlinglem1  42408  stirlinglem3  42410  stirlinglem5  42412  stirlinglem6  42413  stirlinglem7  42414  stirlinglem10  42417  stirlinglem11  42418  stirlinglem12  42419  stirlinglem15  42422  stirlingr  42424  dirker2re  42426  dirkerval2  42428  dirkerre  42429  dirkertrigeqlem1  42432  dirkertrigeqlem2  42433  dirkeritg  42436  dirkercncflem2  42438  dirkercncflem4  42440  fourierdlem4  42445  fourierdlem5  42446  fourierdlem6  42447  fourierdlem7  42448  fourierdlem16  42457  fourierdlem18  42459  fourierdlem19  42460  fourierdlem21  42462  fourierdlem22  42463  fourierdlem26  42467  fourierdlem35  42476  fourierdlem39  42480  fourierdlem41  42482  fourierdlem42  42483  fourierdlem43  42484  fourierdlem48  42488  fourierdlem49  42489  fourierdlem51  42491  fourierdlem55  42495  fourierdlem56  42496  fourierdlem57  42497  fourierdlem58  42498  fourierdlem62  42502  fourierdlem63  42503  fourierdlem64  42504  fourierdlem65  42505  fourierdlem66  42506  fourierdlem67  42507  fourierdlem68  42508  fourierdlem71  42511  fourierdlem72  42512  fourierdlem73  42513  fourierdlem76  42516  fourierdlem77  42517  fourierdlem78  42518  fourierdlem83  42523  fourierdlem84  42524  fourierdlem87  42527  fourierdlem88  42528  fourierdlem89  42529  fourierdlem90  42530  fourierdlem91  42531  fourierdlem94  42534  fourierdlem95  42535  fourierdlem97  42537  fourierdlem103  42543  fourierdlem104  42544  fourierdlem112  42552  fourierdlem113  42553  sqwvfoura  42562  sqwvfourb  42563  fouriersw  42565  etransclem23  42591  etransclem48  42616  rrndistlt  42624  hoidmvlelem1  42926  hoidmvlelem2  42927  hoidmvlelem4  42929  smfmullem1  43115  smfmullem2  43116  smfmullem3  43117  smfmul  43119  fmtno4prmfac  43783  lighneallem4a  43822  requad01  43835  requad1  43836  requad2  43837  perfectALTVlem2  43936  ply1mulgsumlem2  44490  digvalnn0  44708  dignn0fr  44710  dig2nn0  44720  affinecomb1  44738  rrx2linest2  44780  line2  44788  itsclc0lem1  44792  itsclc0lem2  44793  itsclc0lem3  44794  itscnhlc0yqe  44795  itsclc0yqsollem2  44799  itsclc0yqsol  44800  itscnhlc0xyqsol  44801  itsclc0xyqsolr  44805  itsclinecirc0  44809  itsclinecirc0b  44810  itsclinecirc0in  44811  itsclquadb  44812  itsclquadeu  44813  2itscp  44817  itscnhlinecirc02plem1  44818  itscnhlinecirc02p  44821  inlinecirc02plem  44822  amgmwlem  44952