Theorem remulcld 11264

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7416  ℝcr 11124   · cmul 11130

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

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

This theorem is used by:  mulge0  11757  msqge0  11760  redivcl  11959  prodgt0  12087  ltmul1a  12089  ltmul1  12090  ltmuldiv  12113  lt2msq1  12124  lt2msq  12125  le2msq  12140  msq11  12141  supmul1  12209  supmullem2  12211  supmul  12212  div4p1lem1div2  12524  mul2lt0rlt0  13146  mul2lt0bi  13150  prodge0rd  13151  ge2halflem1  13159  qbtwnre  13251  xmulneg1  13321  xmulf  13324  lincmb01cmp  13548  iccf1o  13549  flmulnn0  13888  flhalf  13891  modcl  13934  mod0  13937  modge0  13940  modmulnn  13950  mulp1mod1  13975  muladdmod  13976  2txmodxeq0  13995  modaddmulmod  14002  moddi  14003  modsubdir  14004  modirr  14006  addmodlteq  14010  bernneq  14293  bernneq3  14295  expnbnd  14296  expmulnbnd  14299  discr1  14303  discr  14304  faclbnd  14354  faclbnd6  14363  remullem  15215  01sqrexlem7  15335  sqrtmul  15346  abstri  15418  sqreulem  15447  bhmafibid1  15555  mulcn2  15683  reccn2  15684  o1rlimmul  15706  lo1mul  15715  iseraltlem2  15770  iseraltlem3  15771  iseralt  15772  o1fsum  15900  cvgcmpce  15905  climcndslem1  15938  climcndslem2  15939  climcnds  15940  geomulcvg  15965  cvgrat  15972  mertenslem1  15973  fprodge1  16084  eftlub  16199  sin02gt0  16282  eirrlem  16294  bitsp1o  16525  2mulprm  16785  isprm5  16800  modprm0  16899  prmreclem3  17012  prmreclem4  17013  prmreclem5  17014  2expltfac  17186  metss2lem  24736  nlmvscnlem2  24910  nrginvrcnlem  24916  nmoco  24962  nmotri  24964  nghmcn  24970  icopnfhmeo  25170  nmoleub2lem3  25342  ipcau2  25461  tcphcphlem1  25462  ipcnlem2  25471  rrxcph  25619  csbren  25626  trirn  25627  pjthlem1  25664  opnmbllem  25828  vitalilem4  25838  itg1val2  25911  itg1cl  25912  itg1ge0  25913  itg1addlem4  25926  itg1mulc  25931  itg1ge0a  25938  itg1climres  25941  mbfi1fseqlem1  25942  mbfi1fseqlem3  25944  mbfi1fseqlem4  25945  mbfi1fseqlem5  25946  mbfi1fseqlem6  25947  itg2const2  25968  itg2mulclem  25973  itg2mulc  25974  itg2monolem1  25977  itg2monolem3  25979  itg2cnlem2  25989  iblconst  26045  iblmulc2  26058  itgmulc2lem1  26059  itgmulc2lem2  26060  bddmulibl  26066  bddiblnc  26069  dveflem  26206  cmvth  26218  dvlip  26220  dvlipcn  26221  dvivthlem1  26235  lhop1lem  26240  dvcvx  26247  dvfsumlem2  26254  dvfsumlem3  26255  dvfsumlem4  26256  dvfsum2  26261  ftc1lem4  26266  plyeq0lem  26435  plyn0mulidp  26510  aalioulem3  26565  aalioulem4  26566  aaliou3lem9  26581  ulmdvlem1  26631  itgulm  26639  radcnvlem1  26644  radcnvlem2  26645  dvradcnv  26652  abelthlem2  26663  abelthlem7  26669  tangtx  26738  tanregt0  26772  logdivlti  26853  logcnlem3  26877  logcnlem4  26878  logccv  26896  recxpcl  26908  cxpmul  26921  cxplt  26927  cxple2  26930  abscxpbnd  26986  lawcoslem1  27048  heron  27071  atans2  27164  efrlim  27202  o1cxp  27207  scvxcvx  27218  jensenlem2  27220  amgmlem  27222  fsumharmonic  27244  lgamgulmlem2  27262  lgamgulmlem3  27263  lgamgulmlem4  27264  lgamgulmlem5  27265  lgamgulmlem6  27266  relgamcl  27294  ftalem1  27305  ftalem2  27306  ftalem5  27309  basellem3  27315  basellem8  27320  chpub  27452  logfacubnd  27453  logfaclbnd  27454  logfacbnd3  27455  logexprlim  27457  perfectlem2  27462  bclbnd  27512  efexple  27513  bposlem1  27516  bposlem2  27517  bposlem6  27521  bposlem9  27524  lgsdilem  27556  gausslemma2dlem0c  27590  gausslemma2dlem2  27599  gausslemma2dlem3  27600  gausslemma2dlem6  27604  lgseisenlem4  27610  lgseisen  27611  lgsquadlem1  27612  lgsquadlem2  27613  2lgslem1a1  27621  2sqmod  27668  chebbnd1lem1  27701  chebbnd1lem3  27703  chtppilimlem1  27705  chpchtlim  27711  vmadivsum  27714  rplogsumlem1  27716  rpvmasumlem  27719  dchrisumlem2  27722  dchrisumlem3  27723  dchrmusum2  27726  dchrvmasumlem2  27730  dchrvmasumiflem1  27733  dchrisum0re  27745  dchrisum0lem1  27748  dirith2  27760  mulogsumlem  27763  mulogsum  27764  mulog2sumlem2  27767  vmalogdivsum2  27770  vmalogdivsum  27771  2vmadivsumlem  27772  logsqvma  27774  logsqvma2  27775  log2sumbnd  27776  selberglem2  27778  selberg  27780  selbergb  27781  selberg2lem  27782  selberg2b  27784  chpdifbndlem1  27785  chpdifbndlem2  27786  selberg3lem1  27789  selberg3lem2  27790  selberg3  27791  selberg4lem1  27792  selberg4  27793  pntrsumbnd2  27799  selberg3r  27801  selberg4r  27802  selberg34r  27803  pntsf  27805  pntsval2  27808  pntrlog2bndlem1  27809  pntrlog2bndlem2  27810  pntrlog2bndlem3  27811  pntrlog2bndlem4  27812  pntrlog2bndlem5  27813  pntrlog2bndlem6  27815  pntrlog2bnd  27816  pntpbnd1a  27817  pntpbnd1  27818  pntpbnd2  27819  pntibndlem2a  27822  pntibndlem2  27823  pntlemb  27829  pntlemr  27834  pntlemj  27835  pntlemf  27837  pntlemk  27838  pntlemo  27839  pntlem3  27841  ostth2lem1  27850  ostth2lem2  27866  ostth2lem3  27867  ostth2lem4  27868  ostth3  27870  ttgcontlem1  29325  brbtwn2  29346  colinearalglem4  29350  axsegconlem8  29365  axsegconlem9  29366  axsegconlem10  29367  ax5seglem3  29372  axpaschlem  29381  axpasch  29382  axeuclidlem  29403  numclwwlk5  30852  numclwwlk7  30855  smcnlem  31162  ubthlem2  31336  htthlem  31382  pjhthlem1  31856  cnlnadjlem7  32538  nmopcoadji  32566  branmfn  32570  leopnmid  32603  nexple  33288  constrremulcl  34262  constrmulcl  34266  cos9thpiminplylem1  34277  cos9thpinconstrlem1  34284  rmulccn  34423  xrge0iifhom  34432  dya2icoseg  34773  eulerpartlems  34856  eulerpartlemgc  34858  eulerpartlemb  34864  signsvtp  35076  reprgt  35114  breprexplemc  35125  circlemethhgt  35136  hgt750lemd  35141  logdivsqrle  35143  hgt750lem  35144  hgt750lemf  35146  hgt750lemb  35149  hgt750lema  35150  hgt750leme  35151  tgoldbachgtde  35153  resconn  35810  knoppcnlem2  37176  knoppcnlem4  37178  knoppcnlem10  37184  unbdqndv2lem1  37191  unbdqndv2lem2  37192  knoppndvlem1  37194  knoppndvlem11  37204  knoppndvlem12  37205  knoppndvlem14  37207  knoppndvlem15  37208  knoppndvlem17  37210  knoppndvlem18  37211  knoppndvlem19  37212  knoppndvlem20  37213  knoppndvlem21  37214  opnmbllem0  38390  itg2addnclem2  38406  itg2addnclem3  38407  iblmulc2nc  38419  itgmulc2nclem1  38420  ftc1cnnclem  38425  ftc1anclem3  38429  areacirclem4  38445  geomcau  38494  equivbnd  38525  bfplem1  38557  bfplem2  38558  bfp  38559  rrnequiv  38570  rrntotbnd  38571  lcmineqlem19  42898  lcmineqlem20  42899  lcmineqlem21  42900  lcmineqlem22  42901  3lexlogpow2ineq2  42910  dvrelogpow2b  42919  aks4d1p1p2  42921  aks4d1p1p4  42922  aks4d1p1p6  42924  aks4d1p1p7  42925  aks4d1p1p5  42926  aks4d1p1  42927  aks4d1p8d2  42936  aks4d1p8  42938  posbezout  42951  aks6d1c2lem4  42978  2np3bcnp1  42995  2ap1caineq  42996  aks6d1c6lem4  43024  aks6d1c7lem1  43031  aks6d1c7lem2  43032  resubdi  43256  remul02  43265  remul01  43267  remulinvcom  43293  rediveud  43303  redivcan3d  43308  redivrec2d  43320  rediv23d  43321  sn-0tie0  43324  renegmulnnass  43338  mulgt0con1d  43343  mulgt0con2d  43344  mulgt0b1d  43345  sn-ltmul2d  43346  mulgt0b2d  43351  sn-mulgt1d  43352  mulltgt0d  43355  mullt0b1d  43356  mullt0b2d  43357  sn-mullt0d  43358  sn-itrere  43361  sn-retire  43362  fltnltalem  43493  fltnlta  43494  3cubeslem2  43515  3cubeslem3r  43517  3cubeslem4  43519  irrapxlem1  43648  irrapxlem2  43649  irrapxlem3  43650  irrapxlem4  43651  irrapxlem5  43652  pellexlem2  43656  pellexlem6  43660  pell14qrgt0  43685  pell1qrge1  43696  pell1qrgaplem  43699  pellqrexplicit  43703  pellqrex  43705  rmspecsqrtnq  43732  rmxycomplete  43743  rmxypos  43773  ltrmynn0  43774  ltrmxnn0  43775  jm2.24nn  43785  jm2.17a  43786  jm2.17b  43787  jm2.17c  43788  jm2.27c  43833  jm3.1lem2  43844  areaquad  44042  sqrtcval  44466  resqrtval  44468  imsqrtval  44469  imo72b2lem0  44990  cvgdvgrat  45122  nzprmdif  45128  lt3addmuld  46119  fperiodmullem  46121  fperiodmul  46122  lt4addmuld  46124  xralrple2  46169  xralrple3  46188  ltmulneg  46206  fmul01  46395  fmuldfeqlem1  46397  fmul01lt1lem1  46399  sumnnodd  46445  ltmod  46451  0ellimcdiv  46462  limclner  46464  dvdivbd  46736  dvbdfbdioolem2  46742  dvbdfbdioo  46743  ioodvbdlimc1lem1  46744  ioodvbdlimc1lem2  46745  ioodvbdlimc2lem  46747  stoweidlem1  46814  stoweidlem11  46824  stoweidlem13  46826  stoweidlem14  46827  stoweidlem16  46829  stoweidlem17  46830  stoweidlem22  46835  stoweidlem24  46837  stoweidlem25  46838  stoweidlem26  46839  stoweidlem30  46843  stoweidlem34  46847  stoweidlem36  46849  stoweidlem49  46862  stoweidlem59  46872  stoweidlem60  46873  wallispilem4  46881  wallispilem5  46882  wallispi  46883  wallispi2lem1  46884  wallispi2  46886  stirlinglem1  46887  stirlinglem3  46889  stirlinglem5  46891  stirlinglem6  46892  stirlinglem7  46893  stirlinglem10  46896  stirlinglem11  46897  stirlinglem12  46898  stirlinglem15  46901  stirlingr  46903  dirker2re  46905  dirkerval2  46907  dirkerre  46908  dirkertrigeqlem1  46911  dirkertrigeqlem2  46912  dirkeritg  46915  dirkercncflem2  46917  dirkercncflem4  46919  fourierdlem4  46924  fourierdlem5  46925  fourierdlem6  46926  fourierdlem7  46927  fourierdlem16  46936  fourierdlem18  46938  fourierdlem19  46939  fourierdlem21  46941  fourierdlem22  46942  fourierdlem26  46946  fourierdlem35  46955  fourierdlem39  46959  fourierdlem41  46961  fourierdlem42  46962  fourierdlem43  46963  fourierdlem48  46967  fourierdlem49  46968  fourierdlem51  46970  fourierdlem55  46974  fourierdlem56  46975  fourierdlem57  46976  fourierdlem58  46977  fourierdlem62  46981  fourierdlem63  46982  fourierdlem64  46983  fourierdlem65  46984  fourierdlem66  46985  fourierdlem67  46986  fourierdlem68  46987  fourierdlem71  46990  fourierdlem72  46991  fourierdlem73  46992  fourierdlem76  46995  fourierdlem77  46996  fourierdlem78  46997  fourierdlem83  47002  fourierdlem84  47003  fourierdlem87  47006  fourierdlem88  47007  fourierdlem89  47008  fourierdlem90  47009  fourierdlem91  47010  fourierdlem94  47013  fourierdlem95  47014  fourierdlem97  47016  fourierdlem103  47022  fourierdlem104  47023  fourierdlem112  47031  fourierdlem113  47032  sqwvfoura  47041  sqwvfourb  47042  fouriersw  47044  etransclem23  47070  etransclem48  47095  rrndistlt  47103  hoidmvlelem1  47408  hoidmvlelem2  47409  hoidmvlelem4  47411  smfmullem1  47604  smfmullem2  47605  smfmullem3  47606  smfmul  47608  2timesltsqm1  48252  fmtno4prmfac  48460  lighneallem4a  48496  requad01  48522  requad1  48523  requad2  48524  perfectALTVlem2  48623  gpg3kgrtriexlem1  48984  gpg3kgrtriexlem4  48987  gpg3kgrtriexlem6  48989  ply1mulgsumlem2  49302  digvalnn0  49514  dignn0fr  49516  dig2nn0  49526  affinecomb1  49617  rrx2linest2  49659  line2  49667  itsclc0lem1  49671  itsclc0lem2  49672  itsclc0lem3  49673  itscnhlc0yqe  49674  itsclc0yqsollem2  49678  itsclc0yqsol  49679  itscnhlc0xyqsol  49680  itsclc0xyqsolr  49684  itsclinecirc0  49688  itsclinecirc0b  49689  itsclinecirc0in  49690  itsclquadb  49691  itsclquadeu  49692  2itscp  49696  itscnhlinecirc02plem1  49697  itscnhlinecirc02p  49700  inlinecirc02plem  49701  crosspcle1d  50770  crosspcle2d  50771  crosspcle3d  50772  crosspdotsumlem  50779  crosspdotd  50780  crosspaltd  50781  crossp3d  50782  veronesefvcl  50787  veronesev4lem  50791  veronesev5lem  50792  veronesev6lem  50793  veroquadgsumlem  50798  veroquadmodzerod  50799  amgmwlem  50802