Theorem mulcl 7929

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  (class class class)co 5869  ℂcc 7800   · cmul 7807

This theorem was proved from axioms:  ax-mulcl 7900

This theorem is referenced by:  0cn  7940  mulid1  7945  mulcli  7953  mulcld  7968  mul31  8078  mul4  8079  muladd11r  8103  cnegexlem2  8123  cnegex  8125  muladd  8331  subdi  8332  mul02  8334  submul2  8346  mulsub  8348  recextlem1  8597  recexap  8599  muleqadd  8614  divassap  8636  divmulassap  8641  divmuldivap  8658  divmuleqap  8663  divadddivap  8673  conjmulap  8675  cju  8907  zneo  9343  exp3vallem  10507  exp3val  10508  exp1  10512  expp1  10513  expcl  10524  expclzaplem  10530  mulexp  10545  sqcl  10567  subsq  10612  subsq2  10613  binom2sub  10619  mulbinom2  10622  binom3  10623  zesq  10624  bernneq  10626  bernneq2  10627  facnn  10691  fac0  10692  fac1  10693  facp1  10694  bcval5  10727  bcn2  10728  reim  10845  imcl  10847  crre  10850  crim  10851  remim  10853  mulreap  10857  cjreb  10859  recj  10860  reneg  10861  readd  10862  remullem  10864  remul2  10866  imcj  10868  imneg  10869  imadd  10870  immul2  10873  cjadd  10877  ipcnval  10879  cjmulrcl  10880  cjneg  10883  imval2  10887  cjreim  10896  rennim  10995  sqabsadd  11048  sqabssub  11049  absreimsq  11060  absreim  11061  absmul  11062  mul0inf  11233  mulcn2  11304  climmul  11319  isermulc2  11332  fsummulc2  11440  prodf  11530  clim2prod  11531  clim2divap  11532  prod3fmul  11533  prodf1  11534  prodfap0  11537  prodfrecap  11538  prodrbdclem  11563  fproddccvg  11564  prodmodclem3  11567  prodmodclem2a  11568  zproddc  11571  fprodseq  11575  fprodntrivap  11576  prodsnf  11584  fprodcl  11599  fprodclf  11627  efexp  11674  sinf  11696  cosf  11697  tanval2ap  11705  tanval3ap  11706  resinval  11707  recosval  11708  efi4p  11709  resin4p  11710  recos4p  11711  resincl  11712  recoscl  11713  sinneg  11718  cosneg  11719  efival  11724  efmival  11725  efeul  11726  sinadd  11728  cosadd  11729  sinsub  11732  cossub  11733  subsin  11735  sinmul  11736  cosmul  11737  addcos  11738  subcos  11739  cos2tsin  11743  ef01bndlem  11748  sin01bnd  11749  cos01bnd  11750  absef  11761  absefib  11762  efieq1re  11763  demoivre  11764  demoivreALT  11765  odd2np1lem  11860  odd2np1  11861  opoe  11883  omoe  11884  opeo  11885  omeo  11886  modgcd  11975  qredeq  12079  modprm0  12237  pythagtriplem1  12248  pythagtriplem12  12258  pythagtriplem14  12260  gzmulcl  12359  mulc1cncf  13743  mulcncflem  13757  dvmulxxbr  13833  dvmulxx  13835  dvimulf  13837  efper  13895  sinperlem  13896  sin2kpi  13899  cos2kpi  13900  efimpi  13907  sincosq1eq  13927  abssinper  13934  sinkpi  13935  coskpi  13936  binom4  14064  lgsdilem2  14104  lgsne0  14106  2sqlem2  14118