Theorem mulcl 11265

Description: Alias for ax-mulcl 11243, for naming consistency with mulcli 11297. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
mulcl	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)

Proof of Theorem mulcl

Step	Hyp	Ref	Expression
1		ax-mulcl 11243	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  (class class class)co 7412  ℂcc 11179   · cmul 11186

This proof depends on axioms:  ax-mulcl 11243

This theorem is used by:  mpomulf  11276  0cn  11279  mulrid  11287  mulcli  11297  mulcld  11310  mul31  11458  mul4  11459  mul02  11469  cnegex2  11473  muladd11r  11504  muladd  11729  subdi  11730  submul2  11737  mulsub  11740  recextlem1  11927  recex  11929  muleqadd  11941  mulnzcnf  11943  mulcan1g  11950  divass  11973  divmulass  11978  divmuldiv  11998  divmuleq  12003  divadddiv  12013  conjmul  12015  cju  12297  zneo  12763  cnref1o  13094  modcyc2  14027  muladdmodid  14033  negmod  14039  modaddmulmod  14061  expcl  14202  expclzlem  14206  mulexp  14224  sqcl  14241  subsq  14334  subsq2  14335  binom2sub  14344  mulbinom2  14347  binom3  14348  zesq  14350  bernneq  14353  bernneq2  14354  mulsubdivbinom2  14386  bcval5  14442  reim  15256  imcl  15258  crre  15261  crim  15262  remim  15264  mulre  15268  cjreb  15270  recj  15271  reneg  15272  readd  15273  remullem  15275  remul2  15277  imcj  15279  imneg  15280  imadd  15281  immul2  15284  cjadd  15288  ipcnval  15290  cjmulrcl  15291  cjneg  15294  imval2  15298  cjreim  15307  rennim  15386  cnpart  15387  sqrtneg  15414  sqabsadd  15429  sqabssub  15430  absreimsq  15439  absreim  15440  absmul  15441  sqreulem  15507  sqreu  15508  mulcn2  15743  o1mul  15762  climmul  15780  iseraltlem2  15830  prodf  16036  clim2div  16038  prodfmul  16039  prodfn0  16043  prodfrec  16044  prodfdiv  16045  prodmolem3  16080  prodmolem2a  16081  fprodcl  16099  fprodclf  16139  risefaccl  16162  fallfaccl  16163  bpoly3  16204  fsumcube  16206  efexp  16249  sinf  16272  cosf  16273  tanval2  16281  tanval3  16282  resinval  16283  recosval  16284  efi4p  16285  resin4p  16286  recos4p  16287  resincl  16288  recoscl  16289  sinneg  16294  cosneg  16295  efival  16300  efmival  16301  sinhval  16302  coshval  16303  retanhcl  16307  tanhlt1  16308  tanhbnd  16309  efeul  16310  sinadd  16312  cosadd  16313  sinsub  16316  cossub  16317  subsin  16319  sinmul  16320  cosmul  16321  addcos  16322  subcos  16323  cos2tsin  16327  ef01bndlem  16332  sin01bnd  16333  cos01bnd  16334  absef  16345  absefib  16346  efieq1re  16347  demoivre  16348  demoivreALT  16349  dvdscmulr  16434  dvdsmulcr  16435  odd2np1lem  16490  odd2np1  16491  opoe  16513  omoe  16514  opeo  16515  omeo  16516  gcdaddm  16677  modgcd  16685  bezoutlem1  16692  qredeq  16812  eulerthlem2  16939  modprm0  16963  pythagtriplem1  16974  pythagtriplem12  16984  pythagtriplem14  16986  iserodd  16993  gzmulcl  17096  4sqlem11  17113  4sqlem17  17119  cncrng  21679  cnfldmulg  21690  cnsubrg  21713  mpomulcn  25168  mulc1cncf  25206  icccvx  25251  pcorevlem  25327  cnlmod  25441  cnstrcvs  25442  cncvs  25446  itgcnlem  26090  itgneg  26104  itgconst  26119  itgadd  26125  iblabs  26129  itgmulc2  26134  dvmulbr  26239  dvmulf  26243  dvsincos  26281  plymullem1  26513  plymulcl  26520  plysubcl  26521  dgrcolem1  26572  dgrcolem2  26573  plydivlem4  26599  quotlem  26603  quotcl2  26605  quotdgr  26606  aaliou3lem3  26653  efper  26790  sinperlem  26791  sin2kpi  26794  cos2kpi  26795  efimpi  26802  sincosq1eq  26823  pige3ALT  26830  abssinper  26831  sinkpi  26832  coskpi  26833  sineq0  26834  coseq1  26835  tanregt0  26849  efif1olem4  26855  efifo  26857  eff1olem  26858  lognegb  26900  eflogeq  26912  efiarg  26917  tanarg  26929  logf1o2  26960  cxpcl  26984  cxpne0  26987  cxpsqrtlem  27012  cxpsqrt  27013  dvcxp1  27050  dvcncxp1  27053  root1eq1  27065  cxpeq  27067  relogbmul  27087  quad2  27149  quad  27150  dcubic2  27154  dcubic1  27155  dcubic  27156  mcubic  27157  cubic2  27158  cubic  27159  binom4  27160  dquartlem1  27161  dquartlem2  27162  dquart  27163  quart1cl  27164  quart1lem  27165  quart1  27166  quartlem1  27167  quartlem2  27168  quartlem3  27169  quart  27171  asinlem  27178  asinlem2  27179  asinlem3a  27180  asinlem3  27181  asinf  27182  atandm2  27187  atanf  27190  asinneg  27196  efiasin  27198  sinasin  27199  asinsinlem  27201  asinsin  27202  asinbnd  27209  cosasin  27214  atanneg  27217  atancj  27220  efiatan  27222  atanlogaddlem  27223  atanlogadd  27224  atanlogsublem  27225  atanlogsub  27226  efiatan2  27227  2efiatan  27228  tanatan  27229  cosatan  27231  atantan  27233  atanbndlem  27235  atans2  27241  dvatan  27245  atantayl  27247  atantayl2  27248  leibpilem2  27251  efrlim  27279  zetacvg  27324  ftalem7  27388  basellem3  27392  basellem7  27396  basellem8  27397  basellem9  27398  ppiub  27513  dchrmulcl  27558  bposlem9  27601  lgsdir  27641  lgsdilem2  27642  lgsdi  27643  lgsne0  27644  lgsquadlem1  27689  2sqlem2  27727  rpvmasum2  27821  dchrisum0lem1  27825  dchrisum0lem2  27827  mulogsumlem  27840  mulog2sumlem3  27845  log2sumbnd  27853  selberglem1  27854  selberglem2  27855  selberg2  27860  pntlemk  27915  colinearalglem1  29466  colinearalglem2  29467  ax5seglem1  29488  axcontlem2  29525  axcontlem8  29531  numclwwlk3lem1  30965  smcnlem  31281  ipval2  31291  4ipval2  31292  ipidsq  31294  dipcj  31298  cncph  31403  ipasslem2  31416  ipasslem4  31418  ipasslem9  31422  ipasslem11  31424  hhssnv  31848  spansncol  32152  homulass  32386  lnfnmuli  32628  riesz3i  32646  circum  36408  faclim  36480  mpomulnzcnf  37058  sin2h  38501  cos2h  38502  itg2addnclem3  38559  itgaddnc  38566  iblabsnc  38570  iblmulc2nc  38571  itgmulc2nc  38574  ftc1anclem3  38581  ftc1anclem6  38584  ftc1anclem7  38585  ftc1anclem8  38586  ftc1anc  38587  dvasin  38590  cntotbnd  38698  rmxluc  43896  rmyluc  43897  jm2.17a  43920  jm2.18  43948  jm3.1lem1  43977  jm3.1lem2  43978  proot1ex  44156  lhe4.4ex1a  45272  expgrowthi  45276  expgrowth  45278  binomcxplemnotnn0  45299  dvsinax  46867  dvasinbx  46874  dvcosax  46880  stoweidlem10  46964  wallispi2lem1  47025  wallispi2  47027  fouriersw  47185  sinnpoly  47885  m1modmmod  48378  dfodd6  48679  opoeALTV  48725  opeoALTV  48726  2zrngnmrid  49297  sinh-conventional  50776  amgmwlem  50931