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

Theorem mulcld 9393
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 9353 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
41, 2, 3syl2anc 654 1  |-  ( ph  ->  ( A  x.  B
)  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755  (class class class)co 6080   CCcc 9267    x. cmul 9274
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 9331
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  mul02lem1  9532  addid1  9536  cnegex  9537  receu  9968  divrec  9997  divcan3  10005  divdivdiv  10019  divsubdiv  10034  cru  10301  lincmb01cmp  11414  iccf1o  11415  flpmodeq  11696  moddiffl  11702  modvalp1  11709  modcyc  11726  modadd1  11728  modmul1  11735  modaddmulmod  11748  mulexpz  11887  expmulz  11893  binom3  11968  bernneq  11973  remullem  12600  cjreim2  12633  absimle  12781  abstri  12801  sqreulem  12830  sqreu  12831  mulcn2  13056  reccn2  13057  o1rlimmul  13079  isummulc2  13212  fsummulc2  13233  fsumparts  13251  binomlem  13274  binom1dif  13278  incexclem  13281  incexc  13282  incexc2  13283  geomulcvg  13318  mertenslem1  13326  mertens  13328  efaddlem  13360  sinadd  13430  cosadd  13431  tanaddlem  13432  tanadd  13433  addsin  13436  sincossq  13442  sin2t  13443  dvds2ln  13545  oddm1even  13575  sadadd2lem2  13628  bezoutlem2  13705  bezoutlem3  13706  bezoutlem4  13707  phiprmpw  13833  pythagtriplem12  13875  pythagtriplem14  13877  pythagtriplem16  13879  pcpremul  13892  pcaddlem  13932  fldivp1  13941  mul4sqlem  13996  4sqlem14  14001  vdwapun  14017  vdwlem2  14025  vdwlem6  14029  zringlpirlem3  17746  zlpirlem3  17751  znunit  17837  blcvx  20216  icopnfcnv  20355  mbfmulc2re  20967  mbfmulc2  20982  itg1addlem4  21018  itg1addlem5  21019  itg1mulc  21023  mbfmul  21045  itgcl  21102  itgcnlem  21108  iblmulc2  21149  itgmulc2  21152  itgabs  21153  itgsplit  21154  dvmulbr  21254  dvcmul  21259  dvcmulf  21260  dvexp  21268  dvmptcmul  21279  dvexp3  21291  dvsincos  21294  cmvth  21304  dvlipcn  21307  dvfsumabs  21336  dvfsumlem1  21339  ftc1lem4  21352  itgparts  21360  plyf  21550  ply1termlem  21555  plyeq0lem  21562  plypf1  21564  plyaddlem1  21565  plymullem1  21566  coeeulem  21576  coeidlem  21589  coeid3  21592  plyco  21593  coemullem  21601  coemulhi  21605  coemulc  21606  dgrcolem2  21625  plycjlem  21627  plyrecj  21630  dvply1  21634  vieta1lem2  21661  vieta1  21662  elqaalem3  21671  aareccl  21676  aalioulem1  21682  taylfvallem1  21706  tayl0  21711  dvtaylp  21719  taylthlem2  21723  psergf  21761  radcnvlem1  21762  dvradcnv  21770  psercn2  21772  pserdvlem2  21777  pserdv2  21779  abelthlem4  21783  abelthlem5  21784  abelthlem6  21785  abelthlem7  21787  abelthlem9  21789  tanregt0  21879  cosargd  21941  abslogle  21951  tanarg  21952  advlogexp  21984  logtayllem  21988  logtayl  21989  cxpadd  22008  mulcxp  22014  cxpmul  22017  cxpmul2  22018  cxpmul2z  22020  abscxp  22021  abscxp2  22022  dvcxp2  22065  abscxpbnd  22075  root1eq1  22077  cxpeq  22079  angcan  22082  pythag  22097  ssscongptld  22104  affineequiv  22105  affineequiv2  22106  chordthmlem2  22112  chordthmlem3  22113  chordthmlem4  22114  chordthmlem5  22115  heron  22117  quad2  22118  quad  22119  dcubic1lem  22122  dcubic2  22123  dcubic1  22124  dcubic  22125  mcubic  22126  cubic2  22127  cubic  22128  binom4  22129  dquartlem1  22130  dquartlem2  22131  dquart  22132  quart1cl  22133  quart1lem  22134  quart1  22135  quartlem1  22136  quartlem2  22137  atantayl3  22218  leibpi  22221  birthdaylem2  22230  divsqrsumo1  22261  cvxcl  22262  jensenlem2  22265  wilthlem2  22291  ftalem1  22294  ftalem2  22295  ftalem4  22297  ftalem5  22298  basellem2  22303  basellem3  22304  basellem8  22309  muinv  22417  fsumdvdsmul  22419  logfacrlim  22447  logexprlim  22448  perfectlem2  22453  bposlem9  22515  lgsquad2lem1  22581  2sqlem3  22589  rplogsumlem1  22617  dchrisumlem2  22623  dchrisumlem3  22624  dchrmusum2  22627  dchrvmasumlem1  22628  dchrvmasum2lem  22629  dchrvmasum2if  22630  dchrvmasumlem3  22632  dchrvmasumiflem1  22634  dchrvmasumiflem2  22635  rpvmasum2  22645  dchrisum0lem1  22649  dchrisum0lem2a  22650  dchrisum0lem2  22651  dchrmusumlem  22655  dchrvmasumlem  22656  rplogsum  22660  mudivsum  22663  mulogsumlem  22664  mulogsum  22665  mulog2sumlem1  22667  mulog2sumlem2  22668  mulog2sumlem3  22669  vmalogdivsum  22672  logsqvma  22675  log2sumbnd  22677  selberglem1  22678  selberglem2  22679  selberglem3  22680  selberg  22681  selberg2lem  22683  selberg2  22684  selberg3lem1  22690  selberg3  22692  selberg4lem1  22693  selberg4  22694  pntrsumo1  22698  selbergr  22701  selberg3r  22702  selberg4r  22703  selberg34r  22704  pntsval2  22709  pntrlog2bndlem1  22710  pntrlog2bndlem2  22711  pntrlog2bndlem3  22712  pntrlog2bndlem4  22713  pntrlog2bndlem5  22714  pntrlog2bndlem6  22716  pntrlog2bnd  22717  pntlemb  22730  pntlemf  22738  pntlemo  22740  ostth2lem2  22767  ostth2lem3  22768  ttgcontlem1  22953  brbtwn2  22973  colinearalg  22978  ax5seglem2  22997  ax5seglem9  23005  axeuclidlem  23030  axcontlem2  23033  axcontlem4  23035  axcontlem7  23038  axcontlem8  23039  ipval2  23924  dipcl  23932  riesz3i  25288  mul2lt0rlt0  25862  cnre2csqima  26194  rmulccn  26211  indsum  26332  dya2icoseg  26545  oddpwdc  26584  eulerpartlems  26590  eulerpartlemsv3  26591  eulerpartlemgs2  26610  signsplypnf  26798  lgamgulmlem2  26863  lgamgulmlem3  26864  lgamgulmlem4  26865  lgamgulmlem5  26866  lgamgulmlem6  26867  lgamgulm2  26869  lgamcvg2  26888  gamcvg  26889  gamcvg2lem  26892  subfacval2  26922  subfaclim  26923  rescon  26982  subdivcomb1  27230  subdivcomb2  27231  fprodmul  27317  iprodmul  27349  iprodgam  27352  binomfallfaclem1  27388  binomfallfaclem2  27389  binomrisefac  27391  bpolycl  28041  bpolysum  28042  bpolydiflem  28043  bpoly4  28048  iblmulc2nc  28298  itgmulc2nc  28301  itgabsnc  28302  ftc1cnnclem  28306  ftc1anclem3  28310  dvasin  28321  areacirclem1  28325  areacirclem4  28328  areacirc  28330  cntotbnd  28536  pellexlem1  29012  pellexlem2  29013  pellexlem6  29017  pell1234qrne0  29036  pell1234qrreccl  29037  pell1234qrmulcl  29038  pell1234qrdich  29044  pell14qrdich  29052  pell1qrge1  29053  pell1qrgaplem  29056  qirropth  29091  rmxyneg  29103  rmxyadd  29104  rmxm1  29117  rmym1  29118  rmxluc  29119  rmyluc  29120  rmxdbl  29122  rmydbl  29123  jm2.18  29179  jm2.19lem1  29180  jm2.19lem2  29181  jm2.19lem4  29183  jm2.19  29184  jm2.22  29186  jm2.23  29187  jm2.25  29190  jm2.27c  29198  jm3.1lem2  29209  flcidc  29373  itgpowd  29432  areaquad  29434  expgrowth  29451  mulc1cncfg  29613  clim1fr1  29617  dvsinexp  29630  itgsinexplem1  29637  itgsinexp  29638  stoweidlem1  29639  stoweidlem11  29649  stoweidlem13  29651  stoweidlem14  29652  stoweidlem17  29655  stoweidlem25  29663  stoweidlem26  29664  stoweidlem42  29680  wallispilem4  29706  wallispilem5  29707  wallispi  29708  wallispi2lem1  29709  wallispi2lem2  29710  wallispi2  29711  stirlinglem1  29712  stirlinglem3  29714  stirlinglem4  29715  stirlinglem5  29716  stirlinglem6  29717  stirlinglem7  29718  stirlinglem8  29719  stirlinglem10  29721  stirlinglem11  29722  stirlinglem12  29723  stirlinglem13  29724  stirlinglem14  29725  stirlinglem15  29726  sigarim  29730  sigarac  29731  sigaraf  29732  sigarmf  29733  sigarls  29736  sigardiv  29740  sigarcol  29743  cevathlem1  29746  kcnktkm1cn  30013  i2linesd  30835  sineq0ALT  31372  bj-subcom  32162  bj-lineq  32169  bj-bary1lem  32171  bj-bary1lem1  32172  bj-bary1  32173
  Copyright terms: Public domain W3C validator