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

Theorem mulcl 8821
Description: Alias for ax-mulcl 8799, for naming consistency with mulcli 8842. (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 8799 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 1684  (class class class)co 5858   CCcc 8735    x. cmul 8742
This theorem is referenced by:  0cn  8831  mulid1  8835  mulcli  8842  mulcld  8855  mul31  8980  mul4  8981  mul02  8990  cnegex2  8994  muladd  9212  subdi  9213  submul2  9220  mulsub  9222  recextlem1  9398  recex  9400  muleqadd  9412  mulnzcnopr  9414  divass  9442  divmuldiv  9460  divmuleq  9465  divadddiv  9475  conjmul  9477  cju  9742  zneo  10094  cnref1o  10349  modcyc2  11000  expcl  11121  expclzlem  11127  mulexp  11141  sqcl  11166  subsq  11210  subsq2  11211  binom2sub  11220  binom3  11222  zesq  11224  bernneq  11227  bernneq2  11228  bcval5  11330  reim  11594  imcl  11596  crre  11599  crim  11600  remim  11602  mulre  11606  cjreb  11608  recj  11609  reneg  11610  readd  11611  remullem  11613  remul2  11615  imcj  11617  imneg  11618  imadd  11619  immul2  11622  cjadd  11626  ipcnval  11628  cjmulrcl  11629  cjneg  11632  imval2  11636  cjreim  11645  rennim  11724  cnpart  11725  sqrneg  11753  sqabsadd  11767  sqabssub  11768  absreimsq  11777  absreim  11778  absmul  11779  sqreulem  11843  sqreu  11844  mulcn2  12069  o1mul  12088  climmul  12106  iseraltlem2  12155  efexp  12381  sinf  12404  cosf  12405  tanval2  12413  tanval3  12414  resinval  12415  recosval  12416  efi4p  12417  resin4p  12418  recos4p  12419  resincl  12420  recoscl  12421  sinneg  12426  cosneg  12427  efival  12432  efmival  12433  sinhval  12434  coshval  12435  retanhcl  12439  tanhlt1  12440  tanhbnd  12441  efeul  12442  sinadd  12444  cosadd  12445  sinsub  12448  cossub  12449  subsin  12451  sinmul  12452  cosmul  12453  addcos  12454  subcos  12455  cos2tsin  12459  ef01bndlem  12464  sin01bnd  12465  cos01bnd  12466  absef  12477  absefib  12478  efieq1re  12479  demoivre  12480  demoivreALT  12481  dvdscmulr  12557  dvdsmulcr  12558  odd2np1lem  12586  odd2np1  12587  gcdaddm  12708  modgcd  12715  bezoutlem1  12717  qredeq  12785  eulerthlem2  12850  opoe  12864  omoe  12865  opeo  12866  omeo  12867  pythagtriplem1  12869  pythagtriplem12  12879  pythagtriplem14  12881  iserodd  12888  gzmulcl  12985  4sqlem11  13002  4sqlem17  13008  cncrng  16395  cnfldmulg  16406  cnsubrg  16432  mulc1cncf  18409  icccvx  18448  pcorevlem  18524  itgcnlem  19144  itgneg  19158  itgconst  19173  itgadd  19179  iblabs  19183  itgmulc2  19188  dvmulbr  19288  dvmulf  19292  dvsincos  19328  plymullem1  19596  plymulcl  19603  plysubcl  19604  dgrcolem1  19654  dgrcolem2  19655  plydivlem4  19676  quotlem  19680  quotcl2  19682  quotdgr  19683  aaliou3lem3  19724  efper  19847  sinperlem  19848  sin2kpi  19851  cos2kpi  19852  efimpi  19859  sincosq1eq  19880  pige3  19885  abssinper  19886  sinkpi  19887  coskpi  19888  sineq0  19889  coseq1  19890  tanregt0  19901  efgh  19903  efif1olem4  19907  efifo  19909  eff1olem  19910  lognegb  19943  eflogeq  19955  efiarg  19961  tanarg  19970  logf1o2  19997  cxpcl  20021  cxpne0  20024  cxpsqrlem  20049  cxpsqr  20050  dvcxp1  20082  root1eq1  20095  cxpeq  20097  quad2  20135  quad  20136  dcubic2  20140  dcubic1  20141  dcubic  20142  mcubic  20143  cubic2  20144  cubic  20145  binom4  20146  dquartlem1  20147  dquartlem2  20148  dquart  20149  quart1cl  20150  quart1lem  20151  quart1  20152  quartlem1  20153  quartlem2  20154  quartlem3  20155  quart  20157  asinlem  20164  asinlem2  20165  asinlem3a  20166  asinlem3  20167  asinf  20168  atandm2  20173  atanf  20176  asinneg  20182  efiasin  20184  sinasin  20185  asinsinlem  20187  asinsin  20188  asinbnd  20195  cosasin  20200  atanneg  20203  atancj  20206  efiatan  20208  atanlogaddlem  20209  atanlogadd  20210  atanlogsublem  20211  atanlogsub  20212  efiatan2  20213  2efiatan  20214  tanatan  20215  cosatan  20217  atantan  20219  atanbndlem  20221  atans2  20227  dvatan  20231  atantayl  20233  atantayl2  20234  leibpilem1  20236  leibpilem2  20237  efrlim  20264  ftalem7  20316  basellem3  20320  basellem7  20324  basellem8  20325  basellem9  20326  ppiub  20443  dchrmulcl  20488  bposlem9  20531  lgsdir  20569  lgsdilem2  20570  lgsdi  20571  lgsne0  20572  lgsquadlem1  20593  2sqlem2  20603  rpvmasum2  20661  dchrisum0lem1  20665  dchrisum0lem2  20667  mulogsumlem  20680  mulog2sumlem3  20685  log2sumbnd  20693  selberglem1  20694  selberglem2  20695  selberg2  20700  pntlemk  20755  ablomul  21022  efghgrp  21040  smcnlem  21270  ipval2  21280  4ipval2  21281  4ipval3  21285  ipidsq  21286  dipcj  21290  cncph  21397  ipasslem2  21410  ipasslem4  21412  ipasslem8  21415  ipasslem9  21416  ipasslem11  21418  hhssnv  21841  spansncol  22147  homulass  22382  lnfnmuli  22624  riesz3i  22642  zetacvg  23689  dmgmseqn0  23696  circum  24007  mulcan1g  24084  colinearalglem1  24534  colinearalglem2  24535  ax5seglem1  24556  axcontlem2  24593  axcontlem8  24599  bpoly3  24793  fsumcube  24795  mslb1  25607  2wsms  25608  cnegvex2  25660  clsmulcv  25682  fnmulcv  25684  mulmulvec  25687  cntotbnd  26520  rmxluc  27021  rmyluc  27022  jm2.17a  27047  jm2.18  27081  jm3.1lem1  27110  jm3.1lem2  27111  proot1ex  27520  lhe4.4ex1a  27546  expgrowthi  27550  expgrowth  27552  stoweidlem1  27750  stoweidlem10  27759  stoweidlem11  27760  stoweidlem13  27762  stoweidlem14  27763  stoweidlem17  27766  stoweidlem25  27774  stoweidlem26  27775  stoweidlem42  27791  wallispi2lem1  27820  wallispi2  27822  sinh-conventional  28209  dpfrac1  28242
This theorem was proved from axioms:  ax-mulcl 8799
  Copyright terms: Public domain W3C validator