Theorem mulcld 11170

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7369  ℂcc 11042   · cmul 11049

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

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

This theorem is referenced by:  mul02lem1  11326  addrid  11330  cnegex  11331  kcnktkm1cn  11585  subaddmulsub  11617  mulsubaddmulsub  11618  receu  11799  divrec  11829  divcan3  11839  muldivdir  11851  subdivcomb1  11853  subdivcomb2  11854  divdivdiv  11859  divsubdiv  11874  lineq  11995  cru  12154  mul2lt0rlt0  13031  lincmb01cmp  13432  iccf1o  13433  flpmodeq  13812  moddiffl  13820  modvalp1  13828  modcyc  13844  modadd1  13846  modmuladdnn0  13856  modmul1  13865  modaddmulmod  13879  mulexpz  14043  expmulz  14049  binom3  14165  bernneq  14170  mulsubdivbinom2  14203  muldivbinom2  14204  remullem  15070  cjreim2  15103  absimle  15251  abstri  15273  sqreulem  15302  sqreu  15303  bhmafibid1cn  15408  bhmafibid2cn  15409  bhmafibid1  15410  bhmafibid2  15411  mulcn2  15538  reccn2  15539  o1rlimmul  15561  rlimmul  15587  isummulc2  15704  fsummulc2  15726  fsumparts  15748  binomlem  15771  binom1dif  15775  incexclem  15778  incexc  15779  incexc2  15780  pwdif  15810  geomulcvg  15818  mertenslem1  15826  mertens  15828  fprodmul  15902  fprodn0f  15933  iprodmul  15945  binomfallfaclem1  15981  binomfallfaclem2  15982  binomrisefac  15984  bpolycl  15994  bpolysum  15995  bpolydiflem  15996  bpoly4  16001  efaddlem  16035  sinadd  16108  cosadd  16109  tanaddlem  16110  tanadd  16111  addsin  16114  sincossq  16120  sin2t  16121  dvds2ln  16235  oddm1even  16289  pwp1fsum  16337  flodddiv4  16361  sadadd2lem2  16396  bezoutlem2  16486  bezoutlem3  16487  bezoutlem4  16488  lcmgcdlem  16552  phiprmpw  16722  pythagtriplem12  16773  pythagtriplem14  16775  pythagtriplem16  16777  pcpremul  16790  pcaddlem  16835  fldivp1  16844  mul4sqlem  16900  4sqlem14  16905  vdwapun  16921  vdwlem2  16929  vdwlem6  16933  ablsimpgfindlem1  20015  zringlpirlem3  21350  znunit  21449  blcvx  24662  icopnfcnv  24816  cphipipcj  25076  cphipval2  25117  4cphipval2  25118  cphipval  25119  mbfmulc2re  25525  mbfmulc2  25540  itg1addlem4  25576  itg1addlem5  25577  itg1mulc  25581  mbfmul  25603  itgcl  25661  itgcnlem  25667  iblmulc2  25708  itgmulc2  25711  itgabs  25712  itgsplit  25713  dvmulbr  25817  dvmulbrOLD  25818  dvcmul  25823  dvcmulf  25824  dvexp  25833  dvmptcmul  25844  dvmptdiv  25854  dvexp3  25858  dvsincos  25861  cmvth  25871  cmvthOLD  25872  dvlipcn  25875  dvfsumabs  25905  dvfsumlem1  25908  ftc1lem4  25922  itgparts  25930  itgpowd  25933  plyf  26079  ply1termlem  26084  plyeq0lem  26091  plypf1  26093  plyaddlem1  26094  plymullem1  26095  coeeulem  26105  coeidlem  26118  coeid3  26121  plyco  26122  coemullem  26131  coemulhi  26135  coemulc  26136  dgrcolem2  26156  plycjlem  26158  plyrecj  26163  dvply1  26167  vieta1lem2  26195  vieta1  26196  elqaalem3  26205  aareccl  26210  aalioulem1  26216  taylfvallem1  26240  tayl0  26245  dvtaylp  26254  taylthlem2  26258  taylthlem2OLD  26259  psergf  26297  radcnvlem1  26298  dvradcnv  26306  psercn2  26308  psercn2OLD  26309  pserdvlem2  26314  pserdv2  26316  abelthlem4  26320  abelthlem5  26321  abelthlem6  26322  abelthlem7  26324  abelthlem9  26326  tanregt0  26424  efgh  26426  efabl  26435  efsubm  26436  cosargd  26493  abslogle  26503  tanarg  26504  advlogexp  26540  logtayllem  26544  logtayl  26545  cxpadd  26564  mulcxp  26570  cxpmul  26573  cxpmul2  26574  cxpmul2z  26576  abscxp  26577  abscxp2  26578  dvcxp2  26626  abscxpbnd  26639  root1eq1  26641  cxpeq  26643  angcan  26688  pythag  26703  ssscongptld  26708  affineequiv  26709  affineequiv2  26710  affineequiv3  26711  affineequiv4  26712  chordthmlem2  26719  chordthmlem3  26720  chordthmlem4  26721  chordthmlem5  26722  heron  26724  quad2  26725  quad  26726  dcubic1lem  26729  dcubic2  26730  dcubic1  26731  dcubic  26732  mcubic  26733  cubic2  26734  cubic  26735  binom4  26736  dquartlem1  26737  dquartlem2  26738  dquart  26739  quart1cl  26740  quart1lem  26741  quart1  26742  quartlem1  26743  quartlem2  26744  atantayl3  26825  leibpi  26828  birthdaylem2  26838  divsqrtsumo1  26870  cvxcl  26871  jensenlem2  26874  lgamgulmlem2  26916  lgamgulmlem3  26917  lgamgulmlem4  26918  lgamgulmlem5  26919  lgamgulmlem6  26920  lgamgulm2  26922  lgamcvg2  26941  gamcvg  26942  gamcvg2lem  26945  wilthlem2  26955  ftalem1  26959  ftalem2  26960  ftalem4  26962  ftalem5  26963  basellem2  26968  basellem3  26969  basellem8  26974  muinv  27079  fsumdvdsmul  27081  fsumdvdsmulOLD  27083  logfacrlim  27111  logexprlim  27112  perfectlem2  27117  bposlem9  27179  gausslemma2dlem4  27256  lgsquad2lem1  27271  2lgslem3b  27284  2lgslem3c  27285  2lgslem3d  27286  2sqlem3  27307  2sqmod  27323  rplogsumlem1  27371  dchrisumlem2  27377  dchrisumlem3  27378  dchrmusum2  27381  dchrvmasumlem1  27382  dchrvmasum2lem  27383  dchrvmasum2if  27384  dchrvmasumlem3  27386  dchrvmasumiflem1  27388  dchrvmasumiflem2  27389  rpvmasum2  27399  dchrisum0lem1  27403  dchrisum0lem2a  27404  dchrisum0lem2  27405  dchrmusumlem  27409  dchrvmasumlem  27410  rplogsum  27414  mudivsum  27417  mulogsumlem  27418  mulogsum  27419  mulog2sumlem1  27421  mulog2sumlem2  27422  mulog2sumlem3  27423  vmalogdivsum  27426  logsqvma  27429  log2sumbnd  27431  selberglem1  27432  selberglem2  27433  selberglem3  27434  selberg  27435  selberg2lem  27437  selberg2  27438  selberg3lem1  27444  selberg3  27446  selberg4lem1  27447  selberg4  27448  pntrsumo1  27452  selbergr  27455  selberg3r  27456  selberg4r  27457  selberg34r  27458  pntsval2  27463  pntrlog2bndlem1  27464  pntrlog2bndlem2  27465  pntrlog2bndlem3  27466  pntrlog2bndlem4  27467  pntrlog2bndlem5  27468  pntrlog2bndlem6  27470  pntrlog2bnd  27471  pntlemb  27484  pntlemf  27492  pntlemo  27494  ostth2lem2  27521  ostth2lem3  27522  ttgcontlem1  28788  brbtwn2  28808  colinearalg  28813  ax5seglem2  28832  ax5seglem9  28840  axeuclidlem  28865  axcontlem2  28868  axcontlem4  28870  axcontlem7  28873  axcontlem8  28874  finsumvtxdg2ssteplem4  29452  ex-ind-dvds  30363  nrt2irr  30375  ipval2  30609  dipcl  30614  riesz3i  31964  re0cj  32640  pythagreim  32642  quad3d  32646  indsum  32757  indsumin  32758  dpfrac1  32785  wrdt2ind  32848  zringfrac  33498  ccfldsrarelvec  33639  ccfldextdgrr  33640  constrrtll  33694  constrrtlc1  33695  constrrtcclem  33697  constrrtcc  33698  constrconj  33708  constrfin  33709  constrelextdg2  33710  nn0constr  33724  constraddcl  33725  constrnegcl  33726  constrdircl  33728  iconstr  33729  constrremulcl  33730  constrrecl  33732  constrimcl  33733  constrmulcl  33734  constrreinvcl  33735  constrinvcl  33736  constrresqrtcl  33740  constrabscl  33741  constrsqrtcl  33742  cos9thpiminplylem1  33745  cos9thpiminplylem2  33746  cos9thpiminplylem3  33747  cos9thpiminply  33751  cos9thpinconstrlem1  33752  cos9thpinconstrlem2  33753  cos9thpinconstr  33754  cnre2csqima  33874  rmulccn  33891  dya2icoseg  34241  oddpwdc  34318  eulerpartlems  34324  eulerpartlemsv3  34325  eulerpartlemgs2  34344  signsplypnf  34514  itgexpif  34570  breprexplemc  34596  breprexp  34597  vtscl  34602  vtsprod  34603  circlemeth  34604  logdivsqrle  34614  hgt750lemf  34617  hgt750leme  34622  subfacval2  35147  subfaclim  35148  resconn  35206  iprodgam  35702  fwddifnp1  36126  knoppcnlem10  36463  knoppndvlem2  36474  knoppndvlem7  36479  knoppndvlem9  36481  knoppndvlem11  36483  knoppndvlem14  36486  knoppndvlem16  36488  knoppndvlem17  36489  bj-subcom  37269  bj-bary1lem  37271  bj-bary1lem1  37272  bj-bary1  37273  iblmulc2nc  37652  itgmulc2nc  37655  itgabsnc  37656  ftc1cnnclem  37658  ftc1anclem3  37662  dvasin  37671  areacirclem1  37675  areacirclem4  37678  areacirc  37680  cntotbnd  37763  3factsumint1  41982  3factsumint3  41984  3factsumint4  41985  lcmineqlem2  41991  lcmineqlem6  41995  lcmineqlem8  41997  lcmineqlem10  41999  lcmineqlem11  42000  lcmineqlem12  42001  lcmineqlem16  42005  lcmineqlem18  42007  lcmineqlem23  42012  3lexlogpow5ineq5  42021  aks4d1p1p1  42024  dvrelogpow2b  42029  aks4d1p1p6  42034  aks4d1p1p7  42035  aks4d1p1p5  42036  primrootscoprmpow  42060  posbezout  42061  primrootscoprbij  42063  primrootspoweq0  42067  2np3bcnp1  42105  2ap1caineq  42106  oddnumth  42272  nicomachus  42273  sumcubes  42274  ef11d  42300  cxp112d  42302  cxp111d  42303  readvrec2  42322  sn-addlid  42365  sn-it0e0  42377  sn-negex12  42378  sn-mul01  42387  sn-mullid  42397  sn-0tie0  42412  sn-mul02  42413  cnreeu  42451  fltnltalem  42623  fltnlta  42624  cu3addd  42642  3cubeslem2  42646  3cubeslem3l  42647  3cubeslem3r  42648  3cubeslem4  42650  pellexlem1  42790  pellexlem2  42791  pellexlem6  42795  pell1234qrne0  42814  pell1234qrreccl  42815  pell1234qrmulcl  42816  pell1234qrdich  42822  pell14qrdich  42830  pell1qrge1  42831  pell1qrgaplem  42834  rmspecsqrtnq  42867  qirropth  42869  rmxyneg  42882  rmxyadd  42883  rmxm1  42896  rmym1  42897  rmxluc  42898  rmyluc  42899  rmxdbl  42901  rmydbl  42902  jm2.18  42950  jm2.19lem1  42951  jm2.19lem2  42952  jm2.19lem4  42954  jm2.19  42955  jm2.22  42957  jm2.23  42958  jm2.25  42961  jm2.27c  42969  jm3.1lem2  42980  flcidc  43132  areaquad  43178  sqrtcval  43603  inductionexd  44117  imo72b2lem0  44127  int-leftdistd  44141  radcnvrat  44276  expgrowth  44297  binomcxplemwb  44310  binomcxplemnn0  44311  binomcxplemfrat  44313  binomcxplemdvbinom  44315  binomcxplemnotnn0  44318  sineq0ALT  44899  mul13d  45251  fperiodmullem  45274  fperiodmul  45275  divcan8d  45283  dmmcand  45284  ltdiv23neg  45363  mulc1cncfg  45560  mccllem  45568  clim1fr1  45572  mullimc  45587  mullimcf  45594  sumnnodd  45601  reclimc  45624  sinmulcos  45836  coskpi2  45837  cosknegpi  45840  dvsinexp  45882  dvasinbx  45891  dvdivf  45893  dvdivbd  45894  dvdivcncf  45898  dvbdfbdioolem2  45900  dvxpaek  45911  dvnxpaek  45913  dvnmul  45914  dvmptfprodlem  45915  dvnprodlem2  45918  itgsinexplem1  45925  itgsinexp  45926  itgcoscmulx  45940  itgsincmulx  45945  itgiccshift  45951  itgperiod  45952  stoweidlem1  45972  stoweidlem11  45982  stoweidlem13  45984  stoweidlem14  45985  stoweidlem17  45988  stoweidlem25  45996  stoweidlem26  45997  stoweidlem42  46013  wallispilem4  46039  wallispilem5  46040  wallispi  46041  wallispi2lem1  46042  wallispi2lem2  46043  wallispi2  46044  stirlinglem1  46045  stirlinglem3  46047  stirlinglem4  46048  stirlinglem5  46049  stirlinglem6  46050  stirlinglem7  46051  stirlinglem8  46052  stirlinglem10  46054  stirlinglem11  46055  stirlinglem12  46056  stirlinglem13  46057  stirlinglem14  46058  stirlinglem15  46059  dirker2re  46063  dirkerdenne0  46064  dirkerper  46067  dirkertrigeqlem1  46069  dirkertrigeqlem2  46070  dirkertrigeqlem3  46071  dirkertrigeq  46072  dirkeritg  46073  dirkercncflem2  46075  dirkercncflem4  46077  fourierdlem26  46104  fourierdlem30  46108  fourierdlem39  46117  fourierdlem42  46120  fourierdlem47  46124  fourierdlem48  46125  fourierdlem56  46133  fourierdlem57  46134  fourierdlem58  46135  fourierdlem62  46139  fourierdlem65  46142  fourierdlem66  46143  fourierdlem68  46145  fourierdlem72  46149  fourierdlem73  46150  fourierdlem76  46153  fourierdlem80  46157  fourierdlem83  46160  fourierdlem85  46162  fourierdlem89  46166  fourierdlem90  46167  fourierdlem91  46168  fourierdlem95  46172  fourierdlem97  46174  fourierdlem101  46178  fourierdlem103  46180  fourierdlem104  46181  fourierdlem111  46188  sqwvfoura  46199  sqwvfourb  46200  fourierswlem  46201  fouriersw  46202  elaa2lem  46204  etransclem8  46213  etransclem18  46223  etransclem20  46225  etransclem21  46226  etransclem23  46228  etransclem24  46229  etransclem31  46236  etransclem33  46238  etransclem35  46240  etransclem45  46250  etransclem46  46251  etransclem47  46252  etransclem48  46253  hoicvrrex  46527  hoidmvlelem2  46567  smfmullem1  46762  sigarim  46822  sigarac  46823  sigaraf  46824  sigarmf  46825  sigarls  46828  sigardiv  46832  sigarcol  46835  cevathlem1  46838  fldivmod  47312  fmtnorec2lem  47516  fmtnorec3  47522  fmtnorec4  47523  fmtnoprmfac1  47539  fmtnoprmfac2  47541  fmtnofac2lem  47542  sfprmdvdsmersenne  47577  lighneallem3  47581  quad1  47594  requad01  47595  requad2  47597  opeoALTV  47658  perfectALTVlem2  47696  fppr2odd  47705  0nodd  48131  2nodd  48133  2zlidl  48201  2zrngnmlid  48216  altgsumbcALT  48314  nn0sumshdiglemA  48581  nn0sumshdiglemB  48582  nn0sumshdiglem2  48584  nn0mullong  48587  itcovalt2lem2lem2  48636  ackval2  48644  submuladdmuld  48663  affinecomb2  48665  affineid  48666  1subrec1sub  48667  eenglngeehlnmlem1  48699  eenglngeehlnmlem2  48700  rrx2linest  48704  line2x  48716  line2y  48717  itschlc0yqe  48722  itsclc0yqsollem1  48724  itsclc0yqsol  48726  itscnhlc0xyqsol  48727  itschlc0xyqsol1  48728  itschlc0xyqsol  48729  itsclc0xyqsolr  48731  2itscplem1  48740  2itscplem2  48741  2itscplem3  48742  2itscp  48743  itscnhlinecirc02plem1  48744  itscnhlinecirc02plem2  48745  inlinecirc02plem  48748  inlinecirc02p  48749  i2linesd  49741  aacllem  49763  amgmwlem  49764  amgmlemALT  49765