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

Theorem mulcld 9064
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 9030 . 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 1721  (class class class)co 6040   CCcc 8944    x. cmul 8951
This theorem is referenced by:  mul02lem1  9198  addid1  9202  cnegex  9203  receu  9623  divrec  9650  divcan3  9658  divdivdiv  9671  divsubdiv  9686  cru  9948  lincmb01cmp  10994  iccf1o  10995  moddiffl  11214  modcyc  11231  modadd1  11233  modmul1  11234  mulexpz  11375  expmulz  11381  binom3  11455  bernneq  11460  remullem  11888  cjreim2  11921  absimle  12069  abstri  12089  sqreulem  12118  sqreu  12119  mulcn2  12344  reccn2  12345  o1rlimmul  12367  isummulc2  12501  fsummulc2  12522  fsumparts  12540  binomlem  12563  binom1dif  12567  incexclem  12571  incexc  12572  incexc2  12573  geomulcvg  12608  mertenslem1  12616  mertens  12618  efaddlem  12650  sinadd  12720  cosadd  12721  tanaddlem  12722  tanadd  12723  addsin  12726  sincossq  12732  sin2t  12733  dvds2ln  12835  oddm1even  12864  sadadd2lem2  12917  bezoutlem2  12994  bezoutlem3  12995  bezoutlem4  12996  phiprmpw  13120  pythagtriplem12  13155  pythagtriplem14  13157  pythagtriplem16  13159  pcpremul  13172  pcaddlem  13212  fldivp1  13221  mul4sqlem  13276  4sqlem14  13281  vdwapun  13297  vdwlem2  13305  vdwlem6  13309  zlpirlem3  16725  znunit  16799  blcvx  18782  icopnfcnv  18920  mbfmulc2re  19493  mbfmulc2  19508  itg1addlem4  19544  itg1addlem5  19545  itg1mulc  19549  mbfmul  19571  itgcl  19628  itgcnlem  19634  iblmulc2  19675  itgmulc2  19678  itgabs  19679  itgsplit  19680  dvmulbr  19778  dvcmul  19783  dvcmulf  19784  dvexp  19792  dvmptcmul  19803  dvexp3  19815  dvsincos  19818  cmvth  19828  dvlipcn  19831  dvfsumabs  19860  dvfsumlem1  19863  ftc1lem4  19876  itgparts  19884  plyf  20070  ply1termlem  20075  plyeq0lem  20082  plypf1  20084  plyaddlem1  20085  plymullem1  20086  coeeulem  20096  coeidlem  20109  coeid3  20112  plyco  20113  coemullem  20121  coemulhi  20125  coemulc  20126  dgrcolem2  20145  plycjlem  20147  plyrecj  20150  dvply1  20154  vieta1lem2  20181  vieta1  20182  elqaalem3  20191  aareccl  20196  aalioulem1  20202  taylfvallem1  20226  tayl0  20231  dvtaylp  20239  taylthlem2  20243  psergf  20281  radcnvlem1  20282  dvradcnv  20290  psercn2  20292  pserdvlem2  20297  pserdv2  20299  abelthlem4  20303  abelthlem5  20304  abelthlem6  20305  abelthlem7  20307  abelthlem9  20309  tanregt0  20394  cosargd  20456  abslogle  20466  tanarg  20467  advlogexp  20499  logtayllem  20503  logtayl  20504  cxpadd  20523  mulcxp  20529  cxpmul  20532  cxpmul2  20533  cxpmul2z  20535  abscxp  20536  abscxp2  20537  dvcxp2  20580  abscxpbnd  20590  root1eq1  20592  cxpeq  20594  angcan  20597  pythag  20612  ssscongptld  20619  affineequiv  20620  affineequiv2  20621  chordthmlem2  20627  chordthmlem3  20628  chordthmlem4  20629  chordthmlem5  20630  quad2  20632  quad  20633  dcubic1lem  20636  dcubic2  20637  dcubic1  20638  dcubic  20639  mcubic  20640  cubic2  20641  cubic  20642  binom4  20643  dquartlem1  20644  dquartlem2  20645  dquart  20646  quart1cl  20647  quart1lem  20648  quart1  20649  quartlem1  20650  quartlem2  20651  atantayl3  20732  leibpi  20735  birthdaylem2  20744  divsqrsumo1  20775  cvxcl  20776  jensenlem2  20779  wilthlem2  20805  ftalem1  20808  ftalem2  20809  ftalem4  20811  ftalem5  20812  basellem2  20817  basellem3  20818  basellem8  20823  muinv  20931  fsumdvdsmul  20933  logfacrlim  20961  logexprlim  20962  perfectlem2  20967  bposlem9  21029  lgsquad2lem1  21095  2sqlem3  21103  rplogsumlem1  21131  dchrisumlem2  21137  dchrisumlem3  21138  dchrmusum2  21141  dchrvmasumlem1  21142  dchrvmasum2lem  21143  dchrvmasum2if  21144  dchrvmasumlem3  21146  dchrvmasumiflem1  21148  dchrvmasumiflem2  21149  rpvmasum2  21159  dchrisum0lem1  21163  dchrisum0lem2a  21164  dchrisum0lem2  21165  dchrmusumlem  21169  dchrvmasumlem  21170  rplogsum  21174  mudivsum  21177  mulogsumlem  21178  mulogsum  21179  mulog2sumlem1  21181  mulog2sumlem2  21182  mulog2sumlem3  21183  vmalogdivsum  21186  logsqvma  21189  log2sumbnd  21191  selberglem1  21192  selberglem2  21193  selberglem3  21194  selberg  21195  selberg2lem  21197  selberg2  21198  selberg3lem1  21204  selberg3  21206  selberg4lem1  21207  selberg4  21208  pntrsumo1  21212  selbergr  21215  selberg3r  21216  selberg4r  21217  selberg34r  21218  pntsval2  21223  pntrlog2bndlem1  21224  pntrlog2bndlem2  21225  pntrlog2bndlem3  21226  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  pntrlog2bndlem6  21230  pntrlog2bnd  21231  pntlemb  21244  pntlemf  21252  pntlemo  21254  ostth2lem2  21281  ostth2lem3  21282  ipval2  22156  dipcl  22164  riesz3i  23518  cnre2csqima  24262  rmulccn  24267  indsum  24373  dya2icoseg  24580  lgamgulmlem2  24767  lgamgulmlem3  24768  lgamgulmlem4  24769  lgamgulmlem5  24770  lgamgulmlem6  24771  lgamgulm2  24773  lgamcvg2  24792  gamcvg  24793  gamcvg2lem  24796  subfacval2  24826  subfaclim  24827  rescon  24886  subdivcomb1  25148  subdivcomb2  25149  fprodmul  25237  iprodmul  25269  iprodgam  25272  binomfallfaclem1  25306  binomfallfaclem2  25307  binomrisefac  25309  brbtwn2  25748  colinearalg  25753  ax5seglem2  25772  ax5seglem9  25780  axeuclidlem  25805  axcontlem2  25808  axcontlem4  25810  axcontlem7  25813  axcontlem8  25814  bpolycl  26002  bpolysum  26003  bpolydiflem  26004  bpoly4  26009  iblmulc2nc  26169  itgmulc2nc  26172  itgabsnc  26173  ftc1cnnclem  26177  dvreasin  26179  areacirclem2  26181  areacirclem5  26185  areacirc  26187  cntotbnd  26395  pellexlem1  26782  pellexlem2  26783  pellexlem6  26787  pell1234qrne0  26806  pell1234qrreccl  26807  pell1234qrmulcl  26808  pell1234qrdich  26814  pell14qrdich  26822  pell1qrge1  26823  pell1qrgaplem  26826  qirropth  26861  rmxyneg  26873  rmxyadd  26874  rmxm1  26887  rmym1  26888  rmxluc  26889  rmyluc  26890  rmxdbl  26892  rmydbl  26893  jm2.18  26949  jm2.19lem1  26950  jm2.19lem2  26951  jm2.19lem4  26953  jm2.19  26954  jm2.22  26956  jm2.23  26957  jm2.25  26960  jm2.27c  26968  jm3.1lem2  26979  flcidc  27247  expgrowth  27420  mulc1cncfg  27588  clim1fr1  27594  dvsinexp  27607  itgsinexplem1  27615  itgsinexp  27616  stoweidlem1  27617  stoweidlem11  27627  stoweidlem13  27629  stoweidlem14  27630  stoweidlem17  27633  stoweidlem25  27641  stoweidlem26  27642  stoweidlem42  27658  wallispilem4  27684  wallispilem5  27685  wallispi  27686  wallispi2lem1  27687  wallispi2lem2  27688  wallispi2  27689  stirlinglem1  27690  stirlinglem3  27692  stirlinglem4  27693  stirlinglem5  27694  stirlinglem6  27695  stirlinglem7  27696  stirlinglem8  27697  stirlinglem10  27699  stirlinglem11  27700  stirlinglem12  27701  stirlinglem13  27702  stirlinglem14  27703  stirlinglem15  27704  sigarim  27708  sigarac  27709  sigaraf  27710  sigarmf  27711  sigarls  27714  sigardiv  27718  sigarcol  27721  cevathlem1  27724  kcnktkm1cn  27969
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulcl 9008
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator