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

Theorem mulcld 9619
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 9579 . 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 1804  (class class class)co 6281   CCcc 9493    x. cmul 9500
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 9557
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  mul02lem1  9759  addid1  9763  cnegex  9764  kcnktkm1cn  9994  receu  10200  divrec  10229  divcan3  10237  divdivdiv  10251  divsubdiv  10266  cru  10534  lincmb01cmp  11672  iccf1o  11673  flpmodeq  11980  moddiffl  11986  modvalp1  11993  modcyc  12010  modadd1  12012  modmul1  12019  modaddmulmod  12032  mulexpz  12185  expmulz  12191  binom3  12266  bernneq  12271  remullem  12940  cjreim2  12973  absimle  13121  abstri  13142  sqreulem  13171  sqreu  13172  mulcn2  13397  reccn2  13398  o1rlimmul  13420  isummulc2  13556  fsummulc2  13578  fsumparts  13599  binomlem  13620  binom1dif  13624  incexclem  13627  incexc  13628  incexc2  13629  geomulcvg  13664  mertenslem1  13672  mertens  13674  efaddlem  13706  sinadd  13776  cosadd  13777  tanaddlem  13778  tanadd  13779  addsin  13782  sincossq  13788  sin2t  13789  dvds2ln  13891  oddm1even  13924  sadadd2lem2  13977  bezoutlem2  14054  bezoutlem3  14055  bezoutlem4  14056  phiprmpw  14183  pythagtriplem12  14227  pythagtriplem14  14229  pythagtriplem16  14231  pcpremul  14244  pcaddlem  14284  fldivp1  14293  mul4sqlem  14348  4sqlem14  14353  vdwapun  14369  vdwlem2  14377  vdwlem6  14381  zringlpirlem3  18384  zlpirlem3  18389  znunit  18475  blcvx  21176  icopnfcnv  21315  mbfmulc2re  21928  mbfmulc2  21943  itg1addlem4  21979  itg1addlem5  21980  itg1mulc  21984  mbfmul  22006  itgcl  22063  itgcnlem  22069  iblmulc2  22110  itgmulc2  22113  itgabs  22114  itgsplit  22115  dvmulbr  22215  dvcmul  22220  dvcmulf  22221  dvexp  22229  dvmptcmul  22240  dvexp3  22252  dvsincos  22255  cmvth  22265  dvlipcn  22268  dvfsumabs  22297  dvfsumlem1  22300  ftc1lem4  22313  itgparts  22321  plyf  22468  ply1termlem  22473  plyeq0lem  22480  plypf1  22482  plyaddlem1  22483  plymullem1  22484  coeeulem  22494  coeidlem  22507  coeid3  22510  plyco  22511  coemullem  22519  coemulhi  22523  coemulc  22524  dgrcolem2  22543  plycjlem  22545  plyrecj  22548  dvply1  22552  vieta1lem2  22579  vieta1  22580  elqaalem3  22589  aareccl  22594  aalioulem1  22600  taylfvallem1  22624  tayl0  22629  dvtaylp  22637  taylthlem2  22641  psergf  22679  radcnvlem1  22680  dvradcnv  22688  psercn2  22690  pserdvlem2  22695  pserdv2  22697  abelthlem4  22701  abelthlem5  22702  abelthlem6  22703  abelthlem7  22705  abelthlem9  22707  tanregt0  22798  efgh  22800  efabl  22809  efsubm  22810  cosargd  22865  abslogle  22875  tanarg  22876  advlogexp  22908  logtayllem  22912  logtayl  22913  cxpadd  22932  mulcxp  22938  cxpmul  22941  cxpmul2  22942  cxpmul2z  22944  abscxp  22945  abscxp2  22946  dvcxp2  22989  abscxpbnd  22999  root1eq1  23001  cxpeq  23003  angcan  23006  pythag  23021  ssscongptld  23028  affineequiv  23029  affineequiv2  23030  chordthmlem2  23036  chordthmlem3  23037  chordthmlem4  23038  chordthmlem5  23039  heron  23041  quad2  23042  quad  23043  dcubic1lem  23046  dcubic2  23047  dcubic1  23048  dcubic  23049  mcubic  23050  cubic2  23051  cubic  23052  binom4  23053  dquartlem1  23054  dquartlem2  23055  dquart  23056  quart1cl  23057  quart1lem  23058  quart1  23059  quartlem1  23060  quartlem2  23061  atantayl3  23142  leibpi  23145  birthdaylem2  23154  divsqrtsumo1  23185  cvxcl  23186  jensenlem2  23189  wilthlem2  23215  ftalem1  23218  ftalem2  23219  ftalem4  23221  ftalem5  23222  basellem2  23227  basellem3  23228  basellem8  23233  muinv  23341  fsumdvdsmul  23343  logfacrlim  23371  logexprlim  23372  perfectlem2  23377  bposlem9  23439  lgsquad2lem1  23505  2sqlem3  23513  rplogsumlem1  23541  dchrisumlem2  23547  dchrisumlem3  23548  dchrmusum2  23551  dchrvmasumlem1  23552  dchrvmasum2lem  23553  dchrvmasum2if  23554  dchrvmasumlem3  23556  dchrvmasumiflem1  23558  dchrvmasumiflem2  23559  rpvmasum2  23569  dchrisum0lem1  23573  dchrisum0lem2a  23574  dchrisum0lem2  23575  dchrmusumlem  23579  dchrvmasumlem  23580  rplogsum  23584  mudivsum  23587  mulogsumlem  23588  mulogsum  23589  mulog2sumlem1  23591  mulog2sumlem2  23592  mulog2sumlem3  23593  vmalogdivsum  23596  logsqvma  23599  log2sumbnd  23601  selberglem1  23602  selberglem2  23603  selberglem3  23604  selberg  23605  selberg2lem  23607  selberg2  23608  selberg3lem1  23614  selberg3  23616  selberg4lem1  23617  selberg4  23618  pntrsumo1  23622  selbergr  23625  selberg3r  23626  selberg4r  23627  selberg34r  23628  pntsval2  23633  pntrlog2bndlem1  23634  pntrlog2bndlem2  23635  pntrlog2bndlem3  23636  pntrlog2bndlem4  23637  pntrlog2bndlem5  23638  pntrlog2bndlem6  23640  pntrlog2bnd  23641  pntlemb  23654  pntlemf  23662  pntlemo  23664  ostth2lem2  23691  ostth2lem3  23692  ttgcontlem1  24060  brbtwn2  24080  colinearalg  24085  ax5seglem2  24104  ax5seglem9  24112  axeuclidlem  24137  axcontlem2  24140  axcontlem4  24142  axcontlem7  24145  axcontlem8  24146  ex-ind-dvds  25042  ipval2  25489  dipcl  25497  riesz3i  26853  mul2lt0rlt0  27437  bhmafibid1  27505  bhmafibid2  27506  2sqmod  27509  cnre2csqima  27766  rmulccn  27783  indsum  27909  dya2icoseg  28121  oddpwdc  28166  eulerpartlems  28172  eulerpartlemsv3  28173  eulerpartlemgs2  28192  signsplypnf  28380  lgamgulmlem2  28445  lgamgulmlem3  28446  lgamgulmlem4  28447  lgamgulmlem5  28448  lgamgulmlem6  28449  lgamgulm2  28451  lgamcvg2  28470  gamcvg  28471  gamcvg2lem  28474  subfacval2  28504  subfaclim  28505  rescon  28564  subdivcomb1  28978  subdivcomb2  28979  fprodmul  29065  iprodmul  29097  iprodgam  29100  binomfallfaclem1  29136  binomfallfaclem2  29137  binomrisefac  29139  bpolycl  29789  bpolysum  29790  bpolydiflem  29791  bpoly4  29796  iblmulc2nc  30055  itgmulc2nc  30058  itgabsnc  30059  ftc1cnnclem  30063  ftc1anclem3  30067  dvasin  30078  areacirclem1  30082  areacirclem4  30085  areacirc  30087  cntotbnd  30267  pellexlem1  30740  pellexlem2  30741  pellexlem6  30745  pell1234qrne0  30764  pell1234qrreccl  30765  pell1234qrmulcl  30766  pell1234qrdich  30772  pell14qrdich  30780  pell1qrge1  30781  pell1qrgaplem  30784  qirropth  30819  rmxyneg  30831  rmxyadd  30832  rmxm1  30845  rmym1  30846  rmxluc  30847  rmyluc  30848  rmxdbl  30850  rmydbl  30851  jm2.18  30905  jm2.19lem1  30906  jm2.19lem2  30907  jm2.19lem4  30909  jm2.19  30910  jm2.22  30912  jm2.23  30913  jm2.25  30916  jm2.27c  30924  jm3.1lem2  30935  flcidc  31099  itgpowd  31158  areaquad  31160  radcnvrat  31171  lcmgcdlem  31188  expgrowth  31216  mul13d  31410  fperiodmullem  31452  fperiodmul  31453  mulc1cncfg  31511  clim1fr1  31515  mullimc  31530  mullimcf  31537  sumnnodd  31544  reclimc  31567  sinmulcos  31572  coskpi2  31573  cosknegpi  31576  dvsinexp  31609  dvmptdiv  31618  dvasinbx  31621  dvdivf  31623  dvdivbd  31624  dvdivcncf  31628  dvbdfbdioolem2  31630  itgsinexplem1  31642  itgsinexp  31643  itgcoscmulx  31658  itgsincmulx  31663  itgiccshift  31669  itgperiod  31670  stoweidlem1  31672  stoweidlem11  31682  stoweidlem13  31684  stoweidlem14  31685  stoweidlem17  31688  stoweidlem25  31696  stoweidlem26  31697  stoweidlem42  31713  wallispilem4  31739  wallispilem5  31740  wallispi  31741  wallispi2lem1  31742  wallispi2lem2  31743  wallispi2  31744  stirlinglem1  31745  stirlinglem3  31747  stirlinglem4  31748  stirlinglem5  31749  stirlinglem6  31750  stirlinglem7  31751  stirlinglem8  31752  stirlinglem10  31754  stirlinglem11  31755  stirlinglem12  31756  stirlinglem13  31757  stirlinglem14  31758  stirlinglem15  31759  dirker2re  31763  dirkerdenne0  31764  dirkerper  31767  dirkertrigeqlem1  31769  dirkertrigeqlem2  31770  dirkertrigeqlem3  31771  dirkertrigeq  31772  dirkeritg  31773  dirkercncflem2  31775  dirkercncflem4  31777  fourierdlem26  31804  fourierdlem30  31808  fourierdlem39  31817  fourierdlem42  31820  fourierdlem47  31825  fourierdlem48  31826  fourierdlem56  31834  fourierdlem57  31835  fourierdlem58  31836  fourierdlem62  31840  fourierdlem65  31843  fourierdlem66  31844  fourierdlem68  31846  fourierdlem72  31850  fourierdlem73  31851  fourierdlem76  31854  fourierdlem80  31858  fourierdlem83  31861  fourierdlem85  31863  fourierdlem89  31867  fourierdlem90  31868  fourierdlem91  31869  fourierdlem95  31873  fourierdlem97  31875  fourierdlem101  31879  fourierdlem103  31881  fourierdlem104  31882  fourierdlem111  31889  sqwvfoura  31900  sqwvfourb  31901  fourierswlem  31902  fouriersw  31903  sigarim  31906  sigarac  31907  sigaraf  31908  sigarmf  31909  sigarls  31912  sigardiv  31916  sigarcol  31919  cevathlem1  31922  0nodd  32335  2nodd  32337  2zlidl  32450  2zrngnmlid  32465  altgsumbcALT  32675  i2linesd  32929  sineq0ALT  33470  bj-subcom  34410  bj-lineq  34417  bj-bary1lem  34419  bj-bary1lem1  34420  bj-bary1  34421  inductionexd  37637  imo72b2lem0  37651
  Copyright terms: Public domain W3C validator