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

Theorem mulcld 9507
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 9467 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  ( A  x.  B
)  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758  (class class class)co 6190   CCcc 9381    x. cmul 9388
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 9445
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  mul02lem1  9646  addid1  9650  cnegex  9651  receu  10082  divrec  10111  divcan3  10119  divdivdiv  10133  divsubdiv  10148  cru  10415  lincmb01cmp  11529  iccf1o  11530  flpmodeq  11814  moddiffl  11820  modvalp1  11827  modcyc  11844  modadd1  11846  modmul1  11853  modaddmulmod  11866  mulexpz  12005  expmulz  12011  binom3  12086  bernneq  12091  remullem  12719  cjreim2  12752  absimle  12900  abstri  12920  sqreulem  12949  sqreu  12950  mulcn2  13175  reccn2  13176  o1rlimmul  13198  isummulc2  13331  fsummulc2  13353  fsumparts  13371  binomlem  13394  binom1dif  13398  incexclem  13401  incexc  13402  incexc2  13403  geomulcvg  13438  mertenslem1  13446  mertens  13448  efaddlem  13480  sinadd  13550  cosadd  13551  tanaddlem  13552  tanadd  13553  addsin  13556  sincossq  13562  sin2t  13563  dvds2ln  13665  oddm1even  13695  sadadd2lem2  13748  bezoutlem2  13825  bezoutlem3  13826  bezoutlem4  13827  phiprmpw  13953  pythagtriplem12  13995  pythagtriplem14  13997  pythagtriplem16  13999  pcpremul  14012  pcaddlem  14052  fldivp1  14061  mul4sqlem  14116  4sqlem14  14121  vdwapun  14137  vdwlem2  14145  vdwlem6  14149  zringlpirlem3  18014  zlpirlem3  18019  znunit  18105  blcvx  20491  icopnfcnv  20630  mbfmulc2re  21242  mbfmulc2  21257  itg1addlem4  21293  itg1addlem5  21294  itg1mulc  21298  mbfmul  21320  itgcl  21377  itgcnlem  21383  iblmulc2  21424  itgmulc2  21427  itgabs  21428  itgsplit  21429  dvmulbr  21529  dvcmul  21534  dvcmulf  21535  dvexp  21543  dvmptcmul  21554  dvexp3  21566  dvsincos  21569  cmvth  21579  dvlipcn  21582  dvfsumabs  21611  dvfsumlem1  21614  ftc1lem4  21627  itgparts  21635  plyf  21782  ply1termlem  21787  plyeq0lem  21794  plypf1  21796  plyaddlem1  21797  plymullem1  21798  coeeulem  21808  coeidlem  21821  coeid3  21824  plyco  21825  coemullem  21833  coemulhi  21837  coemulc  21838  dgrcolem2  21857  plycjlem  21859  plyrecj  21862  dvply1  21866  vieta1lem2  21893  vieta1  21894  elqaalem3  21903  aareccl  21908  aalioulem1  21914  taylfvallem1  21938  tayl0  21943  dvtaylp  21951  taylthlem2  21955  psergf  21993  radcnvlem1  21994  dvradcnv  22002  psercn2  22004  pserdvlem2  22009  pserdv2  22011  abelthlem4  22015  abelthlem5  22016  abelthlem6  22017  abelthlem7  22019  abelthlem9  22021  tanregt0  22111  cosargd  22173  abslogle  22183  tanarg  22184  advlogexp  22216  logtayllem  22220  logtayl  22221  cxpadd  22240  mulcxp  22246  cxpmul  22249  cxpmul2  22250  cxpmul2z  22252  abscxp  22253  abscxp2  22254  dvcxp2  22297  abscxpbnd  22307  root1eq1  22309  cxpeq  22311  angcan  22314  pythag  22329  ssscongptld  22336  affineequiv  22337  affineequiv2  22338  chordthmlem2  22344  chordthmlem3  22345  chordthmlem4  22346  chordthmlem5  22347  heron  22349  quad2  22350  quad  22351  dcubic1lem  22354  dcubic2  22355  dcubic1  22356  dcubic  22357  mcubic  22358  cubic2  22359  cubic  22360  binom4  22361  dquartlem1  22362  dquartlem2  22363  dquart  22364  quart1cl  22365  quart1lem  22366  quart1  22367  quartlem1  22368  quartlem2  22369  atantayl3  22450  leibpi  22453  birthdaylem2  22462  divsqrsumo1  22493  cvxcl  22494  jensenlem2  22497  wilthlem2  22523  ftalem1  22526  ftalem2  22527  ftalem4  22529  ftalem5  22530  basellem2  22535  basellem3  22536  basellem8  22541  muinv  22649  fsumdvdsmul  22651  logfacrlim  22679  logexprlim  22680  perfectlem2  22685  bposlem9  22747  lgsquad2lem1  22813  2sqlem3  22821  rplogsumlem1  22849  dchrisumlem2  22855  dchrisumlem3  22856  dchrmusum2  22859  dchrvmasumlem1  22860  dchrvmasum2lem  22861  dchrvmasum2if  22862  dchrvmasumlem3  22864  dchrvmasumiflem1  22866  dchrvmasumiflem2  22867  rpvmasum2  22877  dchrisum0lem1  22881  dchrisum0lem2a  22882  dchrisum0lem2  22883  dchrmusumlem  22887  dchrvmasumlem  22888  rplogsum  22892  mudivsum  22895  mulogsumlem  22896  mulogsum  22897  mulog2sumlem1  22899  mulog2sumlem2  22900  mulog2sumlem3  22901  vmalogdivsum  22904  logsqvma  22907  log2sumbnd  22909  selberglem1  22910  selberglem2  22911  selberglem3  22912  selberg  22913  selberg2lem  22915  selberg2  22916  selberg3lem1  22922  selberg3  22924  selberg4lem1  22925  selberg4  22926  pntrsumo1  22930  selbergr  22933  selberg3r  22934  selberg4r  22935  selberg34r  22936  pntsval2  22941  pntrlog2bndlem1  22942  pntrlog2bndlem2  22943  pntrlog2bndlem3  22944  pntrlog2bndlem4  22945  pntrlog2bndlem5  22946  pntrlog2bndlem6  22948  pntrlog2bnd  22949  pntlemb  22962  pntlemf  22970  pntlemo  22972  ostth2lem2  22999  ostth2lem3  23000  ttgcontlem1  23266  brbtwn2  23286  colinearalg  23291  ax5seglem2  23310  ax5seglem9  23318  axeuclidlem  23343  axcontlem2  23346  axcontlem4  23348  axcontlem7  23351  axcontlem8  23352  ipval2  24237  dipcl  24245  riesz3i  25601  mul2lt0rlt0  26172  cnre2csqima  26475  rmulccn  26492  indsum  26613  dya2icoseg  26826  oddpwdc  26871  eulerpartlems  26877  eulerpartlemsv3  26878  eulerpartlemgs2  26897  signsplypnf  27085  lgamgulmlem2  27150  lgamgulmlem3  27151  lgamgulmlem4  27152  lgamgulmlem5  27153  lgamgulmlem6  27154  lgamgulm2  27156  lgamcvg2  27175  gamcvg  27176  gamcvg2lem  27179  subfacval2  27209  subfaclim  27210  rescon  27269  subdivcomb1  27518  subdivcomb2  27519  fprodmul  27605  iprodmul  27637  iprodgam  27640  binomfallfaclem1  27676  binomfallfaclem2  27677  binomrisefac  27679  bpolycl  28329  bpolysum  28330  bpolydiflem  28331  bpoly4  28336  iblmulc2nc  28595  itgmulc2nc  28598  itgabsnc  28599  ftc1cnnclem  28603  ftc1anclem3  28607  dvasin  28618  areacirclem1  28622  areacirclem4  28625  areacirc  28627  cntotbnd  28833  pellexlem1  29308  pellexlem2  29309  pellexlem6  29313  pell1234qrne0  29332  pell1234qrreccl  29333  pell1234qrmulcl  29334  pell1234qrdich  29340  pell14qrdich  29348  pell1qrge1  29349  pell1qrgaplem  29352  qirropth  29387  rmxyneg  29399  rmxyadd  29400  rmxm1  29413  rmym1  29414  rmxluc  29415  rmyluc  29416  rmxdbl  29418  rmydbl  29419  jm2.18  29475  jm2.19lem1  29476  jm2.19lem2  29477  jm2.19lem4  29479  jm2.19  29480  jm2.22  29482  jm2.23  29483  jm2.25  29486  jm2.27c  29494  jm3.1lem2  29505  flcidc  29669  itgpowd  29728  areaquad  29730  expgrowth  29747  mulc1cncfg  29908  clim1fr1  29912  dvsinexp  29925  itgsinexplem1  29932  itgsinexp  29933  stoweidlem1  29934  stoweidlem11  29944  stoweidlem13  29946  stoweidlem14  29947  stoweidlem17  29950  stoweidlem25  29958  stoweidlem26  29959  stoweidlem42  29975  wallispilem4  30001  wallispilem5  30002  wallispi  30003  wallispi2lem1  30004  wallispi2lem2  30005  wallispi2  30006  stirlinglem1  30007  stirlinglem3  30009  stirlinglem4  30010  stirlinglem5  30011  stirlinglem6  30012  stirlinglem7  30013  stirlinglem8  30014  stirlinglem10  30016  stirlinglem11  30017  stirlinglem12  30018  stirlinglem13  30019  stirlinglem14  30020  stirlinglem15  30021  sigarim  30025  sigarac  30026  sigaraf  30027  sigarmf  30028  sigarls  30031  sigardiv  30035  sigarcol  30038  cevathlem1  30041  kcnktkm1cn  30308  altgsumbcALT  30888  i2linesd  31431  sineq0ALT  31973  bj-subcom  32896  bj-lineq  32903  bj-bary1lem  32905  bj-bary1lem1  32906  bj-bary1  32907
  Copyright terms: Public domain W3C validator