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

Theorem mulcl 9007
Description: Alias for ax-mulcl 8985, for naming consistency with mulcli 9028. (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 8985 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 1717  (class class class)co 6020   CCcc 8921    x. cmul 8928
This theorem is referenced by:  0cn  9017  mulid1  9021  mulcli  9028  mulcld  9041  mul31  9166  mul4  9167  mul02  9176  cnegex2  9180  muladd  9398  subdi  9399  submul2  9406  mulsub  9408  recextlem1  9584  recex  9586  muleqadd  9598  mulnzcnopr  9600  divass  9628  divmuldiv  9646  divmuleq  9651  divadddiv  9661  conjmul  9663  cju  9928  zneo  10284  cnref1o  10539  modcyc2  11204  expcl  11326  expclzlem  11332  mulexp  11346  sqcl  11371  subsq  11415  subsq2  11416  binom2sub  11425  binom3  11427  zesq  11429  bernneq  11432  bernneq2  11433  bcval5  11536  reim  11841  imcl  11843  crre  11846  crim  11847  remim  11849  mulre  11853  cjreb  11855  recj  11856  reneg  11857  readd  11858  remullem  11860  remul2  11862  imcj  11864  imneg  11865  imadd  11866  immul2  11869  cjadd  11873  ipcnval  11875  cjmulrcl  11876  cjneg  11879  imval2  11883  cjreim  11892  rennim  11971  cnpart  11972  sqrneg  12000  sqabsadd  12014  sqabssub  12015  absreimsq  12024  absreim  12025  absmul  12026  sqreulem  12090  sqreu  12091  mulcn2  12316  o1mul  12335  climmul  12353  iseraltlem2  12403  efexp  12629  sinf  12652  cosf  12653  tanval2  12661  tanval3  12662  resinval  12663  recosval  12664  efi4p  12665  resin4p  12666  recos4p  12667  resincl  12668  recoscl  12669  sinneg  12674  cosneg  12675  efival  12680  efmival  12681  sinhval  12682  coshval  12683  retanhcl  12687  tanhlt1  12688  tanhbnd  12689  efeul  12690  sinadd  12692  cosadd  12693  sinsub  12696  cossub  12697  subsin  12699  sinmul  12700  cosmul  12701  addcos  12702  subcos  12703  cos2tsin  12707  ef01bndlem  12712  sin01bnd  12713  cos01bnd  12714  absef  12725  absefib  12726  efieq1re  12727  demoivre  12728  demoivreALT  12729  dvdscmulr  12805  dvdsmulcr  12806  odd2np1lem  12834  odd2np1  12835  gcdaddm  12956  modgcd  12963  bezoutlem1  12965  qredeq  13033  eulerthlem2  13098  opoe  13112  omoe  13113  opeo  13114  omeo  13115  pythagtriplem1  13117  pythagtriplem12  13127  pythagtriplem14  13129  iserodd  13136  gzmulcl  13233  4sqlem11  13250  4sqlem17  13256  cncrng  16645  cnfldmulg  16656  cnsubrg  16682  mulc1cncf  18806  icccvx  18846  pcorevlem  18922  itgcnlem  19548  itgneg  19562  itgconst  19577  itgadd  19583  iblabs  19587  itgmulc2  19592  dvmulbr  19692  dvmulf  19696  dvsincos  19732  plymullem1  20000  plymulcl  20007  plysubcl  20008  dgrcolem1  20058  dgrcolem2  20059  plydivlem4  20080  quotlem  20084  quotcl2  20086  quotdgr  20087  aaliou3lem3  20128  efper  20254  sinperlem  20255  sin2kpi  20258  cos2kpi  20259  efimpi  20266  sincosq1eq  20287  pige3  20292  abssinper  20293  sinkpi  20294  coskpi  20295  sineq0  20296  coseq1  20297  tanregt0  20308  efgh  20310  efif1olem4  20314  efifo  20316  eff1olem  20317  lognegb  20351  eflogeq  20363  efiarg  20369  tanarg  20381  logf1o2  20408  cxpcl  20432  cxpne0  20435  cxpsqrlem  20460  cxpsqr  20461  dvcxp1  20493  root1eq1  20506  cxpeq  20508  quad2  20546  quad  20547  dcubic2  20551  dcubic1  20552  dcubic  20553  mcubic  20554  cubic2  20555  cubic  20556  binom4  20557  dquartlem1  20558  dquartlem2  20559  dquart  20560  quart1cl  20561  quart1lem  20562  quart1  20563  quartlem1  20564  quartlem2  20565  quartlem3  20566  quart  20568  asinlem  20575  asinlem2  20576  asinlem3a  20577  asinlem3  20578  asinf  20579  atandm2  20584  atanf  20587  asinneg  20593  efiasin  20595  sinasin  20596  asinsinlem  20598  asinsin  20599  asinbnd  20606  cosasin  20611  atanneg  20614  atancj  20617  efiatan  20619  atanlogaddlem  20620  atanlogadd  20621  atanlogsublem  20622  atanlogsub  20623  efiatan2  20624  2efiatan  20625  tanatan  20626  cosatan  20628  atantan  20630  atanbndlem  20632  atans2  20638  dvatan  20642  atantayl  20644  atantayl2  20645  leibpilem1  20647  leibpilem2  20648  efrlim  20675  ftalem7  20728  basellem3  20732  basellem7  20736  basellem8  20737  basellem9  20738  ppiub  20855  dchrmulcl  20900  bposlem9  20943  lgsdir  20981  lgsdilem2  20982  lgsdi  20983  lgsne0  20984  lgsquadlem1  21005  2sqlem2  21015  rpvmasum2  21073  dchrisum0lem1  21077  dchrisum0lem2  21079  mulogsumlem  21092  mulog2sumlem3  21097  log2sumbnd  21105  selberglem1  21106  selberglem2  21107  selberg2  21112  pntlemk  21167  ablomul  21791  efghgrp  21809  smcnlem  22041  ipval2  22051  4ipval2  22052  4ipval3  22056  ipidsq  22057  dipcj  22061  cncph  22168  ipasslem2  22181  ipasslem4  22183  ipasslem9  22187  ipasslem11  22189  hhssnv  22612  spansncol  22918  homulass  23153  lnfnmuli  23395  riesz3i  23413  zetacvg  24578  circum  24890  mulcan1g  24968  prodf  24994  clim2div  24996  prodfmul  24997  prodfn0  25001  prodfrec  25002  prodfdiv  25003  prodmolem3  25038  prodmolem2a  25039  fprodcl  25057  risefaccl  25099  fallfaccl  25100  faclim  25123  colinearalglem1  25559  colinearalglem2  25560  ax5seglem1  25581  axcontlem2  25618  axcontlem8  25624  bpoly3  25818  fsumcube  25820  itg2addnc  25959  itgaddnc  25965  iblabsnc  25969  iblmulc2nc  25970  itgmulc2nc  25973  cntotbnd  26196  rmxluc  26690  rmyluc  26691  jm2.17a  26716  jm2.18  26750  jm3.1lem1  26779  jm3.1lem2  26780  proot1ex  27189  lhe4.4ex1a  27215  expgrowthi  27219  expgrowth  27221  stoweidlem10  27427  wallispi2lem1  27488  wallispi2  27490  sinh-conventional  27828  dpfrac1  27861
This theorem was proved from axioms:  ax-mulcl 8985
  Copyright terms: Public domain W3C validator