Theorem remulcld 11204

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7387  ℝcr 11067   · cmul 11073

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

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

This theorem is referenced by:  mulge0  11696  msqge0  11699  redivcl  11901  prodgt0  12029  ltmul1a  12031  ltmul1  12032  ltmuldiv  12056  lt2msq1  12067  lt2msq  12068  le2msq  12083  msq11  12084  supmul1  12152  supmullem2  12154  supmul  12155  div4p1lem1div2  12437  mul2lt0rlt0  13055  mul2lt0bi  13059  prodge0rd  13060  ge2halflem1  13068  qbtwnre  13159  xmulneg1  13229  xmulf  13232  lincmb01cmp  13456  iccf1o  13457  flmulnn0  13789  flhalf  13792  modcl  13835  mod0  13838  modge0  13841  modmulnn  13851  mulp1mod1  13876  muladdmod  13877  2txmodxeq0  13896  modaddmulmod  13903  moddi  13904  modsubdir  13905  modirr  13907  addmodlteq  13911  bernneq  14194  bernneq3  14196  expnbnd  14197  expmulnbnd  14200  discr1  14204  discr  14205  faclbnd  14255  faclbnd6  14264  remullem  15094  01sqrexlem7  15214  sqrtmul  15225  abstri  15297  sqreulem  15326  bhmafibid1  15434  mulcn2  15562  reccn2  15563  o1rlimmul  15585  lo1mul  15594  iseraltlem2  15649  iseraltlem3  15650  iseralt  15651  o1fsum  15779  cvgcmpce  15784  climcndslem1  15815  climcndslem2  15816  climcnds  15817  geomulcvg  15842  cvgrat  15849  mertenslem1  15850  fprodge1  15961  eftlub  16077  sin02gt0  16160  eirrlem  16172  bitsp1o  16403  2mulprm  16663  isprm5  16677  modprm0  16776  prmreclem3  16889  prmreclem4  16890  prmreclem5  16891  2expltfac  17063  metss2lem  24399  nlmvscnlem2  24573  nrginvrcnlem  24579  nmoco  24625  nmotri  24627  nghmcn  24633  icopnfhmeo  24841  nmoleub2lem3  25015  ipcau2  25134  tcphcphlem1  25135  ipcnlem2  25144  rrxcph  25292  csbren  25299  trirn  25300  pjthlem1  25337  opnmbllem  25502  vitalilem4  25512  itg1val2  25585  itg1cl  25586  itg1ge0  25587  itg1addlem4  25600  itg1mulc  25605  itg1ge0a  25612  itg1climres  25615  mbfi1fseqlem1  25616  mbfi1fseqlem3  25618  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  mbfi1fseqlem6  25621  itg2const2  25642  itg2mulclem  25647  itg2mulc  25648  itg2monolem1  25651  itg2monolem3  25653  itg2cnlem2  25663  iblconst  25719  iblmulc2  25732  itgmulc2lem1  25733  itgmulc2lem2  25734  bddmulibl  25740  bddiblnc  25743  dveflem  25883  cmvth  25895  cmvthOLD  25896  dvlip  25898  dvlipcn  25899  dvivthlem1  25913  lhop1lem  25918  dvcvx  25925  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumlem3  25935  dvfsumlem4  25936  dvfsum2  25941  ftc1lem4  25946  plyeq0lem  26115  aalioulem3  26242  aalioulem4  26243  aaliou3lem9  26258  ulmdvlem1  26309  itgulm  26317  radcnvlem1  26322  radcnvlem2  26323  dvradcnv  26330  abelthlem2  26342  abelthlem7  26348  tangtx  26414  tanregt0  26448  logdivlti  26529  logcnlem3  26553  logcnlem4  26554  logccv  26572  recxpcl  26584  cxpmul  26597  cxplt  26603  cxple2  26606  abscxpbnd  26663  lawcoslem1  26725  heron  26748  atans2  26841  efrlim  26879  efrlimOLD  26880  o1cxp  26885  scvxcvx  26896  jensenlem2  26898  amgmlem  26900  fsumharmonic  26922  lgamgulmlem2  26940  lgamgulmlem3  26941  lgamgulmlem4  26942  lgamgulmlem5  26943  lgamgulmlem6  26944  relgamcl  26972  ftalem1  26983  ftalem2  26984  ftalem5  26987  basellem3  26993  basellem8  26998  chpub  27131  logfacubnd  27132  logfaclbnd  27133  logfacbnd3  27134  logexprlim  27136  perfectlem2  27141  bclbnd  27191  efexple  27192  bposlem1  27195  bposlem2  27196  bposlem6  27200  bposlem9  27203  lgsdilem  27235  gausslemma2dlem0c  27269  gausslemma2dlem2  27278  gausslemma2dlem3  27279  gausslemma2dlem6  27283  lgseisenlem4  27289  lgseisen  27290  lgsquadlem1  27291  lgsquadlem2  27292  2lgslem1a1  27300  2sqmod  27347  chebbnd1lem1  27380  chebbnd1lem3  27382  chtppilimlem1  27384  chpchtlim  27390  vmadivsum  27393  rplogsumlem1  27395  rpvmasumlem  27398  dchrisumlem2  27401  dchrisumlem3  27402  dchrmusum2  27405  dchrvmasumlem2  27409  dchrvmasumiflem1  27412  dchrisum0re  27424  dchrisum0lem1  27427  dirith2  27439  mulogsumlem  27442  mulogsum  27443  mulog2sumlem2  27446  vmalogdivsum2  27449  vmalogdivsum  27450  2vmadivsumlem  27451  logsqvma  27453  logsqvma2  27454  log2sumbnd  27455  selberglem2  27457  selberg  27459  selbergb  27460  selberg2lem  27461  selberg2b  27463  chpdifbndlem1  27464  chpdifbndlem2  27465  selberg3lem1  27468  selberg3lem2  27469  selberg3  27470  selberg4lem1  27471  selberg4  27472  pntrsumbnd2  27478  selberg3r  27480  selberg4r  27481  selberg34r  27482  pntsf  27484  pntsval2  27487  pntrlog2bndlem1  27488  pntrlog2bndlem2  27489  pntrlog2bndlem3  27490  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntrlog2bndlem6  27494  pntrlog2bnd  27495  pntpbnd1a  27496  pntpbnd1  27497  pntpbnd2  27498  pntibndlem2a  27501  pntibndlem2  27502  pntlemb  27508  pntlemr  27513  pntlemj  27514  pntlemf  27516  pntlemk  27517  pntlemo  27518  pntlem3  27520  ostth2lem1  27529  ostth2lem2  27545  ostth2lem3  27546  ostth2lem4  27547  ostth3  27549  ttgcontlem1  28812  brbtwn2  28832  colinearalglem4  28836  axsegconlem8  28851  axsegconlem9  28852  axsegconlem10  28853  ax5seglem3  28858  axpaschlem  28867  axpasch  28868  axeuclidlem  28889  numclwwlk5  30317  numclwwlk7  30320  smcnlem  30626  ubthlem2  30800  htthlem  30846  pjhthlem1  31320  cnlnadjlem7  32002  nmopcoadji  32030  branmfn  32034  leopnmid  32067  nexple  32769  constrremulcl  33757  constrmulcl  33761  cos9thpiminplylem1  33772  cos9thpinconstrlem1  33779  rmulccn  33918  xrge0iifhom  33927  dya2icoseg  34268  eulerpartlems  34351  eulerpartlemgc  34353  eulerpartlemb  34359  plymulx0  34538  signsvtp  34574  reprgt  34612  breprexplemc  34623  circlemethhgt  34634  hgt750lemd  34639  logdivsqrle  34641  hgt750lem  34642  hgt750lemf  34644  hgt750lemb  34647  hgt750lema  34648  hgt750leme  34649  tgoldbachgtde  34651  resconn  35233  knoppcnlem2  36482  knoppcnlem4  36484  knoppcnlem10  36490  unbdqndv2lem1  36497  unbdqndv2lem2  36498  knoppndvlem1  36500  knoppndvlem11  36510  knoppndvlem12  36511  knoppndvlem14  36513  knoppndvlem15  36514  knoppndvlem17  36516  knoppndvlem18  36517  knoppndvlem19  36518  knoppndvlem20  36519  knoppndvlem21  36520  opnmbllem0  37650  itg2addnclem2  37666  itg2addnclem3  37667  iblmulc2nc  37679  itgmulc2nclem1  37680  ftc1cnnclem  37685  ftc1anclem3  37689  areacirclem4  37705  geomcau  37753  equivbnd  37784  bfplem1  37816  bfplem2  37817  bfp  37818  rrnequiv  37829  rrntotbnd  37830  lcmineqlem19  42035  lcmineqlem20  42036  lcmineqlem21  42037  lcmineqlem22  42038  3lexlogpow2ineq2  42047  dvrelogpow2b  42056  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1p6  42061  aks4d1p1p7  42062  aks4d1p1p5  42063  aks4d1p1  42064  aks4d1p8d2  42073  aks4d1p8  42075  posbezout  42088  aks6d1c2lem4  42115  2np3bcnp1  42132  2ap1caineq  42133  aks6d1c6lem4  42161  aks6d1c7lem1  42168  aks6d1c7lem2  42169  resubdi  42384  remul02  42393  remul01  42395  remulinvcom  42421  rediveud  42431  redivcan3d  42435  sn-0tie0  42439  renegmulnnass  42453  mulgt0con1d  42458  mulgt0con2d  42459  mulgt0b1d  42460  sn-ltmul2d  42461  mulgt0b2d  42466  sn-mulgt1d  42467  mulltgt0d  42470  mullt0b1d  42471  mullt0b2d  42472  sn-mullt0d  42473  sn-itrere  42476  sn-retire  42477  fltnltalem  42650  fltnlta  42651  3cubeslem2  42673  3cubeslem3r  42675  3cubeslem4  42677  irrapxlem1  42810  irrapxlem2  42811  irrapxlem3  42812  irrapxlem4  42813  irrapxlem5  42814  pellexlem2  42818  pellexlem6  42822  pell14qrgt0  42847  pell1qrge1  42858  pell1qrgaplem  42861  pellqrexplicit  42865  pellqrex  42867  rmspecsqrtnq  42894  rmxycomplete  42906  rmxypos  42936  ltrmynn0  42937  ltrmxnn0  42938  jm2.24nn  42948  jm2.17a  42949  jm2.17b  42950  jm2.17c  42951  jm2.27c  42996  jm3.1lem2  43007  areaquad  43205  sqrtcval  43630  resqrtval  43632  imsqrtval  43633  imo72b2lem0  44154  cvgdvgrat  44302  nzprmdif  44308  lt3addmuld  45299  fperiodmullem  45301  fperiodmul  45302  lt4addmuld  45304  xralrple2  45350  xralrple3  45370  ltmulneg  45388  fmul01  45578  fmuldfeqlem1  45580  fmul01lt1lem1  45582  sumnnodd  45628  ltmod  45636  0ellimcdiv  45647  limclner  45649  dvdivbd  45921  dvbdfbdioolem2  45927  dvbdfbdioo  45928  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  stoweidlem1  45999  stoweidlem11  46009  stoweidlem13  46011  stoweidlem14  46012  stoweidlem16  46014  stoweidlem17  46015  stoweidlem22  46020  stoweidlem24  46022  stoweidlem25  46023  stoweidlem26  46024  stoweidlem30  46028  stoweidlem34  46032  stoweidlem36  46034  stoweidlem49  46047  stoweidlem59  46057  stoweidlem60  46058  wallispilem4  46066  wallispilem5  46067  wallispi  46068  wallispi2lem1  46069  wallispi2  46071  stirlinglem1  46072  stirlinglem3  46074  stirlinglem5  46076  stirlinglem6  46077  stirlinglem7  46078  stirlinglem10  46081  stirlinglem11  46082  stirlinglem12  46083  stirlinglem15  46086  stirlingr  46088  dirker2re  46090  dirkerval2  46092  dirkerre  46093  dirkertrigeqlem1  46096  dirkertrigeqlem2  46097  dirkeritg  46100  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem4  46109  fourierdlem5  46110  fourierdlem6  46111  fourierdlem7  46112  fourierdlem16  46121  fourierdlem18  46123  fourierdlem19  46124  fourierdlem21  46126  fourierdlem22  46127  fourierdlem26  46131  fourierdlem35  46140  fourierdlem39  46144  fourierdlem41  46146  fourierdlem42  46147  fourierdlem43  46148  fourierdlem48  46152  fourierdlem49  46153  fourierdlem51  46155  fourierdlem55  46159  fourierdlem56  46160  fourierdlem57  46161  fourierdlem58  46162  fourierdlem62  46166  fourierdlem63  46167  fourierdlem64  46168  fourierdlem65  46169  fourierdlem66  46170  fourierdlem67  46171  fourierdlem68  46172  fourierdlem71  46175  fourierdlem72  46176  fourierdlem73  46177  fourierdlem76  46180  fourierdlem77  46181  fourierdlem78  46182  fourierdlem83  46187  fourierdlem84  46188  fourierdlem87  46191  fourierdlem88  46192  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem94  46198  fourierdlem95  46199  fourierdlem97  46201  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  fourierdlem113  46217  sqwvfoura  46226  sqwvfourb  46227  fouriersw  46229  etransclem23  46255  etransclem48  46280  rrndistlt  46288  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem4  46596  smfmullem1  46789  smfmullem2  46790  smfmullem3  46791  smfmul  46793  fmtno4prmfac  47573  lighneallem4a  47609  requad01  47622  requad1  47623  requad2  47624  perfectALTVlem2  47723  gpg3kgrtriexlem1  48074  gpg3kgrtriexlem4  48077  gpg3kgrtriexlem6  48079  ply1mulgsumlem2  48376  digvalnn0  48588  dignn0fr  48590  dig2nn0  48600  affinecomb1  48691  rrx2linest2  48733  line2  48741  itsclc0lem1  48745  itsclc0lem2  48746  itsclc0lem3  48747  itscnhlc0yqe  48748  itsclc0yqsollem2  48752  itsclc0yqsol  48753  itscnhlc0xyqsol  48754  itsclc0xyqsolr  48758  itsclinecirc0  48762  itsclinecirc0b  48763  itsclinecirc0in  48764  itsclquadb  48765  itsclquadeu  48766  2itscp  48770  itscnhlinecirc02plem1  48771  itscnhlinecirc02p  48774  inlinecirc02plem  48775  amgmwlem  49791