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

Theorem mulcl 9066
Description: Alias for ax-mulcl 9044, for naming consistency with mulcli 9087. (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 9044 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 6073   CCcc 8980    x. cmul 8987
This theorem is referenced by:  0cn  9076  mulid1  9080  mulcli  9087  mulcld  9100  mul31  9226  mul4  9227  mul02  9236  cnegex2  9240  muladd  9458  subdi  9459  submul2  9466  mulsub  9468  recextlem1  9644  recex  9646  muleqadd  9658  mulnzcnopr  9660  divass  9688  divmuldiv  9706  divmuleq  9711  divadddiv  9721  conjmul  9723  cju  9988  zneo  10344  cnref1o  10599  modcyc2  11269  expcl  11391  expclzlem  11397  mulexp  11411  sqcl  11436  subsq  11480  subsq2  11481  binom2sub  11490  binom3  11492  zesq  11494  bernneq  11497  bernneq2  11498  bcval5  11601  reim  11906  imcl  11908  crre  11911  crim  11912  remim  11914  mulre  11918  cjreb  11920  recj  11921  reneg  11922  readd  11923  remullem  11925  remul2  11927  imcj  11929  imneg  11930  imadd  11931  immul2  11934  cjadd  11938  ipcnval  11940  cjmulrcl  11941  cjneg  11944  imval2  11948  cjreim  11957  rennim  12036  cnpart  12037  sqrneg  12065  sqabsadd  12079  sqabssub  12080  absreimsq  12089  absreim  12090  absmul  12091  sqreulem  12155  sqreu  12156  mulcn2  12381  o1mul  12400  climmul  12418  iseraltlem2  12468  efexp  12694  sinf  12717  cosf  12718  tanval2  12726  tanval3  12727  resinval  12728  recosval  12729  efi4p  12730  resin4p  12731  recos4p  12732  resincl  12733  recoscl  12734  sinneg  12739  cosneg  12740  efival  12745  efmival  12746  sinhval  12747  coshval  12748  retanhcl  12752  tanhlt1  12753  tanhbnd  12754  efeul  12755  sinadd  12757  cosadd  12758  sinsub  12761  cossub  12762  subsin  12764  sinmul  12765  cosmul  12766  addcos  12767  subcos  12768  cos2tsin  12772  ef01bndlem  12777  sin01bnd  12778  cos01bnd  12779  absef  12790  absefib  12791  efieq1re  12792  demoivre  12793  demoivreALT  12794  dvdscmulr  12870  dvdsmulcr  12871  odd2np1lem  12899  odd2np1  12900  gcdaddm  13021  modgcd  13028  bezoutlem1  13030  qredeq  13098  eulerthlem2  13163  opoe  13177  omoe  13178  opeo  13179  omeo  13180  pythagtriplem1  13182  pythagtriplem12  13192  pythagtriplem14  13194  iserodd  13201  gzmulcl  13298  4sqlem11  13315  4sqlem17  13321  cncrng  16714  cnfldmulg  16725  cnsubrg  16751  mulc1cncf  18927  icccvx  18967  pcorevlem  19043  itgcnlem  19673  itgneg  19687  itgconst  19702  itgadd  19708  iblabs  19712  itgmulc2  19717  dvmulbr  19817  dvmulf  19821  dvsincos  19857  plymullem1  20125  plymulcl  20132  plysubcl  20133  dgrcolem1  20183  dgrcolem2  20184  plydivlem4  20205  quotlem  20209  quotcl2  20211  quotdgr  20212  aaliou3lem3  20253  efper  20379  sinperlem  20380  sin2kpi  20383  cos2kpi  20384  efimpi  20391  sincosq1eq  20412  pige3  20417  abssinper  20418  sinkpi  20419  coskpi  20420  sineq0  20421  coseq1  20422  tanregt0  20433  efgh  20435  efif1olem4  20439  efifo  20441  eff1olem  20442  lognegb  20476  eflogeq  20488  efiarg  20494  tanarg  20506  logf1o2  20533  cxpcl  20557  cxpne0  20560  cxpsqrlem  20585  cxpsqr  20586  dvcxp1  20618  root1eq1  20631  cxpeq  20633  quad2  20671  quad  20672  dcubic2  20676  dcubic1  20677  dcubic  20678  mcubic  20679  cubic2  20680  cubic  20681  binom4  20682  dquartlem1  20683  dquartlem2  20684  dquart  20685  quart1cl  20686  quart1lem  20687  quart1  20688  quartlem1  20689  quartlem2  20690  quartlem3  20691  quart  20693  asinlem  20700  asinlem2  20701  asinlem3a  20702  asinlem3  20703  asinf  20704  atandm2  20709  atanf  20712  asinneg  20718  efiasin  20720  sinasin  20721  asinsinlem  20723  asinsin  20724  asinbnd  20731  cosasin  20736  atanneg  20739  atancj  20742  efiatan  20744  atanlogaddlem  20745  atanlogadd  20746  atanlogsublem  20747  atanlogsub  20748  efiatan2  20749  2efiatan  20750  tanatan  20751  cosatan  20753  atantan  20755  atanbndlem  20757  atans2  20763  dvatan  20767  atantayl  20769  atantayl2  20770  leibpilem1  20772  leibpilem2  20773  efrlim  20800  ftalem7  20853  basellem3  20857  basellem7  20861  basellem8  20862  basellem9  20863  ppiub  20980  dchrmulcl  21025  bposlem9  21068  lgsdir  21106  lgsdilem2  21107  lgsdi  21108  lgsne0  21109  lgsquadlem1  21130  2sqlem2  21140  rpvmasum2  21198  dchrisum0lem1  21202  dchrisum0lem2  21204  mulogsumlem  21217  mulog2sumlem3  21222  log2sumbnd  21230  selberglem1  21231  selberglem2  21232  selberg2  21237  pntlemk  21292  ablomul  21935  efghgrp  21953  smcnlem  22185  ipval2  22195  4ipval2  22196  4ipval3  22200  ipidsq  22201  dipcj  22205  cncph  22312  ipasslem2  22325  ipasslem4  22327  ipasslem9  22331  ipasslem11  22333  hhssnv  22756  spansncol  23062  homulass  23297  lnfnmuli  23539  riesz3i  23557  zetacvg  24791  circum  25103  mulcan1g  25181  prodf  25207  clim2div  25209  prodfmul  25210  prodfn0  25214  prodfrec  25215  prodfdiv  25216  prodmolem3  25251  prodmolem2a  25252  fprodcl  25270  risefaccl  25323  fallfaccl  25324  faclim  25357  colinearalglem1  25837  colinearalglem2  25838  ax5seglem1  25859  axcontlem2  25896  axcontlem8  25902  bpoly3  26096  fsumcube  26098  itg2addnclem3  26248  itgaddnc  26255  iblabsnc  26259  iblmulc2nc  26260  itgmulc2nc  26263  ftc1anclem3  26272  ftc1anclem6  26275  ftc1anclem7  26276  ftc1anclem8  26277  ftc1anc  26278  cntotbnd  26496  rmxluc  26990  rmyluc  26991  jm2.17a  27016  jm2.18  27050  jm3.1lem1  27079  jm3.1lem2  27080  proot1ex  27488  lhe4.4ex1a  27514  expgrowthi  27518  expgrowth  27520  stoweidlem10  27726  wallispi2lem1  27787  wallispi2  27789  modaddmulmod  28136  modprm0  28194  sinh-conventional  28419  dpfrac1  28452
This theorem was proved from axioms:  ax-mulcl 9044
  Copyright terms: Public domain W3C validator