Theorem mulcl 8202

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  (class class class)co 6028  ℂcc 8073   · cmul 8080

This theorem was proved from axioms:  ax-mulcl 8173

This theorem is referenced by:  mpomulf  8212  0cn  8214  mulrid  8219  mulcli  8227  mulcld  8243  mul31  8353  mul4  8354  muladd11r  8378  cnegexlem2  8398  cnegex  8400  muladd  8606  subdi  8607  mul02  8609  submul2  8621  mulsub  8623  recextlem1  8874  recexap  8876  muleqadd  8891  divassap  8913  divmulassap  8918  divmuldivap  8935  divmuleqap  8940  divadddivap  8950  conjmulap  8952  cju  9184  ofnegsub  9185  zneo  9624  exp3vallem  10846  exp3val  10847  exp1  10851  expp1  10852  expcl  10863  expclzaplem  10869  mulexp  10884  sqcl  10906  subsq  10952  subsq2  10953  binom2sub  10959  mulbinom2  10962  binom3  10963  zesq  10964  bernneq  10966  bernneq2  10967  mulsubdivbinom2ap  11017  facnn  11033  fac0  11034  fac1  11035  facp1  11036  bcval5  11069  bcn2  11070  reim  11473  imcl  11475  crre  11478  crim  11479  remim  11481  mulreap  11485  cjreb  11487  recj  11488  reneg  11489  readd  11490  remullem  11492  remul2  11494  imcj  11496  imneg  11497  imadd  11498  immul2  11501  cjadd  11505  ipcnval  11507  cjmulrcl  11508  cjneg  11511  imval2  11515  cjreim  11524  rennim  11623  sqabsadd  11676  sqabssub  11677  absreimsq  11688  absreim  11689  absmul  11690  mul0inf  11862  mulcn2  11933  climmul  11948  isermulc2  11961  fsummulc2  12070  prodf  12160  clim2prod  12161  clim2divap  12162  prod3fmul  12163  prodf1  12164  prodfap0  12167  prodfrecap  12168  prodrbdclem  12193  fproddccvg  12194  prodmodclem3  12197  prodmodclem2a  12198  zproddc  12201  fprodseq  12205  fprodntrivap  12206  prodsnf  12214  fprodcl  12229  fprodclf  12257  efexp  12304  sinf  12326  cosf  12327  tanval2ap  12335  tanval3ap  12336  resinval  12337  recosval  12338  efi4p  12339  resin4p  12340  recos4p  12341  resincl  12342  recoscl  12343  sinneg  12348  cosneg  12349  efival  12354  efmival  12355  efeul  12356  sinadd  12358  cosadd  12359  sinsub  12362  cossub  12363  subsin  12365  sinmul  12366  cosmul  12367  addcos  12368  subcos  12369  cos2tsin  12373  ef01bndlem  12378  sin01bnd  12379  cos01bnd  12380  absef  12392  absefib  12393  efieq1re  12394  demoivre  12395  demoivreALT  12396  odd2np1lem  12494  odd2np1  12495  opoe  12517  omoe  12518  opeo  12519  omeo  12520  modgcd  12623  qredeq  12729  modprm0  12888  pythagtriplem1  12899  pythagtriplem12  12909  pythagtriplem14  12911  gzmulcl  13012  4sqlem11  13035  4sqlem17  13041  cncrng  14645  cnfldmulg  14652  mpomulcn  15357  mulc1cncf  15380  mulcncflem  15398  dvmulxxbr  15493  dvmulxx  15495  dvimulf  15497  plymullem1  15539  plymulcl  15546  plysubcl  15547  efper  15598  sinperlem  15599  sin2kpi  15602  cos2kpi  15603  efimpi  15610  sincosq1eq  15630  abssinper  15637  sinkpi  15638  coskpi  15639  binom4  15770  fsumdvdsmul  15785  lgsdilem2  15835  lgsne0  15837  lgsquadlem1  15876  2sqlem2  15914