Theorem remulcld 11211

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7390  ℝcr 11074   · cmul 11080

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

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

This theorem is referenced by:  mulge0  11703  msqge0  11706  redivcl  11908  prodgt0  12036  ltmul1a  12038  ltmul1  12039  ltmuldiv  12063  lt2msq1  12074  lt2msq  12075  le2msq  12090  msq11  12091  supmul1  12159  supmullem2  12161  supmul  12162  div4p1lem1div2  12444  mul2lt0rlt0  13062  mul2lt0bi  13066  prodge0rd  13067  ge2halflem1  13075  qbtwnre  13166  xmulneg1  13236  xmulf  13239  lincmb01cmp  13463  iccf1o  13464  flmulnn0  13796  flhalf  13799  modcl  13842  mod0  13845  modge0  13848  modmulnn  13858  mulp1mod1  13883  muladdmod  13884  2txmodxeq0  13903  modaddmulmod  13910  moddi  13911  modsubdir  13912  modirr  13914  addmodlteq  13918  bernneq  14201  bernneq3  14203  expnbnd  14204  expmulnbnd  14207  discr1  14211  discr  14212  faclbnd  14262  faclbnd6  14271  remullem  15101  01sqrexlem7  15221  sqrtmul  15232  abstri  15304  sqreulem  15333  bhmafibid1  15441  mulcn2  15569  reccn2  15570  o1rlimmul  15592  lo1mul  15601  iseraltlem2  15656  iseraltlem3  15657  iseralt  15658  o1fsum  15786  cvgcmpce  15791  climcndslem1  15822  climcndslem2  15823  climcnds  15824  geomulcvg  15849  cvgrat  15856  mertenslem1  15857  fprodge1  15968  eftlub  16084  sin02gt0  16167  eirrlem  16179  bitsp1o  16410  2mulprm  16670  isprm5  16684  modprm0  16783  prmreclem3  16896  prmreclem4  16897  prmreclem5  16898  2expltfac  17070  metss2lem  24406  nlmvscnlem2  24580  nrginvrcnlem  24586  nmoco  24632  nmotri  24634  nghmcn  24640  icopnfhmeo  24848  nmoleub2lem3  25022  ipcau2  25141  tcphcphlem1  25142  ipcnlem2  25151  rrxcph  25299  csbren  25306  trirn  25307  pjthlem1  25344  opnmbllem  25509  vitalilem4  25519  itg1val2  25592  itg1cl  25593  itg1ge0  25594  itg1addlem4  25607  itg1mulc  25612  itg1ge0a  25619  itg1climres  25622  mbfi1fseqlem1  25623  mbfi1fseqlem3  25625  mbfi1fseqlem4  25626  mbfi1fseqlem5  25627  mbfi1fseqlem6  25628  itg2const2  25649  itg2mulclem  25654  itg2mulc  25655  itg2monolem1  25658  itg2monolem3  25660  itg2cnlem2  25670  iblconst  25726  iblmulc2  25739  itgmulc2lem1  25740  itgmulc2lem2  25741  bddmulibl  25747  bddiblnc  25750  dveflem  25890  cmvth  25902  cmvthOLD  25903  dvlip  25905  dvlipcn  25906  dvivthlem1  25920  lhop1lem  25925  dvcvx  25932  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsumlem3  25942  dvfsumlem4  25943  dvfsum2  25948  ftc1lem4  25953  plyeq0lem  26122  aalioulem3  26249  aalioulem4  26250  aaliou3lem9  26265  ulmdvlem1  26316  itgulm  26324  radcnvlem1  26329  radcnvlem2  26330  dvradcnv  26337  abelthlem2  26349  abelthlem7  26355  tangtx  26421  tanregt0  26455  logdivlti  26536  logcnlem3  26560  logcnlem4  26561  logccv  26579  recxpcl  26591  cxpmul  26604  cxplt  26610  cxple2  26613  abscxpbnd  26670  lawcoslem1  26732  heron  26755  atans2  26848  efrlim  26886  efrlimOLD  26887  o1cxp  26892  scvxcvx  26903  jensenlem2  26905  amgmlem  26907  fsumharmonic  26929  lgamgulmlem2  26947  lgamgulmlem3  26948  lgamgulmlem4  26949  lgamgulmlem5  26950  lgamgulmlem6  26951  relgamcl  26979  ftalem1  26990  ftalem2  26991  ftalem5  26994  basellem3  27000  basellem8  27005  chpub  27138  logfacubnd  27139  logfaclbnd  27140  logfacbnd3  27141  logexprlim  27143  perfectlem2  27148  bclbnd  27198  efexple  27199  bposlem1  27202  bposlem2  27203  bposlem6  27207  bposlem9  27210  lgsdilem  27242  gausslemma2dlem0c  27276  gausslemma2dlem2  27285  gausslemma2dlem3  27286  gausslemma2dlem6  27290  lgseisenlem4  27296  lgseisen  27297  lgsquadlem1  27298  lgsquadlem2  27299  2lgslem1a1  27307  2sqmod  27354  chebbnd1lem1  27387  chebbnd1lem3  27389  chtppilimlem1  27391  chpchtlim  27397  vmadivsum  27400  rplogsumlem1  27402  rpvmasumlem  27405  dchrisumlem2  27408  dchrisumlem3  27409  dchrmusum2  27412  dchrvmasumlem2  27416  dchrvmasumiflem1  27419  dchrisum0re  27431  dchrisum0lem1  27434  dirith2  27446  mulogsumlem  27449  mulogsum  27450  mulog2sumlem2  27453  vmalogdivsum2  27456  vmalogdivsum  27457  2vmadivsumlem  27458  logsqvma  27460  logsqvma2  27461  log2sumbnd  27462  selberglem2  27464  selberg  27466  selbergb  27467  selberg2lem  27468  selberg2b  27470  chpdifbndlem1  27471  chpdifbndlem2  27472  selberg3lem1  27475  selberg3lem2  27476  selberg3  27477  selberg4lem1  27478  selberg4  27479  pntrsumbnd2  27485  selberg3r  27487  selberg4r  27488  selberg34r  27489  pntsf  27491  pntsval2  27494  pntrlog2bndlem1  27495  pntrlog2bndlem2  27496  pntrlog2bndlem3  27497  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  pntrlog2bndlem6  27501  pntrlog2bnd  27502  pntpbnd1a  27503  pntpbnd1  27504  pntpbnd2  27505  pntibndlem2a  27508  pntibndlem2  27509  pntlemb  27515  pntlemr  27520  pntlemj  27521  pntlemf  27523  pntlemk  27524  pntlemo  27525  pntlem3  27527  ostth2lem1  27536  ostth2lem2  27552  ostth2lem3  27553  ostth2lem4  27554  ostth3  27556  ttgcontlem1  28819  brbtwn2  28839  colinearalglem4  28843  axsegconlem8  28858  axsegconlem9  28859  axsegconlem10  28860  ax5seglem3  28865  axpaschlem  28874  axpasch  28875  axeuclidlem  28896  numclwwlk5  30324  numclwwlk7  30327  smcnlem  30633  ubthlem2  30807  htthlem  30853  pjhthlem1  31327  cnlnadjlem7  32009  nmopcoadji  32037  branmfn  32041  leopnmid  32074  nexple  32776  constrremulcl  33764  constrmulcl  33768  cos9thpiminplylem1  33779  cos9thpinconstrlem1  33786  rmulccn  33925  xrge0iifhom  33934  dya2icoseg  34275  eulerpartlems  34358  eulerpartlemgc  34360  eulerpartlemb  34366  plymulx0  34545  signsvtp  34581  reprgt  34619  breprexplemc  34630  circlemethhgt  34641  hgt750lemd  34646  logdivsqrle  34648  hgt750lem  34649  hgt750lemf  34651  hgt750lemb  34654  hgt750lema  34655  hgt750leme  34656  tgoldbachgtde  34658  resconn  35240  knoppcnlem2  36489  knoppcnlem4  36491  knoppcnlem10  36497  unbdqndv2lem1  36504  unbdqndv2lem2  36505  knoppndvlem1  36507  knoppndvlem11  36517  knoppndvlem12  36518  knoppndvlem14  36520  knoppndvlem15  36521  knoppndvlem17  36523  knoppndvlem18  36524  knoppndvlem19  36525  knoppndvlem20  36526  knoppndvlem21  36527  opnmbllem0  37657  itg2addnclem2  37673  itg2addnclem3  37674  iblmulc2nc  37686  itgmulc2nclem1  37687  ftc1cnnclem  37692  ftc1anclem3  37696  areacirclem4  37712  geomcau  37760  equivbnd  37791  bfplem1  37823  bfplem2  37824  bfp  37825  rrnequiv  37836  rrntotbnd  37837  lcmineqlem19  42042  lcmineqlem20  42043  lcmineqlem21  42044  lcmineqlem22  42045  3lexlogpow2ineq2  42054  dvrelogpow2b  42063  aks4d1p1p2  42065  aks4d1p1p4  42066  aks4d1p1p6  42068  aks4d1p1p7  42069  aks4d1p1p5  42070  aks4d1p1  42071  aks4d1p8d2  42080  aks4d1p8  42082  posbezout  42095  aks6d1c2lem4  42122  2np3bcnp1  42139  2ap1caineq  42140  aks6d1c6lem4  42168  aks6d1c7lem1  42175  aks6d1c7lem2  42176  resubdi  42391  remul02  42400  remul01  42402  remulinvcom  42428  rediveud  42438  redivcan3d  42442  sn-0tie0  42446  renegmulnnass  42460  mulgt0con1d  42465  mulgt0con2d  42466  mulgt0b1d  42467  sn-ltmul2d  42468  mulgt0b2d  42473  sn-mulgt1d  42474  mulltgt0d  42477  mullt0b1d  42478  mullt0b2d  42479  sn-mullt0d  42480  sn-itrere  42483  sn-retire  42484  fltnltalem  42657  fltnlta  42658  3cubeslem2  42680  3cubeslem3r  42682  3cubeslem4  42684  irrapxlem1  42817  irrapxlem2  42818  irrapxlem3  42819  irrapxlem4  42820  irrapxlem5  42821  pellexlem2  42825  pellexlem6  42829  pell14qrgt0  42854  pell1qrge1  42865  pell1qrgaplem  42868  pellqrexplicit  42872  pellqrex  42874  rmspecsqrtnq  42901  rmxycomplete  42913  rmxypos  42943  ltrmynn0  42944  ltrmxnn0  42945  jm2.24nn  42955  jm2.17a  42956  jm2.17b  42957  jm2.17c  42958  jm2.27c  43003  jm3.1lem2  43014  areaquad  43212  sqrtcval  43637  resqrtval  43639  imsqrtval  43640  imo72b2lem0  44161  cvgdvgrat  44309  nzprmdif  44315  lt3addmuld  45306  fperiodmullem  45308  fperiodmul  45309  lt4addmuld  45311  xralrple2  45357  xralrple3  45377  ltmulneg  45395  fmul01  45585  fmuldfeqlem1  45587  fmul01lt1lem1  45589  sumnnodd  45635  ltmod  45643  0ellimcdiv  45654  limclner  45656  dvdivbd  45928  dvbdfbdioolem2  45934  dvbdfbdioo  45935  ioodvbdlimc1lem1  45936  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  stoweidlem1  46006  stoweidlem11  46016  stoweidlem13  46018  stoweidlem14  46019  stoweidlem16  46021  stoweidlem17  46022  stoweidlem22  46027  stoweidlem24  46029  stoweidlem25  46030  stoweidlem26  46031  stoweidlem30  46035  stoweidlem34  46039  stoweidlem36  46041  stoweidlem49  46054  stoweidlem59  46064  stoweidlem60  46065  wallispilem4  46073  wallispilem5  46074  wallispi  46075  wallispi2lem1  46076  wallispi2  46078  stirlinglem1  46079  stirlinglem3  46081  stirlinglem5  46083  stirlinglem6  46084  stirlinglem7  46085  stirlinglem10  46088  stirlinglem11  46089  stirlinglem12  46090  stirlinglem15  46093  stirlingr  46095  dirker2re  46097  dirkerval2  46099  dirkerre  46100  dirkertrigeqlem1  46103  dirkertrigeqlem2  46104  dirkeritg  46107  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem4  46116  fourierdlem5  46117  fourierdlem6  46118  fourierdlem7  46119  fourierdlem16  46128  fourierdlem18  46130  fourierdlem19  46131  fourierdlem21  46133  fourierdlem22  46134  fourierdlem26  46138  fourierdlem35  46147  fourierdlem39  46151  fourierdlem41  46153  fourierdlem42  46154  fourierdlem43  46155  fourierdlem48  46159  fourierdlem49  46160  fourierdlem51  46162  fourierdlem55  46166  fourierdlem56  46167  fourierdlem57  46168  fourierdlem58  46169  fourierdlem62  46173  fourierdlem63  46174  fourierdlem64  46175  fourierdlem65  46176  fourierdlem66  46177  fourierdlem67  46178  fourierdlem68  46179  fourierdlem71  46182  fourierdlem72  46183  fourierdlem73  46184  fourierdlem76  46187  fourierdlem77  46188  fourierdlem78  46189  fourierdlem83  46194  fourierdlem84  46195  fourierdlem87  46198  fourierdlem88  46199  fourierdlem89  46200  fourierdlem90  46201  fourierdlem91  46202  fourierdlem94  46205  fourierdlem95  46206  fourierdlem97  46208  fourierdlem103  46214  fourierdlem104  46215  fourierdlem112  46223  fourierdlem113  46224  sqwvfoura  46233  sqwvfourb  46234  fouriersw  46236  etransclem23  46262  etransclem48  46287  rrndistlt  46295  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem4  46603  smfmullem1  46796  smfmullem2  46797  smfmullem3  46798  smfmul  46800  fmtno4prmfac  47577  lighneallem4a  47613  requad01  47626  requad1  47627  requad2  47628  perfectALTVlem2  47727  gpg3kgrtriexlem1  48078  gpg3kgrtriexlem4  48081  gpg3kgrtriexlem6  48083  ply1mulgsumlem2  48380  digvalnn0  48592  dignn0fr  48594  dig2nn0  48604  affinecomb1  48695  rrx2linest2  48737  line2  48745  itsclc0lem1  48749  itsclc0lem2  48750  itsclc0lem3  48751  itscnhlc0yqe  48752  itsclc0yqsollem2  48756  itsclc0yqsol  48757  itscnhlc0xyqsol  48758  itsclc0xyqsolr  48762  itsclinecirc0  48766  itsclinecirc0b  48767  itsclinecirc0in  48768  itsclquadb  48769  itsclquadeu  48770  2itscp  48774  itscnhlinecirc02plem1  48775  itscnhlinecirc02p  48778  inlinecirc02plem  48779  amgmwlem  49795