Theorem mulcld 11164

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036   · cmul 11043

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

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  mul02lem1  11321  addrid  11325  cnegex  11326  kcnktkm1cn  11580  subaddmulsub  11612  mulsubaddmulsub  11613  receu  11794  divrec  11824  divcan3  11834  muldivdir  11846  subdivcomb1  11848  subdivcomb2  11849  divdivdiv  11854  divsubdiv  11869  lineq  11990  cru  12149  mul2lt0rlt0  13021  lincmb01cmp  13423  iccf1o  13424  flpmodeq  13806  moddiffl  13814  modvalp1  13822  modcyc  13838  modadd1  13840  modmuladdnn0  13850  modmul1  13859  modaddmulmod  13873  mulexpz  14037  expmulz  14043  binom3  14159  bernneq  14164  mulsubdivbinom2  14197  muldivbinom2  14198  remullem  15063  cjreim2  15096  absimle  15244  abstri  15266  sqreulem  15295  sqreu  15296  bhmafibid1cn  15401  bhmafibid2cn  15402  bhmafibid1  15403  bhmafibid2  15404  mulcn2  15531  reccn2  15532  o1rlimmul  15554  rlimmul  15580  isummulc2  15697  fsummulc2  15719  fsumparts  15741  binomlem  15764  binom1dif  15768  incexclem  15771  incexc  15772  incexc2  15773  pwdif  15803  geomulcvg  15811  mertenslem1  15819  mertens  15821  fprodmul  15895  fprodn0f  15926  iprodmul  15938  binomfallfaclem1  15974  binomfallfaclem2  15975  binomrisefac  15977  bpolycl  15987  bpolysum  15988  bpolydiflem  15989  bpoly4  15994  efaddlem  16028  sinadd  16101  cosadd  16102  tanaddlem  16103  tanadd  16104  addsin  16107  sincossq  16113  sin2t  16114  dvds2ln  16228  oddm1even  16282  pwp1fsum  16330  flodddiv4  16354  sadadd2lem2  16389  bezoutlem2  16479  bezoutlem3  16480  bezoutlem4  16481  lcmgcdlem  16545  phiprmpw  16715  pythagtriplem12  16766  pythagtriplem14  16768  pythagtriplem16  16770  pcpremul  16783  pcaddlem  16828  fldivp1  16837  mul4sqlem  16893  4sqlem14  16898  vdwapun  16914  vdwlem2  16922  vdwlem6  16926  ablsimpgfindlem1  20050  zringlpirlem3  21431  znunit  21530  blcvx  24754  icopnfcnv  24908  cphipipcj  25168  cphipval2  25209  4cphipval2  25210  cphipval  25211  mbfmulc2re  25617  mbfmulc2  25632  itg1addlem4  25668  itg1addlem5  25669  itg1mulc  25673  mbfmul  25695  itgcl  25753  itgcnlem  25759  iblmulc2  25800  itgmulc2  25803  itgabs  25804  itgsplit  25805  dvmulbr  25909  dvmulbrOLD  25910  dvcmul  25915  dvcmulf  25916  dvexp  25925  dvmptcmul  25936  dvmptdiv  25946  dvexp3  25950  dvsincos  25953  cmvth  25963  cmvthOLD  25964  dvlipcn  25967  dvfsumabs  25997  dvfsumlem1  26000  ftc1lem4  26014  itgparts  26022  itgpowd  26025  plyf  26171  ply1termlem  26176  plyeq0lem  26183  plypf1  26185  plyaddlem1  26186  plymullem1  26187  coeeulem  26197  coeidlem  26210  coeid3  26213  plyco  26214  coemullem  26223  coemulhi  26227  coemulc  26228  dgrcolem2  26248  plycjlem  26250  plyrecj  26255  dvply1  26259  vieta1lem2  26287  vieta1  26288  elqaalem3  26297  aareccl  26302  aalioulem1  26308  taylfvallem1  26332  tayl0  26337  dvtaylp  26346  taylthlem2  26350  taylthlem2OLD  26351  psergf  26389  radcnvlem1  26390  dvradcnv  26398  psercn2  26400  psercn2OLD  26401  pserdvlem2  26406  pserdv2  26408  abelthlem4  26412  abelthlem5  26413  abelthlem6  26414  abelthlem7  26416  abelthlem9  26418  tanregt0  26516  efgh  26518  efabl  26527  efsubm  26528  cosargd  26585  abslogle  26595  tanarg  26596  advlogexp  26632  logtayllem  26636  logtayl  26637  cxpadd  26656  mulcxp  26662  cxpmul  26665  cxpmul2  26666  cxpmul2z  26668  abscxp  26669  abscxp2  26670  dvcxp2  26718  abscxpbnd  26731  root1eq1  26733  cxpeq  26735  angcan  26780  pythag  26795  ssscongptld  26800  affineequiv  26801  affineequiv2  26802  affineequiv3  26803  affineequiv4  26804  chordthmlem2  26811  chordthmlem3  26812  chordthmlem4  26813  chordthmlem5  26814  heron  26816  quad2  26817  quad  26818  dcubic1lem  26821  dcubic2  26822  dcubic1  26823  dcubic  26824  mcubic  26825  cubic2  26826  cubic  26827  binom4  26828  dquartlem1  26829  dquartlem2  26830  dquart  26831  quart1cl  26832  quart1lem  26833  quart1  26834  quartlem1  26835  quartlem2  26836  atantayl3  26917  leibpi  26920  birthdaylem2  26930  divsqrtsumo1  26962  cvxcl  26963  jensenlem2  26966  lgamgulmlem2  27008  lgamgulmlem3  27009  lgamgulmlem4  27010  lgamgulmlem5  27011  lgamgulmlem6  27012  lgamgulm2  27014  lgamcvg2  27033  gamcvg  27034  gamcvg2lem  27037  wilthlem2  27047  ftalem1  27051  ftalem2  27052  ftalem4  27054  ftalem5  27055  basellem2  27060  basellem3  27061  basellem8  27066  muinv  27171  fsumdvdsmul  27173  fsumdvdsmulOLD  27175  logfacrlim  27203  logexprlim  27204  perfectlem2  27209  bposlem9  27271  gausslemma2dlem4  27348  lgsquad2lem1  27363  2lgslem3b  27376  2lgslem3c  27377  2lgslem3d  27378  2sqlem3  27399  2sqmod  27415  rplogsumlem1  27463  dchrisumlem2  27469  dchrisumlem3  27470  dchrmusum2  27473  dchrvmasumlem1  27474  dchrvmasum2lem  27475  dchrvmasum2if  27476  dchrvmasumlem3  27478  dchrvmasumiflem1  27480  dchrvmasumiflem2  27481  rpvmasum2  27491  dchrisum0lem1  27495  dchrisum0lem2a  27496  dchrisum0lem2  27497  dchrmusumlem  27501  dchrvmasumlem  27502  rplogsum  27506  mudivsum  27509  mulogsumlem  27510  mulogsum  27511  mulog2sumlem1  27513  mulog2sumlem2  27514  mulog2sumlem3  27515  vmalogdivsum  27518  logsqvma  27521  log2sumbnd  27523  selberglem1  27524  selberglem2  27525  selberglem3  27526  selberg  27527  selberg2lem  27529  selberg2  27530  selberg3lem1  27536  selberg3  27538  selberg4lem1  27539  selberg4  27540  pntrsumo1  27544  selbergr  27547  selberg3r  27548  selberg4r  27549  selberg34r  27550  pntsval2  27555  pntrlog2bndlem1  27556  pntrlog2bndlem2  27557  pntrlog2bndlem3  27558  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  pntrlog2bndlem6  27562  pntrlog2bnd  27563  pntlemb  27576  pntlemf  27584  pntlemo  27586  ostth2lem2  27613  ostth2lem3  27614  ttgcontlem1  28969  brbtwn2  28990  colinearalg  28995  ax5seglem2  29014  ax5seglem9  29022  axeuclidlem  29047  axcontlem2  29050  axcontlem4  29052  axcontlem7  29055  axcontlem8  29056  finsumvtxdg2ssteplem4  29634  ex-ind-dvds  30548  nrt2irr  30560  ipval2  30795  dipcl  30800  riesz3i  32150  re0cj  32834  pythagreim  32836  quad3d  32840  indsum  32953  indsumin  32954  dpfrac1  32984  wrdt2ind  33046  zringfrac  33647  ccfldsrarelvec  33849  ccfldextdgrr  33850  constrrtll  33909  constrrtlc1  33910  constrrtcclem  33912  constrrtcc  33913  constrconj  33923  constrfin  33924  constrelextdg2  33925  nn0constr  33939  constraddcl  33940  constrnegcl  33941  constrdircl  33943  iconstr  33944  constrremulcl  33945  constrrecl  33947  constrimcl  33948  constrmulcl  33949  constrreinvcl  33950  constrinvcl  33951  constrresqrtcl  33955  constrabscl  33956  constrsqrtcl  33957  cos9thpiminplylem1  33960  cos9thpiminplylem2  33961  cos9thpiminplylem3  33962  cos9thpiminply  33966  cos9thpinconstrlem1  33967  cos9thpinconstrlem2  33968  cos9thpinconstr  33969  cnre2csqima  34089  rmulccn  34106  dya2icoseg  34455  oddpwdc  34532  eulerpartlems  34538  eulerpartlemsv3  34539  eulerpartlemgs2  34558  signsplypnf  34728  itgexpif  34784  breprexplemc  34810  breprexp  34811  vtscl  34816  vtsprod  34817  circlemeth  34818  logdivsqrle  34828  hgt750lemf  34831  hgt750leme  34836  subfacval2  35403  subfaclim  35404  resconn  35462  iprodgam  35958  fwddifnp1  36381  knoppcnlem10  36724  knoppndvlem2  36735  knoppndvlem7  36740  knoppndvlem9  36742  knoppndvlem11  36744  knoppndvlem14  36747  knoppndvlem16  36749  knoppndvlem17  36750  bj-subcom  37563  bj-bary1lem  37565  bj-bary1lem1  37566  bj-bary1  37567  iblmulc2nc  37936  itgmulc2nc  37939  itgabsnc  37940  ftc1cnnclem  37942  ftc1anclem3  37946  dvasin  37955  areacirclem1  37959  areacirclem4  37962  areacirc  37964  cntotbnd  38047  3factsumint1  42391  3factsumint3  42393  3factsumint4  42394  lcmineqlem2  42400  lcmineqlem6  42404  lcmineqlem8  42406  lcmineqlem10  42408  lcmineqlem11  42409  lcmineqlem12  42410  lcmineqlem16  42414  lcmineqlem18  42416  lcmineqlem23  42421  3lexlogpow5ineq5  42430  aks4d1p1p1  42433  dvrelogpow2b  42438  aks4d1p1p6  42443  aks4d1p1p7  42444  aks4d1p1p5  42445  primrootscoprmpow  42469  posbezout  42470  primrootscoprbij  42472  primrootspoweq0  42476  2np3bcnp1  42514  2ap1caineq  42515  oddnumth  42681  nicomachus  42682  sumcubes  42683  ef11d  42709  cxp112d  42711  cxp111d  42712  readvrec2  42731  sn-addlid  42774  sn-it0e0  42786  sn-negex12  42787  sn-mul01  42796  sn-mullid  42806  sn-0tie0  42821  sn-mul02  42822  cnreeu  42860  fltnltalem  43020  fltnlta  43021  cu3addd  43038  3cubeslem2  43042  3cubeslem3l  43043  3cubeslem3r  43044  3cubeslem4  43046  pellexlem1  43186  pellexlem2  43187  pellexlem6  43191  pell1234qrne0  43210  pell1234qrreccl  43211  pell1234qrmulcl  43212  pell1234qrdich  43218  pell14qrdich  43226  pell1qrge1  43227  pell1qrgaplem  43230  rmspecsqrtnq  43263  qirropth  43265  rmxyneg  43277  rmxyadd  43278  rmxm1  43291  rmym1  43292  rmxluc  43293  rmyluc  43294  rmxdbl  43296  rmydbl  43297  jm2.18  43345  jm2.19lem1  43346  jm2.19lem2  43347  jm2.19lem4  43349  jm2.19  43350  jm2.22  43352  jm2.23  43353  jm2.25  43356  jm2.27c  43364  jm3.1lem2  43375  flcidc  43527  areaquad  43573  sqrtcval  43997  inductionexd  44511  imo72b2lem0  44521  int-leftdistd  44535  radcnvrat  44670  expgrowth  44691  binomcxplemwb  44704  binomcxplemnn0  44705  binomcxplemfrat  44707  binomcxplemdvbinom  44709  binomcxplemnotnn0  44712  sineq0ALT  45292  mul13d  45642  fperiodmullem  45665  fperiodmul  45666  divcan8d  45674  dmmcand  45675  ltdiv23neg  45752  mulc1cncfg  45949  mccllem  45957  clim1fr1  45961  mullimc  45976  mullimcf  45983  sumnnodd  45990  reclimc  46011  sinmulcos  46223  coskpi2  46224  cosknegpi  46227  dvsinexp  46269  dvasinbx  46278  dvdivf  46280  dvdivbd  46281  dvdivcncf  46285  dvbdfbdioolem2  46287  dvxpaek  46298  dvnxpaek  46300  dvnmul  46301  dvmptfprodlem  46302  dvnprodlem2  46305  itgsinexplem1  46312  itgsinexp  46313  itgcoscmulx  46327  itgsincmulx  46332  itgiccshift  46338  itgperiod  46339  stoweidlem1  46359  stoweidlem11  46369  stoweidlem13  46371  stoweidlem14  46372  stoweidlem17  46375  stoweidlem25  46383  stoweidlem26  46384  stoweidlem42  46400  wallispilem4  46426  wallispilem5  46427  wallispi  46428  wallispi2lem1  46429  wallispi2lem2  46430  wallispi2  46431  stirlinglem1  46432  stirlinglem3  46434  stirlinglem4  46435  stirlinglem5  46436  stirlinglem6  46437  stirlinglem7  46438  stirlinglem8  46439  stirlinglem10  46441  stirlinglem11  46442  stirlinglem12  46443  stirlinglem13  46444  stirlinglem14  46445  stirlinglem15  46446  dirker2re  46450  dirkerdenne0  46451  dirkerper  46454  dirkertrigeqlem1  46456  dirkertrigeqlem2  46457  dirkertrigeqlem3  46458  dirkertrigeq  46459  dirkeritg  46460  dirkercncflem2  46462  dirkercncflem4  46464  fourierdlem26  46491  fourierdlem30  46495  fourierdlem39  46504  fourierdlem42  46507  fourierdlem47  46511  fourierdlem48  46512  fourierdlem56  46520  fourierdlem57  46521  fourierdlem58  46522  fourierdlem62  46526  fourierdlem65  46529  fourierdlem66  46530  fourierdlem68  46532  fourierdlem72  46536  fourierdlem73  46537  fourierdlem76  46540  fourierdlem80  46544  fourierdlem83  46547  fourierdlem85  46549  fourierdlem89  46553  fourierdlem90  46554  fourierdlem91  46555  fourierdlem95  46559  fourierdlem97  46561  fourierdlem101  46565  fourierdlem103  46567  fourierdlem104  46568  fourierdlem111  46575  sqwvfoura  46586  sqwvfourb  46587  fourierswlem  46588  fouriersw  46589  elaa2lem  46591  etransclem8  46600  etransclem18  46610  etransclem20  46612  etransclem21  46613  etransclem23  46615  etransclem24  46616  etransclem31  46623  etransclem33  46625  etransclem35  46627  etransclem45  46637  etransclem46  46638  etransclem47  46639  etransclem48  46640  hoicvrrex  46914  hoidmvlelem2  46954  smfmullem1  47149  sigarim  47209  sigarac  47210  sigaraf  47211  sigarmf  47212  sigarls  47215  sigardiv  47219  sigarcol  47222  cevathlem1  47225  fldivmod  47698  fmtnorec2lem  47902  fmtnorec3  47908  fmtnorec4  47909  fmtnoprmfac1  47925  fmtnoprmfac2  47927  fmtnofac2lem  47928  sfprmdvdsmersenne  47963  lighneallem3  47967  quad1  47980  requad01  47981  requad2  47983  opeoALTV  48044  perfectALTVlem2  48082  fppr2odd  48091  0nodd  48530  2nodd  48532  2zlidl  48600  2zrngnmlid  48615  altgsumbcALT  48713  nn0sumshdiglemA  48979  nn0sumshdiglemB  48980  nn0sumshdiglem2  48982  nn0mullong  48985  itcovalt2lem2lem2  49034  ackval2  49042  submuladdmuld  49061  affinecomb2  49063  affineid  49064  1subrec1sub  49065  eenglngeehlnmlem1  49097  eenglngeehlnmlem2  49098  rrx2linest  49102  line2x  49114  line2y  49115  itschlc0yqe  49120  itsclc0yqsollem1  49122  itsclc0yqsol  49124  itscnhlc0xyqsol  49125  itschlc0xyqsol1  49126  itschlc0xyqsol  49127  itsclc0xyqsolr  49129  2itscplem1  49138  2itscplem2  49139  2itscplem3  49140  2itscp  49141  itscnhlinecirc02plem1  49142  itscnhlinecirc02plem2  49143  inlinecirc02plem  49146  inlinecirc02p  49147  i2linesd  50138  aacllem  50160  amgmwlem  50161  amgmlemALT  50162