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

Theorem mulcl 8823
Description: Alias for ax-mulcl 8801, for naming consistency with mulcli 8844. (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 8801 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 1686  (class class class)co 5860   CCcc 8737    x. cmul 8744
This theorem is referenced by:  0cn  8833  mulid1  8837  mulcli  8844  mulcld  8857  mul31  8982  mul4  8983  mul02  8992  cnegex2  8996  muladd  9214  subdi  9215  submul2  9222  mulsub  9224  recextlem1  9400  recex  9402  muleqadd  9414  mulnzcnopr  9416  divass  9444  divmuldiv  9462  divmuleq  9467  divadddiv  9477  conjmul  9479  cju  9744  zneo  10096  cnref1o  10351  modcyc2  11002  expcl  11123  expclzlem  11129  mulexp  11143  sqcl  11168  subsq  11212  subsq2  11213  binom2sub  11222  binom3  11224  zesq  11226  bernneq  11229  bernneq2  11230  bcval5  11332  reim  11596  imcl  11598  crre  11601  crim  11602  remim  11604  mulre  11608  cjreb  11610  recj  11611  reneg  11612  readd  11613  remullem  11615  remul2  11617  imcj  11619  imneg  11620  imadd  11621  immul2  11624  cjadd  11628  ipcnval  11630  cjmulrcl  11631  cjneg  11634  imval2  11638  cjreim  11647  rennim  11726  cnpart  11727  sqrneg  11755  sqabsadd  11769  sqabssub  11770  absreimsq  11779  absreim  11780  absmul  11781  sqreulem  11845  sqreu  11846  mulcn2  12071  o1mul  12090  climmul  12108  iseraltlem2  12157  efexp  12383  sinf  12406  cosf  12407  tanval2  12415  tanval3  12416  resinval  12417  recosval  12418  efi4p  12419  resin4p  12420  recos4p  12421  resincl  12422  recoscl  12423  sinneg  12428  cosneg  12429  efival  12434  efmival  12435  sinhval  12436  coshval  12437  retanhcl  12441  tanhlt1  12442  tanhbnd  12443  efeul  12444  sinadd  12446  cosadd  12447  sinsub  12450  cossub  12451  subsin  12453  sinmul  12454  cosmul  12455  addcos  12456  subcos  12457  cos2tsin  12461  ef01bndlem  12466  sin01bnd  12467  cos01bnd  12468  absef  12479  absefib  12480  efieq1re  12481  demoivre  12482  demoivreALT  12483  dvdscmulr  12559  dvdsmulcr  12560  odd2np1lem  12588  odd2np1  12589  gcdaddm  12710  modgcd  12717  bezoutlem1  12719  qredeq  12787  eulerthlem2  12852  opoe  12866  omoe  12867  opeo  12868  omeo  12869  pythagtriplem1  12871  pythagtriplem12  12881  pythagtriplem14  12883  iserodd  12890  gzmulcl  12987  4sqlem11  13004  4sqlem17  13010  cncrng  16397  cnfldmulg  16408  cnsubrg  16434  mulc1cncf  18411  icccvx  18450  pcorevlem  18526  itgcnlem  19146  itgneg  19160  itgconst  19175  itgadd  19181  iblabs  19185  itgmulc2  19190  dvmulbr  19290  dvmulf  19294  dvsincos  19330  plymullem1  19598  plymulcl  19605  plysubcl  19606  dgrcolem1  19656  dgrcolem2  19657  plydivlem4  19678  quotlem  19682  quotcl2  19684  quotdgr  19685  aaliou3lem3  19726  efper  19849  sinperlem  19850  sin2kpi  19853  cos2kpi  19854  efimpi  19861  sincosq1eq  19882  pige3  19887  abssinper  19888  sinkpi  19889  coskpi  19890  sineq0  19891  coseq1  19892  tanregt0  19903  efgh  19905  efif1olem4  19909  efifo  19911  eff1olem  19912  lognegb  19945  eflogeq  19957  efiarg  19963  tanarg  19972  logf1o2  19999  cxpcl  20023  cxpne0  20026  cxpsqrlem  20051  cxpsqr  20052  dvcxp1  20084  root1eq1  20097  cxpeq  20099  quad2  20137  quad  20138  dcubic2  20142  dcubic1  20143  dcubic  20144  mcubic  20145  cubic2  20146  cubic  20147  binom4  20148  dquartlem1  20149  dquartlem2  20150  dquart  20151  quart1cl  20152  quart1lem  20153  quart1  20154  quartlem1  20155  quartlem2  20156  quartlem3  20157  quart  20159  asinlem  20166  asinlem2  20167  asinlem3a  20168  asinlem3  20169  asinf  20170  atandm2  20175  atanf  20178  asinneg  20184  efiasin  20186  sinasin  20187  asinsinlem  20189  asinsin  20190  asinbnd  20197  cosasin  20202  atanneg  20205  atancj  20208  efiatan  20210  atanlogaddlem  20211  atanlogadd  20212  atanlogsublem  20213  atanlogsub  20214  efiatan2  20215  2efiatan  20216  tanatan  20217  cosatan  20219  atantan  20221  atanbndlem  20223  atans2  20229  dvatan  20233  atantayl  20235  atantayl2  20236  leibpilem1  20238  leibpilem2  20239  efrlim  20266  ftalem7  20318  basellem3  20322  basellem7  20326  basellem8  20327  basellem9  20328  ppiub  20445  dchrmulcl  20490  bposlem9  20533  lgsdir  20571  lgsdilem2  20572  lgsdi  20573  lgsne0  20574  lgsquadlem1  20595  2sqlem2  20605  rpvmasum2  20663  dchrisum0lem1  20667  dchrisum0lem2  20669  mulogsumlem  20682  mulog2sumlem3  20687  log2sumbnd  20695  selberglem1  20696  selberglem2  20697  selberg2  20702  pntlemk  20757  ablomul  21024  efghgrp  21042  smcnlem  21272  ipval2  21282  4ipval2  21283  4ipval3  21287  ipidsq  21288  dipcj  21292  cncph  21399  ipasslem2  21412  ipasslem4  21414  ipasslem8  21417  ipasslem9  21418  ipasslem11  21420  hhssnv  21843  spansncol  22149  homulass  22384  lnfnmuli  22626  riesz3i  22644  zetacvg  23691  dmgmseqn0  23698  circum  24009  mulcan1g  24086  colinearalglem1  24536  colinearalglem2  24537  ax5seglem1  24558  axcontlem2  24595  axcontlem8  24601  bpoly3  24795  fsumcube  24797  itg2addnc  24935  mslb1  25618  2wsms  25619  cnegvex2  25671  clsmulcv  25693  fnmulcv  25695  mulmulvec  25698  cntotbnd  26531  rmxluc  27032  rmyluc  27033  jm2.17a  27058  jm2.18  27092  jm3.1lem1  27121  jm3.1lem2  27122  proot1ex  27531  lhe4.4ex1a  27557  expgrowthi  27561  expgrowth  27563  stoweidlem1  27761  stoweidlem10  27770  stoweidlem11  27771  stoweidlem13  27773  stoweidlem14  27774  stoweidlem17  27777  stoweidlem25  27785  stoweidlem26  27786  stoweidlem42  27802  wallispi2lem1  27831  wallispi2  27833  sinh-conventional  28220  dpfrac1  28253
This theorem was proved from axioms:  ax-mulcl 8801
  Copyright terms: Public domain W3C validator