Theorem mulcld 8347

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 8307	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
4	1, 2, 3	syl2anc 415	1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  (class class class)co 6085  ℂcc 8178   · cmul 8185

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

This theorem is used by:  kcnktkm1cn  8712  rereim  8917  cru  8933  apreim  8934  mulreim  8935  apadd1  8939  apneg  8942  mulext1  8943  mulext  8945  aprcl  8977  aptap  8981  mulap0  8985  msq0  9000  receuap  9002  mul0eqap  9003  divrecap  9021  divcanap3  9031  muldivdirap  9040  divdivdivap  9046  divsubdivap  9061  apmul1  9121  apdivmuld  9146  ofnegsub  9295  qapne  10049  cnref1o  10062  mul2lt0rlt0  10171  lincmb01cmp  10416  iccf1o  10418  qbtwnrelemcalc  10701  flqpmodeq  10779  modq0  10781  modqdiffl  10787  modqvalp1  10795  modqcyc  10811  modqcyc2  10812  modqadd1  10813  mulqaddmodid  10816  modqmuladdnn0  10820  qnegmod  10821  modqmul1  10829  mulexpzap  11031  expmulzap  11037  binom2  11103  binom3  11109  resq01  11110  bernneq  11113  mulsubdivbinom2ap  11165  nn0opthd  11176  bcval5  11217  remullem  11652  sq01  11676  cjreim2  11686  cnrecnv  11692  absval  11783  resqrexlemover  11792  resqrexlemcalc1  11796  resqrexlemnm  11800  absimle  11867  abstri  11887  bdtrilem  12024  mulcn2  12097  reccn2ap  12098  climcvg1nlem  12134  isummulc2  12212  fsummulc2  12234  fsumparts  12256  binomlem  12269  binom1dif  12273  trireciplem  12286  mertenslemi1  12321  mertensabs  12323  ntrivcvgap  12334  fprodmul  12377  efaddlem  12460  sinval  12488  cosval  12489  sinadd  12522  cosadd  12523  tanaddaplem  12524  tanaddap  12525  addsin  12528  sincossq  12534  sin2t  12535  cos12dec  12554  eirraplem  12563  dvdscmulr  12606  dvdsmulcr  12607  dvds2ln  12610  oddm1even  12661  divalglemnn  12704  divalglemnqt  12706  flodddiv4  12722  gcdaddm  12780  bezoutlemnewy  12792  bezoutlema  12795  bezoutlemb  12796  lcmgcdlem  12874  nnmaxpw  12972  phiprmpw  13023  eulerthlema  13031  pythagtriplem12  13077  pythagtriplem14  13079  pythagtriplem16  13081  pcpremul  13095  pcaddlem  13141  fldivp1  13150  mul4sqlem  13195  4sqlem14  13206  oddennn  13335  cnfldui  15008  expghmap  15026  znunit  15078  expcn  15761  mulc1cncf  15781  mulcncf  15800  dvmulxxbr  15894  dvimulf  15898  dvexp  15903  dvmptmulx  15912  dvmptcmulcn  15913  plyf  15929  ply1termlem  15934  plyaddlem1  15939  plymullem1  15940  plycoeid3  15949  plycolemc  15950  plycjlemc  15952  plyrecj  15955  dvply1  15957  dvply2g  15958  sin0pilem1  15974  rpcxpef  16091  rpcncxpcl  16099  cxpap0  16101  rpcxpadd  16102  rpmulcxp  16106  cxpmul  16109  rpcxpmul2  16110  abscxp  16112  rpabscxpbnd  16137  binom4  16180  birthdaylem2  16187  pellexlem1  16190  pellexlem2  16191  mpodvdsmulf1o  16245  fsumdvdsmul  16246  perfectlem2  16261  bposlem9  16280  lgsquad2lem1  16366  2lgslem3b  16379  2lgslem3c  16380  2lgslem3d  16381  2sqlem3  16402  qdencn  17238  cvgcmp2nlemabs  17247  qdiff  17265