Theorem mulcl 7842

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2128  (class class class)co 5818  ℂcc 7713   · cmul 7720

This theorem was proved from axioms:  ax-mulcl 7813

This theorem is referenced by:  0cn  7853  mulid1  7858  mulcli  7866  mulcld  7881  mul31  7989  mul4  7990  muladd11r  8014  cnegexlem2  8034  cnegex  8036  muladd  8242  subdi  8243  mul02  8245  submul2  8257  mulsub  8259  recextlem1  8508  recexap  8510  muleqadd  8525  divassap  8546  divmulassap  8551  divmuldivap  8568  divmuleqap  8573  divadddivap  8583  conjmulap  8585  cju  8815  zneo  9248  exp3vallem  10402  exp3val  10403  exp1  10407  expp1  10408  expcl  10419  expclzaplem  10425  mulexp  10440  sqcl  10462  subsq  10507  subsq2  10508  binom2sub  10513  mulbinom2  10516  binom3  10517  zesq  10518  bernneq  10520  bernneq2  10521  facnn  10583  fac0  10584  fac1  10585  facp1  10586  bcval5  10619  bcn2  10620  reim  10734  imcl  10736  crre  10739  crim  10740  remim  10742  mulreap  10746  cjreb  10748  recj  10749  reneg  10750  readd  10751  remullem  10753  remul2  10755  imcj  10757  imneg  10758  imadd  10759  immul2  10762  cjadd  10766  ipcnval  10768  cjmulrcl  10769  cjneg  10772  imval2  10776  cjreim  10785  rennim  10884  sqabsadd  10937  sqabssub  10938  absreimsq  10949  absreim  10950  absmul  10951  mul0inf  11122  mulcn2  11191  climmul  11206  isermulc2  11219  fsummulc2  11327  prodf  11417  clim2prod  11418  clim2divap  11419  prod3fmul  11420  prodf1  11421  prodfap0  11424  prodfrecap  11425  prodrbdclem  11450  fproddccvg  11451  prodmodclem3  11454  prodmodclem2a  11455  zproddc  11458  fprodseq  11462  fprodntrivap  11463  prodsnf  11471  fprodcl  11486  fprodclf  11514  efexp  11561  sinf  11583  cosf  11584  tanval2ap  11592  tanval3ap  11593  resinval  11594  recosval  11595  efi4p  11596  resin4p  11597  recos4p  11598  resincl  11599  recoscl  11600  sinneg  11605  cosneg  11606  efival  11611  efmival  11612  efeul  11613  sinadd  11615  cosadd  11616  sinsub  11619  cossub  11620  subsin  11622  sinmul  11623  cosmul  11624  addcos  11625  subcos  11626  cos2tsin  11630  ef01bndlem  11635  sin01bnd  11636  cos01bnd  11637  absef  11648  absefib  11649  efieq1re  11650  demoivre  11651  demoivreALT  11652  odd2np1lem  11744  odd2np1  11745  opoe  11767  omoe  11768  opeo  11769  omeo  11770  modgcd  11855  qredeq  11953  mulc1cncf  12936  mulcncflem  12950  dvmulxxbr  13026  dvmulxx  13028  dvimulf  13030  efper  13088  sinperlem  13089  sin2kpi  13092  cos2kpi  13093  efimpi  13100  sincosq1eq  13120  abssinper  13127  sinkpi  13128  coskpi  13129