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

Theorem mulcld 9688
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 9648 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
41, 2, 3syl2anc 671 1  |-  ( ph  ->  ( A  x.  B
)  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1897  (class class class)co 6314   CCcc 9562    x. cmul 9569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 9626
This theorem depends on definitions:  df-bi 190  df-an 377
This theorem is referenced by:  mul02lem1  9834  addid1  9838  cnegex  9839  kcnktkm1cn  10077  receu  10284  divrec  10313  divcan3  10321  divdivdiv  10335  divsubdiv  10350  cru  10628  mul2lt0rlt0  11426  lincmb01cmp  11803  iccf1o  11804  flpmodeq  12132  moddiffl  12139  modvalp1  12146  modcyc  12163  modadd1  12165  modmul1  12174  modaddmulmod  12187  mulexpz  12343  expmulz  12349  binom3  12424  bernneq  12429  remullem  13239  cjreim2  13272  absimle  13420  abstri  13441  sqreulem  13470  sqreu  13471  mulcn2  13707  reccn2  13708  o1rlimmul  13730  isummulc2  13871  fsummulc2  13893  fsumparts  13914  binomlem  13935  binom1dif  13939  incexclem  13942  incexc  13943  incexc2  13944  geomulcvg  13980  mertenslem1  13988  mertens  13990  fprodmul  14062  fprodn0f  14093  iprodmul  14104  binomfallfaclem1  14140  binomfallfaclem2  14141  binomrisefac  14143  bpolycl  14153  bpolysum  14154  bpolydiflem  14155  bpoly4  14160  efaddlem  14195  sinadd  14266  cosadd  14267  tanaddlem  14268  tanadd  14269  addsin  14272  sincossq  14278  sin2t  14279  dvds2ln  14381  oddm1even  14414  sadadd2lem2  14472  bezoutlem2OLD  14552  bezoutlem3OLD  14553  bezoutlem4OLD  14554  bezoutlem2  14555  bezoutlem3  14556  bezoutlem4  14557  lcmgcdlem  14619  phiprmpw  14772  pythagtriplem12  14824  pythagtriplem14  14826  pythagtriplem16  14828  pcpremul  14841  pcaddlem  14881  fldivp1  14890  mul4sqlem  14945  4sqlem14OLD  14950  4sqlem14  14956  vdwapun  14972  vdwlem2  14980  vdwlem6  14984  zringlpirlem3OLD  19103  zringlpirlem3  19105  znunit  19182  blcvx  21864  icopnfcnv  22018  mbfmulc2re  22652  mbfmulc2  22667  itg1addlem4  22705  itg1addlem5  22706  itg1mulc  22710  mbfmul  22732  itgcl  22789  itgcnlem  22795  iblmulc2  22836  itgmulc2  22839  itgabs  22840  itgsplit  22841  dvmulbr  22941  dvcmul  22946  dvcmulf  22947  dvexp  22955  dvmptcmul  22966  dvexp3  22978  dvsincos  22981  cmvth  22991  dvlipcn  22994  dvfsumabs  23023  dvfsumlem1  23026  ftc1lem4  23039  itgparts  23047  plyf  23200  ply1termlem  23205  plyeq0lem  23212  plypf1  23214  plyaddlem1  23215  plymullem1  23216  coeeulem  23226  coeidlem  23239  coeid3  23242  plyco  23243  coemullem  23252  coemulhi  23256  coemulc  23257  dgrcolem2  23276  plycjlem  23278  plyrecj  23281  dvply1  23285  vieta1lem2  23312  vieta1  23313  elqaalem3  23322  elqaalem3OLD  23325  aareccl  23330  aalioulem1  23336  taylfvallem1  23360  tayl0  23365  dvtaylp  23373  taylthlem2  23377  psergf  23415  radcnvlem1  23416  dvradcnv  23424  psercn2  23426  pserdvlem2  23431  pserdv2  23433  abelthlem4  23437  abelthlem5  23438  abelthlem6  23439  abelthlem7  23441  abelthlem9  23443  tanregt0  23536  efgh  23538  efabl  23547  efsubm  23548  cosargd  23605  abslogle  23615  tanarg  23616  advlogexp  23648  logtayllem  23652  logtayl  23653  cxpadd  23672  mulcxp  23678  cxpmul  23681  cxpmul2  23682  cxpmul2z  23684  abscxp  23685  abscxp2  23686  dvcxp2  23729  abscxpbnd  23741  root1eq1  23743  cxpeq  23745  angcan  23779  pythag  23794  ssscongptld  23799  affineequiv  23800  affineequiv2  23801  chordthmlem2  23807  chordthmlem3  23808  chordthmlem4  23809  chordthmlem5  23810  heron  23812  quad2  23813  quad  23814  dcubic1lem  23817  dcubic2  23818  dcubic1  23819  dcubic  23820  mcubic  23821  cubic2  23822  cubic  23823  binom4  23824  dquartlem1  23825  dquartlem2  23826  dquart  23827  quart1cl  23828  quart1lem  23829  quart1  23830  quartlem1  23831  quartlem2  23832  atantayl3  23913  leibpi  23916  birthdaylem2  23926  divsqrtsumo1  23957  cvxcl  23958  jensenlem2  23961  lgamgulmlem2  24003  lgamgulmlem3  24004  lgamgulmlem4  24005  lgamgulmlem5  24006  lgamgulmlem6  24007  lgamgulm2  24009  lgamcvg2  24028  gamcvg  24029  gamcvg2lem  24032  wilthlem2  24042  ftalem1  24045  ftalem2  24046  ftalem4  24048  ftalem5  24049  ftalem4OLD  24050  ftalem5OLD  24051  basellem2  24056  basellem3  24057  basellem8  24062  muinv  24170  fsumdvdsmul  24172  logfacrlim  24200  logexprlim  24201  perfectlem2  24206  bposlem9  24268  lgsquad2lem1  24334  2sqlem3  24342  rplogsumlem1  24370  dchrisumlem2  24376  dchrisumlem3  24377  dchrmusum2  24380  dchrvmasumlem1  24381  dchrvmasum2lem  24382  dchrvmasum2if  24383  dchrvmasumlem3  24385  dchrvmasumiflem1  24387  dchrvmasumiflem2  24388  rpvmasum2  24398  dchrisum0lem1  24402  dchrisum0lem2a  24403  dchrisum0lem2  24404  dchrmusumlem  24408  dchrvmasumlem  24409  rplogsum  24413  mudivsum  24416  mulogsumlem  24417  mulogsum  24418  mulog2sumlem1  24420  mulog2sumlem2  24421  mulog2sumlem3  24422  vmalogdivsum  24425  logsqvma  24428  log2sumbnd  24430  selberglem1  24431  selberglem2  24432  selberglem3  24433  selberg  24434  selberg2lem  24436  selberg2  24437  selberg3lem1  24443  selberg3  24445  selberg4lem1  24446  selberg4  24447  pntrsumo1  24451  selbergr  24454  selberg3r  24455  selberg4r  24456  selberg34r  24457  pntsval2  24462  pntrlog2bndlem1  24463  pntrlog2bndlem2  24464  pntrlog2bndlem3  24465  pntrlog2bndlem4  24466  pntrlog2bndlem5  24467  pntrlog2bndlem6  24469  pntrlog2bnd  24470  pntlemb  24483  pntlemf  24491  pntlemo  24493  ostth2lem2  24520  ostth2lem3  24521  ttgcontlem1  24963  brbtwn2  24983  colinearalg  24988  ax5seglem2  25007  ax5seglem9  25015  axeuclidlem  25040  axcontlem2  25043  axcontlem4  25045  axcontlem7  25048  axcontlem8  25049  ex-ind-dvds  25947  ipval2  26391  dipcl  26399  riesz3i  27763  bhmafibid1  28453  bhmafibid2  28454  2sqmod  28457  cnre2csqima  28765  rmulccn  28782  indsum  28892  dya2icoseg  29147  oddpwdc  29235  eulerpartlems  29241  eulerpartlemsv3  29242  eulerpartlemgs2  29261  signsplypnf  29487  subfacval2  29958  subfaclim  29959  rescon  30017  subdivcomb1  30408  subdivcomb2  30409  iprodgam  30426  fwddifnp1  30980  bj-subcom  31753  bj-lineq  31757  bj-bary1lem  31759  bj-bary1lem1  31760  bj-bary1  31761  iblmulc2nc  32051  itgmulc2nc  32054  itgabsnc  32055  ftc1cnnclem  32059  ftc1anclem3  32063  dvasin  32072  areacirclem1  32076  areacirclem4  32079  areacirc  32081  cntotbnd  32172  pellexlem1  35717  pellexlem2  35718  pellexlem6  35722  pell1234qrne0  35743  pell1234qrreccl  35744  pell1234qrmulcl  35745  pell1234qrdich  35751  pell14qrdich  35759  pell1qrge1  35760  pell1qrgaplem  35763  qirropth  35800  rmxyneg  35812  rmxyadd  35813  rmxm1  35826  rmym1  35827  rmxluc  35828  rmyluc  35829  rmxdbl  35831  rmydbl  35832  jm2.18  35887  jm2.19lem1  35888  jm2.19lem2  35889  jm2.19lem4  35891  jm2.19  35892  jm2.22  35894  jm2.23  35895  jm2.25  35898  jm2.27c  35906  jm3.1lem2  35917  flcidc  36084  itgpowd  36143  areaquad  36145  inductionexd  36637  imo72b2lem0  36652  int-leftdistd  36669  radcnvrat  36706  expgrowth  36727  binomcxplemwb  36740  binomcxplemnn0  36741  binomcxplemfrat  36743  binomcxplemdvbinom  36745  binomcxplemnotnn0  36748  sineq0ALT  37373  mul13d  37526  fperiodmullem  37558  fperiodmul  37559  divcan8d  37569  dmmcand  37571  mulc1cncfg  37704  mccllem  37714  clim1fr1  37716  mullimc  37733  mullimcf  37740  sumnnodd  37747  reclimc  37771  sinmulcos  37777  coskpi2  37778  cosknegpi  37781  dvsinexp  37817  dvmptdiv  37826  dvasinbx  37829  dvdivf  37831  dvdivbd  37832  dvdivcncf  37836  dvbdfbdioolem2  37838  dvxpaek  37852  dvnxpaek  37854  dvnmul  37855  dvmptfprodlem  37856  dvnprodlem2  37859  itgsinexplem1  37867  itgsinexp  37868  itgcoscmulx  37883  itgsincmulx  37888  itgiccshift  37894  itgperiod  37895  stoweidlem1  37898  stoweidlem11  37908  stoweidlem13  37910  stoweidlem14  37911  stoweidlem17  37914  stoweidlem25  37922  stoweidlem26  37923  stoweidlem42  37940  wallispilem4  37967  wallispilem5  37968  wallispi  37969  wallispi2lem1  37970  wallispi2lem2  37971  wallispi2  37972  stirlinglem1  37973  stirlinglem3  37975  stirlinglem4  37976  stirlinglem5  37977  stirlinglem6  37978  stirlinglem7  37979  stirlinglem8  37980  stirlinglem10  37982  stirlinglem11  37983  stirlinglem12  37984  stirlinglem13  37985  stirlinglem14  37986  stirlinglem15  37987  dirker2re  37991  dirkerdenne0  37992  dirkerper  37995  dirkertrigeqlem1  37997  dirkertrigeqlem2  37998  dirkertrigeqlem3  37999  dirkertrigeq  38000  dirkeritg  38001  dirkercncflem2  38003  dirkercncflem4  38005  fourierdlem26  38032  fourierdlem30  38036  fourierdlem39  38046  fourierdlem42  38049  fourierdlem42OLD  38050  fourierdlem47  38054  fourierdlem48  38055  fourierdlem56  38063  fourierdlem57  38064  fourierdlem58  38065  fourierdlem62  38069  fourierdlem65  38072  fourierdlem66  38073  fourierdlem68  38075  fourierdlem72  38079  fourierdlem73  38080  fourierdlem76  38083  fourierdlem80  38087  fourierdlem83  38090  fourierdlem85  38092  fourierdlem89  38096  fourierdlem90  38097  fourierdlem91  38098  fourierdlem95  38102  fourierdlem97  38104  fourierdlem101  38108  fourierdlem103  38110  fourierdlem104  38111  fourierdlem111  38118  sqwvfoura  38129  sqwvfourb  38130  fourierswlem  38131  fouriersw  38132  elaa2lem  38134  elaa2lemOLD  38135  etransclem8  38144  etransclem18  38154  etransclem20  38156  etransclem21  38157  etransclem23  38159  etransclem24  38160  etransclem31  38167  etransclem33  38169  etransclem35  38171  etransclem45  38181  etransclem46  38182  etransclem47  38183  etransclem48OLD  38184  etransclem48  38185  hoicvrrex  38415  hoidmvlelem2  38455  sigarim  38497  sigarac  38498  sigaraf  38499  sigarmf  38500  sigarls  38503  sigardiv  38507  sigarcol  38510  cevathlem1  38513  deccarry  38752  opeoALTV  38850  perfectALTVlem2  38881  0nodd  40082  2nodd  40084  2zlidl  40206  2zrngnmlid  40221  altgsumbcALT  40406  fldivmod  40593  nn0sumshdiglemA  40702  nn0sumshdiglemB  40703  nn0sumshdiglem2  40705  nn0mullong  40708  i2linesd  40790  aacllem  40812
  Copyright terms: Public domain W3C validator