Theorem mulcl 8114

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  (class class class)co 5994  ℂcc 7985   · cmul 7992

This theorem was proved from axioms:  ax-mulcl 8085

This theorem is referenced by:  mpomulf  8124  0cn  8126  mulrid  8131  mulcli  8139  mulcld  8155  mul31  8265  mul4  8266  muladd11r  8290  cnegexlem2  8310  cnegex  8312  muladd  8518  subdi  8519  mul02  8521  submul2  8533  mulsub  8535  recextlem1  8786  recexap  8788  muleqadd  8803  divassap  8825  divmulassap  8830  divmuldivap  8847  divmuleqap  8852  divadddivap  8862  conjmulap  8864  cju  9096  ofnegsub  9097  zneo  9536  exp3vallem  10749  exp3val  10750  exp1  10754  expp1  10755  expcl  10766  expclzaplem  10772  mulexp  10787  sqcl  10809  subsq  10855  subsq2  10856  binom2sub  10862  mulbinom2  10865  binom3  10866  zesq  10867  bernneq  10869  bernneq2  10870  mulsubdivbinom2ap  10920  facnn  10936  fac0  10937  fac1  10938  facp1  10939  bcval5  10972  bcn2  10973  reim  11349  imcl  11351  crre  11354  crim  11355  remim  11357  mulreap  11361  cjreb  11363  recj  11364  reneg  11365  readd  11366  remullem  11368  remul2  11370  imcj  11372  imneg  11373  imadd  11374  immul2  11377  cjadd  11381  ipcnval  11383  cjmulrcl  11384  cjneg  11387  imval2  11391  cjreim  11400  rennim  11499  sqabsadd  11552  sqabssub  11553  absreimsq  11564  absreim  11565  absmul  11566  mul0inf  11738  mulcn2  11809  climmul  11824  isermulc2  11837  fsummulc2  11945  prodf  12035  clim2prod  12036  clim2divap  12037  prod3fmul  12038  prodf1  12039  prodfap0  12042  prodfrecap  12043  prodrbdclem  12068  fproddccvg  12069  prodmodclem3  12072  prodmodclem2a  12073  zproddc  12076  fprodseq  12080  fprodntrivap  12081  prodsnf  12089  fprodcl  12104  fprodclf  12132  efexp  12179  sinf  12201  cosf  12202  tanval2ap  12210  tanval3ap  12211  resinval  12212  recosval  12213  efi4p  12214  resin4p  12215  recos4p  12216  resincl  12217  recoscl  12218  sinneg  12223  cosneg  12224  efival  12229  efmival  12230  efeul  12231  sinadd  12233  cosadd  12234  sinsub  12237  cossub  12238  subsin  12240  sinmul  12241  cosmul  12242  addcos  12243  subcos  12244  cos2tsin  12248  ef01bndlem  12253  sin01bnd  12254  cos01bnd  12255  absef  12267  absefib  12268  efieq1re  12269  demoivre  12270  demoivreALT  12271  odd2np1lem  12369  odd2np1  12370  opoe  12392  omoe  12393  opeo  12394  omeo  12395  modgcd  12498  qredeq  12604  modprm0  12763  pythagtriplem1  12774  pythagtriplem12  12784  pythagtriplem14  12786  gzmulcl  12887  4sqlem11  12910  4sqlem17  12916  cncrng  14518  cnfldmulg  14525  mpomulcn  15225  mulc1cncf  15248  mulcncflem  15266  dvmulxxbr  15361  dvmulxx  15363  dvimulf  15365  plymullem1  15407  plymulcl  15414  plysubcl  15415  efper  15466  sinperlem  15467  sin2kpi  15470  cos2kpi  15471  efimpi  15478  sincosq1eq  15498  abssinper  15505  sinkpi  15506  coskpi  15507  binom4  15638  fsumdvdsmul  15650  lgsdilem2  15700  lgsne0  15702  lgsquadlem1  15741  2sqlem2  15779