Theorem mulcl 7999

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2164  (class class class)co 5918  ℂcc 7870   · cmul 7877

This theorem was proved from axioms:  ax-mulcl 7970

This theorem is referenced by:  mpomulf  8009  0cn  8011  mulrid  8016  mulcli  8024  mulcld  8040  mul31  8150  mul4  8151  muladd11r  8175  cnegexlem2  8195  cnegex  8197  muladd  8403  subdi  8404  mul02  8406  submul2  8418  mulsub  8420  recextlem1  8670  recexap  8672  muleqadd  8687  divassap  8709  divmulassap  8714  divmuldivap  8731  divmuleqap  8736  divadddivap  8746  conjmulap  8748  cju  8980  ofnegsub  8981  zneo  9418  exp3vallem  10611  exp3val  10612  exp1  10616  expp1  10617  expcl  10628  expclzaplem  10634  mulexp  10649  sqcl  10671  subsq  10717  subsq2  10718  binom2sub  10724  mulbinom2  10727  binom3  10728  zesq  10729  bernneq  10731  bernneq2  10732  mulsubdivbinom2ap  10782  facnn  10798  fac0  10799  fac1  10800  facp1  10801  bcval5  10834  bcn2  10835  reim  10996  imcl  10998  crre  11001  crim  11002  remim  11004  mulreap  11008  cjreb  11010  recj  11011  reneg  11012  readd  11013  remullem  11015  remul2  11017  imcj  11019  imneg  11020  imadd  11021  immul2  11024  cjadd  11028  ipcnval  11030  cjmulrcl  11031  cjneg  11034  imval2  11038  cjreim  11047  rennim  11146  sqabsadd  11199  sqabssub  11200  absreimsq  11211  absreim  11212  absmul  11213  mul0inf  11384  mulcn2  11455  climmul  11470  isermulc2  11483  fsummulc2  11591  prodf  11681  clim2prod  11682  clim2divap  11683  prod3fmul  11684  prodf1  11685  prodfap0  11688  prodfrecap  11689  prodrbdclem  11714  fproddccvg  11715  prodmodclem3  11718  prodmodclem2a  11719  zproddc  11722  fprodseq  11726  fprodntrivap  11727  prodsnf  11735  fprodcl  11750  fprodclf  11778  efexp  11825  sinf  11847  cosf  11848  tanval2ap  11856  tanval3ap  11857  resinval  11858  recosval  11859  efi4p  11860  resin4p  11861  recos4p  11862  resincl  11863  recoscl  11864  sinneg  11869  cosneg  11870  efival  11875  efmival  11876  efeul  11877  sinadd  11879  cosadd  11880  sinsub  11883  cossub  11884  subsin  11886  sinmul  11887  cosmul  11888  addcos  11889  subcos  11890  cos2tsin  11894  ef01bndlem  11899  sin01bnd  11900  cos01bnd  11901  absef  11913  absefib  11914  efieq1re  11915  demoivre  11916  demoivreALT  11917  odd2np1lem  12013  odd2np1  12014  opoe  12036  omoe  12037  opeo  12038  omeo  12039  modgcd  12128  qredeq  12234  modprm0  12392  pythagtriplem1  12403  pythagtriplem12  12413  pythagtriplem14  12415  gzmulcl  12516  4sqlem11  12539  4sqlem17  12545  cncrng  14057  cnfldmulg  14064  mulc1cncf  14744  mulcncflem  14761  dvmulxxbr  14851  dvmulxx  14853  dvimulf  14855  plymullem1  14894  plymulcl  14901  plysubcl  14902  efper  14942  sinperlem  14943  sin2kpi  14946  cos2kpi  14947  efimpi  14954  sincosq1eq  14974  abssinper  14981  sinkpi  14982  coskpi  14983  binom4  15111  lgsdilem2  15152  lgsne0  15154  lgsquadlem1  15191  2sqlem2  15202