Theorem mulcl 8025

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167  (class class class)co 5925  ℂcc 7896   · cmul 7903

This theorem was proved from axioms:  ax-mulcl 7996

This theorem is referenced by:  mpomulf  8035  0cn  8037  mulrid  8042  mulcli  8050  mulcld  8066  mul31  8176  mul4  8177  muladd11r  8201  cnegexlem2  8221  cnegex  8223  muladd  8429  subdi  8430  mul02  8432  submul2  8444  mulsub  8446  recextlem1  8697  recexap  8699  muleqadd  8714  divassap  8736  divmulassap  8741  divmuldivap  8758  divmuleqap  8763  divadddivap  8773  conjmulap  8775  cju  9007  ofnegsub  9008  zneo  9446  exp3vallem  10651  exp3val  10652  exp1  10656  expp1  10657  expcl  10668  expclzaplem  10674  mulexp  10689  sqcl  10711  subsq  10757  subsq2  10758  binom2sub  10764  mulbinom2  10767  binom3  10768  zesq  10769  bernneq  10771  bernneq2  10772  mulsubdivbinom2ap  10822  facnn  10838  fac0  10839  fac1  10840  facp1  10841  bcval5  10874  bcn2  10875  reim  11036  imcl  11038  crre  11041  crim  11042  remim  11044  mulreap  11048  cjreb  11050  recj  11051  reneg  11052  readd  11053  remullem  11055  remul2  11057  imcj  11059  imneg  11060  imadd  11061  immul2  11064  cjadd  11068  ipcnval  11070  cjmulrcl  11071  cjneg  11074  imval2  11078  cjreim  11087  rennim  11186  sqabsadd  11239  sqabssub  11240  absreimsq  11251  absreim  11252  absmul  11253  mul0inf  11425  mulcn2  11496  climmul  11511  isermulc2  11524  fsummulc2  11632  prodf  11722  clim2prod  11723  clim2divap  11724  prod3fmul  11725  prodf1  11726  prodfap0  11729  prodfrecap  11730  prodrbdclem  11755  fproddccvg  11756  prodmodclem3  11759  prodmodclem2a  11760  zproddc  11763  fprodseq  11767  fprodntrivap  11768  prodsnf  11776  fprodcl  11791  fprodclf  11819  efexp  11866  sinf  11888  cosf  11889  tanval2ap  11897  tanval3ap  11898  resinval  11899  recosval  11900  efi4p  11901  resin4p  11902  recos4p  11903  resincl  11904  recoscl  11905  sinneg  11910  cosneg  11911  efival  11916  efmival  11917  efeul  11918  sinadd  11920  cosadd  11921  sinsub  11924  cossub  11925  subsin  11927  sinmul  11928  cosmul  11929  addcos  11930  subcos  11931  cos2tsin  11935  ef01bndlem  11940  sin01bnd  11941  cos01bnd  11942  absef  11954  absefib  11955  efieq1re  11956  demoivre  11957  demoivreALT  11958  odd2np1lem  12056  odd2np1  12057  opoe  12079  omoe  12080  opeo  12081  omeo  12082  modgcd  12185  qredeq  12291  modprm0  12450  pythagtriplem1  12461  pythagtriplem12  12471  pythagtriplem14  12473  gzmulcl  12574  4sqlem11  12597  4sqlem17  12603  cncrng  14203  cnfldmulg  14210  mpomulcn  14910  mulc1cncf  14933  mulcncflem  14951  dvmulxxbr  15046  dvmulxx  15048  dvimulf  15050  plymullem1  15092  plymulcl  15099  plysubcl  15100  efper  15151  sinperlem  15152  sin2kpi  15155  cos2kpi  15156  efimpi  15163  sincosq1eq  15183  abssinper  15190  sinkpi  15191  coskpi  15192  binom4  15323  fsumdvdsmul  15335  lgsdilem2  15385  lgsne0  15387  lgsquadlem1  15426  2sqlem2  15464