Theorem mulcl 8270

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205  (class class class)co 6058  ℂcc 8141   · cmul 8148

This theorem was proved from axioms:  ax-mulcl 8241

This theorem is referenced by:  mpomulf  8280  0cn  8282  mulrid  8287  mulcli  8295  mulcld  8310  mul31  8420  mul4  8421  muladd11r  8445  cnegexlem2  8465  cnegex  8467  muladd  8674  subdi  8675  mul02  8677  submul2  8689  mulsub  8691  recextlem1  8942  recexap  8944  muleqadd  8959  divassap  8981  divmulassap  8986  divmuldivap  9003  divmuleqap  9008  divadddivap  9018  conjmulap  9020  cju  9252  ofnegsub  9253  zneo  9697  exp3vallem  10926  exp3val  10927  exp1  10931  expp1  10932  expcl  10943  expclzaplem  10949  mulexp  10964  sqcl  10986  subsq  11032  subsq2  11033  binom2sub  11039  mulbinom2  11042  binom3  11043  zesq  11045  bernneq  11047  bernneq2  11048  mulsubdivbinom2ap  11098  facnn  11114  fac0  11115  fac1  11116  facp1  11117  bcval5  11150  bcn2  11151  reim  11562  imcl  11564  crre  11567  crim  11568  remim  11570  mulreap  11574  cjreb  11576  recj  11577  reneg  11578  readd  11579  remullem  11581  remul2  11583  imcj  11585  imneg  11586  imadd  11587  immul2  11590  cjadd  11594  ipcnval  11596  cjmulrcl  11597  cjneg  11600  imval2  11604  cjreim  11613  rennim  11712  sqabsadd  11765  sqabssub  11766  absreimsq  11777  absreim  11778  absmul  11779  mul0inf  11951  mulcn2  12022  climmul  12037  isermulc2  12050  fsummulc2  12159  prodf  12249  clim2prod  12250  clim2divap  12251  prod3fmul  12252  prodf1  12253  prodfap0  12256  prodfrecap  12257  prodrbdclem  12282  fproddccvg  12283  prodmodclem3  12286  prodmodclem2a  12287  zproddc  12290  fprodseq  12294  fprodntrivap  12295  prodsnf  12303  fprodcl  12318  fprodclf  12346  efexp  12393  sinf  12415  cosf  12416  tanval2ap  12424  tanval3ap  12425  resinval  12426  recosval  12427  efi4p  12428  resin4p  12429  recos4p  12430  resincl  12431  recoscl  12432  sinneg  12437  cosneg  12438  efival  12443  efmival  12444  efeul  12445  sinadd  12447  cosadd  12448  sinsub  12451  cossub  12452  subsin  12454  sinmul  12455  cosmul  12456  addcos  12457  subcos  12458  cos2tsin  12462  ef01bndlem  12467  sin01bnd  12468  cos01bnd  12469  absef  12481  absefib  12482  efieq1re  12483  demoivre  12484  demoivreALT  12485  odd2np1lem  12583  odd2np1  12584  opoe  12606  omoe  12607  opeo  12608  omeo  12609  modgcd  12712  qredeq  12818  modprm0  12977  pythagtriplem1  12988  pythagtriplem12  12998  pythagtriplem14  13000  gzmulcl  13101  4sqlem11  13124  4sqlem17  13130  cncrng  14829  cnfldmulg  14836  mpomulcn  15543  mulc1cncf  15566  mulcncflem  15584  dvmulxxbr  15679  dvmulxx  15681  dvimulf  15683  plymullem1  15725  plymulcl  15732  plysubcl  15733  efper  15784  sinperlem  15785  sin2kpi  15788  cos2kpi  15789  efimpi  15796  sincosq1eq  15816  abssinper  15823  sinkpi  15824  coskpi  15825  binom4  15956  fsumdvdsmul  15971  lgsdilem2  16021  lgsne0  16023  lgsquadlem1  16062  2sqlem2  16100