Theorem mulcl 11268

Description: Alias for ax-mulcl 11246, 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 11246	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182   · cmul 11189

This theorem was proved from axioms:  ax-mulcl 11246

This theorem is referenced by:  mpomulf  11279  0cn  11282  mulrid  11288  mulcli  11297  mulcld  11310  mul31  11457  mul4  11458  mul02  11468  cnegex2  11472  muladd11r  11503  muladd  11722  subdi  11723  submul2  11730  mulsub  11733  recextlem1  11920  recex  11922  muleqadd  11934  mulnzcnf  11936  mulcan1g  11943  divass  11967  divmulass  11972  divmuldiv  11994  divmuleq  11999  divadddiv  12009  conjmul  12011  cju  12289  zneo  12726  cnref1o  13050  modcyc2  13958  muladdmodid  13962  negmod  13967  modaddmulmod  13989  expcl  14130  expclzlem  14134  mulexp  14152  sqcl  14168  subsq  14259  subsq2  14260  binom2sub  14269  mulbinom2  14272  binom3  14273  zesq  14275  bernneq  14278  bernneq2  14279  mulsubdivbinom2  14311  bcval5  14367  reim  15158  imcl  15160  crre  15163  crim  15164  remim  15166  mulre  15170  cjreb  15172  recj  15173  reneg  15174  readd  15175  remullem  15177  remul2  15179  imcj  15181  imneg  15182  imadd  15183  immul2  15186  cjadd  15190  ipcnval  15192  cjmulrcl  15193  cjneg  15196  imval2  15200  cjreim  15209  rennim  15288  cnpart  15289  sqrtneg  15316  sqabsadd  15331  sqabssub  15332  absreimsq  15341  absreim  15342  absmul  15343  sqreulem  15408  sqreu  15409  mulcn2  15642  o1mul  15661  climmul  15679  iseraltlem2  15731  prodf  15935  clim2div  15937  prodfmul  15938  prodfn0  15942  prodfrec  15943  prodfdiv  15944  prodmolem3  15981  prodmolem2a  15982  fprodcl  16000  fprodclf  16040  risefaccl  16063  fallfaccl  16064  bpoly3  16106  fsumcube  16108  efexp  16149  sinf  16172  cosf  16173  tanval2  16181  tanval3  16182  resinval  16183  recosval  16184  efi4p  16185  resin4p  16186  recos4p  16187  resincl  16188  recoscl  16189  sinneg  16194  cosneg  16195  efival  16200  efmival  16201  sinhval  16202  coshval  16203  retanhcl  16207  tanhlt1  16208  tanhbnd  16209  efeul  16210  sinadd  16212  cosadd  16213  sinsub  16216  cossub  16217  subsin  16219  sinmul  16220  cosmul  16221  addcos  16222  subcos  16223  cos2tsin  16227  ef01bndlem  16232  sin01bnd  16233  cos01bnd  16234  absef  16245  absefib  16246  efieq1re  16247  demoivre  16248  demoivreALT  16249  dvdscmulr  16333  dvdsmulcr  16334  odd2np1lem  16388  odd2np1  16389  opoe  16411  omoe  16412  opeo  16413  omeo  16414  gcdaddm  16571  modgcd  16579  bezoutlem1  16586  qredeq  16704  eulerthlem2  16829  modprm0  16852  pythagtriplem1  16863  pythagtriplem12  16873  pythagtriplem14  16875  iserodd  16882  gzmulcl  16985  4sqlem11  17002  4sqlem17  17008  cncrng  21424  cncrngOLD  21425  cnfldmulg  21439  cnsubrg  21468  mpomulcn  24910  mulc1cncf  24950  icccvx  25000  pcorevlem  25078  cnlmod  25192  cnstrcvs  25193  cncvs  25197  itgcnlem  25845  itgneg  25859  itgconst  25874  itgadd  25880  iblabs  25884  itgmulc2  25889  dvmulbr  25995  dvmulbrOLD  25996  dvmulf  26000  dvsincos  26039  plymullem1  26273  plymulcl  26280  plysubcl  26281  dgrcolem1  26333  dgrcolem2  26334  plydivlem4  26356  quotlem  26360  quotcl2  26362  quotdgr  26363  aaliou3lem3  26404  efper  26539  sinperlem  26540  sin2kpi  26543  cos2kpi  26544  efimpi  26551  sincosq1eq  26572  pige3ALT  26580  abssinper  26581  sinkpi  26582  coskpi  26583  sineq0  26584  coseq1  26585  tanregt0  26599  efif1olem4  26605  efifo  26607  eff1olem  26608  lognegb  26650  eflogeq  26662  efiarg  26667  tanarg  26679  logf1o2  26710  cxpcl  26734  cxpne0  26737  cxpsqrtlem  26762  cxpsqrt  26763  dvcxp1  26800  dvcncxp1  26803  root1eq1  26816  cxpeq  26818  relogbmul  26838  quad2  26900  quad  26901  dcubic2  26905  dcubic1  26906  dcubic  26907  mcubic  26908  cubic2  26909  cubic  26910  binom4  26911  dquartlem1  26912  dquartlem2  26913  dquart  26914  quart1cl  26915  quart1lem  26916  quart1  26917  quartlem1  26918  quartlem2  26919  quartlem3  26920  quart  26922  asinlem  26929  asinlem2  26930  asinlem3a  26931  asinlem3  26932  asinf  26933  atandm2  26938  atanf  26941  asinneg  26947  efiasin  26949  sinasin  26950  asinsinlem  26952  asinsin  26953  asinbnd  26960  cosasin  26965  atanneg  26968  atancj  26971  efiatan  26973  atanlogaddlem  26974  atanlogadd  26975  atanlogsublem  26976  atanlogsub  26977  efiatan2  26978  2efiatan  26979  tanatan  26980  cosatan  26982  atantan  26984  atanbndlem  26986  atans2  26992  dvatan  26996  atantayl  26998  atantayl2  26999  leibpilem2  27002  efrlim  27030  efrlimOLD  27031  zetacvg  27076  ftalem7  27140  basellem3  27144  basellem7  27148  basellem8  27149  basellem9  27150  ppiub  27266  dchrmulcl  27311  bposlem9  27354  lgsdir  27394  lgsdilem2  27395  lgsdi  27396  lgsne0  27397  lgsquadlem1  27442  2sqlem2  27480  rpvmasum2  27574  dchrisum0lem1  27578  dchrisum0lem2  27580  mulogsumlem  27593  mulog2sumlem3  27598  log2sumbnd  27606  selberglem1  27607  selberglem2  27608  selberg2  27613  pntlemk  27668  colinearalglem1  28939  colinearalglem2  28940  ax5seglem1  28961  axcontlem2  28998  axcontlem8  29004  numclwwlk3lem1  30414  smcnlem  30729  ipval2  30739  4ipval2  30740  ipidsq  30742  dipcj  30746  cncph  30851  ipasslem2  30864  ipasslem4  30866  ipasslem9  30870  ipasslem11  30872  hhssnv  31296  spansncol  31600  homulass  31834  lnfnmuli  32076  riesz3i  32094  circum  35642  faclim  35708  mpomulnzcnf  36265  sin2h  37570  cos2h  37571  itg2addnclem3  37633  itgaddnc  37640  iblabsnc  37644  iblmulc2nc  37645  itgmulc2nc  37648  ftc1anclem3  37655  ftc1anclem6  37658  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  dvasin  37664  cntotbnd  37756  fac2xp3  42196  rmxluc  42893  rmyluc  42894  jm2.17a  42917  jm2.18  42945  jm3.1lem1  42974  jm3.1lem2  42975  proot1ex  43157  lhe4.4ex1a  44298  expgrowthi  44302  expgrowth  44304  binomcxplemnotnn0  44325  dvsinax  45834  dvasinbx  45841  dvcosax  45847  stoweidlem10  45931  wallispi2lem1  45992  wallispi2  45994  fouriersw  46152  dfodd6  47511  opoeALTV  47557  opeoALTV  47558  2zrngnmrid  47979  m1modmmod  48255  sinh-conventional  48831  amgmwlem  48896