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

Theorem mulcld 9605
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 9565 . 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 1762  (class class class)co 6275   CCcc 9479    x. cmul 9486
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 9543
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  mul02lem1  9744  addid1  9748  cnegex  9749  kcnktkm1cn  9977  receu  10183  divrec  10212  divcan3  10220  divdivdiv  10234  divsubdiv  10249  cru  10517  lincmb01cmp  11652  iccf1o  11653  flpmodeq  11957  moddiffl  11963  modvalp1  11970  modcyc  11987  modadd1  11989  modmul1  11996  modaddmulmod  12009  mulexpz  12161  expmulz  12167  binom3  12242  bernneq  12247  remullem  12911  cjreim2  12944  absimle  13092  abstri  13112  sqreulem  13141  sqreu  13142  mulcn2  13367  reccn2  13368  o1rlimmul  13390  isummulc2  13526  fsummulc2  13548  fsumparts  13569  binomlem  13593  binom1dif  13597  incexclem  13600  incexc  13601  incexc2  13602  geomulcvg  13637  mertenslem1  13645  mertens  13647  efaddlem  13679  sinadd  13749  cosadd  13750  tanaddlem  13751  tanadd  13752  addsin  13755  sincossq  13761  sin2t  13762  dvds2ln  13864  oddm1even  13895  sadadd2lem2  13948  bezoutlem2  14025  bezoutlem3  14026  bezoutlem4  14027  phiprmpw  14154  pythagtriplem12  14198  pythagtriplem14  14200  pythagtriplem16  14202  pcpremul  14215  pcaddlem  14255  fldivp1  14264  mul4sqlem  14319  4sqlem14  14324  vdwapun  14340  vdwlem2  14348  vdwlem6  14352  zringlpirlem3  18271  zlpirlem3  18276  znunit  18362  blcvx  21031  icopnfcnv  21170  mbfmulc2re  21783  mbfmulc2  21798  itg1addlem4  21834  itg1addlem5  21835  itg1mulc  21839  mbfmul  21861  itgcl  21918  itgcnlem  21924  iblmulc2  21965  itgmulc2  21968  itgabs  21969  itgsplit  21970  dvmulbr  22070  dvcmul  22075  dvcmulf  22076  dvexp  22084  dvmptcmul  22095  dvexp3  22107  dvsincos  22110  cmvth  22120  dvlipcn  22123  dvfsumabs  22152  dvfsumlem1  22155  ftc1lem4  22168  itgparts  22176  plyf  22323  ply1termlem  22328  plyeq0lem  22335  plypf1  22337  plyaddlem1  22338  plymullem1  22339  coeeulem  22349  coeidlem  22362  coeid3  22365  plyco  22366  coemullem  22374  coemulhi  22378  coemulc  22379  dgrcolem2  22398  plycjlem  22400  plyrecj  22403  dvply1  22407  vieta1lem2  22434  vieta1  22435  elqaalem3  22444  aareccl  22449  aalioulem1  22455  taylfvallem1  22479  tayl0  22484  dvtaylp  22492  taylthlem2  22496  psergf  22534  radcnvlem1  22535  dvradcnv  22543  psercn2  22545  pserdvlem2  22550  pserdv2  22552  abelthlem4  22556  abelthlem5  22557  abelthlem6  22558  abelthlem7  22560  abelthlem9  22562  tanregt0  22652  cosargd  22714  abslogle  22724  tanarg  22725  advlogexp  22757  logtayllem  22761  logtayl  22762  cxpadd  22781  mulcxp  22787  cxpmul  22790  cxpmul2  22791  cxpmul2z  22793  abscxp  22794  abscxp2  22795  dvcxp2  22838  abscxpbnd  22848  root1eq1  22850  cxpeq  22852  angcan  22855  pythag  22870  ssscongptld  22877  affineequiv  22878  affineequiv2  22879  chordthmlem2  22885  chordthmlem3  22886  chordthmlem4  22887  chordthmlem5  22888  heron  22890  quad2  22891  quad  22892  dcubic1lem  22895  dcubic2  22896  dcubic1  22897  dcubic  22898  mcubic  22899  cubic2  22900  cubic  22901  binom4  22902  dquartlem1  22903  dquartlem2  22904  dquart  22905  quart1cl  22906  quart1lem  22907  quart1  22908  quartlem1  22909  quartlem2  22910  atantayl3  22991  leibpi  22994  birthdaylem2  23003  divsqrsumo1  23034  cvxcl  23035  jensenlem2  23038  wilthlem2  23064  ftalem1  23067  ftalem2  23068  ftalem4  23070  ftalem5  23071  basellem2  23076  basellem3  23077  basellem8  23082  muinv  23190  fsumdvdsmul  23192  logfacrlim  23220  logexprlim  23221  perfectlem2  23226  bposlem9  23288  lgsquad2lem1  23354  2sqlem3  23362  rplogsumlem1  23390  dchrisumlem2  23396  dchrisumlem3  23397  dchrmusum2  23400  dchrvmasumlem1  23401  dchrvmasum2lem  23402  dchrvmasum2if  23403  dchrvmasumlem3  23405  dchrvmasumiflem1  23407  dchrvmasumiflem2  23408  rpvmasum2  23418  dchrisum0lem1  23422  dchrisum0lem2a  23423  dchrisum0lem2  23424  dchrmusumlem  23428  dchrvmasumlem  23429  rplogsum  23433  mudivsum  23436  mulogsumlem  23437  mulogsum  23438  mulog2sumlem1  23440  mulog2sumlem2  23441  mulog2sumlem3  23442  vmalogdivsum  23445  logsqvma  23448  log2sumbnd  23450  selberglem1  23451  selberglem2  23452  selberglem3  23453  selberg  23454  selberg2lem  23456  selberg2  23457  selberg3lem1  23463  selberg3  23465  selberg4lem1  23466  selberg4  23467  pntrsumo1  23471  selbergr  23474  selberg3r  23475  selberg4r  23476  selberg34r  23477  pntsval2  23482  pntrlog2bndlem1  23483  pntrlog2bndlem2  23484  pntrlog2bndlem3  23485  pntrlog2bndlem4  23486  pntrlog2bndlem5  23487  pntrlog2bndlem6  23489  pntrlog2bnd  23490  pntlemb  23503  pntlemf  23511  pntlemo  23513  ostth2lem2  23540  ostth2lem3  23541  ttgcontlem1  23857  brbtwn2  23877  colinearalg  23882  ax5seglem2  23901  ax5seglem9  23909  axeuclidlem  23934  axcontlem2  23937  axcontlem4  23939  axcontlem7  23942  axcontlem8  23943  ipval2  25143  dipcl  25151  riesz3i  26507  mul2lt0rlt0  27083  cnre2csqima  27379  rmulccn  27396  indsum  27526  dya2icoseg  27738  oddpwdc  27783  eulerpartlems  27789  eulerpartlemsv3  27790  eulerpartlemgs2  27809  signsplypnf  27997  lgamgulmlem2  28062  lgamgulmlem3  28063  lgamgulmlem4  28064  lgamgulmlem5  28065  lgamgulmlem6  28066  lgamgulm2  28068  lgamcvg2  28087  gamcvg  28088  gamcvg2lem  28091  subfacval2  28121  subfaclim  28122  rescon  28181  subdivcomb1  28430  subdivcomb2  28431  fprodmul  28517  iprodmul  28549  iprodgam  28552  binomfallfaclem1  28588  binomfallfaclem2  28589  binomrisefac  28591  bpolycl  29241  bpolysum  29242  bpolydiflem  29243  bpoly4  29248  iblmulc2nc  29508  itgmulc2nc  29511  itgabsnc  29512  ftc1cnnclem  29516  ftc1anclem3  29520  dvasin  29531  areacirclem1  29535  areacirclem4  29538  areacirc  29540  cntotbnd  29746  pellexlem1  30220  pellexlem2  30221  pellexlem6  30225  pell1234qrne0  30244  pell1234qrreccl  30245  pell1234qrmulcl  30246  pell1234qrdich  30252  pell14qrdich  30260  pell1qrge1  30261  pell1qrgaplem  30264  qirropth  30299  rmxyneg  30311  rmxyadd  30312  rmxm1  30325  rmym1  30326  rmxluc  30327  rmyluc  30328  rmxdbl  30330  rmydbl  30331  jm2.18  30387  jm2.19lem1  30388  jm2.19lem2  30389  jm2.19lem4  30391  jm2.19  30392  jm2.22  30394  jm2.23  30395  jm2.25  30398  jm2.27c  30406  jm3.1lem2  30417  flcidc  30581  itgpowd  30640  areaquad  30642  expgrowth  30659  mul13d  30857  fperiodmullem  30899  fperiodmul  30900  mulc1cncfg  30958  clim1fr1  30962  mullimc  30977  mullimcf  30984  sumnnodd  30991  reclimc  31014  sinmulcos  31020  coskpi2  31021  cosknegpi  31024  dvsinexp  31057  dvmptdiv  31066  dvasinbx  31069  dvdivf  31071  dvdivcncf  31076  dvbdfbdioolem2  31078  itgsinexplem1  31090  itgsinexp  31091  itgcoscmulx  31106  itgsincmulx  31111  itgiccshift  31117  itgperiod  31118  stoweidlem1  31120  stoweidlem11  31130  stoweidlem13  31132  stoweidlem14  31133  stoweidlem17  31136  stoweidlem25  31144  stoweidlem26  31145  stoweidlem42  31161  wallispilem4  31187  wallispilem5  31188  wallispi  31189  wallispi2lem1  31190  wallispi2lem2  31191  wallispi2  31192  stirlinglem1  31193  stirlinglem3  31195  stirlinglem4  31196  stirlinglem5  31197  stirlinglem6  31198  stirlinglem7  31199  stirlinglem8  31200  stirlinglem10  31202  stirlinglem11  31203  stirlinglem12  31204  stirlinglem13  31205  stirlinglem14  31206  stirlinglem15  31207  dirker2re  31211  dirkerdenne0  31212  dirkerval2  31213  dirkerper  31215  dirkertrigeqlem1  31217  dirkertrigeqlem2  31218  dirkertrigeqlem3  31219  dirkertrigeq  31220  dirkeritg  31221  dirkercncflem2  31223  dirkercncflem4  31225  fourierdlem26  31252  fourierdlem30  31256  fourierdlem39  31265  fourierdlem47  31273  fourierdlem48  31274  fourierdlem56  31282  fourierdlem57  31283  fourierdlem58  31284  fourierdlem62  31288  fourierdlem66  31292  fourierdlem68  31294  fourierdlem72  31298  fourierdlem73  31299  fourierdlem76  31302  fourierdlem80  31306  fourierdlem83  31309  fourierdlem85  31311  fourierdlem89  31315  fourierdlem90  31316  fourierdlem91  31317  fourierdlem95  31321  fourierdlem97  31323  fourierdlem101  31327  fourierdlem104  31330  fourierdlem111  31337  sqwvfoura  31348  sqwvfourb  31349  fourierswlem  31350  fouriersw  31351  sigarim  31354  sigarac  31355  sigaraf  31356  sigarmf  31357  sigarls  31360  sigardiv  31364  sigarcol  31367  cevathlem1  31370  altgsumbcALT  31881  i2linesd  32150  sineq0ALT  32692  bj-subcom  33617  bj-lineq  33624  bj-bary1lem  33626  bj-bary1lem1  33627  bj-bary1  33628
  Copyright terms: Public domain W3C validator