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

Theorem mulcld 9098
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 9064 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ( A  x.  B
)  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725  (class class class)co 6073   CCcc 8978    x. cmul 8985
This theorem is referenced by:  mul02lem1  9232  addid1  9236  cnegex  9237  receu  9657  divrec  9684  divcan3  9692  divdivdiv  9705  divsubdiv  9720  cru  9982  lincmb01cmp  11028  iccf1o  11029  moddiffl  11249  modcyc  11266  modadd1  11268  modmul1  11269  mulexpz  11410  expmulz  11416  binom3  11490  bernneq  11495  remullem  11923  cjreim2  11956  absimle  12104  abstri  12124  sqreulem  12153  sqreu  12154  mulcn2  12379  reccn2  12380  o1rlimmul  12402  isummulc2  12536  fsummulc2  12557  fsumparts  12575  binomlem  12598  binom1dif  12602  incexclem  12606  incexc  12607  incexc2  12608  geomulcvg  12643  mertenslem1  12651  mertens  12653  efaddlem  12685  sinadd  12755  cosadd  12756  tanaddlem  12757  tanadd  12758  addsin  12761  sincossq  12767  sin2t  12768  dvds2ln  12870  oddm1even  12899  sadadd2lem2  12952  bezoutlem2  13029  bezoutlem3  13030  bezoutlem4  13031  phiprmpw  13155  pythagtriplem12  13190  pythagtriplem14  13192  pythagtriplem16  13194  pcpremul  13207  pcaddlem  13247  fldivp1  13256  mul4sqlem  13311  4sqlem14  13316  vdwapun  13332  vdwlem2  13340  vdwlem6  13344  zlpirlem3  16760  znunit  16834  blcvx  18819  icopnfcnv  18957  mbfmulc2re  19530  mbfmulc2  19545  itg1addlem4  19581  itg1addlem5  19582  itg1mulc  19586  mbfmul  19608  itgcl  19665  itgcnlem  19671  iblmulc2  19712  itgmulc2  19715  itgabs  19716  itgsplit  19717  dvmulbr  19815  dvcmul  19820  dvcmulf  19821  dvexp  19829  dvmptcmul  19840  dvexp3  19852  dvsincos  19855  cmvth  19865  dvlipcn  19868  dvfsumabs  19897  dvfsumlem1  19900  ftc1lem4  19913  itgparts  19921  plyf  20107  ply1termlem  20112  plyeq0lem  20119  plypf1  20121  plyaddlem1  20122  plymullem1  20123  coeeulem  20133  coeidlem  20146  coeid3  20149  plyco  20150  coemullem  20158  coemulhi  20162  coemulc  20163  dgrcolem2  20182  plycjlem  20184  plyrecj  20187  dvply1  20191  vieta1lem2  20218  vieta1  20219  elqaalem3  20228  aareccl  20233  aalioulem1  20239  taylfvallem1  20263  tayl0  20268  dvtaylp  20276  taylthlem2  20280  psergf  20318  radcnvlem1  20319  dvradcnv  20327  psercn2  20329  pserdvlem2  20334  pserdv2  20336  abelthlem4  20340  abelthlem5  20341  abelthlem6  20342  abelthlem7  20344  abelthlem9  20346  tanregt0  20431  cosargd  20493  abslogle  20503  tanarg  20504  advlogexp  20536  logtayllem  20540  logtayl  20541  cxpadd  20560  mulcxp  20566  cxpmul  20569  cxpmul2  20570  cxpmul2z  20572  abscxp  20573  abscxp2  20574  dvcxp2  20617  abscxpbnd  20627  root1eq1  20629  cxpeq  20631  angcan  20634  pythag  20649  ssscongptld  20656  affineequiv  20657  affineequiv2  20658  chordthmlem2  20664  chordthmlem3  20665  chordthmlem4  20666  chordthmlem5  20667  quad2  20669  quad  20670  dcubic1lem  20673  dcubic2  20674  dcubic1  20675  dcubic  20676  mcubic  20677  cubic2  20678  cubic  20679  binom4  20680  dquartlem1  20681  dquartlem2  20682  dquart  20683  quart1cl  20684  quart1lem  20685  quart1  20686  quartlem1  20687  quartlem2  20688  atantayl3  20769  leibpi  20772  birthdaylem2  20781  divsqrsumo1  20812  cvxcl  20813  jensenlem2  20816  wilthlem2  20842  ftalem1  20845  ftalem2  20846  ftalem4  20848  ftalem5  20849  basellem2  20854  basellem3  20855  basellem8  20860  muinv  20968  fsumdvdsmul  20970  logfacrlim  20998  logexprlim  20999  perfectlem2  21004  bposlem9  21066  lgsquad2lem1  21132  2sqlem3  21140  rplogsumlem1  21168  dchrisumlem2  21174  dchrisumlem3  21175  dchrmusum2  21178  dchrvmasumlem1  21179  dchrvmasum2lem  21180  dchrvmasum2if  21181  dchrvmasumlem3  21183  dchrvmasumiflem1  21185  dchrvmasumiflem2  21186  rpvmasum2  21196  dchrisum0lem1  21200  dchrisum0lem2a  21201  dchrisum0lem2  21202  dchrmusumlem  21206  dchrvmasumlem  21207  rplogsum  21211  mudivsum  21214  mulogsumlem  21215  mulogsum  21216  mulog2sumlem1  21218  mulog2sumlem2  21219  mulog2sumlem3  21220  vmalogdivsum  21223  logsqvma  21226  log2sumbnd  21228  selberglem1  21229  selberglem2  21230  selberglem3  21231  selberg  21232  selberg2lem  21234  selberg2  21235  selberg3lem1  21241  selberg3  21243  selberg4lem1  21244  selberg4  21245  pntrsumo1  21249  selbergr  21252  selberg3r  21253  selberg4r  21254  selberg34r  21255  pntsval2  21260  pntrlog2bndlem1  21261  pntrlog2bndlem2  21262  pntrlog2bndlem3  21263  pntrlog2bndlem4  21264  pntrlog2bndlem5  21265  pntrlog2bndlem6  21267  pntrlog2bnd  21268  pntlemb  21281  pntlemf  21289  pntlemo  21291  ostth2lem2  21318  ostth2lem3  21319  ipval2  22193  dipcl  22201  riesz3i  23555  cnre2csqima  24299  rmulccn  24304  indsum  24410  dya2icoseg  24617  lgamgulmlem2  24804  lgamgulmlem3  24805  lgamgulmlem4  24806  lgamgulmlem5  24807  lgamgulmlem6  24808  lgamgulm2  24810  lgamcvg2  24829  gamcvg  24830  gamcvg2lem  24833  subfacval2  24863  subfaclim  24864  rescon  24923  subdivcomb1  25185  subdivcomb2  25186  fprodmul  25274  iprodmul  25306  iprodgam  25309  binomfallfaclem1  25345  binomfallfaclem2  25346  binomrisefac  25348  brbtwn2  25809  colinearalg  25814  ax5seglem2  25833  ax5seglem9  25841  axeuclidlem  25866  axcontlem2  25869  axcontlem4  25871  axcontlem7  25874  axcontlem8  25875  bpolycl  26063  bpolysum  26064  bpolydiflem  26065  bpoly4  26070  iblmulc2nc  26233  itgmulc2nc  26236  itgabsnc  26237  ftc1cnnclem  26241  dvreasin  26243  areacirclem2  26245  areacirclem5  26249  areacirc  26251  cntotbnd  26459  pellexlem1  26846  pellexlem2  26847  pellexlem6  26851  pell1234qrne0  26870  pell1234qrreccl  26871  pell1234qrmulcl  26872  pell1234qrdich  26878  pell14qrdich  26886  pell1qrge1  26887  pell1qrgaplem  26890  qirropth  26925  rmxyneg  26937  rmxyadd  26938  rmxm1  26951  rmym1  26952  rmxluc  26953  rmyluc  26954  rmxdbl  26956  rmydbl  26957  jm2.18  27013  jm2.19lem1  27014  jm2.19lem2  27015  jm2.19lem4  27017  jm2.19  27018  jm2.22  27020  jm2.23  27021  jm2.25  27024  jm2.27c  27032  jm3.1lem2  27043  flcidc  27311  expgrowth  27484  mulc1cncfg  27652  clim1fr1  27658  dvsinexp  27671  itgsinexplem1  27679  itgsinexp  27680  stoweidlem1  27681  stoweidlem11  27691  stoweidlem13  27693  stoweidlem14  27694  stoweidlem17  27697  stoweidlem25  27705  stoweidlem26  27706  stoweidlem42  27722  wallispilem4  27748  wallispilem5  27749  wallispi  27750  wallispi2lem1  27751  wallispi2lem2  27752  wallispi2  27753  stirlinglem1  27754  stirlinglem3  27756  stirlinglem4  27757  stirlinglem5  27758  stirlinglem6  27759  stirlinglem7  27760  stirlinglem8  27761  stirlinglem10  27763  stirlinglem11  27764  stirlinglem12  27765  stirlinglem13  27766  stirlinglem14  27767  stirlinglem15  27768  sigarim  27772  sigarac  27773  sigaraf  27774  sigarmf  27775  sigarls  27778  sigardiv  27782  sigarcol  27785  cevathlem1  27788  kcnktkm1cn  28038  flpmodeq  28092  modvalp1  28093  modaddmulmod  28100  sineq0ALT  28950
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulcl 9042
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator