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

Theorem mulcl 8817
Description: Alias for ax-mulcl 8795, for naming consistency with mulcli 8838. (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 8795 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 1685  (class class class)co 5820   CCcc 8731    x. cmul 8738
This theorem is referenced by:  0cn  8827  mulid1  8831  mulcli  8838  mulcld  8851  mul31  8976  mul4  8977  mul02  8986  cnegex2  8990  muladd  9208  subdi  9209  submul2  9216  mulsub  9218  recextlem1  9394  recex  9396  muleqadd  9408  mulnzcnopr  9410  divass  9438  divmuldiv  9456  divmuleq  9461  divadddiv  9471  conjmul  9473  cju  9738  zneo  10090  cnref1o  10345  modcyc2  10996  expcl  11117  expclzlem  11123  mulexp  11137  sqcl  11162  subsq  11206  subsq2  11207  binom2sub  11216  binom3  11218  zesq  11220  bernneq  11223  bernneq2  11224  bcval5  11326  reim  11590  imcl  11592  crre  11595  crim  11596  remim  11598  mulre  11602  cjreb  11604  recj  11605  reneg  11606  readd  11607  remullem  11609  remul2  11611  imcj  11613  imneg  11614  imadd  11615  immul2  11618  cjadd  11622  ipcnval  11624  cjmulrcl  11625  cjneg  11628  imval2  11632  cjreim  11641  rennim  11720  cnpart  11721  sqrneg  11749  sqabsadd  11763  sqabssub  11764  absreimsq  11773  absreim  11774  absmul  11775  sqreulem  11839  sqreu  11840  mulcn2  12065  o1mul  12084  climmul  12102  iseraltlem2  12151  efexp  12377  sinf  12400  cosf  12401  tanval2  12409  tanval3  12410  resinval  12411  recosval  12412  efi4p  12413  resin4p  12414  recos4p  12415  resincl  12416  recoscl  12417  sinneg  12422  cosneg  12423  efival  12428  efmival  12429  sinhval  12430  coshval  12431  retanhcl  12435  tanhlt1  12436  tanhbnd  12437  efeul  12438  sinadd  12440  cosadd  12441  sinsub  12444  cossub  12445  subsin  12447  sinmul  12448  cosmul  12449  addcos  12450  subcos  12451  cos2tsin  12455  ef01bndlem  12460  sin01bnd  12461  cos01bnd  12462  absef  12473  absefib  12474  efieq1re  12475  demoivre  12476  demoivreALT  12477  dvdscmulr  12553  dvdsmulcr  12554  odd2np1lem  12582  odd2np1  12583  gcdaddm  12704  modgcd  12711  bezoutlem1  12713  qredeq  12781  eulerthlem2  12846  opoe  12860  omoe  12861  opeo  12862  omeo  12863  pythagtriplem1  12865  pythagtriplem12  12875  pythagtriplem14  12877  iserodd  12884  gzmulcl  12981  4sqlem11  12998  4sqlem17  13004  cncrng  16391  cnfldmulg  16402  cnsubrg  16428  mulc1cncf  18405  icccvx  18444  pcorevlem  18520  itgcnlem  19140  itgneg  19154  itgconst  19169  itgadd  19175  iblabs  19179  itgmulc2  19184  dvmulbr  19284  dvmulf  19288  dvsincos  19324  plymullem1  19592  plymulcl  19599  plysubcl  19600  dgrcolem1  19650  dgrcolem2  19651  plydivlem4  19672  quotlem  19676  quotcl2  19678  quotdgr  19679  aaliou3lem3  19720  efper  19843  sinperlem  19844  sin2kpi  19847  cos2kpi  19848  efimpi  19855  sincosq1eq  19876  pige3  19881  abssinper  19882  sinkpi  19883  coskpi  19884  sineq0  19885  coseq1  19886  tanregt0  19897  efgh  19899  efif1olem4  19903  efifo  19905  eff1olem  19906  lognegb  19939  eflogeq  19951  efiarg  19957  tanarg  19966  logf1o2  19993  cxpcl  20017  cxpne0  20020  cxpsqrlem  20045  cxpsqr  20046  dvcxp1  20078  root1eq1  20091  cxpeq  20093  quad2  20131  quad  20132  dcubic2  20136  dcubic1  20137  dcubic  20138  mcubic  20139  cubic2  20140  cubic  20141  binom4  20142  dquartlem1  20143  dquartlem2  20144  dquart  20145  quart1cl  20146  quart1lem  20147  quart1  20148  quartlem1  20149  quartlem2  20150  quartlem3  20151  quart  20153  asinlem  20160  asinlem2  20161  asinlem3a  20162  asinlem3  20163  asinf  20164  atandm2  20169  atanf  20172  asinneg  20178  efiasin  20180  sinasin  20181  asinsinlem  20183  asinsin  20184  asinbnd  20191  cosasin  20196  atanneg  20199  atancj  20202  efiatan  20204  atanlogaddlem  20205  atanlogadd  20206  atanlogsublem  20207  atanlogsub  20208  efiatan2  20209  2efiatan  20210  tanatan  20211  cosatan  20213  atantan  20215  atanbndlem  20217  atans2  20223  dvatan  20227  atantayl  20229  atantayl2  20230  leibpilem1  20232  leibpilem2  20233  efrlim  20260  ftalem7  20312  basellem3  20316  basellem7  20320  basellem8  20321  basellem9  20322  ppiub  20439  dchrmulcl  20484  bposlem9  20527  lgsdir  20565  lgsdilem2  20566  lgsdi  20567  lgsne0  20568  lgsquadlem1  20589  2sqlem2  20599  rpvmasum2  20657  dchrisum0lem1  20661  dchrisum0lem2  20663  mulogsumlem  20676  mulog2sumlem3  20681  log2sumbnd  20689  selberglem1  20690  selberglem2  20691  selberg2  20696  pntlemk  20751  ablomul  21016  efghgrp  21034  smcnlem  21264  ipval2  21274  4ipval2  21275  4ipval3  21279  ipidsq  21280  dipcj  21284  cncph  21391  ipasslem2  21404  ipasslem4  21406  ipasslem8  21409  ipasslem9  21410  ipasslem11  21412  hhssnv  21837  spansncol  22143  homulass  22378  lnfnmuli  22620  riesz3i  22638  zetacvg  23096  dmgmseqn0  23103  circum  23414  mulcan1g  23490  colinearalglem1  23944  colinearalglem2  23945  ax5seglem1  23966  axcontlem2  24003  axcontlem8  24009  bpoly3  24203  fsumcube  24205  mslb1  25018  2wsms  25019  cnegvex2  25071  clsmulcv  25093  fnmulcv  25095  mulmulvec  25098  cntotbnd  25931  rmxluc  26432  rmyluc  26433  jm2.17a  26458  jm2.18  26492  jm3.1lem1  26521  jm3.1lem2  26522  proot1ex  26931  lhe4.4ex1a  26957  expgrowthi  26961  expgrowth  26963  stoweidlem1  27161  stoweidlem10  27170  stoweidlem11  27171  stoweidlem13  27173  stoweidlem14  27174  stoweidlem17  27177  stoweidlem25  27185  stoweidlem26  27186  stoweidlem42  27202  wallispi2lem1  27231  wallispi2  27233  sinh-conventional  27481  dpfrac1  27514
This theorem was proved from axioms:  ax-mulcl 8795
  Copyright terms: Public domain W3C validator