Theorem mulcld 11132

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

Syntax hints:   → wi 4   ∈ wcel 2111  (class class class)co 7346  ℂcc 11004   · cmul 11011

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

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

This theorem is referenced by:  mul02lem1  11289  addrid  11293  cnegex  11294  kcnktkm1cn  11548  subaddmulsub  11580  mulsubaddmulsub  11581  receu  11762  divrec  11792  divcan3  11802  muldivdir  11814  subdivcomb1  11816  subdivcomb2  11817  divdivdiv  11822  divsubdiv  11837  lineq  11958  cru  12117  mul2lt0rlt0  12994  lincmb01cmp  13395  iccf1o  13396  flpmodeq  13778  moddiffl  13786  modvalp1  13794  modcyc  13810  modadd1  13812  modmuladdnn0  13822  modmul1  13831  modaddmulmod  13845  mulexpz  14009  expmulz  14015  binom3  14131  bernneq  14136  mulsubdivbinom2  14169  muldivbinom2  14170  remullem  15035  cjreim2  15068  absimle  15216  abstri  15238  sqreulem  15267  sqreu  15268  bhmafibid1cn  15373  bhmafibid2cn  15374  bhmafibid1  15375  bhmafibid2  15376  mulcn2  15503  reccn2  15504  o1rlimmul  15526  rlimmul  15552  isummulc2  15669  fsummulc2  15691  fsumparts  15713  binomlem  15736  binom1dif  15740  incexclem  15743  incexc  15744  incexc2  15745  pwdif  15775  geomulcvg  15783  mertenslem1  15791  mertens  15793  fprodmul  15867  fprodn0f  15898  iprodmul  15910  binomfallfaclem1  15946  binomfallfaclem2  15947  binomrisefac  15949  bpolycl  15959  bpolysum  15960  bpolydiflem  15961  bpoly4  15966  efaddlem  16000  sinadd  16073  cosadd  16074  tanaddlem  16075  tanadd  16076  addsin  16079  sincossq  16085  sin2t  16086  dvds2ln  16200  oddm1even  16254  pwp1fsum  16302  flodddiv4  16326  sadadd2lem2  16361  bezoutlem2  16451  bezoutlem3  16452  bezoutlem4  16453  lcmgcdlem  16517  phiprmpw  16687  pythagtriplem12  16738  pythagtriplem14  16740  pythagtriplem16  16742  pcpremul  16755  pcaddlem  16800  fldivp1  16809  mul4sqlem  16865  4sqlem14  16870  vdwapun  16886  vdwlem2  16894  vdwlem6  16898  ablsimpgfindlem1  20021  zringlpirlem3  21401  znunit  21500  blcvx  24713  icopnfcnv  24867  cphipipcj  25127  cphipval2  25168  4cphipval2  25169  cphipval  25170  mbfmulc2re  25576  mbfmulc2  25591  itg1addlem4  25627  itg1addlem5  25628  itg1mulc  25632  mbfmul  25654  itgcl  25712  itgcnlem  25718  iblmulc2  25759  itgmulc2  25762  itgabs  25763  itgsplit  25764  dvmulbr  25868  dvmulbrOLD  25869  dvcmul  25874  dvcmulf  25875  dvexp  25884  dvmptcmul  25895  dvmptdiv  25905  dvexp3  25909  dvsincos  25912  cmvth  25922  cmvthOLD  25923  dvlipcn  25926  dvfsumabs  25956  dvfsumlem1  25959  ftc1lem4  25973  itgparts  25981  itgpowd  25984  plyf  26130  ply1termlem  26135  plyeq0lem  26142  plypf1  26144  plyaddlem1  26145  plymullem1  26146  coeeulem  26156  coeidlem  26169  coeid3  26172  plyco  26173  coemullem  26182  coemulhi  26186  coemulc  26187  dgrcolem2  26207  plycjlem  26209  plyrecj  26214  dvply1  26218  vieta1lem2  26246  vieta1  26247  elqaalem3  26256  aareccl  26261  aalioulem1  26267  taylfvallem1  26291  tayl0  26296  dvtaylp  26305  taylthlem2  26309  taylthlem2OLD  26310  psergf  26348  radcnvlem1  26349  dvradcnv  26357  psercn2  26359  psercn2OLD  26360  pserdvlem2  26365  pserdv2  26367  abelthlem4  26371  abelthlem5  26372  abelthlem6  26373  abelthlem7  26375  abelthlem9  26377  tanregt0  26475  efgh  26477  efabl  26486  efsubm  26487  cosargd  26544  abslogle  26554  tanarg  26555  advlogexp  26591  logtayllem  26595  logtayl  26596  cxpadd  26615  mulcxp  26621  cxpmul  26624  cxpmul2  26625  cxpmul2z  26627  abscxp  26628  abscxp2  26629  dvcxp2  26677  abscxpbnd  26690  root1eq1  26692  cxpeq  26694  angcan  26739  pythag  26754  ssscongptld  26759  affineequiv  26760  affineequiv2  26761  affineequiv3  26762  affineequiv4  26763  chordthmlem2  26770  chordthmlem3  26771  chordthmlem4  26772  chordthmlem5  26773  heron  26775  quad2  26776  quad  26777  dcubic1lem  26780  dcubic2  26781  dcubic1  26782  dcubic  26783  mcubic  26784  cubic2  26785  cubic  26786  binom4  26787  dquartlem1  26788  dquartlem2  26789  dquart  26790  quart1cl  26791  quart1lem  26792  quart1  26793  quartlem1  26794  quartlem2  26795  atantayl3  26876  leibpi  26879  birthdaylem2  26889  divsqrtsumo1  26921  cvxcl  26922  jensenlem2  26925  lgamgulmlem2  26967  lgamgulmlem3  26968  lgamgulmlem4  26969  lgamgulmlem5  26970  lgamgulmlem6  26971  lgamgulm2  26973  lgamcvg2  26992  gamcvg  26993  gamcvg2lem  26996  wilthlem2  27006  ftalem1  27010  ftalem2  27011  ftalem4  27013  ftalem5  27014  basellem2  27019  basellem3  27020  basellem8  27025  muinv  27130  fsumdvdsmul  27132  fsumdvdsmulOLD  27134  logfacrlim  27162  logexprlim  27163  perfectlem2  27168  bposlem9  27230  gausslemma2dlem4  27307  lgsquad2lem1  27322  2lgslem3b  27335  2lgslem3c  27336  2lgslem3d  27337  2sqlem3  27358  2sqmod  27374  rplogsumlem1  27422  dchrisumlem2  27428  dchrisumlem3  27429  dchrmusum2  27432  dchrvmasumlem1  27433  dchrvmasum2lem  27434  dchrvmasum2if  27435  dchrvmasumlem3  27437  dchrvmasumiflem1  27439  dchrvmasumiflem2  27440  rpvmasum2  27450  dchrisum0lem1  27454  dchrisum0lem2a  27455  dchrisum0lem2  27456  dchrmusumlem  27460  dchrvmasumlem  27461  rplogsum  27465  mudivsum  27468  mulogsumlem  27469  mulogsum  27470  mulog2sumlem1  27472  mulog2sumlem2  27473  mulog2sumlem3  27474  vmalogdivsum  27477  logsqvma  27480  log2sumbnd  27482  selberglem1  27483  selberglem2  27484  selberglem3  27485  selberg  27486  selberg2lem  27488  selberg2  27489  selberg3lem1  27495  selberg3  27497  selberg4lem1  27498  selberg4  27499  pntrsumo1  27503  selbergr  27506  selberg3r  27507  selberg4r  27508  selberg34r  27509  pntsval2  27514  pntrlog2bndlem1  27515  pntrlog2bndlem2  27516  pntrlog2bndlem3  27517  pntrlog2bndlem4  27518  pntrlog2bndlem5  27519  pntrlog2bndlem6  27521  pntrlog2bnd  27522  pntlemb  27535  pntlemf  27543  pntlemo  27545  ostth2lem2  27572  ostth2lem3  27573  ttgcontlem1  28863  brbtwn2  28883  colinearalg  28888  ax5seglem2  28907  ax5seglem9  28915  axeuclidlem  28940  axcontlem2  28943  axcontlem4  28945  axcontlem7  28948  axcontlem8  28949  finsumvtxdg2ssteplem4  29527  ex-ind-dvds  30441  nrt2irr  30453  ipval2  30687  dipcl  30692  riesz3i  32042  re0cj  32727  pythagreim  32729  quad3d  32733  indsum  32842  indsumin  32843  dpfrac1  32872  wrdt2ind  32934  zringfrac  33519  ccfldsrarelvec  33684  ccfldextdgrr  33685  constrrtll  33744  constrrtlc1  33745  constrrtcclem  33747  constrrtcc  33748  constrconj  33758  constrfin  33759  constrelextdg2  33760  nn0constr  33774  constraddcl  33775  constrnegcl  33776  constrdircl  33778  iconstr  33779  constrremulcl  33780  constrrecl  33782  constrimcl  33783  constrmulcl  33784  constrreinvcl  33785  constrinvcl  33786  constrresqrtcl  33790  constrabscl  33791  constrsqrtcl  33792  cos9thpiminplylem1  33795  cos9thpiminplylem2  33796  cos9thpiminplylem3  33797  cos9thpiminply  33801  cos9thpinconstrlem1  33802  cos9thpinconstrlem2  33803  cos9thpinconstr  33804  cnre2csqima  33924  rmulccn  33941  dya2icoseg  34290  oddpwdc  34367  eulerpartlems  34373  eulerpartlemsv3  34374  eulerpartlemgs2  34393  signsplypnf  34563  itgexpif  34619  breprexplemc  34645  breprexp  34646  vtscl  34651  vtsprod  34652  circlemeth  34653  logdivsqrle  34663  hgt750lemf  34666  hgt750leme  34671  subfacval2  35231  subfaclim  35232  resconn  35290  iprodgam  35786  fwddifnp1  36209  knoppcnlem10  36546  knoppndvlem2  36557  knoppndvlem7  36562  knoppndvlem9  36564  knoppndvlem11  36566  knoppndvlem14  36569  knoppndvlem16  36571  knoppndvlem17  36572  bj-subcom  37352  bj-bary1lem  37354  bj-bary1lem1  37355  bj-bary1  37356  iblmulc2nc  37735  itgmulc2nc  37738  itgabsnc  37739  ftc1cnnclem  37741  ftc1anclem3  37745  dvasin  37754  areacirclem1  37758  areacirclem4  37761  areacirc  37763  cntotbnd  37846  3factsumint1  42124  3factsumint3  42126  3factsumint4  42127  lcmineqlem2  42133  lcmineqlem6  42137  lcmineqlem8  42139  lcmineqlem10  42141  lcmineqlem11  42142  lcmineqlem12  42143  lcmineqlem16  42147  lcmineqlem18  42149  lcmineqlem23  42154  3lexlogpow5ineq5  42163  aks4d1p1p1  42166  dvrelogpow2b  42171  aks4d1p1p6  42176  aks4d1p1p7  42177  aks4d1p1p5  42178  primrootscoprmpow  42202  posbezout  42203  primrootscoprbij  42205  primrootspoweq0  42209  2np3bcnp1  42247  2ap1caineq  42248  oddnumth  42414  nicomachus  42415  sumcubes  42416  ef11d  42442  cxp112d  42444  cxp111d  42445  readvrec2  42464  sn-addlid  42507  sn-it0e0  42519  sn-negex12  42520  sn-mul01  42529  sn-mullid  42539  sn-0tie0  42554  sn-mul02  42555  cnreeu  42593  fltnltalem  42765  fltnlta  42766  cu3addd  42784  3cubeslem2  42788  3cubeslem3l  42789  3cubeslem3r  42790  3cubeslem4  42792  pellexlem1  42932  pellexlem2  42933  pellexlem6  42937  pell1234qrne0  42956  pell1234qrreccl  42957  pell1234qrmulcl  42958  pell1234qrdich  42964  pell14qrdich  42972  pell1qrge1  42973  pell1qrgaplem  42976  rmspecsqrtnq  43009  qirropth  43011  rmxyneg  43023  rmxyadd  43024  rmxm1  43037  rmym1  43038  rmxluc  43039  rmyluc  43040  rmxdbl  43042  rmydbl  43043  jm2.18  43091  jm2.19lem1  43092  jm2.19lem2  43093  jm2.19lem4  43095  jm2.19  43096  jm2.22  43098  jm2.23  43099  jm2.25  43102  jm2.27c  43110  jm3.1lem2  43121  flcidc  43273  areaquad  43319  sqrtcval  43744  inductionexd  44258  imo72b2lem0  44268  int-leftdistd  44282  radcnvrat  44417  expgrowth  44438  binomcxplemwb  44451  binomcxplemnn0  44452  binomcxplemfrat  44454  binomcxplemdvbinom  44456  binomcxplemnotnn0  44459  sineq0ALT  45039  mul13d  45391  fperiodmullem  45414  fperiodmul  45415  divcan8d  45423  dmmcand  45424  ltdiv23neg  45502  mulc1cncfg  45699  mccllem  45707  clim1fr1  45711  mullimc  45726  mullimcf  45733  sumnnodd  45740  reclimc  45761  sinmulcos  45973  coskpi2  45974  cosknegpi  45977  dvsinexp  46019  dvasinbx  46028  dvdivf  46030  dvdivbd  46031  dvdivcncf  46035  dvbdfbdioolem2  46037  dvxpaek  46048  dvnxpaek  46050  dvnmul  46051  dvmptfprodlem  46052  dvnprodlem2  46055  itgsinexplem1  46062  itgsinexp  46063  itgcoscmulx  46077  itgsincmulx  46082  itgiccshift  46088  itgperiod  46089  stoweidlem1  46109  stoweidlem11  46119  stoweidlem13  46121  stoweidlem14  46122  stoweidlem17  46125  stoweidlem25  46133  stoweidlem26  46134  stoweidlem42  46150  wallispilem4  46176  wallispilem5  46177  wallispi  46178  wallispi2lem1  46179  wallispi2lem2  46180  wallispi2  46181  stirlinglem1  46182  stirlinglem3  46184  stirlinglem4  46185  stirlinglem5  46186  stirlinglem6  46187  stirlinglem7  46188  stirlinglem8  46189  stirlinglem10  46191  stirlinglem11  46192  stirlinglem12  46193  stirlinglem13  46194  stirlinglem14  46195  stirlinglem15  46196  dirker2re  46200  dirkerdenne0  46201  dirkerper  46204  dirkertrigeqlem1  46206  dirkertrigeqlem2  46207  dirkertrigeqlem3  46208  dirkertrigeq  46209  dirkeritg  46210  dirkercncflem2  46212  dirkercncflem4  46214  fourierdlem26  46241  fourierdlem30  46245  fourierdlem39  46254  fourierdlem42  46257  fourierdlem47  46261  fourierdlem48  46262  fourierdlem56  46270  fourierdlem57  46271  fourierdlem58  46272  fourierdlem62  46276  fourierdlem65  46279  fourierdlem66  46280  fourierdlem68  46282  fourierdlem72  46286  fourierdlem73  46287  fourierdlem76  46290  fourierdlem80  46294  fourierdlem83  46297  fourierdlem85  46299  fourierdlem89  46303  fourierdlem90  46304  fourierdlem91  46305  fourierdlem95  46309  fourierdlem97  46311  fourierdlem101  46315  fourierdlem103  46317  fourierdlem104  46318  fourierdlem111  46325  sqwvfoura  46336  sqwvfourb  46337  fourierswlem  46338  fouriersw  46339  elaa2lem  46341  etransclem8  46350  etransclem18  46360  etransclem20  46362  etransclem21  46363  etransclem23  46365  etransclem24  46366  etransclem31  46373  etransclem33  46375  etransclem35  46377  etransclem45  46387  etransclem46  46388  etransclem47  46389  etransclem48  46390  hoicvrrex  46664  hoidmvlelem2  46704  smfmullem1  46899  sigarim  46959  sigarac  46960  sigaraf  46961  sigarmf  46962  sigarls  46965  sigardiv  46969  sigarcol  46972  cevathlem1  46975  fldivmod  47448  fmtnorec2lem  47652  fmtnorec3  47658  fmtnorec4  47659  fmtnoprmfac1  47675  fmtnoprmfac2  47677  fmtnofac2lem  47678  sfprmdvdsmersenne  47713  lighneallem3  47717  quad1  47730  requad01  47731  requad2  47733  opeoALTV  47794  perfectALTVlem2  47832  fppr2odd  47841  0nodd  48280  2nodd  48282  2zlidl  48350  2zrngnmlid  48365  altgsumbcALT  48463  nn0sumshdiglemA  48730  nn0sumshdiglemB  48731  nn0sumshdiglem2  48733  nn0mullong  48736  itcovalt2lem2lem2  48785  ackval2  48793  submuladdmuld  48812  affinecomb2  48814  affineid  48815  1subrec1sub  48816  eenglngeehlnmlem1  48848  eenglngeehlnmlem2  48849  rrx2linest  48853  line2x  48865  line2y  48866  itschlc0yqe  48871  itsclc0yqsollem1  48873  itsclc0yqsol  48875  itscnhlc0xyqsol  48876  itschlc0xyqsol1  48877  itschlc0xyqsol  48878  itsclc0xyqsolr  48880  2itscplem1  48889  2itscplem2  48890  2itscplem3  48891  2itscp  48892  itscnhlinecirc02plem1  48893  itscnhlinecirc02plem2  48894  inlinecirc02plem  48897  inlinecirc02p  48898  i2linesd  49890  aacllem  49912  amgmwlem  49913  amgmlemALT  49914