Theorem mulcl 8006

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167  (class class class)co 5922  ℂcc 7877   · cmul 7884

This theorem was proved from axioms:  ax-mulcl 7977

This theorem is referenced by:  mpomulf  8016  0cn  8018  mulrid  8023  mulcli  8031  mulcld  8047  mul31  8157  mul4  8158  muladd11r  8182  cnegexlem2  8202  cnegex  8204  muladd  8410  subdi  8411  mul02  8413  submul2  8425  mulsub  8427  recextlem1  8678  recexap  8680  muleqadd  8695  divassap  8717  divmulassap  8722  divmuldivap  8739  divmuleqap  8744  divadddivap  8754  conjmulap  8756  cju  8988  ofnegsub  8989  zneo  9427  exp3vallem  10632  exp3val  10633  exp1  10637  expp1  10638  expcl  10649  expclzaplem  10655  mulexp  10670  sqcl  10692  subsq  10738  subsq2  10739  binom2sub  10745  mulbinom2  10748  binom3  10749  zesq  10750  bernneq  10752  bernneq2  10753  mulsubdivbinom2ap  10803  facnn  10819  fac0  10820  fac1  10821  facp1  10822  bcval5  10855  bcn2  10856  reim  11017  imcl  11019  crre  11022  crim  11023  remim  11025  mulreap  11029  cjreb  11031  recj  11032  reneg  11033  readd  11034  remullem  11036  remul2  11038  imcj  11040  imneg  11041  imadd  11042  immul2  11045  cjadd  11049  ipcnval  11051  cjmulrcl  11052  cjneg  11055  imval2  11059  cjreim  11068  rennim  11167  sqabsadd  11220  sqabssub  11221  absreimsq  11232  absreim  11233  absmul  11234  mul0inf  11406  mulcn2  11477  climmul  11492  isermulc2  11505  fsummulc2  11613  prodf  11703  clim2prod  11704  clim2divap  11705  prod3fmul  11706  prodf1  11707  prodfap0  11710  prodfrecap  11711  prodrbdclem  11736  fproddccvg  11737  prodmodclem3  11740  prodmodclem2a  11741  zproddc  11744  fprodseq  11748  fprodntrivap  11749  prodsnf  11757  fprodcl  11772  fprodclf  11800  efexp  11847  sinf  11869  cosf  11870  tanval2ap  11878  tanval3ap  11879  resinval  11880  recosval  11881  efi4p  11882  resin4p  11883  recos4p  11884  resincl  11885  recoscl  11886  sinneg  11891  cosneg  11892  efival  11897  efmival  11898  efeul  11899  sinadd  11901  cosadd  11902  sinsub  11905  cossub  11906  subsin  11908  sinmul  11909  cosmul  11910  addcos  11911  subcos  11912  cos2tsin  11916  ef01bndlem  11921  sin01bnd  11922  cos01bnd  11923  absef  11935  absefib  11936  efieq1re  11937  demoivre  11938  demoivreALT  11939  odd2np1lem  12037  odd2np1  12038  opoe  12060  omoe  12061  opeo  12062  omeo  12063  modgcd  12158  qredeq  12264  modprm0  12423  pythagtriplem1  12434  pythagtriplem12  12444  pythagtriplem14  12446  gzmulcl  12547  4sqlem11  12570  4sqlem17  12576  cncrng  14125  cnfldmulg  14132  mpomulcn  14802  mulc1cncf  14825  mulcncflem  14843  dvmulxxbr  14938  dvmulxx  14940  dvimulf  14942  plymullem1  14984  plymulcl  14991  plysubcl  14992  efper  15043  sinperlem  15044  sin2kpi  15047  cos2kpi  15048  efimpi  15055  sincosq1eq  15075  abssinper  15082  sinkpi  15083  coskpi  15084  binom4  15215  fsumdvdsmul  15227  lgsdilem2  15277  lgsne0  15279  lgsquadlem1  15318  2sqlem2  15356