Theorem mulcl 8270

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205  (class class class)co 6058  ℂcc 8141   · cmul 8148

This theorem was proved from axioms:  ax-mulcl 8241

This theorem is referenced by:  mpomulf  8280  0cn  8282  mulrid  8287  mulcli  8295  mulcld  8310  mul31  8421  mul4  8422  muladd11r  8446  cnegexlem2  8466  cnegex  8468  muladd  8675  subdi  8676  mul02  8678  submul2  8690  mulsub  8692  recextlem1  8943  recexap  8945  muleqadd  8962  divassap  8984  divmulassap  8989  divmuldivap  9006  divmuleqap  9011  divadddivap  9021  conjmulap  9023  cju  9255  ofnegsub  9256  zneo  9700  exp3vallem  10929  exp3val  10930  exp1  10934  expp1  10935  expcl  10946  expclzaplem  10952  mulexp  10967  sqcl  10989  subsq  11035  subsq2  11036  binom2sub  11042  mulbinom2  11045  binom3  11046  zesq  11048  bernneq  11050  bernneq2  11051  mulsubdivbinom2ap  11101  facnn  11117  fac0  11118  fac1  11119  facp1  11120  bcval5  11153  bcn2  11154  reim  11565  imcl  11567  crre  11570  crim  11571  remim  11573  mulreap  11577  cjreb  11579  recj  11580  reneg  11581  readd  11582  remullem  11584  remul2  11586  imcj  11588  imneg  11589  imadd  11590  immul2  11593  cjadd  11597  ipcnval  11599  cjmulrcl  11600  cjneg  11603  imval2  11607  cjreim  11617  rennim  11716  sqabsadd  11769  sqabssub  11770  absreimsq  11781  absreim  11782  absmul  11783  mul0inf  11955  mulcn2  12026  climmul  12041  isermulc2  12054  fsummulc2  12163  prodf  12253  clim2prod  12254  clim2divap  12255  prod3fmul  12256  prodf1  12257  prodfap0  12260  prodfrecap  12261  prodrbdclem  12286  fproddccvg  12287  prodmodclem3  12290  prodmodclem2a  12291  zproddc  12294  fprodseq  12298  fprodntrivap  12299  prodsnf  12307  fprodcl  12322  fprodclf  12350  efexp  12397  sinf  12419  cosf  12420  tanval2ap  12428  tanval3ap  12429  resinval  12430  recosval  12431  efi4p  12432  resin4p  12433  recos4p  12434  resincl  12435  recoscl  12436  sinneg  12441  cosneg  12442  efival  12447  efmival  12448  efeul  12449  sinadd  12451  cosadd  12452  sinsub  12455  cossub  12456  subsin  12458  sinmul  12459  cosmul  12460  addcos  12461  subcos  12462  cos2tsin  12466  ef01bndlem  12471  sin01bnd  12472  cos01bnd  12473  absef  12485  absefib  12486  efieq1re  12487  demoivre  12488  demoivreALT  12489  odd2np1lem  12587  odd2np1  12588  opoe  12610  omoe  12611  opeo  12612  omeo  12613  modgcd  12716  qredeq  12822  modprm0  12981  pythagtriplem1  12992  pythagtriplem12  13002  pythagtriplem14  13004  gzmulcl  13105  4sqlem11  13128  4sqlem17  13134  cncrng  14847  cnfldmulg  14854  mpomulcn  15561  mulc1cncf  15584  mulcncflem  15602  dvmulxxbr  15697  dvmulxx  15699  dvimulf  15701  plymullem1  15743  plymulcl  15750  plysubcl  15751  efper  15802  sinperlem  15803  sin2kpi  15806  cos2kpi  15807  efimpi  15814  sincosq1eq  15834  abssinper  15841  sinkpi  15842  coskpi  15843  binom4  15974  fsumdvdsmul  15989  lgsdilem2  16039  lgsne0  16041  lgsquadlem1  16080  2sqlem2  16118