Theorem mulcl 8306

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

Assertion

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

Proof of Theorem mulcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  (class class class)co 6085  ℂcc 8177   · cmul 8184

This proof depends on axioms:  ax-mulcl 8277

This theorem is used by:  mpomulf  8316  0cn  8318  mulrid  8323  mulcli  8331  mulcld  8346  mul31  8457  mul4  8458  muladd11r  8482  cnegexlem2  8502  cnegex  8504  muladd  8711  subdi  8712  mul02  8714  submul2  8726  mulsub  8728  recextlem1  8980  recexap  8982  muleqadd  8999  divassap  9021  divmulassap  9026  divmuldivap  9043  divmuleqap  9048  divadddivap  9058  conjmulap  9060  cju  9292  ofnegsub  9293  zneo  9749  exp3vallem  10979  exp3val  10980  exp1  10984  expp1  10985  expcl  10996  expclzaplem  11002  mulexp  11017  sqcl  11039  subsq  11085  subsq2  11086  binom2sub  11092  mulbinom2  11095  binom3  11096  zesq  11098  bernneq  11100  bernneq2  11101  mulsubdivbinom2ap  11151  facnn  11167  fac0  11168  fac1  11169  facp1  11170  bcval5  11203  bcn2  11204  reim  11619  imcl  11621  crre  11624  crim  11625  remim  11627  mulreap  11631  cjreb  11633  recj  11634  reneg  11635  readd  11636  remullem  11638  remul2  11640  imcj  11642  imneg  11643  imadd  11644  immul2  11647  cjadd  11651  ipcnval  11653  cjmulrcl  11654  cjneg  11657  imval2  11661  cjreim  11671  rennim  11770  sqabsadd  11823  sqabssub  11824  absreimsq  11835  absreim  11836  absmul  11837  mul0inf  12009  mulcn2  12080  climmul  12095  isermulc2  12108  fsummulc2  12217  prodf  12307  clim2prod  12308  clim2divap  12309  prod3fmul  12310  prodf1  12311  prodfap0  12314  prodfrecap  12315  prodrbdclem  12340  fproddccvg  12341  prodmodclem3  12344  prodmodclem2a  12345  zproddc  12348  fprodseq  12352  fprodntrivap  12353  prodsnf  12361  fprodcl  12376  fprodclf  12404  efexp  12451  sinf  12473  cosf  12474  tanval2ap  12482  tanval3ap  12483  resinval  12484  recosval  12485  efi4p  12486  resin4p  12487  recos4p  12488  resincl  12489  recoscl  12490  sinneg  12495  cosneg  12496  efival  12501  efmival  12502  efeul  12503  sinadd  12505  cosadd  12506  sinsub  12509  cossub  12510  subsin  12512  sinmul  12513  cosmul  12514  addcos  12515  subcos  12516  cos2tsin  12520  ef01bndlem  12525  sin01bnd  12526  cos01bnd  12527  absef  12539  absefib  12540  efieq1re  12541  demoivre  12542  demoivreALT  12543  odd2np1lem  12641  odd2np1  12642  opoe  12664  omoe  12665  opeo  12666  omeo  12667  modgcd  12770  qredeq  12876  modprm0  13035  pythagtriplem1  13046  pythagtriplem12  13056  pythagtriplem14  13058  gzmulcl  13159  4sqlem11  13182  4sqlem17  13188  cncrng  14908  cnfldmulg  14915  mpomulcn  15669  mulc1cncf  15692  mulcncflem  15710  dvmulxxbr  15805  dvmulxx  15807  dvimulf  15809  plymullem1  15851  plymulcl  15858  plysubcl  15859  efper  15911  sinperlem  15912  sin2kpi  15915  cos2kpi  15916  efimpi  15923  sincosq1eq  15943  abssinper  15950  sinkpi  15951  coskpi  15952  binom4  16087  fsumdvdsmul  16111  lgsdilem2  16167  lgsne0  16169  lgsquadlem1  16208  2sqlem2  16246