Theorem mulcld 9939

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

Syntax hints:   → wi 4   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813   · cmul 9820

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

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

This theorem is referenced by:  mul02lem1  10091  addid1  10095  cnegex  10096  kcnktkm1cn  10340  receu  10551  divrec  10580  divcan3  10590  muldivdir  10599  divdivdiv  10605  divsubdiv  10620  cru  10889  mul2lt0rlt0  11808  lincmb01cmp  12186  iccf1o  12187  flpmodeq  12535  moddiffl  12543  modvalp1  12551  modcyc  12567  modadd1  12569  modmuladdnn0  12576  modmul1  12585  modaddmulmod  12599  mulexpz  12762  expmulz  12768  binom3  12847  bernneq  12852  mulsubdivbinom2  12908  muldivbinom2  12909  remullem  13716  cjreim2  13749  absimle  13897  abstri  13918  sqreulem  13947  sqreu  13948  mulcn2  14174  reccn2  14175  o1rlimmul  14197  isummulc2  14335  fsummulc2  14358  fsumparts  14379  binomlem  14400  binom1dif  14404  incexclem  14407  incexc  14408  incexc2  14409  geomulcvg  14446  mertenslem1  14455  mertens  14457  fprodmul  14529  fprodn0f  14561  iprodmul  14573  binomfallfaclem1  14609  binomfallfaclem2  14610  binomrisefac  14612  bpolycl  14622  bpolysum  14623  bpolydiflem  14624  bpoly4  14629  efaddlem  14662  sinadd  14733  cosadd  14734  tanaddlem  14735  tanadd  14736  addsin  14739  sincossq  14745  sin2t  14746  dvds2ln  14852  oddm1even  14905  pwp1fsum  14952  flodddiv4  14975  sadadd2lem2  15010  bezoutlem2  15095  bezoutlem3  15096  bezoutlem4  15097  lcmgcdlem  15157  phiprmpw  15319  pythagtriplem12  15369  pythagtriplem14  15371  pythagtriplem16  15373  pcpremul  15386  pcaddlem  15430  fldivp1  15439  mul4sqlem  15495  4sqlem14  15500  vdwapun  15516  vdwlem2  15524  vdwlem6  15528  zringlpirlem3  19653  znunit  19731  blcvx  22409  icopnfcnv  22549  cphipipcj  22808  cphipval2  22848  4cphipval2  22849  cphipval  22850  mbfmulc2re  23221  mbfmulc2  23236  itg1addlem4  23272  itg1addlem5  23273  itg1mulc  23277  mbfmul  23299  itgcl  23356  itgcnlem  23362  iblmulc2  23403  itgmulc2  23406  itgabs  23407  itgsplit  23408  dvmulbr  23508  dvcmul  23513  dvcmulf  23514  dvexp  23522  dvmptcmul  23533  dvexp3  23545  dvsincos  23548  cmvth  23558  dvlipcn  23561  dvfsumabs  23590  dvfsumlem1  23593  ftc1lem4  23606  itgparts  23614  plyf  23758  ply1termlem  23763  plyeq0lem  23770  plypf1  23772  plyaddlem1  23773  plymullem1  23774  coeeulem  23784  coeidlem  23797  coeid3  23800  plyco  23801  coemullem  23810  coemulhi  23814  coemulc  23815  dgrcolem2  23834  plycjlem  23836  plyrecj  23839  dvply1  23843  vieta1lem2  23870  vieta1  23871  elqaalem3  23880  aareccl  23885  aalioulem1  23891  taylfvallem1  23915  tayl0  23920  dvtaylp  23928  taylthlem2  23932  psergf  23970  radcnvlem1  23971  dvradcnv  23979  psercn2  23981  pserdvlem2  23986  pserdv2  23988  abelthlem4  23992  abelthlem5  23993  abelthlem6  23994  abelthlem7  23996  abelthlem9  23998  tanregt0  24089  efgh  24091  efabl  24100  efsubm  24101  cosargd  24158  abslogle  24168  tanarg  24169  advlogexp  24201  logtayllem  24205  logtayl  24206  cxpadd  24225  mulcxp  24231  cxpmul  24234  cxpmul2  24235  cxpmul2z  24237  abscxp  24238  abscxp2  24239  dvcxp2  24282  abscxpbnd  24294  root1eq1  24296  cxpeq  24298  angcan  24332  pythag  24347  ssscongptld  24352  affineequiv  24353  affineequiv2  24354  chordthmlem2  24360  chordthmlem3  24361  chordthmlem4  24362  chordthmlem5  24363  heron  24365  quad2  24366  quad  24367  dcubic1lem  24370  dcubic2  24371  dcubic1  24372  dcubic  24373  mcubic  24374  cubic2  24375  cubic  24376  binom4  24377  dquartlem1  24378  dquartlem2  24379  dquart  24380  quart1cl  24381  quart1lem  24382  quart1  24383  quartlem1  24384  quartlem2  24385  atantayl3  24466  leibpi  24469  birthdaylem2  24479  divsqrtsumo1  24510  cvxcl  24511  jensenlem2  24514  lgamgulmlem2  24556  lgamgulmlem3  24557  lgamgulmlem4  24558  lgamgulmlem5  24559  lgamgulmlem6  24560  lgamgulm2  24562  lgamcvg2  24581  gamcvg  24582  gamcvg2lem  24585  wilthlem2  24595  ftalem1  24599  ftalem2  24600  ftalem4  24602  ftalem5  24603  basellem2  24608  basellem3  24609  basellem8  24614  muinv  24719  fsumdvdsmul  24721  logfacrlim  24749  logexprlim  24750  perfectlem2  24755  bposlem9  24817  gausslemma2dlem4  24894  lgsquad2lem1  24909  2lgslem3b  24922  2lgslem3c  24923  2lgslem3d  24924  2sqlem3  24945  rplogsumlem1  24973  dchrisumlem2  24979  dchrisumlem3  24980  dchrmusum2  24983  dchrvmasumlem1  24984  dchrvmasum2lem  24985  dchrvmasum2if  24986  dchrvmasumlem3  24988  dchrvmasumiflem1  24990  dchrvmasumiflem2  24991  rpvmasum2  25001  dchrisum0lem1  25005  dchrisum0lem2a  25006  dchrisum0lem2  25007  dchrmusumlem  25011  dchrvmasumlem  25012  rplogsum  25016  mudivsum  25019  mulogsumlem  25020  mulogsum  25021  mulog2sumlem1  25023  mulog2sumlem2  25024  mulog2sumlem3  25025  vmalogdivsum  25028  logsqvma  25031  log2sumbnd  25033  selberglem1  25034  selberglem2  25035  selberglem3  25036  selberg  25037  selberg2lem  25039  selberg2  25040  selberg3lem1  25046  selberg3  25048  selberg4lem1  25049  selberg4  25050  pntrsumo1  25054  selbergr  25057  selberg3r  25058  selberg4r  25059  selberg34r  25060  pntsval2  25065  pntrlog2bndlem1  25066  pntrlog2bndlem2  25067  pntrlog2bndlem3  25068  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntrlog2bndlem6  25072  pntrlog2bnd  25073  pntlemb  25086  pntlemf  25094  pntlemo  25096  ostth2lem2  25123  ostth2lem3  25124  ttgcontlem1  25565  brbtwn2  25585  colinearalg  25590  ax5seglem2  25609  ax5seglem9  25617  axeuclidlem  25642  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  axcontlem8  25651  ex-ind-dvds  26710  ipval2  26946  dipcl  26951  riesz3i  28305  bhmafibid1  28975  bhmafibid2  28976  2sqmod  28979  cnre2csqima  29285  rmulccn  29302  indsum  29412  dya2icoseg  29666  oddpwdc  29743  eulerpartlems  29749  eulerpartlemsv3  29750  eulerpartlemgs2  29769  signsplypnf  29953  subfacval2  30423  subfaclim  30424  rescon  30482  subdivcomb1  30864  subdivcomb2  30865  iprodgam  30881  fwddifnp1  31442  knoppndvlem2  31674  knoppndvlem7  31679  knoppndvlem9  31681  knoppndvlem11  31683  knoppndvlem14  31686  knoppndvlem16  31688  knoppndvlem17  31689  bj-subcom  32331  bj-lineq  32335  bj-bary1lem  32337  bj-bary1lem1  32338  bj-bary1  32339  iblmulc2nc  32645  itgmulc2nc  32648  itgabsnc  32649  ftc1cnnclem  32653  ftc1anclem3  32657  dvasin  32666  areacirclem1  32670  areacirclem4  32673  areacirc  32675  cntotbnd  32765  pellexlem1  36411  pellexlem2  36412  pellexlem6  36416  pell1234qrne0  36435  pell1234qrreccl  36436  pell1234qrmulcl  36437  pell1234qrdich  36443  pell14qrdich  36451  pell1qrge1  36452  pell1qrgaplem  36455  rmspecsqrtnq  36488  qirropth  36491  rmxyneg  36503  rmxyadd  36504  rmxm1  36517  rmym1  36518  rmxluc  36519  rmyluc  36520  rmxdbl  36522  rmydbl  36523  jm2.18  36573  jm2.19lem1  36574  jm2.19lem2  36575  jm2.19lem4  36577  jm2.19  36578  jm2.22  36580  jm2.23  36581  jm2.25  36584  jm2.27c  36592  jm3.1lem2  36603  flcidc  36763  itgpowd  36819  areaquad  36821  inductionexd  37473  imo72b2lem0  37487  int-leftdistd  37504  radcnvrat  37535  expgrowth  37556  binomcxplemwb  37569  binomcxplemnn0  37570  binomcxplemfrat  37572  binomcxplemdvbinom  37574  binomcxplemnotnn0  37577  sineq0ALT  38195  mul13d  38432  fperiodmullem  38458  fperiodmul  38459  divcan8d  38468  dmmcand  38469  ltdiv23neg  38558  mulc1cncfg  38656  mccllem  38664  clim1fr1  38668  mullimc  38683  mullimcf  38690  sumnnodd  38697  reclimc  38720  sinmulcos  38748  coskpi2  38749  cosknegpi  38752  dvsinexp  38798  dvmptdiv  38807  dvasinbx  38810  dvdivf  38812  dvdivbd  38813  dvdivcncf  38817  dvbdfbdioolem2  38819  dvxpaek  38830  dvnxpaek  38832  dvnmul  38833  dvmptfprodlem  38834  dvnprodlem2  38837  itgsinexplem1  38845  itgsinexp  38846  itgcoscmulx  38861  itgsincmulx  38866  itgiccshift  38872  itgperiod  38873  stoweidlem1  38894  stoweidlem11  38904  stoweidlem13  38906  stoweidlem14  38907  stoweidlem17  38910  stoweidlem25  38918  stoweidlem26  38919  stoweidlem42  38935  wallispilem4  38961  wallispilem5  38962  wallispi  38963  wallispi2lem1  38964  wallispi2lem2  38965  wallispi2  38966  stirlinglem1  38967  stirlinglem3  38969  stirlinglem4  38970  stirlinglem5  38971  stirlinglem6  38972  stirlinglem7  38973  stirlinglem8  38974  stirlinglem10  38976  stirlinglem11  38977  stirlinglem12  38978  stirlinglem13  38979  stirlinglem14  38980  stirlinglem15  38981  dirker2re  38985  dirkerdenne0  38986  dirkerper  38989  dirkertrigeqlem1  38991  dirkertrigeqlem2  38992  dirkertrigeqlem3  38993  dirkertrigeq  38994  dirkeritg  38995  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem26  39026  fourierdlem30  39030  fourierdlem39  39039  fourierdlem42  39042  fourierdlem47  39046  fourierdlem48  39047  fourierdlem56  39055  fourierdlem57  39056  fourierdlem58  39057  fourierdlem62  39061  fourierdlem65  39064  fourierdlem66  39065  fourierdlem68  39067  fourierdlem72  39071  fourierdlem73  39072  fourierdlem76  39075  fourierdlem80  39079  fourierdlem83  39082  fourierdlem85  39084  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem95  39094  fourierdlem97  39096  fourierdlem101  39100  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  sqwvfoura  39121  sqwvfourb  39122  fourierswlem  39123  fouriersw  39124  elaa2lem  39126  etransclem8  39135  etransclem18  39145  etransclem20  39147  etransclem21  39148  etransclem23  39150  etransclem24  39151  etransclem31  39158  etransclem33  39160  etransclem35  39162  etransclem45  39172  etransclem46  39173  etransclem47  39174  etransclem48  39175  hoicvrrex  39446  hoidmvlelem2  39486  smfmullem1  39676  sigarim  39689  sigarac  39690  sigaraf  39691  sigarmf  39692  sigarls  39695  sigardiv  39699  sigarcol  39702  cevathlem1  39705  fmtnorec2lem  39992  fmtnorec3  39998  fmtnorec4  39999  fmtnoprmfac1  40015  fmtnoprmfac2  40017  fmtnofac2lem  40018  pwdif  40039  sfprmdvdsmersenne  40058  lighneallem3  40062  opeoALTV  40133  perfectALTVlem2  40165  0nodd  41600  2nodd  41602  2zlidl  41724  2zrngnmlid  41739  altgsumbcALT  41924  fldivmod  42107  nn0sumshdiglemA  42211  nn0sumshdiglemB  42212  nn0sumshdiglem2  42214  nn0mullong  42217  dpfrac1  42312  i2linesd  42334  aacllem  42356  amgmwlem  42357  amgmlemALT  42358