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

Theorem mulcld 8855
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 8821 . 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 1684  (class class class)co 5858   CCcc 8735    x. cmul 8742
This theorem is referenced by:  mul02lem1  8988  addid1  8992  cnegex  8993  receu  9413  divrec  9440  divcan3  9448  divdivdiv  9461  divsubdiv  9476  cru  9738  lincmb01cmp  10777  iccf1o  10778  moddiffl  10982  modcyc  10999  modadd1  11001  modmul1  11002  mulexpz  11142  expmulz  11148  binom3  11222  bernneq  11227  remullem  11613  cjreim2  11646  absimle  11794  abstri  11814  sqreulem  11843  sqreu  11844  mulcn2  12069  reccn2  12070  o1rlimmul  12092  isummulc2  12225  fsummulc2  12246  fsumparts  12264  binomlem  12287  binom1dif  12291  incexclem  12295  incexc  12296  incexc2  12297  geomulcvg  12332  mertenslem1  12340  mertens  12342  efaddlem  12374  sinadd  12444  cosadd  12445  tanaddlem  12446  tanadd  12447  addsin  12450  sincossq  12456  sin2t  12457  dvds2ln  12559  oddm1even  12588  sadadd2lem2  12641  bezoutlem2  12718  bezoutlem3  12719  bezoutlem4  12720  phiprmpw  12844  pythagtriplem12  12879  pythagtriplem14  12881  pythagtriplem16  12883  pcpremul  12896  pcaddlem  12936  fldivp1  12945  mul4sqlem  13000  4sqlem14  13005  vdwapun  13021  vdwlem2  13029  vdwlem6  13033  zlpirlem3  16443  znunit  16517  blcvx  18304  icopnfcnv  18440  mbfmulc2re  19003  mbfmulc2  19018  itg1addlem4  19054  itg1addlem5  19055  itg1mulc  19059  mbfmul  19081  itgcl  19138  itgcnlem  19144  iblmulc2  19185  itgmulc2  19188  itgabs  19189  itgsplit  19190  dvmulbr  19288  dvcmul  19293  dvcmulf  19294  dvexp  19302  dvmptcmul  19313  dvexp3  19325  dvsincos  19328  cmvth  19338  dvlipcn  19341  dvfsumabs  19370  dvfsumlem1  19373  ftc1lem4  19386  itgparts  19394  plyf  19580  ply1termlem  19585  plyeq0lem  19592  plypf1  19594  plyaddlem1  19595  plymullem1  19596  coeeulem  19606  coeidlem  19619  coeid3  19622  plyco  19623  coemullem  19631  coemulhi  19635  coemulc  19636  dgrcolem2  19655  plycjlem  19657  plyrecj  19660  dvply1  19664  vieta1lem2  19691  vieta1  19692  elqaalem3  19701  aareccl  19706  aalioulem1  19712  taylfvallem1  19736  tayl0  19741  dvtaylp  19749  taylthlem2  19753  psergf  19788  radcnvlem1  19789  dvradcnv  19797  psercn2  19799  pserdvlem2  19804  pserdv2  19806  abelthlem4  19810  abelthlem5  19811  abelthlem6  19812  abelthlem7  19814  abelthlem9  19816  tanregt0  19901  cosargd  19962  tanarg  19970  advlogexp  20002  logtayllem  20006  logtayl  20007  cxpadd  20026  mulcxp  20032  cxpmul  20035  cxpmul2  20036  cxpmul2z  20038  abscxp  20039  abscxp2  20040  dvcxp2  20083  abscxpbnd  20093  root1eq1  20095  cxpeq  20097  angcan  20100  pythag  20115  ssscongptld  20122  affineequiv  20123  affineequiv2  20124  chordthmlem2  20130  chordthmlem3  20131  chordthmlem4  20132  chordthmlem5  20133  quad2  20135  quad  20136  dcubic1lem  20139  dcubic2  20140  dcubic1  20141  dcubic  20142  mcubic  20143  cubic2  20144  cubic  20145  binom4  20146  dquartlem1  20147  dquartlem2  20148  dquart  20149  quart1cl  20150  quart1lem  20151  quart1  20152  quartlem1  20153  quartlem2  20154  atantayl3  20235  leibpi  20238  birthdaylem2  20247  divsqrsumo1  20278  cvxcl  20279  jensenlem2  20282  wilthlem2  20307  ftalem1  20310  ftalem2  20311  ftalem4  20313  ftalem5  20314  basellem2  20319  basellem3  20320  basellem8  20325  muinv  20433  fsumdvdsmul  20435  logfacrlim  20463  logexprlim  20464  perfectlem2  20469  bposlem9  20531  lgsquad2lem1  20597  2sqlem3  20605  rplogsumlem1  20633  dchrisumlem2  20639  dchrisumlem3  20640  dchrmusum2  20643  dchrvmasumlem1  20644  dchrvmasum2lem  20645  dchrvmasum2if  20646  dchrvmasumlem3  20648  dchrvmasumiflem1  20650  dchrvmasumiflem2  20651  rpvmasum2  20661  dchrisum0lem1  20665  dchrisum0lem2a  20666  dchrisum0lem2  20667  dchrmusumlem  20671  dchrvmasumlem  20672  rplogsum  20676  mudivsum  20679  mulogsumlem  20680  mulogsum  20681  mulog2sumlem1  20683  mulog2sumlem2  20684  mulog2sumlem3  20685  vmalogdivsum  20688  logsqvma  20691  log2sumbnd  20693  selberglem1  20694  selberglem2  20695  selberglem3  20696  selberg  20697  selberg2lem  20699  selberg2  20700  selberg3lem1  20706  selberg3  20708  selberg4lem1  20709  selberg4  20710  pntrsumo1  20714  selbergr  20717  selberg3r  20718  selberg4r  20719  selberg34r  20720  pntsval2  20725  pntrlog2bndlem1  20726  pntrlog2bndlem2  20727  pntrlog2bndlem3  20728  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  pntrlog2bndlem6  20732  pntrlog2bnd  20733  pntlemb  20746  pntlemf  20754  pntlemo  20756  ostth2lem2  20783  ostth2lem3  20784  ipval2  21280  dipcl  21288  riesz3i  22642  cnre2csqima  23295  rmulccn  23301  dya2iocseg  23579  indsum  23606  subfacval2  23718  subfaclim  23719  rescon  23777  subdivcomb1  24090  subdivcomb2  24091  brbtwn2  24533  colinearalg  24538  ax5seglem2  24557  ax5seglem9  24565  axeuclidlem  24590  axcontlem2  24593  axcontlem4  24595  axcontlem7  24598  axcontlem8  24599  bpolycl  24787  bpolysum  24788  bpolydiflem  24789  bpoly4  24794  dvreasin  24923  areacirclem2  24925  areacirclem5  24929  areacirc  24931  rdr  26435  cntotbnd  26520  pellexlem1  26914  pellexlem2  26915  pellexlem6  26919  pell1234qrne0  26938  pell1234qrreccl  26939  pell1234qrmulcl  26940  pell1234qrdich  26946  pell14qrdich  26954  pell1qrge1  26955  pell1qrgaplem  26958  qirropth  26993  rmxyneg  27005  rmxyadd  27006  rmxm1  27019  rmym1  27020  rmxluc  27021  rmyluc  27022  rmxdbl  27024  rmydbl  27025  jm2.18  27081  jm2.19lem1  27082  jm2.19lem2  27083  jm2.19lem4  27085  jm2.19  27086  jm2.22  27088  jm2.23  27089  jm2.25  27092  jm2.27c  27100  jm3.1lem2  27111  flcidc  27379  expgrowth  27552  mulc1cncfg  27721  clim1fr1  27727  dvsinexp  27740  itgsinexplem1  27748  itgsinexp  27749  wallispilem4  27817  wallispilem5  27818  wallispi  27819  wallispi2lem1  27820  wallispi2lem2  27821  wallispi2  27822  stirlinglem1  27823  stirlinglem3  27825  stirlinglem4  27826  stirlinglem5  27827  stirlinglem6  27828  stirlinglem7  27829  stirlinglem8  27830  stirlinglem10  27832  stirlinglem11  27833  stirlinglem12  27834  stirlinglem13  27835  stirlinglem14  27836  stirlinglem15  27837  sigarim  27841  sigarac  27842  sigaraf  27843  sigarmf  27844  sigarls  27847  sigardiv  27851  sigarcol  27854  cevathlem1  27857
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulcl 8799
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator