Theorem mulcld 8294

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

Syntax hints:   → wi 4   ∈ wcel 2203  (class class class)co 6050  ℂcc 8125   · cmul 8132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulcl 8225

This theorem is referenced by:  kcnktkm1cn  8656  rereim  8860  cru  8876  apreim  8877  mulreim  8878  apadd1  8882  apneg  8885  mulext1  8886  mulext  8888  aprcl  8920  aptap  8924  mulap0  8928  receuap  8943  mul0eqap  8944  divrecap  8962  divcanap3  8972  muldivdirap  8981  divdivdivap  8987  divsubdivap  9002  apmul1  9062  apdivmuld  9087  ofnegsub  9236  qapne  9971  cnref1o  9983  mul2lt0rlt0  10092  lincmb01cmp  10336  iccf1o  10338  qbtwnrelemcalc  10615  flqpmodeq  10689  modq0  10691  modqdiffl  10697  modqvalp1  10705  modqcyc  10721  modqcyc2  10722  modqadd1  10723  mulqaddmodid  10726  modqmuladdnn0  10730  qnegmod  10731  modqmul1  10739  mulexpzap  10941  expmulzap  10947  binom2  11013  binom3  11019  bernneq  11022  mulsubdivbinom2ap  11073  nn0opthd  11084  bcval5  11125  remullem  11556  cjreim2  11589  cnrecnv  11595  absval  11686  resqrexlemover  11695  resqrexlemcalc1  11699  resqrexlemnm  11703  absimle  11769  abstri  11789  bdtrilem  11924  mulcn2  11997  reccn2ap  11998  climcvg1nlem  12034  isummulc2  12112  fsummulc2  12134  fsumparts  12156  binomlem  12169  binom1dif  12173  trireciplem  12186  mertenslemi1  12221  mertensabs  12223  ntrivcvgap  12234  fprodmul  12277  efaddlem  12360  sinval  12388  cosval  12389  sinadd  12422  cosadd  12423  tanaddaplem  12424  tanaddap  12425  addsin  12428  sincossq  12434  sin2t  12435  cos12dec  12454  eirraplem  12463  dvdscmulr  12506  dvdsmulcr  12507  dvds2ln  12510  oddm1even  12561  divalglemnn  12604  divalglemnqt  12606  flodddiv4  12622  gcdaddm  12680  bezoutlemnewy  12692  bezoutlema  12695  bezoutlemb  12696  lcmgcdlem  12774  oddpwdc  12871  phiprmpw  12919  eulerthlema  12927  pythagtriplem12  12973  pythagtriplem14  12975  pythagtriplem16  12977  pcpremul  12991  pcaddlem  13037  fldivp1  13046  mul4sqlem  13091  4sqlem14  13102  oddennn  13143  cnfldui  14737  expghmap  14755  znunit  14807  expcn  15434  mulc1cncf  15454  mulcncf  15473  dvmulxxbr  15567  dvimulf  15571  dvexp  15576  dvmptmulx  15585  dvmptcmulcn  15586  plyf  15602  ply1termlem  15607  plyaddlem1  15612  plymullem1  15613  plycoeid3  15622  plycolemc  15623  plycjlemc  15625  plyrecj  15628  dvply1  15630  dvply2g  15631  sin0pilem1  15646  rpcxpef  15759  rpcncxpcl  15767  cxpap0  15769  rpcxpadd  15770  rpmulcxp  15774  cxpmul  15777  rpcxpmul2  15778  abscxp  15780  rpabscxpbnd  15805  binom4  15844  pellexlem1  15845  pellexlem2  15846  mpodvdsmulf1o  15858  fsumdvdsmul  15859  perfectlem2  15868  lgsquad2lem1  15954  2lgslem3b  15967  2lgslem3c  15968  2lgslem3d  15969  2sqlem3  15990  qdencn  16807  cvgcmp2nlemabs  16816  qdiff  16833  trimul0or  16845