Theorem mulcl 11120

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034   · cmul 11041

This theorem was proved from axioms:  ax-mulcl 11098

This theorem is referenced by:  mpomulf  11131  0cn  11134  mulrid  11140  mulcli  11150  mulcld  11163  mul31  11311  mul4  11312  mul02  11322  cnegex2  11326  muladd11r  11357  muladd  11580  subdi  11581  submul2  11588  mulsub  11591  recextlem1  11778  recex  11780  muleqadd  11792  mulnzcnf  11794  mulcan1g  11801  divass  11825  divmulass  11830  divmuldiv  11853  divmuleq  11858  divadddiv  11868  conjmul  11870  cju  12153  zneo  12610  cnref1o  12933  modcyc2  13864  muladdmodid  13870  negmod  13876  modaddmulmod  13898  expcl  14039  expclzlem  14043  mulexp  14061  sqcl  14078  subsq  14170  subsq2  14171  binom2sub  14180  mulbinom2  14183  binom3  14184  zesq  14186  bernneq  14189  bernneq2  14190  mulsubdivbinom2  14222  bcval5  14278  reim  15069  imcl  15071  crre  15074  crim  15075  remim  15077  mulre  15081  cjreb  15083  recj  15084  reneg  15085  readd  15086  remullem  15088  remul2  15090  imcj  15092  imneg  15093  imadd  15094  immul2  15097  cjadd  15101  ipcnval  15103  cjmulrcl  15104  cjneg  15107  imval2  15111  cjreim  15120  rennim  15199  cnpart  15200  sqrtneg  15227  sqabsadd  15242  sqabssub  15243  absreimsq  15252  absreim  15253  absmul  15254  sqreulem  15320  sqreu  15321  mulcn2  15556  o1mul  15575  climmul  15593  iseraltlem2  15643  prodf  15850  clim2div  15852  prodfmul  15853  prodfn0  15857  prodfrec  15858  prodfdiv  15859  prodmolem3  15896  prodmolem2a  15897  fprodcl  15915  fprodclf  15955  risefaccl  15978  fallfaccl  15979  bpoly3  16021  fsumcube  16023  efexp  16066  sinf  16089  cosf  16090  tanval2  16098  tanval3  16099  resinval  16100  recosval  16101  efi4p  16102  resin4p  16103  recos4p  16104  resincl  16105  recoscl  16106  sinneg  16111  cosneg  16112  efival  16117  efmival  16118  sinhval  16119  coshval  16120  retanhcl  16124  tanhlt1  16125  tanhbnd  16126  efeul  16127  sinadd  16129  cosadd  16130  sinsub  16133  cossub  16134  subsin  16136  sinmul  16137  cosmul  16138  addcos  16139  subcos  16140  cos2tsin  16144  ef01bndlem  16149  sin01bnd  16150  cos01bnd  16151  absef  16162  absefib  16163  efieq1re  16164  demoivre  16165  demoivreALT  16166  dvdscmulr  16251  dvdsmulcr  16252  odd2np1lem  16307  odd2np1  16308  opoe  16330  omoe  16331  opeo  16332  omeo  16333  gcdaddm  16492  modgcd  16499  bezoutlem1  16506  qredeq  16624  eulerthlem2  16750  modprm0  16774  pythagtriplem1  16785  pythagtriplem12  16795  pythagtriplem14  16797  iserodd  16804  gzmulcl  16907  4sqlem11  16924  4sqlem17  16930  cncrng  21375  cnfldmulg  21386  cnsubrg  21409  mpomulcn  24859  mulc1cncf  24897  icccvx  24942  pcorevlem  25018  cnlmod  25132  cnstrcvs  25133  cncvs  25137  itgcnlem  25782  itgneg  25796  itgconst  25811  itgadd  25817  iblabs  25821  itgmulc2  25826  dvmulbr  25931  dvmulf  25935  dvsincos  25973  plymullem1  26204  plymulcl  26211  plysubcl  26212  dgrcolem1  26263  dgrcolem2  26264  plydivlem4  26287  quotlem  26291  quotcl2  26293  quotdgr  26294  aaliou3lem3  26335  efper  26468  sinperlem  26469  sin2kpi  26472  cos2kpi  26473  efimpi  26480  sincosq1eq  26501  pige3ALT  26509  abssinper  26510  sinkpi  26511  coskpi  26512  sineq0  26513  coseq1  26514  tanregt0  26528  efif1olem4  26534  efifo  26536  eff1olem  26537  lognegb  26579  eflogeq  26591  efiarg  26596  tanarg  26608  logf1o2  26639  cxpcl  26663  cxpne0  26666  cxpsqrtlem  26691  cxpsqrt  26692  dvcxp1  26729  dvcncxp1  26732  root1eq1  26744  cxpeq  26746  relogbmul  26766  quad2  26828  quad  26829  dcubic2  26833  dcubic1  26834  dcubic  26835  mcubic  26836  cubic2  26837  cubic  26838  binom4  26839  dquartlem1  26840  dquartlem2  26841  dquart  26842  quart1cl  26843  quart1lem  26844  quart1  26845  quartlem1  26846  quartlem2  26847  quartlem3  26848  quart  26850  asinlem  26857  asinlem2  26858  asinlem3a  26859  asinlem3  26860  asinf  26861  atandm2  26866  atanf  26869  asinneg  26875  efiasin  26877  sinasin  26878  asinsinlem  26880  asinsin  26881  asinbnd  26888  cosasin  26893  atanneg  26896  atancj  26899  efiatan  26901  atanlogaddlem  26902  atanlogadd  26903  atanlogsublem  26904  atanlogsub  26905  efiatan2  26906  2efiatan  26907  tanatan  26908  cosatan  26910  atantan  26912  atanbndlem  26914  atans2  26920  dvatan  26924  atantayl  26926  atantayl2  26927  leibpilem2  26930  efrlim  26958  zetacvg  27003  ftalem7  27067  basellem3  27071  basellem7  27075  basellem8  27076  basellem9  27077  ppiub  27192  dchrmulcl  27237  bposlem9  27280  lgsdir  27320  lgsdilem2  27321  lgsdi  27322  lgsne0  27323  lgsquadlem1  27368  2sqlem2  27406  rpvmasum2  27500  dchrisum0lem1  27504  dchrisum0lem2  27506  mulogsumlem  27519  mulog2sumlem3  27524  log2sumbnd  27532  selberglem1  27533  selberglem2  27534  selberg2  27539  pntlemk  27594  colinearalglem1  29000  colinearalglem2  29001  ax5seglem1  29022  axcontlem2  29059  axcontlem8  29065  numclwwlk3lem1  30477  smcnlem  30793  ipval2  30803  4ipval2  30804  ipidsq  30806  dipcj  30810  cncph  30915  ipasslem2  30928  ipasslem4  30930  ipasslem9  30934  ipasslem11  30936  hhssnv  31360  spansncol  31664  homulass  31898  lnfnmuli  32140  riesz3i  32158  circum  35909  faclim  35981  mpomulnzcnf  36534  sin2h  37984  cos2h  37985  itg2addnclem3  38047  itgaddnc  38054  iblabsnc  38058  iblmulc2nc  38059  itgmulc2nc  38062  ftc1anclem3  38069  ftc1anclem6  38072  ftc1anclem7  38073  ftc1anclem8  38074  ftc1anc  38075  dvasin  38078  cntotbnd  38170  rmxluc  43388  rmyluc  43389  jm2.17a  43412  jm2.18  43440  jm3.1lem1  43469  jm3.1lem2  43470  proot1ex  43648  lhe4.4ex1a  44780  expgrowthi  44784  expgrowth  44786  binomcxplemnotnn0  44807  dvsinax  46363  dvasinbx  46370  dvcosax  46376  stoweidlem10  46460  wallispi2lem1  46521  wallispi2  46523  fouriersw  46681  sinnpoly  47361  m1modmmod  47834  dfodd6  48135  opoeALTV  48181  opeoALTV  48182  2zrngnmrid  48754  sinh-conventional  50236  amgmwlem  50299