Theorem remulcld 11296

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7409  ℝcr 11156   · cmul 11162

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

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

This theorem is used by:  mulge0  11789  msqge0  11792  redivcl  11991  prodgt0  12119  ltmul1a  12121  ltmul1  12122  ltmuldiv  12145  lt2msq1  12156  lt2msq  12157  le2msq  12172  msq11  12173  supmul1  12241  supmullem2  12243  supmul  12244  div4p1lem1div2  12556  mul2lt0rlt0  13179  mul2lt0bi  13183  prodge0rd  13184  ge2halflem1  13192  qbtwnre  13284  xmulneg1  13354  xmulf  13357  lincmb01cmp  13581  iccf1o  13582  flmulnn0  13921  flhalf  13924  modcl  13967  mod0  13970  modge0  13973  modmulnn  13983  mulp1mod1  14008  muladdmod  14009  2txmodxeq0  14028  modaddmulmod  14035  moddi  14036  modsubdir  14037  modirr  14039  addmodlteq  14043  bernneq  14326  bernneq3  14328  expnbnd  14329  expmulnbnd  14332  discr1  14336  discr  14337  faclbnd  14387  faclbnd6  14396  remullem  15248  01sqrexlem7  15368  sqrtmul  15379  abstri  15451  sqreulem  15480  bhmafibid1  15588  mulcn2  15716  reccn2  15717  o1rlimmul  15739  lo1mul  15748  iseraltlem2  15803  iseraltlem3  15804  iseralt  15805  o1fsum  15933  cvgcmpce  15938  climcndslem1  15971  climcndslem2  15972  climcnds  15973  geomulcvg  15998  cvgrat  16005  mertenslem1  16006  fprodge1  16115  eftlub  16230  sin02gt0  16313  eirrlem  16325  bitsp1o  16556  2mulprm  16816  isprm5  16831  modprm0  16930  prmreclem3  17043  prmreclem4  17044  prmreclem5  17045  2expltfac  17217  metss2lem  24777  nlmvscnlem2  24951  nrginvrcnlem  24957  nmoco  25003  nmotri  25005  nghmcn  25011  icopnfhmeo  25211  nmoleub2lem3  25383  ipcau2  25502  tcphcphlem1  25503  ipcnlem2  25512  rrxcph  25660  csbren  25667  trirn  25668  pjthlem1  25705  opnmbllem  25869  vitalilem4  25879  itg1val2  25952  itg1cl  25953  itg1ge0  25954  itg1addlem4  25967  itg1mulc  25972  itg1ge0a  25979  itg1climres  25982  mbfi1fseqlem1  25983  mbfi1fseqlem3  25985  mbfi1fseqlem4  25986  mbfi1fseqlem5  25987  mbfi1fseqlem6  25988  itg2const2  26009  itg2mulclem  26014  itg2mulc  26015  itg2monolem1  26018  itg2monolem3  26020  itg2cnlem2  26030  iblconst  26085  iblmulc2  26098  itgmulc2lem1  26099  itgmulc2lem2  26100  bddmulibl  26106  bddiblnc  26109  dveflem  26246  cmvth  26258  dvlip  26260  dvlipcn  26261  dvivthlem1  26275  lhop1lem  26280  dvcvx  26287  dvfsumlem2  26294  dvfsumlem3  26295  dvfsumlem4  26296  dvfsum2  26301  ftc1lem4  26306  plyeq0lem  26476  plyn0mulidp  26551  aalioulem3  26610  aalioulem4  26611  aaliou3lem9  26626  ulmdvlem1  26676  itgulm  26684  radcnvlem1  26689  radcnvlem2  26690  dvradcnv  26697  abelthlem2  26708  abelthlem7  26714  tangtx  26783  tanregt0  26816  logdivlti  26897  logcnlem3  26921  logcnlem4  26922  logccv  26940  recxpcl  26952  cxpmul  26965  cxplt  26971  cxple2  26974  abscxpbnd  27030  lawcoslem1  27092  heron  27115  atans2  27208  efrlim  27246  o1cxp  27251  scvxcvx  27262  jensenlem2  27264  amgmlem  27266  fsumharmonic  27288  lgamgulmlem2  27306  lgamgulmlem3  27307  lgamgulmlem4  27308  lgamgulmlem5  27309  lgamgulmlem6  27310  relgamcl  27338  ftalem1  27349  ftalem2  27350  ftalem5  27353  basellem3  27359  basellem8  27364  chpub  27496  logfacubnd  27497  logfaclbnd  27498  logfacbnd3  27499  logexprlim  27501  perfectlem2  27506  bclbnd  27556  efexple  27557  bposlem1  27560  bposlem2  27561  bposlem6  27565  bposlem9  27568  lgsdilem  27600  gausslemma2dlem0c  27634  gausslemma2dlem2  27643  gausslemma2dlem3  27644  gausslemma2dlem6  27648  lgseisenlem4  27654  lgseisen  27655  lgsquadlem1  27656  lgsquadlem2  27657  2lgslem1a1  27665  2sqmod  27712  chebbnd1lem1  27745  chebbnd1lem3  27747  chtppilimlem1  27749  chpchtlim  27755  vmadivsum  27758  rplogsumlem1  27760  rpvmasumlem  27763  dchrisumlem2  27766  dchrisumlem3  27767  dchrmusum2  27770  dchrvmasumlem2  27774  dchrvmasumiflem1  27777  dchrisum0re  27789  dchrisum0lem1  27792  dirith2  27804  mulogsumlem  27807  mulogsum  27808  mulog2sumlem2  27811  vmalogdivsum2  27814  vmalogdivsum  27815  2vmadivsumlem  27816  logsqvma  27818  logsqvma2  27819  log2sumbnd  27820  selberglem2  27822  selberg  27824  selbergb  27825  selberg2lem  27826  selberg2b  27828  chpdifbndlem1  27829  chpdifbndlem2  27830  selberg3lem1  27833  selberg3lem2  27834  selberg3  27835  selberg4lem1  27836  selberg4  27837  pntrsumbnd2  27843  selberg3r  27845  selberg4r  27846  selberg34r  27847  pntsf  27849  pntsval2  27852  pntrlog2bndlem1  27853  pntrlog2bndlem2  27854  pntrlog2bndlem3  27855  pntrlog2bndlem4  27856  pntrlog2bndlem5  27857  pntrlog2bndlem6  27859  pntrlog2bnd  27860  pntpbnd1a  27861  pntpbnd1  27862  pntpbnd2  27863  pntibndlem2a  27866  pntibndlem2  27867  pntlemb  27873  pntlemr  27878  pntlemj  27879  pntlemf  27881  pntlemk  27882  pntlemo  27883  pntlem3  27885  ostth2lem1  27894  ostth2lem2  27910  ostth2lem3  27911  ostth2lem4  27912  ostth3  27914  ttgcontlem1  29381  brbtwn2  29402  colinearalglem4  29406  axsegconlem8  29421  axsegconlem9  29422  axsegconlem10  29423  ax5seglem3  29428  axpaschlem  29437  axpasch  29438  axeuclidlem  29459  numclwwlk5  30908  numclwwlk7  30911  smcnlem  31218  ubthlem2  31392  htthlem  31438  pjhthlem1  31912  cnlnadjlem7  32594  nmopcoadji  32622  branmfn  32626  leopnmid  32659  nexple  33343  constrremulcl  34318  constrmulcl  34322  cos9thpiminplylem1  34333  cos9thpinconstrlem1  34340  rmulccn  34479  xrge0iifhom  34488  dya2icoseg  34829  eulerpartlems  34912  eulerpartlemgc  34914  eulerpartlemb  34920  signsvtp  35132  reprgt  35170  breprexplemc  35181  circlemethhgt  35192  hgt750lemd  35197  logdivsqrle  35199  hgt750lem  35200  hgt750lemf  35202  hgt750lemb  35205  hgt750lema  35206  hgt750leme  35207  tgoldbachgtde  35209  resconn  35926  knoppcnlem2  37276  knoppcnlem4  37278  knoppcnlem10  37284  unbdqndv2lem1  37291  unbdqndv2lem2  37292  knoppndvlem1  37294  knoppndvlem11  37304  knoppndvlem12  37305  knoppndvlem14  37307  knoppndvlem15  37308  knoppndvlem17  37310  knoppndvlem18  37311  knoppndvlem19  37312  knoppndvlem20  37313  knoppndvlem21  37314  opnmbllem0  38488  itg2addnclem2  38504  itg2addnclem3  38505  iblmulc2nc  38517  itgmulc2nclem1  38518  ftc1cnnclem  38523  ftc1anclem3  38527  areacirclem4  38543  geomcau  38607  equivbnd  38638  bfplem1  38670  bfplem2  38671  bfp  38672  rrnequiv  38683  rrntotbnd  38684  lcmineqlem19  43011  lcmineqlem20  43012  lcmineqlem21  43013  lcmineqlem22  43014  3lexlogpow2ineq2  43023  dvrelogpow2b  43032  aks4d1p1p2  43034  aks4d1p1p4  43035  aks4d1p1p6  43037  aks4d1p1p7  43038  aks4d1p1p5  43039  aks4d1p1  43040  aks4d1p8d2  43049  aks4d1p8  43051  posbezout  43064  aks6d1c2lem4  43091  2np3bcnp1  43108  2ap1caineq  43109  aks6d1c6lem4  43137  aks6d1c7lem1  43144  aks6d1c7lem2  43145  resubdi  43369  remul02  43378  remul01  43380  remulinvcom  43406  rediveud  43416  redivcan3d  43421  redivrec2d  43433  rediv23d  43434  sn-0tie0  43437  renegmulnnass  43451  mulgt0con1d  43456  mulgt0con2d  43457  mulgt0b1d  43458  sn-ltmul2d  43459  mulgt0b2d  43464  sn-mulgt1d  43465  mulltgt0d  43468  mullt0b1d  43469  mullt0b2d  43470  sn-mullt0d  43471  sn-itrere  43474  sn-retire  43475  fltnltalem  43606  fltnlta  43607  3cubeslem2  43628  3cubeslem3r  43630  3cubeslem4  43632  irrapxlem1  43761  irrapxlem2  43762  irrapxlem3  43763  irrapxlem4  43764  irrapxlem5  43765  pellexlem2  43769  pellexlem6  43773  pell14qrgt0  43798  pell1qrge1  43809  pell1qrgaplem  43812  pellqrexplicit  43816  pellqrex  43818  rmspecsqrtnq  43845  rmxycomplete  43856  rmxypos  43886  ltrmynn0  43887  ltrmxnn0  43888  jm2.24nn  43898  jm2.17a  43899  jm2.17b  43900  jm2.17c  43901  jm2.27c  43946  jm3.1lem2  43957  areaquad  44155  sqrtcval  44579  resqrtval  44581  imsqrtval  44582  imo72b2lem0  45103  cvgdvgrat  45235  nzprmdif  45241  lt3addmuld  46232  fperiodmullem  46234  fperiodmul  46235  lt4addmuld  46237  xralrple2  46282  xralrple3  46301  ltmulneg  46319  fmul01  46508  fmuldfeqlem1  46510  fmul01lt1lem1  46512  sumnnodd  46558  ltmod  46564  0ellimcdiv  46575  limclner  46577  dvdivbd  46849  dvbdfbdioolem2  46855  dvbdfbdioo  46856  ioodvbdlimc1lem1  46857  ioodvbdlimc1lem2  46858  ioodvbdlimc2lem  46860  stoweidlem1  46927  stoweidlem11  46937  stoweidlem13  46939  stoweidlem14  46940  stoweidlem16  46942  stoweidlem17  46943  stoweidlem22  46948  stoweidlem24  46950  stoweidlem25  46951  stoweidlem26  46952  stoweidlem30  46956  stoweidlem34  46960  stoweidlem36  46962  stoweidlem49  46975  stoweidlem59  46985  stoweidlem60  46986  wallispilem4  46994  wallispilem5  46995  wallispi  46996  wallispi2lem1  46997  wallispi2  46999  stirlinglem1  47000  stirlinglem3  47002  stirlinglem5  47004  stirlinglem6  47005  stirlinglem7  47006  stirlinglem10  47009  stirlinglem11  47010  stirlinglem12  47011  stirlinglem15  47014  stirlingr  47016  dirker2re  47018  dirkerval2  47020  dirkerre  47021  dirkertrigeqlem1  47024  dirkertrigeqlem2  47025  dirkeritg  47028  dirkercncflem2  47030  dirkercncflem4  47032  fourierdlem4  47037  fourierdlem5  47038  fourierdlem6  47039  fourierdlem7  47040  fourierdlem16  47049  fourierdlem18  47051  fourierdlem19  47052  fourierdlem21  47054  fourierdlem22  47055  fourierdlem26  47059  fourierdlem35  47068  fourierdlem39  47072  fourierdlem41  47074  fourierdlem42  47075  fourierdlem43  47076  fourierdlem48  47080  fourierdlem49  47081  fourierdlem51  47083  fourierdlem55  47087  fourierdlem56  47088  fourierdlem57  47089  fourierdlem58  47090  fourierdlem62  47094  fourierdlem63  47095  fourierdlem64  47096  fourierdlem65  47097  fourierdlem66  47098  fourierdlem67  47099  fourierdlem68  47100  fourierdlem71  47103  fourierdlem72  47104  fourierdlem73  47105  fourierdlem76  47108  fourierdlem77  47109  fourierdlem78  47110  fourierdlem83  47115  fourierdlem84  47116  fourierdlem87  47119  fourierdlem88  47120  fourierdlem89  47121  fourierdlem90  47122  fourierdlem91  47123  fourierdlem94  47126  fourierdlem95  47127  fourierdlem97  47129  fourierdlem103  47135  fourierdlem104  47136  fourierdlem112  47144  fourierdlem113  47145  sqwvfoura  47154  sqwvfourb  47155  fouriersw  47157  etransclem23  47183  etransclem48  47208  rrndistlt  47216  hoidmvlelem1  47521  hoidmvlelem2  47522  hoidmvlelem4  47524  smfmullem1  47717  smfmullem2  47718  smfmullem3  47719  smfmul  47721  2timesltsqm1  48365  fmtno4prmfac  48573  lighneallem4a  48609  requad01  48635  requad1  48636  requad2  48637  perfectALTVlem2  48736  gpg3kgrtriexlem1  49097  gpg3kgrtriexlem4  49100  gpg3kgrtriexlem6  49102  ply1mulgsumlem2  49415  digvalnn0  49627  dignn0fr  49629  dig2nn0  49639  affinecomb1  49730  rrx2linest2  49772  line2  49780  itsclc0lem1  49784  itsclc0lem2  49785  itsclc0lem3  49786  itscnhlc0yqe  49787  itsclc0yqsollem2  49791  itsclc0yqsol  49792  itscnhlc0xyqsol  49793  itsclc0xyqsolr  49797  itsclinecirc0  49801  itsclinecirc0b  49802  itsclinecirc0in  49803  itsclquadb  49804  itsclquadeu  49805  2itscp  49809  itscnhlinecirc02plem1  49810  itscnhlinecirc02p  49813  inlinecirc02plem  49814  crosspcle1d  50871  crosspcle2d  50872  crosspcle3d  50873  crosspdotsumlem  50880  crosspdotd  50881  crosspaltd  50882  crossp3d  50883  veronesefvcl  50888  veronesev4lem  50892  veronesev5lem  50893  veronesev6lem  50894  veroquadgsumlem  50899  veroquadmodzerod  50900  amgmwlem  50903