Theorem remulcld 11363

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  (class class class)co 7440  ℝcr 11223   · cmul 11229

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

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

This theorem is used by:  mulge0  11858  msqge0  11861  redivcl  12060  prodgt0  12188  ltmul1a  12190  ltmul1  12191  ltmuldiv  12214  lt2msq1  12225  lt2msq  12226  le2msq  12241  msq11  12242  supmul1  12310  supmullem2  12312  supmul  12313  div4p1lem1div2  12625  mul2lt0rlt0  13248  mul2lt0bi  13252  prodge0rd  13253  ge2halflem1  13261  qbtwnre  13353  xmulneg1  13423  xmulf  13426  lincmb01cmp  13650  iccf1o  13651  flmulnn0  13991  flhalf  13994  modcl  14037  mod0  14040  modge0  14043  modmulnn  14053  mulp1mod1  14078  muladdmod  14079  2txmodxeq0  14098  modaddmulmod  14105  moddi  14106  modsubdir  14107  modirr  14109  addmodlteq  14113  bernneq  14397  bernneq3  14399  expnbnd  14400  expmulnbnd  14403  discr1  14407  discr  14408  faclbnd  14458  faclbnd6  14467  remullem  15321  01sqrexlem7  15441  sqrtmul  15452  abstri  15524  sqreulem  15553  bhmafibid1  15661  mulcn2  15789  reccn2  15790  o1rlimmul  15812  lo1mul  15821  iseraltlem2  15876  iseraltlem3  15877  iseralt  15878  o1fsum  16006  cvgcmpce  16011  climcndslem1  16044  climcndslem2  16045  climcnds  16046  geomulcvg  16071  cvgrat  16078  mertenslem1  16079  fprodge1  16188  eftlub  16303  sin02gt0  16386  eirrlem  16398  bitsp1o  16629  2mulprm  16894  isprm5  16909  modprm0  17009  prmreclem3  17122  prmreclem4  17123  prmreclem5  17124  2expltfac  17296  metss2lem  24857  nlmvscnlem2  25031  nrginvrcnlem  25037  nmoco  25083  nmotri  25085  nghmcn  25091  icopnfhmeo  25291  nmoleub2lem3  25463  ipcau2  25582  tcphcphlem1  25583  ipcnlem2  25592  rrxcph  25740  csbren  25747  trirn  25748  pjthlem1  25785  opnmbllem  25949  vitalilem4  25959  itg1val2  26032  itg1cl  26033  itg1ge0  26034  itg1addlem4  26047  itg1mulc  26052  itg1ge0a  26059  itg1climres  26062  mbfi1fseqlem1  26063  mbfi1fseqlem3  26065  mbfi1fseqlem4  26066  mbfi1fseqlem5  26067  mbfi1fseqlem6  26068  itg2const2  26089  itg2mulclem  26094  itg2mulc  26095  itg2monolem1  26098  itg2monolem3  26100  itg2cnlem2  26110  iblconst  26165  iblmulc2  26178  itgmulc2lem1  26179  itgmulc2lem2  26180  bddmulibl  26186  bddiblnc  26189  dveflem  26326  cmvth  26338  dvlip  26340  dvlipcn  26341  dvivthlem1  26355  lhop1lem  26360  dvcvx  26367  dvfsumlem2  26374  dvfsumlem3  26375  dvfsumlem4  26376  dvfsum2  26381  ftc1lem4  26386  plyeq0lem  26556  plyn0mulidp  26629  aalioulem3  26688  aalioulem4  26689  aaliou3lem9  26704  ulmdvlem1  26754  itgulm  26762  radcnvlem1  26767  radcnvlem2  26768  dvradcnv  26775  abelthlem2  26786  abelthlem7  26792  tangtx  26861  tanregt0  26894  logdivlti  26975  logcnlem3  26999  logcnlem4  27000  logccv  27018  recxpcl  27030  cxpmul  27043  cxplt  27049  cxple2  27052  abscxpbnd  27108  lawcoslem1  27170  heron  27193  atans2  27286  efrlim  27324  o1cxp  27329  scvxcvx  27340  jensenlem2  27342  amgmlem  27344  fsumharmonic  27366  lgamgulmlem2  27384  lgamgulmlem3  27385  lgamgulmlem4  27386  lgamgulmlem5  27387  lgamgulmlem6  27388  relgamcl  27416  ftalem1  27427  ftalem2  27428  ftalem5  27431  basellem3  27437  basellem8  27442  chpub  27574  logfacubnd  27575  logfaclbnd  27576  logfacbnd3  27577  logexprlim  27579  perfectlem2  27584  bclbnd  27634  efexple  27635  bposlem1  27638  bposlem2  27639  bposlem6  27643  bposlem9  27646  lgsdilem  27678  gausslemma2dlem0c  27712  gausslemma2dlem2  27721  gausslemma2dlem3  27722  gausslemma2dlem6  27726  lgseisenlem4  27732  lgseisen  27733  lgsquadlem1  27734  lgsquadlem2  27735  2lgslem1a1  27743  2sqmod  27790  chebbnd1lem1  27823  chebbnd1lem3  27825  chtppilimlem1  27827  chpchtlim  27833  vmadivsum  27836  rplogsumlem1  27838  rpvmasumlem  27841  dchrisumlem2  27844  dchrisumlem3  27845  dchrmusum2  27848  dchrvmasumlem2  27852  dchrvmasumiflem1  27855  dchrisum0re  27867  dchrisum0lem1  27870  dirith2  27882  mulogsumlem  27885  mulogsum  27886  mulog2sumlem2  27889  vmalogdivsum2  27892  vmalogdivsum  27893  2vmadivsumlem  27894  logsqvma  27896  logsqvma2  27897  log2sumbnd  27898  selberglem2  27900  selberg  27902  selbergb  27903  selberg2lem  27904  selberg2b  27906  chpdifbndlem1  27907  chpdifbndlem2  27908  selberg3lem1  27911  selberg3lem2  27912  selberg3  27913  selberg4lem1  27914  selberg4  27915  pntrsumbnd2  27921  selberg3r  27923  selberg4r  27924  selberg34r  27925  pntsf  27927  pntsval2  27930  pntrlog2bndlem1  27931  pntrlog2bndlem2  27932  pntrlog2bndlem3  27933  pntrlog2bndlem4  27934  pntrlog2bndlem5  27935  pntrlog2bndlem6  27937  pntrlog2bnd  27938  pntpbnd1a  27939  pntpbnd1  27940  pntpbnd2  27941  pntibndlem2a  27944  pntibndlem2  27945  pntlemb  27951  pntlemr  27956  pntlemj  27957  pntlemf  27959  pntlemk  27960  pntlemo  27961  pntlem3  27963  ostth2lem1  27972  ostth2lem2  27988  ostth2lem3  27989  ostth2lem4  27990  ostth3  27992  ttgcontlem1  29489  brbtwn2  29510  colinearalglem4  29514  axsegconlem8  29529  axsegconlem9  29530  axsegconlem10  29531  ax5seglem3  29536  axpaschlem  29545  axpasch  29546  axeuclidlem  29567  numclwwlk5  31016  numclwwlk7  31019  smcnlem  31326  ubthlem2  31500  htthlem  31546  pjhthlem1  32020  cnlnadjlem7  32702  nmopcoadji  32730  branmfn  32734  leopnmid  32767  nexple  33491  constrremulcl  34466  constrmulcl  34470  cos9thpiminplylem1  34481  cos9thpinconstrlem1  34488  rmulccn  34627  xrge0iifhom  34636  dya2icoseg  34976  eulerpartlems  35059  eulerpartlemgc  35061  eulerpartlemb  35067  signsvtp  35279  reprgt  35317  breprexplemc  35328  circlemethhgt  35339  hgt750lemd  35344  logdivsqrle  35346  hgt750lem  35347  hgt750lemf  35349  hgt750lemb  35352  hgt750lema  35353  hgt750leme  35354  tgoldbachgtde  35356  resconn  36177  knoppcnlem2  37537  knoppcnlem4  37539  knoppcnlem10  37545  unbdqndv2lem1  37552  unbdqndv2lem2  37553  knoppndvlem1  37555  knoppndvlem11  37565  knoppndvlem12  37566  knoppndvlem14  37568  knoppndvlem15  37569  knoppndvlem17  37571  knoppndvlem18  37572  knoppndvlem19  37573  knoppndvlem20  37574  knoppndvlem21  37575  opnmbllem0  38765  itg2addnclem2  38781  itg2addnclem3  38782  iblmulc2nc  38794  itgmulc2nclem1  38795  ftc1cnnclem  38800  ftc1anclem3  38804  areacirclem4  38820  geomcau  38884  equivbnd  38915  bfplem1  38947  bfplem2  38948  bfp  38949  rrnequiv  38960  rrntotbnd  38961  lcmineqlem19  43288  lcmineqlem20  43289  lcmineqlem21  43290  lcmineqlem22  43291  3lexlogpow2ineq2  43300  dvrelogpow2b  43309  aks4d1p1p2  43311  aks4d1p1p4  43312  aks4d1p1p6  43314  aks4d1p1p7  43315  aks4d1p1p5  43316  aks4d1p1  43317  aks4d1p8d2  43326  aks4d1p8  43328  posbezout  43341  aks6d1c2lem4  43368  2np3bcnp1  43385  2ap1caineq  43386  aks6d1c6lem4  43414  aks6d1c7lem1  43421  aks6d1c7lem2  43422  resubdi  43638  remul02  43647  remul01  43649  remulinvcom  43675  rediveud  43685  redivcan3d  43690  redivrec2d  43702  rediv23d  43703  sn-0tie0  43706  renegmulnnass  43720  mulgt0con1d  43725  mulgt0con2d  43726  mulgt0b1d  43727  sn-ltmul2d  43728  mulgt0b2d  43733  sn-mulgt1d  43734  mulltgt0d  43737  mullt0b1d  43738  mullt0b2d  43739  sn-mullt0d  43740  sn-itrere  43743  sn-retire  43744  fltnltalem  43864  fltnlta  43865  3cubeslem2  43886  3cubeslem3r  43888  3cubeslem4  43890  irrapxlem1  44020  irrapxlem2  44021  irrapxlem3  44022  irrapxlem4  44023  irrapxlem5  44024  pellexlem2  44028  pellexlem6  44032  pell14qrgt0  44057  pell1qrge1  44068  pell1qrgaplem  44071  pellqrexplicit  44075  pellqrex  44077  rmspecsqrtnq  44104  rmxycomplete  44115  rmxypos  44145  ltrmynn0  44146  ltrmxnn0  44147  jm2.24nn  44157  jm2.17a  44158  jm2.17b  44159  jm2.17c  44160  jm2.27c  44205  jm3.1lem2  44216  areaquad  44408  sqrtcval  44831  resqrtval  44833  imsqrtval  44834  imo72b2lem0  45355  cvgdvgrat  45487  nzprmdif  45493  lt3addmuld  46520  fperiodmullem  46522  fperiodmul  46523  lt4addmuld  46525  xralrple2  46569  xralrple3  46588  ltmulneg  46606  fmul01  46795  fmuldfeqlem1  46797  fmul01lt1lem1  46799  sumnnodd  46845  ltmod  46851  0ellimcdiv  46862  limclner  46864  dvdivbd  47136  dvbdfbdioolem2  47142  dvbdfbdioo  47143  ioodvbdlimc1lem1  47144  ioodvbdlimc1lem2  47145  ioodvbdlimc2lem  47147  stoweidlem1  47214  stoweidlem11  47224  stoweidlem13  47226  stoweidlem14  47227  stoweidlem16  47229  stoweidlem17  47230  stoweidlem22  47235  stoweidlem24  47237  stoweidlem25  47238  stoweidlem26  47239  stoweidlem30  47243  stoweidlem34  47247  stoweidlem36  47249  stoweidlem49  47262  stoweidlem59  47272  stoweidlem60  47273  wallispilem4  47281  wallispilem5  47282  wallispi  47283  wallispi2lem1  47284  wallispi2  47286  stirlinglem1  47287  stirlinglem3  47289  stirlinglem5  47291  stirlinglem6  47292  stirlinglem7  47293  stirlinglem10  47296  stirlinglem11  47297  stirlinglem12  47298  stirlinglem15  47301  stirlingr  47303  dirker2re  47305  dirkerval2  47307  dirkerre  47308  dirkertrigeqlem1  47311  dirkertrigeqlem2  47312  dirkeritg  47315  dirkercncflem2  47317  dirkercncflem4  47319  fourierdlem4  47324  fourierdlem5  47325  fourierdlem6  47326  fourierdlem7  47327  fourierdlem16  47336  fourierdlem18  47338  fourierdlem19  47339  fourierdlem21  47341  fourierdlem22  47342  fourierdlem26  47346  fourierdlem35  47355  fourierdlem39  47359  fourierdlem41  47361  fourierdlem42  47362  fourierdlem43  47363  fourierdlem48  47367  fourierdlem49  47368  fourierdlem51  47370  fourierdlem55  47374  fourierdlem56  47375  fourierdlem57  47376  fourierdlem58  47377  fourierdlem62  47381  fourierdlem63  47382  fourierdlem64  47383  fourierdlem65  47384  fourierdlem66  47385  fourierdlem67  47386  fourierdlem68  47387  fourierdlem71  47390  fourierdlem72  47391  fourierdlem73  47392  fourierdlem76  47395  fourierdlem77  47396  fourierdlem78  47397  fourierdlem83  47402  fourierdlem84  47403  fourierdlem87  47406  fourierdlem88  47407  fourierdlem89  47408  fourierdlem90  47409  fourierdlem91  47410  fourierdlem94  47413  fourierdlem95  47414  fourierdlem97  47416  fourierdlem103  47422  fourierdlem104  47423  fourierdlem112  47431  fourierdlem113  47432  sqwvfoura  47441  sqwvfourb  47442  fouriersw  47444  etransclem23  47470  etransclem48  47495  rrndistlt  47503  hoidmvlelem1  47808  hoidmvlelem2  47809  hoidmvlelem4  47811  smfmullem1  48004  smfmullem2  48005  smfmullem3  48006  smfmul  48008  2timesltsqm1  48652  fmtno4prmfac  48860  lighneallem4a  48896  requad01  48922  requad1  48923  requad2  48924  perfectALTVlem2  49023  gpg3kgrtriexlem1  49384  gpg3kgrtriexlem4  49387  gpg3kgrtriexlem6  49389  ply1mulgsumlem2  49702  digvalnn0  49914  dignn0fr  49916  dig2nn0  49926  affinecomb1  50017  rrx2linest2  50059  line2  50067  itsclc0lem1  50071  itsclc0lem2  50072  itsclc0lem3  50073  itscnhlc0yqe  50074  itsclc0yqsollem2  50078  itsclc0yqsol  50079  itscnhlc0xyqsol  50080  itsclc0xyqsolr  50084  itsclinecirc0  50088  itsclinecirc0b  50089  itsclinecirc0in  50090  itsclquadb  50091  itsclquadeu  50092  2itscp  50096  itscnhlinecirc02plem1  50097  itscnhlinecirc02p  50100  inlinecirc02plem  50101  crosspcle1d  51233  crosspcle2d  51234  crosspcle3d  51235  crosspdotsumlem  51242  crosspdotd  51243  crosspaltd  51244  crossp3d  51245  veronesefvcl  51250  veronesev4lem  51254  veronesev5lem  51255  veronesev6lem  51256  veroquadgsumlem  51261  veroquadmodzerod  51262  amgmwlem  51265