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

Theorem mulcl 8837
Description: Alias for ax-mulcl 8815, for naming consistency with mulcli 8858. (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 8815 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 1696  (class class class)co 5874   CCcc 8751    x. cmul 8758
This theorem is referenced by:  0cn  8847  mulid1  8851  mulcli  8858  mulcld  8871  mul31  8996  mul4  8997  mul02  9006  cnegex2  9010  muladd  9228  subdi  9229  submul2  9236  mulsub  9238  recextlem1  9414  recex  9416  muleqadd  9428  mulnzcnopr  9430  divass  9458  divmuldiv  9476  divmuleq  9481  divadddiv  9491  conjmul  9493  cju  9758  zneo  10110  cnref1o  10365  modcyc2  11016  expcl  11137  expclzlem  11143  mulexp  11157  sqcl  11182  subsq  11226  subsq2  11227  binom2sub  11236  binom3  11238  zesq  11240  bernneq  11243  bernneq2  11244  bcval5  11346  reim  11610  imcl  11612  crre  11615  crim  11616  remim  11618  mulre  11622  cjreb  11624  recj  11625  reneg  11626  readd  11627  remullem  11629  remul2  11631  imcj  11633  imneg  11634  imadd  11635  immul2  11638  cjadd  11642  ipcnval  11644  cjmulrcl  11645  cjneg  11648  imval2  11652  cjreim  11661  rennim  11740  cnpart  11741  sqrneg  11769  sqabsadd  11783  sqabssub  11784  absreimsq  11793  absreim  11794  absmul  11795  sqreulem  11859  sqreu  11860  mulcn2  12085  o1mul  12104  climmul  12122  iseraltlem2  12171  efexp  12397  sinf  12420  cosf  12421  tanval2  12429  tanval3  12430  resinval  12431  recosval  12432  efi4p  12433  resin4p  12434  recos4p  12435  resincl  12436  recoscl  12437  sinneg  12442  cosneg  12443  efival  12448  efmival  12449  sinhval  12450  coshval  12451  retanhcl  12455  tanhlt1  12456  tanhbnd  12457  efeul  12458  sinadd  12460  cosadd  12461  sinsub  12464  cossub  12465  subsin  12467  sinmul  12468  cosmul  12469  addcos  12470  subcos  12471  cos2tsin  12475  ef01bndlem  12480  sin01bnd  12481  cos01bnd  12482  absef  12493  absefib  12494  efieq1re  12495  demoivre  12496  demoivreALT  12497  dvdscmulr  12573  dvdsmulcr  12574  odd2np1lem  12602  odd2np1  12603  gcdaddm  12724  modgcd  12731  bezoutlem1  12733  qredeq  12801  eulerthlem2  12866  opoe  12880  omoe  12881  opeo  12882  omeo  12883  pythagtriplem1  12885  pythagtriplem12  12895  pythagtriplem14  12897  iserodd  12904  gzmulcl  13001  4sqlem11  13018  4sqlem17  13024  cncrng  16411  cnfldmulg  16422  cnsubrg  16448  mulc1cncf  18425  icccvx  18464  pcorevlem  18540  itgcnlem  19160  itgneg  19174  itgconst  19189  itgadd  19195  iblabs  19199  itgmulc2  19204  dvmulbr  19304  dvmulf  19308  dvsincos  19344  plymullem1  19612  plymulcl  19619  plysubcl  19620  dgrcolem1  19670  dgrcolem2  19671  plydivlem4  19692  quotlem  19696  quotcl2  19698  quotdgr  19699  aaliou3lem3  19740  efper  19863  sinperlem  19864  sin2kpi  19867  cos2kpi  19868  efimpi  19875  sincosq1eq  19896  pige3  19901  abssinper  19902  sinkpi  19903  coskpi  19904  sineq0  19905  coseq1  19906  tanregt0  19917  efgh  19919  efif1olem4  19923  efifo  19925  eff1olem  19926  lognegb  19959  eflogeq  19971  efiarg  19977  tanarg  19986  logf1o2  20013  cxpcl  20037  cxpne0  20040  cxpsqrlem  20065  cxpsqr  20066  dvcxp1  20098  root1eq1  20111  cxpeq  20113  quad2  20151  quad  20152  dcubic2  20156  dcubic1  20157  dcubic  20158  mcubic  20159  cubic2  20160  cubic  20161  binom4  20162  dquartlem1  20163  dquartlem2  20164  dquart  20165  quart1cl  20166  quart1lem  20167  quart1  20168  quartlem1  20169  quartlem2  20170  quartlem3  20171  quart  20173  asinlem  20180  asinlem2  20181  asinlem3a  20182  asinlem3  20183  asinf  20184  atandm2  20189  atanf  20192  asinneg  20198  efiasin  20200  sinasin  20201  asinsinlem  20203  asinsin  20204  asinbnd  20211  cosasin  20216  atanneg  20219  atancj  20222  efiatan  20224  atanlogaddlem  20225  atanlogadd  20226  atanlogsublem  20227  atanlogsub  20228  efiatan2  20229  2efiatan  20230  tanatan  20231  cosatan  20233  atantan  20235  atanbndlem  20237  atans2  20243  dvatan  20247  atantayl  20249  atantayl2  20250  leibpilem1  20252  leibpilem2  20253  efrlim  20280  ftalem7  20332  basellem3  20336  basellem7  20340  basellem8  20341  basellem9  20342  ppiub  20459  dchrmulcl  20504  bposlem9  20547  lgsdir  20585  lgsdilem2  20586  lgsdi  20587  lgsne0  20588  lgsquadlem1  20609  2sqlem2  20619  rpvmasum2  20677  dchrisum0lem1  20681  dchrisum0lem2  20683  mulogsumlem  20696  mulog2sumlem3  20701  log2sumbnd  20709  selberglem1  20710  selberglem2  20711  selberg2  20716  pntlemk  20771  ablomul  21038  efghgrp  21056  smcnlem  21286  ipval2  21296  4ipval2  21297  4ipval3  21301  ipidsq  21302  dipcj  21306  cncph  21413  ipasslem2  21426  ipasslem4  21428  ipasslem8  21431  ipasslem9  21432  ipasslem11  21434  hhssnv  21857  spansncol  22163  homulass  22398  lnfnmuli  22640  riesz3i  22658  zetacvg  23704  dmgmseqn0  23711  circum  24022  mulcan1g  24099  faclimlem5  24121  faclimlem7  24123  prodf  24151  prodmolem3  24156  prodmolem2a  24157  colinearalglem1  24605  colinearalglem2  24606  ax5seglem1  24627  axcontlem2  24664  axcontlem8  24670  bpoly3  24864  fsumcube  24866  itg2addnc  25004  itgaddnc  25010  iblabsnc  25014  iblmulc2nc  25015  itgmulc2nc  25018  mslb1  25709  2wsms  25710  cnegvex2  25762  clsmulcv  25784  fnmulcv  25786  mulmulvec  25789  cntotbnd  26622  rmxluc  27123  rmyluc  27124  jm2.17a  27149  jm2.18  27183  jm3.1lem1  27212  jm3.1lem2  27213  proot1ex  27622  lhe4.4ex1a  27648  expgrowthi  27652  expgrowth  27654  stoweidlem1  27852  stoweidlem10  27861  stoweidlem11  27862  stoweidlem13  27864  stoweidlem14  27865  stoweidlem17  27868  stoweidlem25  27876  stoweidlem26  27877  stoweidlem42  27893  wallispi2lem1  27922  wallispi2  27924  sinh-conventional  28462  dpfrac1  28495
This theorem was proved from axioms:  ax-mulcl 8815
  Copyright terms: Public domain W3C validator