Theorem mulcld 8352

Description: Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
mulcld	⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)

Proof of Theorem mulcld

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		mulcl 8312	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
4	1, 2, 3	syl2anc 415	1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  (class class class)co 6088  ℂcc 8183   · cmul 8190

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulcl 8283

This theorem is used by:  kcnktkm1cn  8717  rereim  8922  cru  8938  apreim  8939  mulreim  8940  apadd1  8944  apneg  8947  mulext1  8948  mulext  8950  aprcl  8982  aptap  8986  mulap0  8990  msq0  9005  receuap  9007  mul0eqap  9008  divrecap  9026  divcanap3  9036  muldivdirap  9045  divdivdivap  9051  divsubdivap  9066  apmul1  9126  apdivmuld  9151  ofnegsub  9301  qapne  10055  cnref1o  10068  mul2lt0rlt0  10177  lincmb01cmp  10422  iccf1o  10424  qbtwnrelemcalc  10707  flqpmodeq  10785  modq0  10787  modqdiffl  10793  modqvalp1  10801  modqcyc  10817  modqcyc2  10818  modqadd1  10819  mulqaddmodid  10822  modqmuladdnn0  10826  qnegmod  10827  modqmul1  10835  mulexpzap  11037  expmulzap  11043  binom2  11109  binom3  11115  resq01  11116  bernneq  11119  mulsubdivbinom2ap  11171  nn0opthd  11182  bcval5  11223  remullem  11658  sq01  11682  cjreim2  11692  cnrecnv  11698  absval  11789  resqrexlemover  11798  resqrexlemcalc1  11802  resqrexlemnm  11806  absimle  11873  abstri  11893  bdtrilem  12030  mulcn2  12103  reccn2ap  12104  climcvg1nlem  12140  isummulc2  12218  fsummulc2  12240  fsumparts  12262  binomlem  12275  binom1dif  12279  trireciplem  12292  mertenslemi1  12327  mertensabs  12329  ntrivcvgap  12340  fprodmul  12383  efaddlem  12466  sinval  12494  cosval  12495  sinadd  12528  cosadd  12529  tanaddaplem  12530  tanaddap  12531  addsin  12534  sincossq  12540  sin2t  12541  cos12dec  12560  eirraplem  12569  dvdscmulr  12612  dvdsmulcr  12613  dvds2ln  12616  oddm1even  12667  divalglemnn  12710  divalglemnqt  12712  flodddiv4  12728  gcdaddm  12786  bezoutlemnewy  12798  bezoutlema  12801  bezoutlemb  12802  lcmgcdlem  12880  nnmaxpw  12978  phiprmpw  13029  eulerthlema  13037  pythagtriplem12  13083  pythagtriplem14  13085  pythagtriplem16  13087  pcpremul  13101  pcaddlem  13147  fldivp1  13156  mul4sqlem  13201  4sqlem14  13212  oddennn  13341  cnfldui  15033  expghmap  15051  znunit  15103  expcn  15795  mulc1cncf  15815  mulcncf  15834  dvmulxxbr  15928  dvimulf  15932  dvexp  15937  dvmptmulx  15946  dvmptcmulcn  15947  plyf  15963  ply1termlem  15968  plyaddlem1  15973  plymullem1  15974  plycoeid3  15983  plycolemc  15984  plycjlemc  15986  plyrecj  15989  dvply1  15991  dvply2g  15992  sin0pilem1  16008  rpcxpef  16127  rpcncxpcl  16135  cxpap0  16137  rpcxpadd  16138  rpmulcxp  16142  cxpmul  16145  rpcxpmul2  16146  rpcxpmul2z  16148  abscxp  16150  rpabscxpbnd  16175  binom4  16219  birthdaylem2  16226  pellexlem1  16229  pellexlem2  16230  mpodvdsmulf1o  16284  fsumdvdsmul  16285  perfectlem2  16300  bposlem9  16319  lgsquad2lem1  16405  2lgslem3b  16418  2lgslem3c  16419  2lgslem3d  16420  2sqlem3  16441  qdencn  17278  cvgcmp2nlemabs  17287  qdiff  17305