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

Theorem mulcl 8911
Description: Alias for ax-mulcl 8889, for naming consistency with mulcli 8932. (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 8889 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1710  (class class class)co 5945   CCcc 8825    x. cmul 8832
This theorem is referenced by:  0cn  8921  mulid1  8925  mulcli  8932  mulcld  8945  mul31  9070  mul4  9071  mul02  9080  cnegex2  9084  muladd  9302  subdi  9303  submul2  9310  mulsub  9312  recextlem1  9488  recex  9490  muleqadd  9502  mulnzcnopr  9504  divass  9532  divmuldiv  9550  divmuleq  9555  divadddiv  9565  conjmul  9567  cju  9832  zneo  10186  cnref1o  10441  modcyc2  11092  expcl  11214  expclzlem  11220  mulexp  11234  sqcl  11259  subsq  11303  subsq2  11304  binom2sub  11313  binom3  11315  zesq  11317  bernneq  11320  bernneq2  11321  bcval5  11423  reim  11690  imcl  11692  crre  11695  crim  11696  remim  11698  mulre  11702  cjreb  11704  recj  11705  reneg  11706  readd  11707  remullem  11709  remul2  11711  imcj  11713  imneg  11714  imadd  11715  immul2  11718  cjadd  11722  ipcnval  11724  cjmulrcl  11725  cjneg  11728  imval2  11732  cjreim  11741  rennim  11820  cnpart  11821  sqrneg  11849  sqabsadd  11863  sqabssub  11864  absreimsq  11873  absreim  11874  absmul  11875  sqreulem  11939  sqreu  11940  mulcn2  12165  o1mul  12184  climmul  12202  iseraltlem2  12252  efexp  12478  sinf  12501  cosf  12502  tanval2  12510  tanval3  12511  resinval  12512  recosval  12513  efi4p  12514  resin4p  12515  recos4p  12516  resincl  12517  recoscl  12518  sinneg  12523  cosneg  12524  efival  12529  efmival  12530  sinhval  12531  coshval  12532  retanhcl  12536  tanhlt1  12537  tanhbnd  12538  efeul  12539  sinadd  12541  cosadd  12542  sinsub  12545  cossub  12546  subsin  12548  sinmul  12549  cosmul  12550  addcos  12551  subcos  12552  cos2tsin  12556  ef01bndlem  12561  sin01bnd  12562  cos01bnd  12563  absef  12574  absefib  12575  efieq1re  12576  demoivre  12577  demoivreALT  12578  dvdscmulr  12654  dvdsmulcr  12655  odd2np1lem  12683  odd2np1  12684  gcdaddm  12805  modgcd  12812  bezoutlem1  12814  qredeq  12882  eulerthlem2  12947  opoe  12961  omoe  12962  opeo  12963  omeo  12964  pythagtriplem1  12966  pythagtriplem12  12976  pythagtriplem14  12978  iserodd  12985  gzmulcl  13082  4sqlem11  13099  4sqlem17  13105  cncrng  16501  cnfldmulg  16512  cnsubrg  16538  mulc1cncf  18512  icccvx  18552  pcorevlem  18628  itgcnlem  19248  itgneg  19262  itgconst  19277  itgadd  19283  iblabs  19287  itgmulc2  19292  dvmulbr  19392  dvmulf  19396  dvsincos  19432  plymullem1  19700  plymulcl  19707  plysubcl  19708  dgrcolem1  19758  dgrcolem2  19759  plydivlem4  19780  quotlem  19784  quotcl2  19786  quotdgr  19787  aaliou3lem3  19828  efper  19954  sinperlem  19955  sin2kpi  19958  cos2kpi  19959  efimpi  19966  sincosq1eq  19987  pige3  19992  abssinper  19993  sinkpi  19994  coskpi  19995  sineq0  19996  coseq1  19997  tanregt0  20008  efgh  20010  efif1olem4  20014  efifo  20016  eff1olem  20017  lognegb  20051  eflogeq  20063  efiarg  20069  tanarg  20081  logf1o2  20108  cxpcl  20132  cxpne0  20135  cxpsqrlem  20160  cxpsqr  20161  dvcxp1  20193  root1eq1  20206  cxpeq  20208  quad2  20246  quad  20247  dcubic2  20251  dcubic1  20252  dcubic  20253  mcubic  20254  cubic2  20255  cubic  20256  binom4  20257  dquartlem1  20258  dquartlem2  20259  dquart  20260  quart1cl  20261  quart1lem  20262  quart1  20263  quartlem1  20264  quartlem2  20265  quartlem3  20266  quart  20268  asinlem  20275  asinlem2  20276  asinlem3a  20277  asinlem3  20278  asinf  20279  atandm2  20284  atanf  20287  asinneg  20293  efiasin  20295  sinasin  20296  asinsinlem  20298  asinsin  20299  asinbnd  20306  cosasin  20311  atanneg  20314  atancj  20317  efiatan  20319  atanlogaddlem  20320  atanlogadd  20321  atanlogsublem  20322  atanlogsub  20323  efiatan2  20324  2efiatan  20325  tanatan  20326  cosatan  20328  atantan  20330  atanbndlem  20332  atans2  20338  dvatan  20342  atantayl  20344  atantayl2  20345  leibpilem1  20347  leibpilem2  20348  efrlim  20375  ftalem7  20428  basellem3  20432  basellem7  20436  basellem8  20437  basellem9  20438  ppiub  20555  dchrmulcl  20600  bposlem9  20643  lgsdir  20681  lgsdilem2  20682  lgsdi  20683  lgsne0  20684  lgsquadlem1  20705  2sqlem2  20715  rpvmasum2  20773  dchrisum0lem1  20777  dchrisum0lem2  20779  mulogsumlem  20792  mulog2sumlem3  20797  log2sumbnd  20805  selberglem1  20806  selberglem2  20807  selberg2  20812  pntlemk  20867  ablomul  21134  efghgrp  21152  smcnlem  21384  ipval2  21394  4ipval2  21395  4ipval3  21399  ipidsq  21400  dipcj  21404  cncph  21511  ipasslem2  21524  ipasslem4  21526  ipasslem8  21529  ipasslem9  21530  ipasslem11  21532  hhssnv  21955  spansncol  22261  homulass  22496  lnfnmuli  22738  riesz3i  22756  zetacvg  24048  circum  24411  mulcan1g  24490  prodf  24516  clim2prod  24517  clim2div  24518  prodfmul  24519  prodfn0  24523  prodfrec  24524  prodfdiv  24525  prodmolem3  24560  prodmolem2a  24561  fprodcl  24579  risefaccl  24621  fallfaccl  24622  faclim  24657  colinearalglem1  25093  colinearalglem2  25094  ax5seglem1  25115  axcontlem2  25152  axcontlem8  25158  bpoly3  25352  fsumcube  25354  itg2addnc  25494  itgaddnc  25500  iblabsnc  25504  iblmulc2nc  25505  itgmulc2nc  25508  cntotbnd  25843  rmxluc  26344  rmyluc  26345  jm2.17a  26370  jm2.18  26404  jm3.1lem1  26433  jm3.1lem2  26434  proot1ex  26843  lhe4.4ex1a  26869  expgrowthi  26873  expgrowth  26875  stoweidlem1  27073  stoweidlem10  27082  stoweidlem11  27083  stoweidlem13  27085  stoweidlem14  27086  stoweidlem17  27089  stoweidlem25  27097  stoweidlem26  27098  stoweidlem42  27114  wallispi2lem1  27143  wallispi2  27145  sinh-conventional  27909  dpfrac1  27942
This theorem was proved from axioms:  ax-mulcl 8889
  Copyright terms: Public domain W3C validator