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

Theorem mulcl 10614
Description: Alias for ax-mulcl 10592, for naming consistency with mulcli 10641. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
mulcl ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)

Proof of Theorem mulcl
StepHypRef Expression
1 ax-mulcl 10592 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2112  (class class class)co 7139  cc 10528   · cmul 10535
This theorem was proved from axioms:  ax-mulcl 10592
This theorem is referenced by:  0cn  10626  mulid1  10632  mulcli  10641  mulcld  10654  mul31  10800  mul4  10801  mul02  10811  cnegex2  10815  muladd11r  10846  muladd  11065  subdi  11066  submul2  11073  mulsub  11076  recextlem1  11263  recex  11265  muleqadd  11277  mulnzcnopr  11279  mulcan1g  11286  divass  11309  divmulass  11314  divmuldiv  11333  divmuleq  11338  divadddiv  11348  conjmul  11350  cju  11625  zneo  12057  cnref1o  12376  modcyc2  13274  muladdmodid  13278  negmod  13283  modaddmulmod  13305  expcl  13447  expclzlem  13453  mulexp  13468  sqcl  13484  subsq  13572  subsq2  13573  binom2sub  13581  mulbinom2  13584  binom3  13585  zesq  13587  bernneq  13590  bernneq2  13591  mulsubdivbinom2  13622  bcval5  13678  reim  14464  imcl  14466  crre  14469  crim  14470  remim  14472  mulre  14476  cjreb  14478  recj  14479  reneg  14480  readd  14481  remullem  14483  remul2  14485  imcj  14487  imneg  14488  imadd  14489  immul2  14492  cjadd  14496  ipcnval  14498  cjmulrcl  14499  cjneg  14502  imval2  14506  cjreim  14515  rennim  14594  cnpart  14595  sqrtneg  14623  sqabsadd  14638  sqabssub  14639  absreimsq  14648  absreim  14649  absmul  14650  sqreulem  14715  sqreu  14716  mulcn2  14948  o1mul  14967  climmul  14985  iseraltlem2  15035  prodf  15239  clim2div  15241  prodfmul  15242  prodfn0  15246  prodfrec  15247  prodfdiv  15248  prodmolem3  15283  prodmolem2a  15284  fprodcl  15302  fprodclf  15342  risefaccl  15365  fallfaccl  15366  bpoly3  15408  fsumcube  15410  efexp  15450  sinf  15473  cosf  15474  tanval2  15482  tanval3  15483  resinval  15484  recosval  15485  efi4p  15486  resin4p  15487  recos4p  15488  resincl  15489  recoscl  15490  sinneg  15495  cosneg  15496  efival  15501  efmival  15502  sinhval  15503  coshval  15504  retanhcl  15508  tanhlt1  15509  tanhbnd  15510  efeul  15511  sinadd  15513  cosadd  15514  sinsub  15517  cossub  15518  subsin  15520  sinmul  15521  cosmul  15522  addcos  15523  subcos  15524  cos2tsin  15528  ef01bndlem  15533  sin01bnd  15534  cos01bnd  15535  absef  15546  absefib  15547  efieq1re  15548  demoivre  15549  demoivreALT  15550  dvdscmulr  15634  dvdsmulcr  15635  odd2np1lem  15685  odd2np1  15686  opoe  15708  omoe  15709  opeo  15710  omeo  15711  gcdaddm  15867  modgcd  15874  bezoutlem1  15881  qredeq  15995  eulerthlem2  16113  modprm0  16136  pythagtriplem1  16147  pythagtriplem12  16157  pythagtriplem14  16159  iserodd  16166  gzmulcl  16268  4sqlem11  16285  4sqlem17  16291  cncrng  20116  cnfldmulg  20127  cnsubrg  20155  mulc1cncf  23514  icccvx  23559  pcorevlem  23635  cnlmod  23749  cnstrcvs  23750  cncvs  23754  itgcnlem  24397  itgneg  24411  itgconst  24426  itgadd  24432  iblabs  24436  itgmulc2  24441  dvmulbr  24546  dvmulf  24550  dvsincos  24588  plymullem1  24815  plymulcl  24822  plysubcl  24823  dgrcolem1  24874  dgrcolem2  24875  plydivlem4  24896  quotlem  24900  quotcl2  24902  quotdgr  24903  aaliou3lem3  24944  efper  25076  sinperlem  25077  sin2kpi  25080  cos2kpi  25081  efimpi  25088  sincosq1eq  25109  pige3ALT  25116  abssinper  25117  sinkpi  25118  coskpi  25119  sineq0  25120  coseq1  25121  tanregt0  25135  efif1olem4  25141  efifo  25143  eff1olem  25144  lognegb  25185  eflogeq  25197  efiarg  25202  tanarg  25214  logf1o2  25245  cxpcl  25269  cxpne0  25272  cxpsqrtlem  25297  cxpsqrt  25298  dvcxp1  25333  dvcncxp1  25336  root1eq1  25348  cxpeq  25350  relogbmul  25367  quad2  25429  quad  25430  dcubic2  25434  dcubic1  25435  dcubic  25436  mcubic  25437  cubic2  25438  cubic  25439  binom4  25440  dquartlem1  25441  dquartlem2  25442  dquart  25443  quart1cl  25444  quart1lem  25445  quart1  25446  quartlem1  25447  quartlem2  25448  quartlem3  25449  quart  25451  asinlem  25458  asinlem2  25459  asinlem3a  25460  asinlem3  25461  asinf  25462  atandm2  25467  atanf  25470  asinneg  25476  efiasin  25478  sinasin  25479  asinsinlem  25481  asinsin  25482  asinbnd  25489  cosasin  25494  atanneg  25497  atancj  25500  efiatan  25502  atanlogaddlem  25503  atanlogadd  25504  atanlogsublem  25505  atanlogsub  25506  efiatan2  25507  2efiatan  25508  tanatan  25509  cosatan  25511  atantan  25513  atanbndlem  25515  atans2  25521  dvatan  25525  atantayl  25527  atantayl2  25528  leibpilem2  25531  efrlim  25559  zetacvg  25604  ftalem7  25668  basellem3  25672  basellem7  25676  basellem8  25677  basellem9  25678  ppiub  25792  dchrmulcl  25837  bposlem9  25880  lgsdir  25920  lgsdilem2  25921  lgsdi  25922  lgsne0  25923  lgsquadlem1  25968  2sqlem2  26006  rpvmasum2  26100  dchrisum0lem1  26104  dchrisum0lem2  26106  mulogsumlem  26119  mulog2sumlem3  26124  log2sumbnd  26132  selberglem1  26133  selberglem2  26134  selberg2  26139  pntlemk  26194  colinearalglem1  26704  colinearalglem2  26705  ax5seglem1  26726  axcontlem2  26763  axcontlem8  26769  numclwwlk3lem1  28171  smcnlem  28484  ipval2  28494  4ipval2  28495  ipidsq  28497  dipcj  28501  cncph  28606  ipasslem2  28619  ipasslem4  28621  ipasslem9  28625  ipasslem11  28627  hhssnv  29051  spansncol  29355  homulass  29589  lnfnmuli  29831  riesz3i  29849  circum  33031  faclim  33092  sin2h  35046  cos2h  35047  itg2addnclem3  35109  itgaddnc  35116  iblabsnc  35120  iblmulc2nc  35121  itgmulc2nc  35124  ftc1anclem3  35131  ftc1anclem6  35134  ftc1anclem7  35135  ftc1anclem8  35136  ftc1anc  35137  dvasin  35140  cntotbnd  35233  fac2xp3  39378  rmxluc  39870  rmyluc  39871  jm2.17a  39894  jm2.18  39922  jm3.1lem1  39951  jm3.1lem2  39952  proot1ex  40138  lhe4.4ex1a  41026  expgrowthi  41030  expgrowth  41032  binomcxplemnotnn0  41053  dvsinax  42548  dvasinbx  42555  dvcosax  42561  stoweidlem10  42645  wallispi2lem1  42706  wallispi2  42708  fouriersw  42866  dfodd6  44148  opoeALTV  44194  opeoALTV  44195  2zrngnmrid  44567  m1modmmod  44928  sinh-conventional  45258  amgmwlem  45323
  Copyright terms: Public domain W3C validator