Theorem mulcld 11165

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 7367  ℂ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  11322  addrid  11326  cnegex  11327  kcnktkm1cn  11581  subaddmulsub  11613  mulsubaddmulsub  11614  receu  11795  divrec  11825  divcan3  11835  muldivdir  11847  subdivcomb1  11850  subdivcomb2  11851  divdivdiv  11856  divsubdiv  11871  lineq  11992  cru  12151  mul2lt0rlt0  13046  lincmb01cmp  13448  iccf1o  13449  flpmodeq  13833  moddiffl  13841  modvalp1  13849  modcyc  13865  modadd1  13867  modmuladdnn0  13877  modmul1  13886  modaddmulmod  13900  mulexpz  14064  expmulz  14070  binom3  14186  bernneq  14191  mulsubdivbinom2  14224  muldivbinom2  14225  remullem  15090  cjreim2  15123  absimle  15271  abstri  15293  sqreulem  15322  sqreu  15323  bhmafibid1cn  15428  bhmafibid2cn  15429  bhmafibid1  15430  bhmafibid2  15431  mulcn2  15558  reccn2  15559  o1rlimmul  15581  rlimmul  15607  isummulc2  15724  fsummulc2  15746  fsumparts  15769  indsum  15791  binomlem  15794  binom1dif  15798  incexclem  15801  incexc  15802  incexc2  15803  pwdif  15833  geomulcvg  15841  mertenslem1  15849  mertens  15851  fprodmul  15925  fprodn0f  15956  iprodmul  15968  binomfallfaclem1  16004  binomfallfaclem2  16005  binomrisefac  16007  bpolycl  16017  bpolysum  16018  bpolydiflem  16019  bpoly4  16024  efaddlem  16058  sinadd  16131  cosadd  16132  tanaddlem  16133  tanadd  16134  addsin  16137  sincossq  16143  sin2t  16144  dvds2ln  16258  oddm1even  16312  pwp1fsum  16360  flodddiv4  16384  sadadd2lem2  16419  bezoutlem2  16509  bezoutlem3  16510  bezoutlem4  16511  lcmgcdlem  16575  phiprmpw  16746  pythagtriplem12  16797  pythagtriplem14  16799  pythagtriplem16  16801  pcpremul  16814  pcaddlem  16859  fldivp1  16868  mul4sqlem  16924  4sqlem14  16929  vdwapun  16945  vdwlem2  16953  vdwlem6  16957  ablsimpgfindlem1  20084  zringlpirlem3  21444  znunit  21543  blcvx  24763  icopnfcnv  24909  cphipipcj  25167  cphipval2  25208  4cphipval2  25209  cphipval  25210  mbfmulc2re  25615  mbfmulc2  25630  itg1addlem4  25666  itg1addlem5  25667  itg1mulc  25671  mbfmul  25693  itgcl  25751  itgcnlem  25757  iblmulc2  25798  itgmulc2  25801  itgabs  25802  itgsplit  25803  dvmulbr  25906  dvcmul  25911  dvcmulf  25912  dvexp  25920  dvmptcmul  25931  dvmptdiv  25941  dvexp3  25945  dvsincos  25948  cmvth  25958  dvlipcn  25961  dvfsumabs  25990  dvfsumlem1  25993  ftc1lem4  26006  itgparts  26014  itgpowd  26017  plyf  26163  ply1termlem  26168  plyeq0lem  26175  plypf1  26177  plyaddlem1  26178  plymullem1  26179  coeeulem  26189  coeidlem  26202  coeid3  26205  plyco  26206  coemullem  26215  coemulhi  26219  coemulc  26220  dgrcolem2  26239  plycjlem  26241  plyrecj  26246  dvply1  26250  vieta1lem2  26277  vieta1  26278  elqaalem3  26287  aareccl  26292  aalioulem1  26298  taylfvallem1  26322  tayl0  26327  dvtaylp  26335  taylthlem2  26339  psergf  26377  radcnvlem1  26378  dvradcnv  26386  psercn2  26388  pserdvlem2  26393  pserdv2  26395  abelthlem4  26399  abelthlem5  26400  abelthlem6  26401  abelthlem7  26403  abelthlem9  26405  tanregt0  26503  efgh  26505  efabl  26514  efsubm  26515  cosargd  26572  abslogle  26582  tanarg  26583  advlogexp  26619  logtayllem  26623  logtayl  26624  cxpadd  26643  mulcxp  26649  cxpmul  26652  cxpmul2  26653  cxpmul2z  26655  abscxp  26656  abscxp2  26657  dvcxp2  26705  abscxpbnd  26717  root1eq1  26719  cxpeq  26721  angcan  26766  pythag  26781  ssscongptld  26786  affineequiv  26787  affineequiv2  26788  affineequiv3  26789  affineequiv4  26790  chordthmlem2  26797  chordthmlem3  26798  chordthmlem4  26799  chordthmlem5  26800  heron  26802  quad2  26803  quad  26804  dcubic1lem  26807  dcubic2  26808  dcubic1  26809  dcubic  26810  mcubic  26811  cubic2  26812  cubic  26813  binom4  26814  dquartlem1  26815  dquartlem2  26816  dquart  26817  quart1cl  26818  quart1lem  26819  quart1  26820  quartlem1  26821  quartlem2  26822  atantayl3  26903  leibpi  26906  birthdaylem2  26916  divsqrtsumo1  26947  cvxcl  26948  jensenlem2  26951  lgamgulmlem2  26993  lgamgulmlem3  26994  lgamgulmlem4  26995  lgamgulmlem5  26996  lgamgulmlem6  26997  lgamgulm2  26999  lgamcvg2  27018  gamcvg  27019  gamcvg2lem  27022  wilthlem2  27032  ftalem1  27036  ftalem2  27037  ftalem4  27039  ftalem5  27040  basellem2  27045  basellem3  27046  basellem8  27051  muinv  27156  fsumdvdsmul  27158  logfacrlim  27187  logexprlim  27188  perfectlem2  27193  bposlem9  27255  gausslemma2dlem4  27332  lgsquad2lem1  27347  2lgslem3b  27360  2lgslem3c  27361  2lgslem3d  27362  2sqlem3  27383  2sqmod  27399  rplogsumlem1  27447  dchrisumlem2  27453  dchrisumlem3  27454  dchrmusum2  27457  dchrvmasumlem1  27458  dchrvmasum2lem  27459  dchrvmasum2if  27460  dchrvmasumlem3  27462  dchrvmasumiflem1  27464  dchrvmasumiflem2  27465  rpvmasum2  27475  dchrisum0lem1  27479  dchrisum0lem2a  27480  dchrisum0lem2  27481  dchrmusumlem  27485  dchrvmasumlem  27486  rplogsum  27490  mudivsum  27493  mulogsumlem  27494  mulogsum  27495  mulog2sumlem1  27497  mulog2sumlem2  27498  mulog2sumlem3  27499  vmalogdivsum  27502  logsqvma  27505  log2sumbnd  27507  selberglem1  27508  selberglem2  27509  selberglem3  27510  selberg  27511  selberg2lem  27513  selberg2  27514  selberg3lem1  27520  selberg3  27522  selberg4lem1  27523  selberg4  27524  pntrsumo1  27528  selbergr  27531  selberg3r  27532  selberg4r  27533  selberg34r  27534  pntsval2  27539  pntrlog2bndlem1  27540  pntrlog2bndlem2  27541  pntrlog2bndlem3  27542  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntrlog2bndlem6  27546  pntrlog2bnd  27547  pntlemb  27560  pntlemf  27568  pntlemo  27570  ostth2lem2  27597  ostth2lem3  27598  ttgcontlem1  28953  brbtwn2  28974  colinearalg  28979  ax5seglem2  28998  ax5seglem9  29006  axeuclidlem  29031  axcontlem2  29034  axcontlem4  29036  axcontlem7  29039  axcontlem8  29040  finsumvtxdg2ssteplem4  29617  ex-ind-dvds  30531  nrt2irr  30543  ipval2  30778  dipcl  30783  riesz3i  32133  re0cj  32816  pythagreim  32818  quad3d  32822  indsumin  32921  dpfrac1  32951  wrdt2ind  33013  zringfrac  33614  ccfldsrarelvec  33815  ccfldextdgrr  33816  constrrtll  33875  constrrtlc1  33876  constrrtcclem  33878  constrrtcc  33879  constrconj  33889  constrfin  33890  constrelextdg2  33891  nn0constr  33905  constraddcl  33906  constrnegcl  33907  constrdircl  33909  iconstr  33910  constrremulcl  33911  constrrecl  33913  constrimcl  33914  constrmulcl  33915  constrreinvcl  33916  constrinvcl  33917  constrresqrtcl  33921  constrabscl  33922  constrsqrtcl  33923  cos9thpiminplylem1  33926  cos9thpiminplylem2  33927  cos9thpiminplylem3  33928  cos9thpiminply  33932  cos9thpinconstrlem1  33933  cos9thpinconstrlem2  33934  cos9thpinconstr  33935  cnre2csqima  34055  rmulccn  34072  dya2icoseg  34421  oddpwdc  34498  eulerpartlems  34504  eulerpartlemsv3  34505  eulerpartlemgs2  34524  signsplypnf  34694  itgexpif  34750  breprexplemc  34776  breprexp  34777  vtscl  34782  vtsprod  34783  circlemeth  34784  logdivsqrle  34794  hgt750lemf  34797  hgt750leme  34802  subfacval2  35369  subfaclim  35370  resconn  35428  iprodgam  35924  fwddifnp1  36347  knoppcnlem10  36762  knoppndvlem2  36773  knoppndvlem7  36778  knoppndvlem9  36780  knoppndvlem11  36782  knoppndvlem14  36785  knoppndvlem16  36787  knoppndvlem17  36788  bj-subcom  37622  bj-bary1lem  37624  bj-bary1lem1  37625  bj-bary1  37626  qdiff  37641  iblmulc2nc  38006  itgmulc2nc  38009  itgabsnc  38010  ftc1cnnclem  38012  ftc1anclem3  38016  dvasin  38025  areacirclem1  38029  areacirclem4  38032  areacirc  38034  cntotbnd  38117  3factsumint1  42460  3factsumint3  42462  3factsumint4  42463  lcmineqlem2  42469  lcmineqlem6  42473  lcmineqlem8  42475  lcmineqlem10  42477  lcmineqlem11  42478  lcmineqlem12  42479  lcmineqlem16  42483  lcmineqlem18  42485  lcmineqlem23  42490  3lexlogpow5ineq5  42499  aks4d1p1p1  42502  dvrelogpow2b  42507  aks4d1p1p6  42512  aks4d1p1p7  42513  aks4d1p1p5  42514  primrootscoprmpow  42538  posbezout  42539  primrootscoprbij  42541  primrootspoweq0  42545  2np3bcnp1  42583  2ap1caineq  42584  oddnumth  42743  nicomachus  42744  sumcubes  42745  ef11d  42771  cxp112d  42773  cxp111d  42774  readvrec2  42793  sn-addlid  42836  sn-it0e0  42848  sn-negex12  42849  sn-mul01  42858  sn-mullid  42868  sn-0tie0  42896  sn-mul02  42897  cnreeu  42935  fltnltalem  43095  fltnlta  43096  cu3addd  43113  3cubeslem2  43117  3cubeslem3l  43118  3cubeslem3r  43119  3cubeslem4  43121  pellexlem1  43257  pellexlem2  43258  pellexlem6  43262  pell1234qrne0  43281  pell1234qrreccl  43282  pell1234qrmulcl  43283  pell1234qrdich  43289  pell14qrdich  43297  pell1qrge1  43298  pell1qrgaplem  43301  rmspecsqrtnq  43334  qirropth  43336  rmxyneg  43348  rmxyadd  43349  rmxm1  43362  rmym1  43363  rmxluc  43364  rmyluc  43365  rmxdbl  43367  rmydbl  43368  jm2.18  43416  jm2.19lem1  43417  jm2.19lem2  43418  jm2.19lem4  43420  jm2.19  43421  jm2.22  43423  jm2.23  43424  jm2.25  43427  jm2.27c  43435  jm3.1lem2  43446  flcidc  43598  areaquad  43644  sqrtcval  44068  inductionexd  44582  imo72b2lem0  44592  int-leftdistd  44606  radcnvrat  44741  expgrowth  44762  binomcxplemwb  44775  binomcxplemnn0  44776  binomcxplemfrat  44778  binomcxplemdvbinom  44780  binomcxplemnotnn0  44783  sineq0ALT  45363  mul13d  45713  fperiodmullem  45736  fperiodmul  45737  divcan8d  45745  dmmcand  45746  ltdiv23neg  45823  mulc1cncfg  46019  mccllem  46027  clim1fr1  46031  mullimc  46046  mullimcf  46053  sumnnodd  46060  reclimc  46081  sinmulcos  46293  coskpi2  46294  cosknegpi  46297  dvsinexp  46339  dvasinbx  46348  dvdivf  46350  dvdivbd  46351  dvdivcncf  46355  dvbdfbdioolem2  46357  dvxpaek  46368  dvnxpaek  46370  dvnmul  46371  dvmptfprodlem  46372  dvnprodlem2  46375  itgsinexplem1  46382  itgsinexp  46383  itgcoscmulx  46397  itgsincmulx  46402  itgiccshift  46408  itgperiod  46409  stoweidlem1  46429  stoweidlem11  46439  stoweidlem13  46441  stoweidlem14  46442  stoweidlem17  46445  stoweidlem25  46453  stoweidlem26  46454  stoweidlem42  46470  wallispilem4  46496  wallispilem5  46497  wallispi  46498  wallispi2lem1  46499  wallispi2lem2  46500  wallispi2  46501  stirlinglem1  46502  stirlinglem3  46504  stirlinglem4  46505  stirlinglem5  46506  stirlinglem6  46507  stirlinglem7  46508  stirlinglem8  46509  stirlinglem10  46511  stirlinglem11  46512  stirlinglem12  46513  stirlinglem13  46514  stirlinglem14  46515  stirlinglem15  46516  dirker2re  46520  dirkerdenne0  46521  dirkerper  46524  dirkertrigeqlem1  46526  dirkertrigeqlem2  46527  dirkertrigeqlem3  46528  dirkertrigeq  46529  dirkeritg  46530  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem26  46561  fourierdlem30  46565  fourierdlem39  46574  fourierdlem42  46577  fourierdlem47  46581  fourierdlem48  46582  fourierdlem56  46590  fourierdlem57  46591  fourierdlem58  46592  fourierdlem62  46596  fourierdlem65  46599  fourierdlem66  46600  fourierdlem68  46602  fourierdlem72  46606  fourierdlem73  46607  fourierdlem76  46610  fourierdlem80  46614  fourierdlem83  46617  fourierdlem85  46619  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem95  46629  fourierdlem97  46631  fourierdlem101  46635  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  sqwvfoura  46656  sqwvfourb  46657  fourierswlem  46658  fouriersw  46659  elaa2lem  46661  etransclem8  46670  etransclem18  46680  etransclem20  46682  etransclem21  46683  etransclem23  46685  etransclem24  46686  etransclem31  46693  etransclem33  46695  etransclem35  46697  etransclem45  46707  etransclem46  46708  etransclem47  46709  etransclem48  46710  hoicvrrex  46984  hoidmvlelem2  47024  smfmullem1  47219  sigarim  47279  sigarac  47280  sigaraf  47281  sigarmf  47282  sigarls  47285  sigardiv  47289  sigarcol  47292  cevathlem1  47295  sin3t  47319  cos3t  47320  sin5tlem1  47321  sin5tlem2  47322  sin5tlem3  47323  sin5tlem4  47324  sin5tlem5  47325  sin5t  47326  cos5t  47327  fldivmod  47792  fmtnorec2lem  48005  fmtnorec3  48011  fmtnorec4  48012  fmtnoprmfac1  48028  fmtnoprmfac2  48030  fmtnofac2lem  48031  sfprmdvdsmersenne  48066  lighneallem3  48070  quad1  48096  requad01  48097  requad2  48099  opeoALTV  48160  perfectALTVlem2  48198  fppr2odd  48207  0nodd  48646  2nodd  48648  2zlidl  48716  2zrngnmlid  48731  altgsumbcALT  48829  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096  nn0sumshdiglem2  49098  nn0mullong  49101  itcovalt2lem2lem2  49150  ackval2  49158  submuladdmuld  49177  affinecomb2  49179  affineid  49180  1subrec1sub  49181  eenglngeehlnmlem1  49213  eenglngeehlnmlem2  49214  rrx2linest  49218  line2x  49230  line2y  49231  itschlc0yqe  49236  itsclc0yqsollem1  49238  itsclc0yqsol  49240  itscnhlc0xyqsol  49241  itschlc0xyqsol1  49242  itschlc0xyqsol  49243  itsclc0xyqsolr  49245  2itscplem1  49254  2itscplem2  49255  2itscplem3  49256  2itscp  49257  itscnhlinecirc02plem1  49258  itscnhlinecirc02plem2  49259  inlinecirc02plem  49262  inlinecirc02p  49263  i2linesd  50254  aacllem  50276  amgmwlem  50277  amgmlemALT  50278