Theorem mulcld 10341

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

Syntax hints:   → wi 4   ∈ wcel 2156  (class class class)co 6870  ℂcc 10215   · cmul 10222

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 10279

This theorem depends on definitions:  df-bi 198  df-an 385

This theorem is referenced by:  mul02lem1  10493  addid1  10497  cnegex  10498  kcnktkm1cn  10742  receu  10953  divrec  10982  divcan3  10992  muldivdir  11001  divdivdiv  11007  divsubdiv  11022  cru  11293  mul2lt0rlt0  12142  lincmb01cmp  12534  iccf1o  12535  flpmodeq  12893  moddiffl  12901  modvalp1  12909  modcyc  12925  modadd1  12927  modmuladdnn0  12934  modmul1  12943  modaddmulmod  12957  mulexpz  13119  expmulz  13125  binom3  13204  bernneq  13209  mulsubdivbinom2  13265  muldivbinom2  13266  remullem  14087  cjreim2  14120  absimle  14268  abstri  14289  sqreulem  14318  sqreu  14319  mulcn2  14545  reccn2  14546  o1rlimmul  14568  isummulc2  14712  fsummulc2  14734  fsumparts  14756  binomlem  14779  binom1dif  14783  incexclem  14786  incexc  14787  incexc2  14788  geomulcvg  14825  mertenslem1  14833  mertens  14835  fprodmul  14907  fprodn0f  14938  iprodmul  14950  binomfallfaclem1  14986  binomfallfaclem2  14987  binomrisefac  14989  bpolycl  14999  bpolysum  15000  bpolydiflem  15001  bpoly4  15006  efaddlem  15039  sinadd  15110  cosadd  15111  tanaddlem  15112  tanadd  15113  addsin  15116  sincossq  15122  sin2t  15123  dvds2ln  15233  oddm1even  15283  pwp1fsum  15330  flodddiv4  15352  sadadd2lem2  15387  bezoutlem2  15472  bezoutlem3  15473  bezoutlem4  15474  lcmgcdlem  15534  phiprmpw  15694  pythagtriplem12  15744  pythagtriplem14  15746  pythagtriplem16  15748  pcpremul  15761  pcaddlem  15805  fldivp1  15814  mul4sqlem  15870  4sqlem14  15875  vdwapun  15891  vdwlem2  15899  vdwlem6  15903  zringlpirlem3  20038  znunit  20115  blcvx  22811  icopnfcnv  22951  cphipipcj  23209  cphipval2  23249  4cphipval2  23250  cphipval  23251  mbfmulc2re  23628  mbfmulc2  23643  itg1addlem4  23679  itg1addlem5  23680  itg1mulc  23684  mbfmul  23706  itgcl  23763  itgcnlem  23769  iblmulc2  23810  itgmulc2  23813  itgabs  23814  itgsplit  23815  dvmulbr  23915  dvcmul  23920  dvcmulf  23921  dvexp  23929  dvmptcmul  23940  dvmptdiv  23950  dvexp3  23954  dvsincos  23957  cmvth  23967  dvlipcn  23970  dvfsumabs  23999  dvfsumlem1  24002  ftc1lem4  24015  itgparts  24023  plyf  24167  ply1termlem  24172  plyeq0lem  24179  plypf1  24181  plyaddlem1  24182  plymullem1  24183  coeeulem  24193  coeidlem  24206  coeid3  24209  plyco  24210  coemullem  24219  coemulhi  24223  coemulc  24224  dgrcolem2  24243  plycjlem  24245  plyrecj  24248  dvply1  24252  vieta1lem2  24279  vieta1  24280  elqaalem3  24289  aareccl  24294  aalioulem1  24300  taylfvallem1  24324  tayl0  24329  dvtaylp  24337  taylthlem2  24341  psergf  24379  radcnvlem1  24380  dvradcnv  24388  psercn2  24390  pserdvlem2  24395  pserdv2  24397  abelthlem4  24401  abelthlem5  24402  abelthlem6  24403  abelthlem7  24405  abelthlem9  24407  tanregt0  24499  efgh  24501  efabl  24510  efsubm  24511  cosargd  24567  abslogle  24577  tanarg  24578  advlogexp  24614  logtayllem  24618  logtayl  24619  cxpadd  24638  mulcxp  24644  cxpmul  24647  cxpmul2  24648  cxpmul2z  24650  abscxp  24651  abscxp2  24652  dvcxp2  24695  abscxpbnd  24707  root1eq1  24709  cxpeq  24711  angcan  24745  pythag  24760  ssscongptld  24765  affineequiv  24766  affineequiv2  24767  chordthmlem2  24773  chordthmlem3  24774  chordthmlem4  24775  chordthmlem5  24776  heron  24778  quad2  24779  quad  24780  dcubic1lem  24783  dcubic2  24784  dcubic1  24785  dcubic  24786  mcubic  24787  cubic2  24788  cubic  24789  binom4  24790  dquartlem1  24791  dquartlem2  24792  dquart  24793  quart1cl  24794  quart1lem  24795  quart1  24796  quartlem1  24797  quartlem2  24798  atantayl3  24879  leibpi  24882  birthdaylem2  24892  divsqrtsumo1  24923  cvxcl  24924  jensenlem2  24927  lgamgulmlem2  24969  lgamgulmlem3  24970  lgamgulmlem4  24971  lgamgulmlem5  24972  lgamgulmlem6  24973  lgamgulm2  24975  lgamcvg2  24994  gamcvg  24995  gamcvg2lem  24998  wilthlem2  25008  ftalem1  25012  ftalem2  25013  ftalem4  25015  ftalem5  25016  basellem2  25021  basellem3  25022  basellem8  25027  muinv  25132  fsumdvdsmul  25134  logfacrlim  25162  logexprlim  25163  perfectlem2  25168  bposlem9  25230  gausslemma2dlem4  25307  lgsquad2lem1  25322  2lgslem3b  25335  2lgslem3c  25336  2lgslem3d  25337  2sqlem3  25358  rplogsumlem1  25386  dchrisumlem2  25392  dchrisumlem3  25393  dchrmusum2  25396  dchrvmasumlem1  25397  dchrvmasum2lem  25398  dchrvmasum2if  25399  dchrvmasumlem3  25401  dchrvmasumiflem1  25403  dchrvmasumiflem2  25404  rpvmasum2  25414  dchrisum0lem1  25418  dchrisum0lem2a  25419  dchrisum0lem2  25420  dchrmusumlem  25424  dchrvmasumlem  25425  rplogsum  25429  mudivsum  25432  mulogsumlem  25433  mulogsum  25434  mulog2sumlem1  25436  mulog2sumlem2  25437  mulog2sumlem3  25438  vmalogdivsum  25441  logsqvma  25444  log2sumbnd  25446  selberglem1  25447  selberglem2  25448  selberglem3  25449  selberg  25450  selberg2lem  25452  selberg2  25453  selberg3lem1  25459  selberg3  25461  selberg4lem1  25462  selberg4  25463  pntrsumo1  25467  selbergr  25470  selberg3r  25471  selberg4r  25472  selberg34r  25473  pntsval2  25478  pntrlog2bndlem1  25479  pntrlog2bndlem2  25480  pntrlog2bndlem3  25481  pntrlog2bndlem4  25482  pntrlog2bndlem5  25483  pntrlog2bndlem6  25485  pntrlog2bnd  25486  pntlemb  25499  pntlemf  25507  pntlemo  25509  ostth2lem2  25536  ostth2lem3  25537  ttgcontlem1  25978  brbtwn2  25998  colinearalg  26003  ax5seglem2  26022  ax5seglem9  26030  axeuclidlem  26055  axcontlem2  26058  axcontlem4  26060  axcontlem7  26063  axcontlem8  26064  finsumvtxdg2ssteplem4  26671  ex-ind-dvds  27648  ipval2  27889  dipcl  27894  riesz3i  29248  dpfrac1  29924  bhmafibid1  29968  bhmafibid2  29969  2sqmod  29972  cnre2csqima  30281  rmulccn  30298  indsum  30407  indsumin  30408  dya2icoseg  30663  oddpwdc  30740  eulerpartlems  30746  eulerpartlemsv3  30747  eulerpartlemgs2  30766  signsplypnf  30951  itgexpif  31008  breprexplemc  31034  breprexp  31035  vtscl  31040  vtsprod  31041  circlemeth  31042  logdivsqrle  31052  hgt750lemf  31055  hgt750leme  31060  subfacval2  31490  subfaclim  31491  resconn  31549  subdivcomb1  31931  subdivcomb2  31932  iprodgam  31948  fwddifnp1  32591  knoppndvlem2  32819  knoppndvlem7  32824  knoppndvlem9  32826  knoppndvlem11  32828  knoppndvlem14  32831  knoppndvlem16  32833  knoppndvlem17  32834  bj-subcom  33469  bj-lineq  33473  bj-bary1lem  33475  bj-bary1lem1  33476  bj-bary1  33477  iblmulc2nc  33785  itgmulc2nc  33788  itgabsnc  33789  ftc1cnnclem  33793  ftc1anclem3  33797  dvasin  33806  areacirclem1  33810  areacirclem4  33813  areacirc  33815  cntotbnd  33904  pellexlem1  37892  pellexlem2  37893  pellexlem6  37897  pell1234qrne0  37916  pell1234qrreccl  37917  pell1234qrmulcl  37918  pell1234qrdich  37924  pell14qrdich  37932  pell1qrge1  37933  pell1qrgaplem  37936  rmspecsqrtnq  37969  qirropth  37971  rmxyneg  37983  rmxyadd  37984  rmxm1  37997  rmym1  37998  rmxluc  37999  rmyluc  38000  rmxdbl  38002  rmydbl  38003  jm2.18  38053  jm2.19lem1  38054  jm2.19lem2  38055  jm2.19lem4  38057  jm2.19  38058  jm2.22  38060  jm2.23  38061  jm2.25  38064  jm2.27c  38072  jm3.1lem2  38083  flcidc  38242  itgpowd  38297  areaquad  38299  inductionexd  38950  imo72b2lem0  38962  int-leftdistd  38979  radcnvrat  39010  expgrowth  39031  binomcxplemwb  39044  binomcxplemnn0  39045  binomcxplemfrat  39047  binomcxplemdvbinom  39049  binomcxplemnotnn0  39052  sineq0ALT  39664  mul13d  39970  fperiodmullem  39995  fperiodmul  39996  divcan8d  40004  dmmcand  40005  ltdiv23neg  40093  mulc1cncfg  40298  mccllem  40306  clim1fr1  40310  mullimc  40325  mullimcf  40332  sumnnodd  40339  reclimc  40362  sinmulcos  40553  coskpi2  40554  cosknegpi  40557  dvsinexp  40602  dvasinbx  40612  dvdivf  40614  dvdivbd  40615  dvdivcncf  40619  dvbdfbdioolem2  40621  dvxpaek  40632  dvnxpaek  40634  dvnmul  40635  dvmptfprodlem  40636  dvnprodlem2  40639  itgsinexplem1  40646  itgsinexp  40647  itgcoscmulx  40661  itgsincmulx  40666  itgiccshift  40672  itgperiod  40673  stoweidlem1  40694  stoweidlem11  40704  stoweidlem13  40706  stoweidlem14  40707  stoweidlem17  40710  stoweidlem25  40718  stoweidlem26  40719  stoweidlem42  40735  wallispilem4  40761  wallispilem5  40762  wallispi  40763  wallispi2lem1  40764  wallispi2lem2  40765  wallispi2  40766  stirlinglem1  40767  stirlinglem3  40769  stirlinglem4  40770  stirlinglem5  40771  stirlinglem6  40772  stirlinglem7  40773  stirlinglem8  40774  stirlinglem10  40776  stirlinglem11  40777  stirlinglem12  40778  stirlinglem13  40779  stirlinglem14  40780  stirlinglem15  40781  dirker2re  40785  dirkerdenne0  40786  dirkerper  40789  dirkertrigeqlem1  40791  dirkertrigeqlem2  40792  dirkertrigeqlem3  40793  dirkertrigeq  40794  dirkeritg  40795  dirkercncflem2  40797  dirkercncflem4  40799  fourierdlem26  40826  fourierdlem30  40830  fourierdlem39  40839  fourierdlem42  40842  fourierdlem47  40846  fourierdlem48  40847  fourierdlem56  40855  fourierdlem57  40856  fourierdlem58  40857  fourierdlem62  40861  fourierdlem65  40864  fourierdlem66  40865  fourierdlem68  40867  fourierdlem72  40871  fourierdlem73  40872  fourierdlem76  40875  fourierdlem80  40879  fourierdlem83  40882  fourierdlem85  40884  fourierdlem89  40888  fourierdlem90  40889  fourierdlem91  40890  fourierdlem95  40894  fourierdlem97  40896  fourierdlem101  40900  fourierdlem103  40902  fourierdlem104  40903  fourierdlem111  40910  sqwvfoura  40921  sqwvfourb  40922  fourierswlem  40923  fouriersw  40924  elaa2lem  40926  etransclem8  40935  etransclem18  40945  etransclem20  40947  etransclem21  40948  etransclem23  40950  etransclem24  40951  etransclem31  40958  etransclem33  40960  etransclem35  40962  etransclem45  40972  etransclem46  40973  etransclem47  40974  etransclem48  40975  hoicvrrex  41249  hoidmvlelem2  41289  smfmullem1  41477  sigarim  41519  sigarac  41520  sigaraf  41521  sigarmf  41522  sigarls  41525  sigardiv  41529  sigarcol  41532  cevathlem1  41535  fmtnorec2lem  42026  fmtnorec3  42032  fmtnorec4  42033  fmtnoprmfac1  42049  fmtnoprmfac2  42051  fmtnofac2lem  42052  pwdif  42073  sfprmdvdsmersenne  42092  lighneallem3  42096  opeoALTV  42167  perfectALTVlem2  42203  0nodd  42375  2nodd  42377  2zlidl  42499  2zrngnmlid  42514  altgsumbcALT  42696  fldivmod  42878  nn0sumshdiglemA  42978  nn0sumshdiglemB  42979  nn0sumshdiglem2  42981  nn0mullong  42984  i2linesd  43093  aacllem  43115  amgmwlem  43116  amgmlemALT  43117