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

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

Proof of Theorem mulcl
StepHypRef Expression
1 ax-mulcl 10190 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2139  (class class class)co 6813  cc 10126   · cmul 10133
This theorem was proved from axioms:  ax-mulcl 10190
This theorem is referenced by:  0cn  10224  mulid1  10229  mulcli  10237  mulcld  10252  mul31  10396  mul4  10397  mul02  10406  cnegex2  10410  muladd11r  10441  muladd  10654  subdi  10655  submul2  10662  mulsub  10665  recextlem1  10849  recex  10851  muleqadd  10863  mulnzcnopr  10865  mulcan1g  10872  divass  10895  divmulass  10900  divmuldiv  10917  divmuleq  10922  divadddiv  10932  conjmul  10934  cju  11208  zneo  11652  cnref1o  12020  modcyc2  12900  muladdmodid  12904  negmod  12909  modaddmulmod  12931  expcl  13072  expclzlem  13078  mulexp  13093  sqcl  13119  subsq  13166  subsq2  13167  binom2sub  13175  mulbinom2  13178  binom3  13179  zesq  13181  bernneq  13184  bernneq2  13185  mulsubdivbinom2  13240  bcval5  13299  reim  14048  imcl  14050  crre  14053  crim  14054  remim  14056  mulre  14060  cjreb  14062  recj  14063  reneg  14064  readd  14065  remullem  14067  remul2  14069  imcj  14071  imneg  14072  imadd  14073  immul2  14076  cjadd  14080  ipcnval  14082  cjmulrcl  14083  cjneg  14086  imval2  14090  cjreim  14099  rennim  14178  cnpart  14179  sqrtneg  14207  sqabsadd  14221  sqabssub  14222  absreimsq  14231  absreim  14232  absmul  14233  sqreulem  14298  sqreu  14299  mulcn2  14525  o1mul  14544  climmul  14562  iseraltlem2  14612  prodf  14818  clim2div  14820  prodfmul  14821  prodfn0  14825  prodfrec  14826  prodfdiv  14827  prodmolem3  14862  prodmolem2a  14863  fprodcl  14881  fprodclf  14922  risefaccl  14945  fallfaccl  14946  bpoly3  14988  fsumcube  14990  efexp  15030  sinf  15053  cosf  15054  tanval2  15062  tanval3  15063  resinval  15064  recosval  15065  efi4p  15066  resin4p  15067  recos4p  15068  resincl  15069  recoscl  15070  sinneg  15075  cosneg  15076  efival  15081  efmival  15082  sinhval  15083  coshval  15084  retanhcl  15088  tanhlt1  15089  tanhbnd  15090  efeul  15091  sinadd  15093  cosadd  15094  sinsub  15097  cossub  15098  subsin  15100  sinmul  15101  cosmul  15102  addcos  15103  subcos  15104  cos2tsin  15108  ef01bndlem  15113  sin01bnd  15114  cos01bnd  15115  absef  15126  absefib  15127  efieq1re  15128  demoivre  15129  demoivreALT  15130  dvdscmulr  15212  dvdsmulcr  15213  odd2np1lem  15266  odd2np1  15267  opoe  15289  omoe  15290  opeo  15291  omeo  15292  gcdaddm  15448  modgcd  15455  bezoutlem1  15458  qredeq  15573  eulerthlem2  15689  modprm0  15712  pythagtriplem1  15723  pythagtriplem12  15733  pythagtriplem14  15735  iserodd  15742  gzmulcl  15844  4sqlem11  15861  4sqlem17  15867  cncrng  19969  cnfldmulg  19980  cnsubrg  20008  mulc1cncf  22909  icccvx  22950  pcorevlem  23026  cnlmod  23140  cnstrcvs  23141  cncvs  23145  itgcnlem  23755  itgneg  23769  itgconst  23784  itgadd  23790  iblabs  23794  itgmulc2  23799  dvmulbr  23901  dvmulf  23905  dvsincos  23943  plymullem1  24169  plymulcl  24176  plysubcl  24177  dgrcolem1  24228  dgrcolem2  24229  plydivlem4  24250  quotlem  24254  quotcl2  24256  quotdgr  24257  aaliou3lem3  24298  efper  24430  sinperlem  24431  sin2kpi  24434  cos2kpi  24435  efimpi  24442  sincosq1eq  24463  pige3  24468  abssinper  24469  sinkpi  24470  coskpi  24471  sineq0  24472  coseq1  24473  tanregt0  24484  efif1olem4  24490  efifo  24492  eff1olem  24493  lognegb  24535  eflogeq  24547  efiarg  24552  tanarg  24564  logf1o2  24595  cxpcl  24619  cxpne0  24622  cxpsqrtlem  24647  cxpsqrt  24648  dvcxp1  24680  dvcncxp1  24683  root1eq1  24695  cxpeq  24697  relogbmul  24714  quad2  24765  quad  24766  dcubic2  24770  dcubic1  24771  dcubic  24772  mcubic  24773  cubic2  24774  cubic  24775  binom4  24776  dquartlem1  24777  dquartlem2  24778  dquart  24779  quart1cl  24780  quart1lem  24781  quart1  24782  quartlem1  24783  quartlem2  24784  quartlem3  24785  quart  24787  asinlem  24794  asinlem2  24795  asinlem3a  24796  asinlem3  24797  asinf  24798  atandm2  24803  atanf  24806  asinneg  24812  efiasin  24814  sinasin  24815  asinsinlem  24817  asinsin  24818  asinbnd  24825  cosasin  24830  atanneg  24833  atancj  24836  efiatan  24838  atanlogaddlem  24839  atanlogadd  24840  atanlogsublem  24841  atanlogsub  24842  efiatan2  24843  2efiatan  24844  tanatan  24845  cosatan  24847  atantan  24849  atanbndlem  24851  atans2  24857  dvatan  24861  atantayl  24863  atantayl2  24864  leibpilem1  24866  leibpilem2  24867  efrlim  24895  zetacvg  24940  ftalem7  25004  basellem3  25008  basellem7  25012  basellem8  25013  basellem9  25014  ppiub  25128  dchrmulcl  25173  bposlem9  25216  lgsdir  25256  lgsdilem2  25257  lgsdi  25258  lgsne0  25259  lgsquadlem1  25304  2sqlem2  25342  rpvmasum2  25400  dchrisum0lem1  25404  dchrisum0lem2  25406  mulogsumlem  25419  mulog2sumlem3  25424  log2sumbnd  25432  selberglem1  25433  selberglem2  25434  selberg2  25439  pntlemk  25494  colinearalglem1  25985  colinearalglem2  25986  ax5seglem1  26007  axcontlem2  26044  axcontlem8  26050  numclwlk3lem3  27496  smcnlem  27861  ipval2  27871  4ipval2  27872  ipidsq  27874  dipcj  27878  cncph  27983  ipasslem2  27996  ipasslem4  27998  ipasslem9  28002  ipasslem11  28004  hhssnv  28430  spansncol  28736  homulass  28970  lnfnmuli  29212  riesz3i  29230  dpfrac1OLD  29909  circum  31875  faclim  31939  sin2h  33712  cos2h  33713  itg2addnclem3  33776  itgaddnc  33783  iblabsnc  33787  iblmulc2nc  33788  itgmulc2nc  33791  ftc1anclem3  33800  ftc1anclem6  33803  ftc1anclem7  33804  ftc1anclem8  33805  ftc1anc  33806  dvasin  33809  cntotbnd  33908  rmxluc  38003  rmyluc  38004  jm2.17a  38029  jm2.18  38057  jm3.1lem1  38086  jm3.1lem2  38087  proot1ex  38281  lhe4.4ex1a  39030  expgrowthi  39034  expgrowth  39036  binomcxplemnotnn0  39057  dvsinax  40630  dvasinbx  40638  dvcosax  40644  stoweidlem10  40730  wallispi2lem1  40791  wallispi2  40793  fouriersw  40951  dfodd6  42060  opoeALTV  42104  opeoALTV  42105  2zrngnmrid  42460  m1modmmod  42826  sinh-conventional  42993  amgmwlem  43061
  Copyright terms: Public domain W3C validator