MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulcld Unicode version

Theorem mulcld 8871
Description: Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1  |-  ( ph  ->  A  e.  CC )
addcld.2  |-  ( ph  ->  B  e.  CC )
Assertion
Ref Expression
mulcld  |-  ( ph  ->  ( A  x.  B
)  e.  CC )

Proof of Theorem mulcld
StepHypRef Expression
1 addcld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addcld.2 . 2  |-  ( ph  ->  B  e.  CC )
3 mulcl 8837 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
41, 2, 3syl2anc 642 1  |-  ( ph  ->  ( A  x.  B
)  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696  (class class class)co 5874   CCcc 8751    x. cmul 8758
This theorem is referenced by:  mul02lem1  9004  addid1  9008  cnegex  9009  receu  9429  divrec  9456  divcan3  9464  divdivdiv  9477  divsubdiv  9492  cru  9754  lincmb01cmp  10793  iccf1o  10794  moddiffl  10998  modcyc  11015  modadd1  11017  modmul1  11018  mulexpz  11158  expmulz  11164  binom3  11238  bernneq  11243  remullem  11629  cjreim2  11662  absimle  11810  abstri  11830  sqreulem  11859  sqreu  11860  mulcn2  12085  reccn2  12086  o1rlimmul  12108  isummulc2  12241  fsummulc2  12262  fsumparts  12280  binomlem  12303  binom1dif  12307  incexclem  12311  incexc  12312  incexc2  12313  geomulcvg  12348  mertenslem1  12356  mertens  12358  efaddlem  12390  sinadd  12460  cosadd  12461  tanaddlem  12462  tanadd  12463  addsin  12466  sincossq  12472  sin2t  12473  dvds2ln  12575  oddm1even  12604  sadadd2lem2  12657  bezoutlem2  12734  bezoutlem3  12735  bezoutlem4  12736  phiprmpw  12860  pythagtriplem12  12895  pythagtriplem14  12897  pythagtriplem16  12899  pcpremul  12912  pcaddlem  12952  fldivp1  12961  mul4sqlem  13016  4sqlem14  13021  vdwapun  13037  vdwlem2  13045  vdwlem6  13049  zlpirlem3  16459  znunit  16533  blcvx  18320  icopnfcnv  18456  mbfmulc2re  19019  mbfmulc2  19034  itg1addlem4  19070  itg1addlem5  19071  itg1mulc  19075  mbfmul  19097  itgcl  19154  itgcnlem  19160  iblmulc2  19201  itgmulc2  19204  itgabs  19205  itgsplit  19206  dvmulbr  19304  dvcmul  19309  dvcmulf  19310  dvexp  19318  dvmptcmul  19329  dvexp3  19341  dvsincos  19344  cmvth  19354  dvlipcn  19357  dvfsumabs  19386  dvfsumlem1  19389  ftc1lem4  19402  itgparts  19410  plyf  19596  ply1termlem  19601  plyeq0lem  19608  plypf1  19610  plyaddlem1  19611  plymullem1  19612  coeeulem  19622  coeidlem  19635  coeid3  19638  plyco  19639  coemullem  19647  coemulhi  19651  coemulc  19652  dgrcolem2  19671  plycjlem  19673  plyrecj  19676  dvply1  19680  vieta1lem2  19707  vieta1  19708  elqaalem3  19717  aareccl  19722  aalioulem1  19728  taylfvallem1  19752  tayl0  19757  dvtaylp  19765  taylthlem2  19769  psergf  19804  radcnvlem1  19805  dvradcnv  19813  psercn2  19815  pserdvlem2  19820  pserdv2  19822  abelthlem4  19826  abelthlem5  19827  abelthlem6  19828  abelthlem7  19830  abelthlem9  19832  tanregt0  19917  cosargd  19978  tanarg  19986  advlogexp  20018  logtayllem  20022  logtayl  20023  cxpadd  20042  mulcxp  20048  cxpmul  20051  cxpmul2  20052  cxpmul2z  20054  abscxp  20055  abscxp2  20056  dvcxp2  20099  abscxpbnd  20109  root1eq1  20111  cxpeq  20113  angcan  20116  pythag  20131  ssscongptld  20138  affineequiv  20139  affineequiv2  20140  chordthmlem2  20146  chordthmlem3  20147  chordthmlem4  20148  chordthmlem5  20149  quad2  20151  quad  20152  dcubic1lem  20155  dcubic2  20156  dcubic1  20157  dcubic  20158  mcubic  20159  cubic2  20160  cubic  20161  binom4  20162  dquartlem1  20163  dquartlem2  20164  dquart  20165  quart1cl  20166  quart1lem  20167  quart1  20168  quartlem1  20169  quartlem2  20170  atantayl3  20251  leibpi  20254  birthdaylem2  20263  divsqrsumo1  20294  cvxcl  20295  jensenlem2  20298  wilthlem2  20323  ftalem1  20326  ftalem2  20327  ftalem4  20329  ftalem5  20330  basellem2  20335  basellem3  20336  basellem8  20341  muinv  20449  fsumdvdsmul  20451  logfacrlim  20479  logexprlim  20480  perfectlem2  20485  bposlem9  20547  lgsquad2lem1  20613  2sqlem3  20621  rplogsumlem1  20649  dchrisumlem2  20655  dchrisumlem3  20656  dchrmusum2  20659  dchrvmasumlem1  20660  dchrvmasum2lem  20661  dchrvmasum2if  20662  dchrvmasumlem3  20664  dchrvmasumiflem1  20666  dchrvmasumiflem2  20667  rpvmasum2  20677  dchrisum0lem1  20681  dchrisum0lem2a  20682  dchrisum0lem2  20683  dchrmusumlem  20687  dchrvmasumlem  20688  rplogsum  20692  mudivsum  20695  mulogsumlem  20696  mulogsum  20697  mulog2sumlem1  20699  mulog2sumlem2  20700  mulog2sumlem3  20701  vmalogdivsum  20704  logsqvma  20707  log2sumbnd  20709  selberglem1  20710  selberglem2  20711  selberglem3  20712  selberg  20713  selberg2lem  20715  selberg2  20716  selberg3lem1  20722  selberg3  20724  selberg4lem1  20725  selberg4  20726  pntrsumo1  20730  selbergr  20733  selberg3r  20734  selberg4r  20735  selberg34r  20736  pntsval2  20741  pntrlog2bndlem1  20742  pntrlog2bndlem2  20743  pntrlog2bndlem3  20744  pntrlog2bndlem4  20745  pntrlog2bndlem5  20746  pntrlog2bndlem6  20748  pntrlog2bnd  20749  pntlemb  20762  pntlemf  20770  pntlemo  20772  ostth2lem2  20799  ostth2lem3  20800  ipval2  21296  dipcl  21304  riesz3i  22658  cnre2csqima  23310  rmulccn  23316  dya2iocseg  23594  indsum  23621  subfacval2  23733  subfaclim  23734  rescon  23792  subdivcomb1  24105  subdivcomb2  24106  faclim  24126  brbtwn2  24605  colinearalg  24610  ax5seglem2  24629  ax5seglem9  24637  axeuclidlem  24662  axcontlem2  24665  axcontlem4  24667  axcontlem7  24670  axcontlem8  24671  bpolycl  24859  bpolysum  24860  bpolydiflem  24861  bpoly4  24866  itg2addnc  25005  iblmulc2nc  25016  itgmulc2nc  25019  itgabsnc  25020  ftc1cnnclem  25024  dvreasin  25026  areacirclem2  25028  areacirclem5  25032  areacirc  25034  rdr  26538  cntotbnd  26623  pellexlem1  27017  pellexlem2  27018  pellexlem6  27022  pell1234qrne0  27041  pell1234qrreccl  27042  pell1234qrmulcl  27043  pell1234qrdich  27049  pell14qrdich  27057  pell1qrge1  27058  pell1qrgaplem  27061  qirropth  27096  rmxyneg  27108  rmxyadd  27109  rmxm1  27122  rmym1  27123  rmxluc  27124  rmyluc  27125  rmxdbl  27127  rmydbl  27128  jm2.18  27184  jm2.19lem1  27185  jm2.19lem2  27186  jm2.19lem4  27188  jm2.19  27189  jm2.22  27191  jm2.23  27192  jm2.25  27195  jm2.27c  27203  jm3.1lem2  27214  flcidc  27482  expgrowth  27655  mulc1cncfg  27824  clim1fr1  27830  dvsinexp  27843  itgsinexplem1  27851  itgsinexp  27852  wallispilem4  27920  wallispilem5  27921  wallispi  27922  wallispi2lem1  27923  wallispi2lem2  27924  wallispi2  27925  stirlinglem1  27926  stirlinglem3  27928  stirlinglem4  27929  stirlinglem5  27930  stirlinglem6  27931  stirlinglem7  27932  stirlinglem8  27933  stirlinglem10  27935  stirlinglem11  27936  stirlinglem12  27937  stirlinglem13  27938  stirlinglem14  27939  stirlinglem15  27940  sigarim  27944  sigarac  27945  sigaraf  27946  sigarmf  27947  sigarls  27950  sigardiv  27954  sigarcol  27957  cevathlem1  27960
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulcl 8815
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator