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

Theorem mulcl 9074
Description: Alias for ax-mulcl 9052, for naming consistency with mulcli 9095. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
mulcl  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )

Proof of Theorem mulcl
StepHypRef Expression
1 ax-mulcl 9052 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725  (class class class)co 6081   CCcc 8988    x. cmul 8995
This theorem is referenced by:  0cn  9084  mulid1  9088  mulcli  9095  mulcld  9108  mul31  9234  mul4  9235  mul02  9244  cnegex2  9248  muladd  9466  subdi  9467  submul2  9474  mulsub  9476  recextlem1  9652  recex  9654  muleqadd  9666  mulnzcnopr  9668  divass  9696  divmuldiv  9714  divmuleq  9719  divadddiv  9729  conjmul  9731  cju  9996  zneo  10352  cnref1o  10607  modcyc2  11277  expcl  11399  expclzlem  11405  mulexp  11419  sqcl  11444  subsq  11488  subsq2  11489  binom2sub  11498  binom3  11500  zesq  11502  bernneq  11505  bernneq2  11506  bcval5  11609  reim  11914  imcl  11916  crre  11919  crim  11920  remim  11922  mulre  11926  cjreb  11928  recj  11929  reneg  11930  readd  11931  remullem  11933  remul2  11935  imcj  11937  imneg  11938  imadd  11939  immul2  11942  cjadd  11946  ipcnval  11948  cjmulrcl  11949  cjneg  11952  imval2  11956  cjreim  11965  rennim  12044  cnpart  12045  sqrneg  12073  sqabsadd  12087  sqabssub  12088  absreimsq  12097  absreim  12098  absmul  12099  sqreulem  12163  sqreu  12164  mulcn2  12389  o1mul  12408  climmul  12426  iseraltlem2  12476  efexp  12702  sinf  12725  cosf  12726  tanval2  12734  tanval3  12735  resinval  12736  recosval  12737  efi4p  12738  resin4p  12739  recos4p  12740  resincl  12741  recoscl  12742  sinneg  12747  cosneg  12748  efival  12753  efmival  12754  sinhval  12755  coshval  12756  retanhcl  12760  tanhlt1  12761  tanhbnd  12762  efeul  12763  sinadd  12765  cosadd  12766  sinsub  12769  cossub  12770  subsin  12772  sinmul  12773  cosmul  12774  addcos  12775  subcos  12776  cos2tsin  12780  ef01bndlem  12785  sin01bnd  12786  cos01bnd  12787  absef  12798  absefib  12799  efieq1re  12800  demoivre  12801  demoivreALT  12802  dvdscmulr  12878  dvdsmulcr  12879  odd2np1lem  12907  odd2np1  12908  gcdaddm  13029  modgcd  13036  bezoutlem1  13038  qredeq  13106  eulerthlem2  13171  opoe  13185  omoe  13186  opeo  13187  omeo  13188  pythagtriplem1  13190  pythagtriplem12  13200  pythagtriplem14  13202  iserodd  13209  gzmulcl  13306  4sqlem11  13323  4sqlem17  13329  cncrng  16722  cnfldmulg  16733  cnsubrg  16759  mulc1cncf  18935  icccvx  18975  pcorevlem  19051  itgcnlem  19681  itgneg  19695  itgconst  19710  itgadd  19716  iblabs  19720  itgmulc2  19725  dvmulbr  19825  dvmulf  19829  dvsincos  19865  plymullem1  20133  plymulcl  20140  plysubcl  20141  dgrcolem1  20191  dgrcolem2  20192  plydivlem4  20213  quotlem  20217  quotcl2  20219  quotdgr  20220  aaliou3lem3  20261  efper  20387  sinperlem  20388  sin2kpi  20391  cos2kpi  20392  efimpi  20399  sincosq1eq  20420  pige3  20425  abssinper  20426  sinkpi  20427  coskpi  20428  sineq0  20429  coseq1  20430  tanregt0  20441  efgh  20443  efif1olem4  20447  efifo  20449  eff1olem  20450  lognegb  20484  eflogeq  20496  efiarg  20502  tanarg  20514  logf1o2  20541  cxpcl  20565  cxpne0  20568  cxpsqrlem  20593  cxpsqr  20594  dvcxp1  20626  root1eq1  20639  cxpeq  20641  quad2  20679  quad  20680  dcubic2  20684  dcubic1  20685  dcubic  20686  mcubic  20687  cubic2  20688  cubic  20689  binom4  20690  dquartlem1  20691  dquartlem2  20692  dquart  20693  quart1cl  20694  quart1lem  20695  quart1  20696  quartlem1  20697  quartlem2  20698  quartlem3  20699  quart  20701  asinlem  20708  asinlem2  20709  asinlem3a  20710  asinlem3  20711  asinf  20712  atandm2  20717  atanf  20720  asinneg  20726  efiasin  20728  sinasin  20729  asinsinlem  20731  asinsin  20732  asinbnd  20739  cosasin  20744  atanneg  20747  atancj  20750  efiatan  20752  atanlogaddlem  20753  atanlogadd  20754  atanlogsublem  20755  atanlogsub  20756  efiatan2  20757  2efiatan  20758  tanatan  20759  cosatan  20761  atantan  20763  atanbndlem  20765  atans2  20771  dvatan  20775  atantayl  20777  atantayl2  20778  leibpilem1  20780  leibpilem2  20781  efrlim  20808  ftalem7  20861  basellem3  20865  basellem7  20869  basellem8  20870  basellem9  20871  ppiub  20988  dchrmulcl  21033  bposlem9  21076  lgsdir  21114  lgsdilem2  21115  lgsdi  21116  lgsne0  21117  lgsquadlem1  21138  2sqlem2  21148  rpvmasum2  21206  dchrisum0lem1  21210  dchrisum0lem2  21212  mulogsumlem  21225  mulog2sumlem3  21230  log2sumbnd  21238  selberglem1  21239  selberglem2  21240  selberg2  21245  pntlemk  21300  ablomul  21943  efghgrp  21961  smcnlem  22193  ipval2  22203  4ipval2  22204  4ipval3  22208  ipidsq  22209  dipcj  22213  cncph  22320  ipasslem2  22333  ipasslem4  22335  ipasslem9  22339  ipasslem11  22341  hhssnv  22764  spansncol  23070  homulass  23305  lnfnmuli  23547  riesz3i  23565  zetacvg  24799  circum  25111  mulcan1g  25189  prodf  25215  clim2div  25217  prodfmul  25218  prodfn0  25222  prodfrec  25223  prodfdiv  25224  prodmolem3  25259  prodmolem2a  25260  fprodcl  25278  risefaccl  25331  fallfaccl  25332  faclim  25365  colinearalglem1  25845  colinearalglem2  25846  ax5seglem1  25867  axcontlem2  25904  axcontlem8  25910  bpoly3  26104  fsumcube  26106  itg2addnclem3  26258  itgaddnc  26265  iblabsnc  26269  iblmulc2nc  26270  itgmulc2nc  26273  ftc1anclem3  26282  ftc1anclem6  26285  ftc1anclem7  26286  ftc1anclem8  26287  ftc1anc  26288  cntotbnd  26505  rmxluc  26999  rmyluc  27000  jm2.17a  27025  jm2.18  27059  jm3.1lem1  27088  jm3.1lem2  27089  proot1ex  27497  lhe4.4ex1a  27523  expgrowthi  27527  expgrowth  27529  stoweidlem10  27735  wallispi2lem1  27796  wallispi2  27798  modaddmulmod  28158  modprm0  28228  sinh-conventional  28482  dpfrac1  28515
This theorem was proved from axioms:  ax-mulcl 9052
  Copyright terms: Public domain W3C validator