Theorem remulcld 10828

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

Syntax hints:   → wi 4   ∈ wcel 2112  (class class class)co 7191  ℝcr 10693   · cmul 10699

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

This theorem depends on definitions:  df-bi 210  df-an 400

This theorem is referenced by:  mulge0  11315  msqge0  11318  redivcl  11516  prodgt0  11644  ltmul1a  11646  ltmul1  11647  ltmuldiv  11670  lt2msq1  11681  lt2msq  11682  le2msq  11697  msq11  11698  supmul1  11766  supmullem2  11768  supmul  11769  div4p1lem1div2  12050  mul2lt0rlt0  12653  mul2lt0bi  12657  prodge0rd  12658  qbtwnre  12754  xmulneg1  12824  xmulf  12827  lincmb01cmp  13048  iccf1o  13049  flmulnn0  13367  flhalf  13370  modcl  13411  mod0  13414  modge0  13417  modmulnn  13427  mulp1mod1  13450  2txmodxeq0  13469  modaddmulmod  13476  moddi  13477  modsubdir  13478  modirr  13480  addmodlteq  13484  bernneq  13761  bernneq3  13763  expnbnd  13764  expmulnbnd  13767  discr1  13771  discr  13772  faclbnd  13821  faclbnd6  13830  remullem  14656  sqrlem7  14777  sqrtmul  14788  abstri  14859  sqreulem  14888  bhmafibid1  14994  mulcn2  15122  reccn2  15123  o1rlimmul  15145  lo1mul  15154  iseraltlem2  15211  iseraltlem3  15212  iseralt  15213  o1fsum  15340  cvgcmpce  15345  climcndslem1  15376  climcndslem2  15377  climcnds  15378  geomulcvg  15403  cvgrat  15410  mertenslem1  15411  fprodge1  15520  eftlub  15633  sin02gt0  15716  eirrlem  15728  bitsp1o  15955  2mulprm  16213  isprm5  16227  modprm0  16321  prmreclem3  16434  prmreclem4  16435  prmreclem5  16436  2expltfac  16609  metss2lem  23363  nlmvscnlem2  23537  nrginvrcnlem  23543  nmoco  23589  nmotri  23591  nghmcn  23597  icopnfhmeo  23794  nmoleub2lem3  23966  ipcau2  24085  tcphcphlem1  24086  ipcnlem2  24095  rrxcph  24243  csbren  24250  trirn  24251  pjthlem1  24288  opnmbllem  24452  vitalilem4  24462  itg1val2  24535  itg1cl  24536  itg1ge0  24537  itg1addlem4  24550  itg1addlem4OLD  24551  itg1mulc  24556  itg1ge0a  24563  itg1climres  24566  mbfi1fseqlem1  24567  mbfi1fseqlem3  24569  mbfi1fseqlem4  24570  mbfi1fseqlem5  24571  mbfi1fseqlem6  24572  itg2const2  24593  itg2mulclem  24598  itg2mulc  24599  itg2monolem1  24602  itg2monolem3  24604  itg2cnlem2  24614  iblconst  24669  iblmulc2  24682  itgmulc2lem1  24683  itgmulc2lem2  24684  bddmulibl  24690  bddiblnc  24693  dveflem  24830  cmvth  24842  dvlip  24844  dvlipcn  24845  dvivthlem1  24859  lhop1lem  24864  dvcvx  24871  dvfsumlem2  24878  dvfsumlem3  24879  dvfsumlem4  24880  dvfsum2  24885  ftc1lem4  24890  plyeq0lem  25058  aalioulem3  25181  aalioulem4  25182  aaliou3lem9  25197  ulmdvlem1  25246  itgulm  25254  radcnvlem1  25259  radcnvlem2  25260  dvradcnv  25267  abelthlem2  25278  abelthlem7  25284  tangtx  25349  tanregt0  25382  logdivlti  25462  logcnlem3  25486  logcnlem4  25487  logccv  25505  recxpcl  25517  cxpmul  25530  cxplt  25536  cxple2  25539  abscxpbnd  25593  lawcoslem1  25652  heron  25675  atans2  25768  efrlim  25806  o1cxp  25811  scvxcvx  25822  jensenlem2  25824  amgmlem  25826  fsumharmonic  25848  lgamgulmlem2  25866  lgamgulmlem3  25867  lgamgulmlem4  25868  lgamgulmlem5  25869  lgamgulmlem6  25870  relgamcl  25898  ftalem1  25909  ftalem2  25910  ftalem5  25913  basellem3  25919  basellem8  25924  chpub  26055  logfacubnd  26056  logfaclbnd  26057  logfacbnd3  26058  logexprlim  26060  perfectlem2  26065  bclbnd  26115  efexple  26116  bposlem1  26119  bposlem2  26120  bposlem6  26124  bposlem9  26127  lgsdilem  26159  gausslemma2dlem0c  26193  gausslemma2dlem2  26202  gausslemma2dlem3  26203  gausslemma2dlem6  26207  lgseisenlem4  26213  lgseisen  26214  lgsquadlem1  26215  lgsquadlem2  26216  2lgslem1a1  26224  2sqmod  26271  chebbnd1lem1  26304  chebbnd1lem3  26306  chtppilimlem1  26308  chpchtlim  26314  vmadivsum  26317  rplogsumlem1  26319  rpvmasumlem  26322  dchrisumlem2  26325  dchrisumlem3  26326  dchrmusum2  26329  dchrvmasumlem2  26333  dchrvmasumiflem1  26336  dchrisum0re  26348  dchrisum0lem1  26351  dirith2  26363  mulogsumlem  26366  mulogsum  26367  mulog2sumlem2  26370  vmalogdivsum2  26373  vmalogdivsum  26374  2vmadivsumlem  26375  logsqvma  26377  logsqvma2  26378  log2sumbnd  26379  selberglem2  26381  selberg  26383  selbergb  26384  selberg2lem  26385  selberg2b  26387  chpdifbndlem1  26388  chpdifbndlem2  26389  selberg3lem1  26392  selberg3lem2  26393  selberg3  26394  selberg4lem1  26395  selberg4  26396  pntrsumbnd2  26402  selberg3r  26404  selberg4r  26405  selberg34r  26406  pntsf  26408  pntsval2  26411  pntrlog2bndlem1  26412  pntrlog2bndlem2  26413  pntrlog2bndlem3  26414  pntrlog2bndlem4  26415  pntrlog2bndlem5  26416  pntrlog2bndlem6  26418  pntrlog2bnd  26419  pntpbnd1a  26420  pntpbnd1  26421  pntpbnd2  26422  pntibndlem2a  26425  pntibndlem2  26426  pntlemb  26432  pntlemr  26437  pntlemj  26438  pntlemf  26440  pntlemk  26441  pntlemo  26442  pntlem3  26444  ostth2lem1  26453  ostth2lem2  26469  ostth2lem3  26470  ostth2lem4  26471  ostth3  26473  ttgcontlem1  26930  brbtwn2  26950  colinearalglem4  26954  axsegconlem8  26969  axsegconlem9  26970  axsegconlem10  26971  ax5seglem3  26976  axpaschlem  26985  axpasch  26986  axeuclidlem  27007  numclwwlk5  28425  numclwwlk7  28428  smcnlem  28732  ubthlem2  28906  htthlem  28952  pjhthlem1  29426  cnlnadjlem7  30108  nmopcoadji  30136  branmfn  30140  leopnmid  30173  rmulccn  31546  xrge0iifhom  31555  nexple  31643  dya2icoseg  31910  eulerpartlems  31993  eulerpartlemgc  31995  eulerpartlemb  32001  plymulx0  32192  signsvtp  32228  reprgt  32267  breprexplemc  32278  circlemethhgt  32289  hgt750lemd  32294  logdivsqrle  32296  hgt750lem  32297  hgt750lemf  32299  hgt750lemb  32302  hgt750lema  32303  hgt750leme  32304  tgoldbachgtde  32306  resconn  32875  knoppcnlem2  34360  knoppcnlem4  34362  knoppcnlem10  34368  unbdqndv2lem1  34375  unbdqndv2lem2  34376  knoppndvlem1  34378  knoppndvlem11  34388  knoppndvlem12  34389  knoppndvlem14  34391  knoppndvlem15  34392  knoppndvlem17  34394  knoppndvlem18  34395  knoppndvlem19  34396  knoppndvlem20  34397  knoppndvlem21  34398  opnmbllem0  35499  itg2addnclem2  35515  itg2addnclem3  35516  iblmulc2nc  35528  itgmulc2nclem1  35529  ftc1cnnclem  35534  ftc1anclem3  35538  areacirclem4  35554  geomcau  35603  equivbnd  35634  bfplem1  35666  bfplem2  35667  bfp  35668  rrnequiv  35679  rrntotbnd  35680  lcmineqlem19  39738  lcmineqlem20  39739  lcmineqlem21  39740  lcmineqlem22  39741  3lexlogpow2ineq2  39750  dvrelogpow2b  39758  aks4d1p1p2  39760  aks4d1p1p4  39761  aks4d1p1p6  39763  aks4d1p1p7  39764  aks4d1p1p5  39765  aks4d1p1  39766  2np3bcnp1  39769  2ap1caineq  39770  cxpgt0d  39993  resubdi  40028  remul02  40037  remul01  40039  remulinvcom  40063  sn-0tie0  40070  mulgt0con1d  40077  mulgt0con2d  40078  mulgt0b2d  40079  sn-ltmul2d  40080  sn-inelr  40084  itrere  40085  retire  40086  fltnltalem  40143  fltnlta  40144  3cubeslem2  40151  3cubeslem3r  40153  3cubeslem4  40155  irrapxlem1  40288  irrapxlem2  40289  irrapxlem3  40290  irrapxlem4  40291  irrapxlem5  40292  pellexlem2  40296  pellexlem6  40300  pell14qrgt0  40325  pell1qrge1  40336  pell1qrgaplem  40339  pellqrexplicit  40343  pellqrex  40345  rmspecsqrtnq  40372  rmxycomplete  40383  rmxypos  40413  ltrmynn0  40414  ltrmxnn0  40415  jm2.24nn  40425  jm2.17a  40426  jm2.17b  40427  jm2.17c  40428  jm2.27c  40473  jm3.1lem2  40484  areaquad  40691  sqrtcval  40866  resqrtval  40868  imsqrtval  40869  imo72b2lem0  41394  cvgdvgrat  41545  nzprmdif  41551  lt3addmuld  42454  fperiodmullem  42456  fperiodmul  42457  lt4addmuld  42459  xralrple2  42507  xralrple3  42527  ltmulneg  42546  fmul01  42739  fmuldfeqlem1  42741  fmul01lt1lem1  42743  sumnnodd  42789  ltmod  42797  0ellimcdiv  42808  limclner  42810  dvdivbd  43082  dvbdfbdioolem2  43088  dvbdfbdioo  43089  ioodvbdlimc1lem1  43090  ioodvbdlimc1lem2  43091  ioodvbdlimc2lem  43093  stoweidlem1  43160  stoweidlem11  43170  stoweidlem13  43172  stoweidlem14  43173  stoweidlem16  43175  stoweidlem17  43176  stoweidlem22  43181  stoweidlem24  43183  stoweidlem25  43184  stoweidlem26  43185  stoweidlem30  43189  stoweidlem34  43193  stoweidlem36  43195  stoweidlem49  43208  stoweidlem59  43218  stoweidlem60  43219  wallispilem4  43227  wallispilem5  43228  wallispi  43229  wallispi2lem1  43230  wallispi2  43232  stirlinglem1  43233  stirlinglem3  43235  stirlinglem5  43237  stirlinglem6  43238  stirlinglem7  43239  stirlinglem10  43242  stirlinglem11  43243  stirlinglem12  43244  stirlinglem15  43247  stirlingr  43249  dirker2re  43251  dirkerval2  43253  dirkerre  43254  dirkertrigeqlem1  43257  dirkertrigeqlem2  43258  dirkeritg  43261  dirkercncflem2  43263  dirkercncflem4  43265  fourierdlem4  43270  fourierdlem5  43271  fourierdlem6  43272  fourierdlem7  43273  fourierdlem16  43282  fourierdlem18  43284  fourierdlem19  43285  fourierdlem21  43287  fourierdlem22  43288  fourierdlem26  43292  fourierdlem35  43301  fourierdlem39  43305  fourierdlem41  43307  fourierdlem42  43308  fourierdlem43  43309  fourierdlem48  43313  fourierdlem49  43314  fourierdlem51  43316  fourierdlem55  43320  fourierdlem56  43321  fourierdlem57  43322  fourierdlem58  43323  fourierdlem62  43327  fourierdlem63  43328  fourierdlem64  43329  fourierdlem65  43330  fourierdlem66  43331  fourierdlem67  43332  fourierdlem68  43333  fourierdlem71  43336  fourierdlem72  43337  fourierdlem73  43338  fourierdlem76  43341  fourierdlem77  43342  fourierdlem78  43343  fourierdlem83  43348  fourierdlem84  43349  fourierdlem87  43352  fourierdlem88  43353  fourierdlem89  43354  fourierdlem90  43355  fourierdlem91  43356  fourierdlem94  43359  fourierdlem95  43360  fourierdlem97  43362  fourierdlem103  43368  fourierdlem104  43369  fourierdlem112  43377  fourierdlem113  43378  sqwvfoura  43387  sqwvfourb  43388  fouriersw  43390  etransclem23  43416  etransclem48  43441  rrndistlt  43449  hoidmvlelem1  43751  hoidmvlelem2  43752  hoidmvlelem4  43754  smfmullem1  43940  smfmullem2  43941  smfmullem3  43942  smfmul  43944  fmtno4prmfac  44640  lighneallem4a  44676  requad01  44689  requad1  44690  requad2  44691  perfectALTVlem2  44790  ply1mulgsumlem2  45344  digvalnn0  45561  dignn0fr  45563  dig2nn0  45573  affinecomb1  45664  rrx2linest2  45706  line2  45714  itsclc0lem1  45718  itsclc0lem2  45719  itsclc0lem3  45720  itscnhlc0yqe  45721  itsclc0yqsollem2  45725  itsclc0yqsol  45726  itscnhlc0xyqsol  45727  itsclc0xyqsolr  45731  itsclinecirc0  45735  itsclinecirc0b  45736  itsclinecirc0in  45737  itsclquadb  45738  itsclquadeu  45739  2itscp  45743  itscnhlinecirc02plem1  45744  itscnhlinecirc02p  45747  inlinecirc02plem  45748  amgmwlem  46120