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

Theorem mulcld 9662
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 9622 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
41, 2, 3syl2anc 665 1  |-  ( ph  ->  ( A  x.  B
)  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870  (class class class)co 6305   CCcc 9536    x. cmul 9543
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 9600
This theorem depends on definitions:  df-bi 188  df-an 372
This theorem is referenced by:  mul02lem1  9808  addid1  9812  cnegex  9813  kcnktkm1cn  10049  receu  10256  divrec  10285  divcan3  10293  divdivdiv  10307  divsubdiv  10322  cru  10601  mul2lt0rlt0  11398  lincmb01cmp  11773  iccf1o  11774  flpmodeq  12098  moddiffl  12105  modvalp1  12112  modcyc  12129  modadd1  12131  modmul1  12140  modaddmulmod  12153  mulexpz  12309  expmulz  12315  binom3  12390  bernneq  12395  remullem  13170  cjreim2  13203  absimle  13351  abstri  13372  sqreulem  13401  sqreu  13402  mulcn2  13637  reccn2  13638  o1rlimmul  13660  isummulc2  13801  fsummulc2  13823  fsumparts  13844  binomlem  13865  binom1dif  13869  incexclem  13872  incexc  13873  incexc2  13874  geomulcvg  13910  mertenslem1  13918  mertens  13920  fprodmul  13992  fprodn0f  14023  iprodmul  14034  binomfallfaclem1  14070  binomfallfaclem2  14071  binomrisefac  14073  bpolycl  14083  bpolysum  14084  bpolydiflem  14085  bpoly4  14090  efaddlem  14125  sinadd  14196  cosadd  14197  tanaddlem  14198  tanadd  14199  addsin  14202  sincossq  14208  sin2t  14209  dvds2ln  14311  oddm1even  14344  sadadd2lem2  14398  bezoutlem2  14478  bezoutlem3  14479  bezoutlem4  14480  lcmgcdlem  14536  phiprmpw  14684  pythagtriplem12  14730  pythagtriplem14  14732  pythagtriplem16  14734  pcpremul  14747  pcaddlem  14787  fldivp1  14796  mul4sqlem  14851  4sqlem14OLD  14856  4sqlem14  14862  vdwapun  14878  vdwlem2  14886  vdwlem6  14890  zringlpirlem3  18980  znunit  19056  blcvx  21718  icopnfcnv  21857  mbfmulc2re  22472  mbfmulc2  22487  itg1addlem4  22525  itg1addlem5  22526  itg1mulc  22530  mbfmul  22552  itgcl  22609  itgcnlem  22615  iblmulc2  22656  itgmulc2  22659  itgabs  22660  itgsplit  22661  dvmulbr  22761  dvcmul  22766  dvcmulf  22767  dvexp  22775  dvmptcmul  22786  dvexp3  22798  dvsincos  22801  cmvth  22811  dvlipcn  22814  dvfsumabs  22843  dvfsumlem1  22846  ftc1lem4  22859  itgparts  22867  plyf  23011  ply1termlem  23016  plyeq0lem  23023  plypf1  23025  plyaddlem1  23026  plymullem1  23027  coeeulem  23037  coeidlem  23050  coeid3  23053  plyco  23054  coemullem  23063  coemulhi  23067  coemulc  23068  dgrcolem2  23087  plycjlem  23089  plyrecj  23092  dvply1  23096  vieta1lem2  23123  vieta1  23124  elqaalem3  23133  aareccl  23138  aalioulem1  23144  taylfvallem1  23168  tayl0  23173  dvtaylp  23181  taylthlem2  23185  psergf  23223  radcnvlem1  23224  dvradcnv  23232  psercn2  23234  pserdvlem2  23239  pserdv2  23241  abelthlem4  23245  abelthlem5  23246  abelthlem6  23247  abelthlem7  23249  abelthlem9  23251  tanregt0  23344  efgh  23346  efabl  23355  efsubm  23356  cosargd  23413  abslogle  23423  tanarg  23424  advlogexp  23456  logtayllem  23460  logtayl  23461  cxpadd  23480  mulcxp  23486  cxpmul  23489  cxpmul2  23490  cxpmul2z  23492  abscxp  23493  abscxp2  23494  dvcxp2  23537  abscxpbnd  23549  root1eq1  23551  cxpeq  23553  angcan  23587  pythag  23602  ssscongptld  23607  affineequiv  23608  affineequiv2  23609  chordthmlem2  23615  chordthmlem3  23616  chordthmlem4  23617  chordthmlem5  23618  heron  23620  quad2  23621  quad  23622  dcubic1lem  23625  dcubic2  23626  dcubic1  23627  dcubic  23628  mcubic  23629  cubic2  23630  cubic  23631  binom4  23632  dquartlem1  23633  dquartlem2  23634  dquart  23635  quart1cl  23636  quart1lem  23637  quart1  23638  quartlem1  23639  quartlem2  23640  atantayl3  23721  leibpi  23724  birthdaylem2  23734  divsqrtsumo1  23765  cvxcl  23766  jensenlem2  23769  lgamgulmlem2  23811  lgamgulmlem3  23812  lgamgulmlem4  23813  lgamgulmlem5  23814  lgamgulmlem6  23815  lgamgulm2  23817  lgamcvg2  23836  gamcvg  23837  gamcvg2lem  23840  wilthlem2  23850  ftalem1  23853  ftalem2  23854  ftalem4  23856  ftalem5  23857  basellem2  23862  basellem3  23863  basellem8  23868  muinv  23976  fsumdvdsmul  23978  logfacrlim  24006  logexprlim  24007  perfectlem2  24012  bposlem9  24074  lgsquad2lem1  24140  2sqlem3  24148  rplogsumlem1  24176  dchrisumlem2  24182  dchrisumlem3  24183  dchrmusum2  24186  dchrvmasumlem1  24187  dchrvmasum2lem  24188  dchrvmasum2if  24189  dchrvmasumlem3  24191  dchrvmasumiflem1  24193  dchrvmasumiflem2  24194  rpvmasum2  24204  dchrisum0lem1  24208  dchrisum0lem2a  24209  dchrisum0lem2  24210  dchrmusumlem  24214  dchrvmasumlem  24215  rplogsum  24219  mudivsum  24222  mulogsumlem  24223  mulogsum  24224  mulog2sumlem1  24226  mulog2sumlem2  24227  mulog2sumlem3  24228  vmalogdivsum  24231  logsqvma  24234  log2sumbnd  24236  selberglem1  24237  selberglem2  24238  selberglem3  24239  selberg  24240  selberg2lem  24242  selberg2  24243  selberg3lem1  24249  selberg3  24251  selberg4lem1  24252  selberg4  24253  pntrsumo1  24257  selbergr  24260  selberg3r  24261  selberg4r  24262  selberg34r  24263  pntsval2  24268  pntrlog2bndlem1  24269  pntrlog2bndlem2  24270  pntrlog2bndlem3  24271  pntrlog2bndlem4  24272  pntrlog2bndlem5  24273  pntrlog2bndlem6  24275  pntrlog2bnd  24276  pntlemb  24289  pntlemf  24297  pntlemo  24299  ostth2lem2  24326  ostth2lem3  24327  ttgcontlem1  24752  brbtwn2  24772  colinearalg  24777  ax5seglem2  24796  ax5seglem9  24804  axeuclidlem  24829  axcontlem2  24832  axcontlem4  24834  axcontlem7  24837  axcontlem8  24838  ex-ind-dvds  25735  ipval2  26179  dipcl  26187  riesz3i  27541  bhmafibid1  28234  bhmafibid2  28235  2sqmod  28238  cnre2csqima  28547  rmulccn  28564  indsum  28674  dya2icoseg  28929  oddpwdc  29004  eulerpartlems  29010  eulerpartlemsv3  29011  eulerpartlemgs2  29030  signsplypnf  29218  subfacval2  29689  subfaclim  29690  rescon  29748  subdivcomb1  30138  subdivcomb2  30139  iprodgam  30156  fwddifnp1  30708  bj-subcom  31445  bj-lineq  31449  bj-bary1lem  31451  bj-bary1lem1  31452  bj-bary1  31453  iblmulc2nc  31701  itgmulc2nc  31704  itgabsnc  31705  ftc1cnnclem  31709  ftc1anclem3  31713  dvasin  31722  areacirclem1  31726  areacirclem4  31729  areacirc  31731  cntotbnd  31822  pellexlem1  35373  pellexlem2  35374  pellexlem6  35378  pell1234qrne0  35397  pell1234qrreccl  35398  pell1234qrmulcl  35399  pell1234qrdich  35405  pell14qrdich  35413  pell1qrge1  35414  pell1qrgaplem  35417  qirropth  35452  rmxyneg  35464  rmxyadd  35465  rmxm1  35478  rmym1  35479  rmxluc  35480  rmyluc  35481  rmxdbl  35483  rmydbl  35484  jm2.18  35539  jm2.19lem1  35540  jm2.19lem2  35541  jm2.19lem4  35543  jm2.19  35544  jm2.22  35546  jm2.23  35547  jm2.25  35550  jm2.27c  35558  jm3.1lem2  35569  flcidc  35729  itgpowd  35788  areaquad  35790  inductionexd  36220  imo72b2lem0  36235  int-leftdistd  36253  radcnvrat  36290  expgrowth  36311  binomcxplemwb  36324  binomcxplemnn0  36325  binomcxplemfrat  36327  binomcxplemdvbinom  36329  binomcxplemnotnn0  36332  sineq0ALT  36964  mul13d  37088  fperiodmullem  37120  fperiodmul  37121  divcan8d  37131  dmmcand  37133  mulc1cncfg  37229  mccllem  37239  clim1fr1  37241  mullimc  37258  mullimcf  37265  sumnnodd  37272  reclimc  37296  sinmulcos  37302  coskpi2  37303  cosknegpi  37306  dvsinexp  37342  dvmptdiv  37351  dvasinbx  37354  dvdivf  37356  dvdivbd  37357  dvdivcncf  37361  dvbdfbdioolem2  37363  dvxpaek  37374  dvnxpaek  37376  dvnmul  37377  dvmptfprodlem  37378  dvnprodlem2  37381  itgsinexplem1  37389  itgsinexp  37390  itgcoscmulx  37405  itgsincmulx  37410  itgiccshift  37416  itgperiod  37417  stoweidlem1  37420  stoweidlem11  37430  stoweidlem13  37432  stoweidlem14  37433  stoweidlem17  37436  stoweidlem25  37444  stoweidlem26  37445  stoweidlem42  37462  wallispilem4  37489  wallispilem5  37490  wallispi  37491  wallispi2lem1  37492  wallispi2lem2  37493  wallispi2  37494  stirlinglem1  37495  stirlinglem3  37497  stirlinglem4  37498  stirlinglem5  37499  stirlinglem6  37500  stirlinglem7  37501  stirlinglem8  37502  stirlinglem10  37504  stirlinglem11  37505  stirlinglem12  37506  stirlinglem13  37507  stirlinglem14  37508  stirlinglem15  37509  dirker2re  37513  dirkerdenne0  37514  dirkerper  37517  dirkertrigeqlem1  37519  dirkertrigeqlem2  37520  dirkertrigeqlem3  37521  dirkertrigeq  37522  dirkeritg  37523  dirkercncflem2  37525  dirkercncflem4  37527  fourierdlem26  37554  fourierdlem30  37558  fourierdlem39  37567  fourierdlem42  37570  fourierdlem47  37575  fourierdlem48  37576  fourierdlem56  37584  fourierdlem57  37585  fourierdlem58  37586  fourierdlem62  37590  fourierdlem65  37593  fourierdlem66  37594  fourierdlem68  37596  fourierdlem72  37600  fourierdlem73  37601  fourierdlem76  37604  fourierdlem80  37608  fourierdlem83  37611  fourierdlem85  37613  fourierdlem89  37617  fourierdlem90  37618  fourierdlem91  37619  fourierdlem95  37623  fourierdlem97  37625  fourierdlem101  37629  fourierdlem103  37631  fourierdlem104  37632  fourierdlem111  37639  sqwvfoura  37650  sqwvfourb  37651  fourierswlem  37652  fouriersw  37653  elaa2lem  37655  etransclem8  37664  etransclem18  37674  etransclem20  37676  etransclem21  37677  etransclem23  37679  etransclem24  37680  etransclem31  37687  etransclem33  37689  etransclem35  37691  etransclem45  37701  etransclem46  37702  etransclem47  37703  etransclem48  37704  sigarim  37850  sigarac  37851  sigaraf  37852  sigarmf  37853  sigarls  37856  sigardiv  37860  sigarcol  37863  cevathlem1  37866  deccarry  38095  opeoALTV  38193  perfectALTVlem2  38224  0nodd  38558  2nodd  38560  2zlidl  38682  2zrngnmlid  38697  altgsumbcALT  38884  fldivmod  39072  nn0sumshdiglemA  39181  nn0sumshdiglemB  39182  nn0sumshdiglem2  39184  nn0mullong  39187  i2linesd  39269  aacllem  39291
  Copyright terms: Public domain W3C validator