Theorem mulcl 8159

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  (class class class)co 6018  ℂcc 8030   · cmul 8037

This theorem was proved from axioms:  ax-mulcl 8130

This theorem is referenced by:  mpomulf  8169  0cn  8171  mulrid  8176  mulcli  8184  mulcld  8200  mul31  8310  mul4  8311  muladd11r  8335  cnegexlem2  8355  cnegex  8357  muladd  8563  subdi  8564  mul02  8566  submul2  8578  mulsub  8580  recextlem1  8831  recexap  8833  muleqadd  8848  divassap  8870  divmulassap  8875  divmuldivap  8892  divmuleqap  8897  divadddivap  8907  conjmulap  8909  cju  9141  ofnegsub  9142  zneo  9581  exp3vallem  10803  exp3val  10804  exp1  10808  expp1  10809  expcl  10820  expclzaplem  10826  mulexp  10841  sqcl  10863  subsq  10909  subsq2  10910  binom2sub  10916  mulbinom2  10919  binom3  10920  zesq  10921  bernneq  10923  bernneq2  10924  mulsubdivbinom2ap  10974  facnn  10990  fac0  10991  fac1  10992  facp1  10993  bcval5  11026  bcn2  11027  reim  11417  imcl  11419  crre  11422  crim  11423  remim  11425  mulreap  11429  cjreb  11431  recj  11432  reneg  11433  readd  11434  remullem  11436  remul2  11438  imcj  11440  imneg  11441  imadd  11442  immul2  11445  cjadd  11449  ipcnval  11451  cjmulrcl  11452  cjneg  11455  imval2  11459  cjreim  11468  rennim  11567  sqabsadd  11620  sqabssub  11621  absreimsq  11632  absreim  11633  absmul  11634  mul0inf  11806  mulcn2  11877  climmul  11892  isermulc2  11905  fsummulc2  12014  prodf  12104  clim2prod  12105  clim2divap  12106  prod3fmul  12107  prodf1  12108  prodfap0  12111  prodfrecap  12112  prodrbdclem  12137  fproddccvg  12138  prodmodclem3  12141  prodmodclem2a  12142  zproddc  12145  fprodseq  12149  fprodntrivap  12150  prodsnf  12158  fprodcl  12173  fprodclf  12201  efexp  12248  sinf  12270  cosf  12271  tanval2ap  12279  tanval3ap  12280  resinval  12281  recosval  12282  efi4p  12283  resin4p  12284  recos4p  12285  resincl  12286  recoscl  12287  sinneg  12292  cosneg  12293  efival  12298  efmival  12299  efeul  12300  sinadd  12302  cosadd  12303  sinsub  12306  cossub  12307  subsin  12309  sinmul  12310  cosmul  12311  addcos  12312  subcos  12313  cos2tsin  12317  ef01bndlem  12322  sin01bnd  12323  cos01bnd  12324  absef  12336  absefib  12337  efieq1re  12338  demoivre  12339  demoivreALT  12340  odd2np1lem  12438  odd2np1  12439  opoe  12461  omoe  12462  opeo  12463  omeo  12464  modgcd  12567  qredeq  12673  modprm0  12832  pythagtriplem1  12843  pythagtriplem12  12853  pythagtriplem14  12855  gzmulcl  12956  4sqlem11  12979  4sqlem17  12985  cncrng  14589  cnfldmulg  14596  mpomulcn  15296  mulc1cncf  15319  mulcncflem  15337  dvmulxxbr  15432  dvmulxx  15434  dvimulf  15436  plymullem1  15478  plymulcl  15485  plysubcl  15486  efper  15537  sinperlem  15538  sin2kpi  15541  cos2kpi  15542  efimpi  15549  sincosq1eq  15569  abssinper  15576  sinkpi  15577  coskpi  15578  binom4  15709  fsumdvdsmul  15721  lgsdilem2  15771  lgsne0  15773  lgsquadlem1  15812  2sqlem2  15850