MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulcld Structured version   Visualization version   GIF version

Theorem mulcld 10057
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
StepHypRef Expression
1 addcld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addcld.2 . 2 (𝜑𝐵 ∈ ℂ)
3 mulcl 10017 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
41, 2, 3syl2anc 693 1 (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1989  (class class class)co 6647  cc 9931   · cmul 9938
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 9995
This theorem depends on definitions:  df-bi 197  df-an 386
This theorem is referenced by:  mul02lem1  10209  addid1  10213  cnegex  10214  kcnktkm1cn  10458  receu  10669  divrec  10698  divcan3  10708  muldivdir  10717  divdivdiv  10723  divsubdiv  10738  cru  11009  mul2lt0rlt0  11929  lincmb01cmp  12312  iccf1o  12313  flpmodeq  12668  moddiffl  12676  modvalp1  12684  modcyc  12700  modadd1  12702  modmuladdnn0  12709  modmul1  12718  modaddmulmod  12732  mulexpz  12895  expmulz  12901  binom3  12980  bernneq  12985  mulsubdivbinom2  13041  muldivbinom2  13042  remullem  13862  cjreim2  13895  absimle  14043  abstri  14064  sqreulem  14093  sqreu  14094  mulcn2  14320  reccn2  14321  o1rlimmul  14343  isummulc2  14487  fsummulc2  14510  fsumparts  14532  binomlem  14555  binom1dif  14559  incexclem  14562  incexc  14563  incexc2  14564  geomulcvg  14601  mertenslem1  14610  mertens  14612  fprodmul  14684  fprodn0f  14716  iprodmul  14728  binomfallfaclem1  14764  binomfallfaclem2  14765  binomrisefac  14767  bpolycl  14777  bpolysum  14778  bpolydiflem  14779  bpoly4  14784  efaddlem  14817  sinadd  14888  cosadd  14889  tanaddlem  14890  tanadd  14891  addsin  14894  sincossq  14900  sin2t  14901  dvds2ln  15008  oddm1even  15061  pwp1fsum  15108  flodddiv4  15131  sadadd2lem2  15166  bezoutlem2  15251  bezoutlem3  15252  bezoutlem4  15253  lcmgcdlem  15313  phiprmpw  15475  pythagtriplem12  15525  pythagtriplem14  15527  pythagtriplem16  15529  pcpremul  15542  pcaddlem  15586  fldivp1  15595  mul4sqlem  15651  4sqlem14  15656  vdwapun  15672  vdwlem2  15680  vdwlem6  15684  zringlpirlem3  19828  znunit  19906  blcvx  22595  icopnfcnv  22735  cphipipcj  22994  cphipval2  23034  4cphipval2  23035  cphipval  23036  mbfmulc2re  23409  mbfmulc2  23424  itg1addlem4  23460  itg1addlem5  23461  itg1mulc  23465  mbfmul  23487  itgcl  23544  itgcnlem  23550  iblmulc2  23591  itgmulc2  23594  itgabs  23595  itgsplit  23596  dvmulbr  23696  dvcmul  23701  dvcmulf  23702  dvexp  23710  dvmptcmul  23721  dvmptdiv  23731  dvexp3  23735  dvsincos  23738  cmvth  23748  dvlipcn  23751  dvfsumabs  23780  dvfsumlem1  23783  ftc1lem4  23796  itgparts  23804  plyf  23948  ply1termlem  23953  plyeq0lem  23960  plypf1  23962  plyaddlem1  23963  plymullem1  23964  coeeulem  23974  coeidlem  23987  coeid3  23990  plyco  23991  coemullem  24000  coemulhi  24004  coemulc  24005  dgrcolem2  24024  plycjlem  24026  plyrecj  24029  dvply1  24033  vieta1lem2  24060  vieta1  24061  elqaalem3  24070  aareccl  24075  aalioulem1  24081  taylfvallem1  24105  tayl0  24110  dvtaylp  24118  taylthlem2  24122  psergf  24160  radcnvlem1  24161  dvradcnv  24169  psercn2  24171  pserdvlem2  24176  pserdv2  24178  abelthlem4  24182  abelthlem5  24183  abelthlem6  24184  abelthlem7  24186  abelthlem9  24188  tanregt0  24279  efgh  24281  efabl  24290  efsubm  24291  cosargd  24348  abslogle  24358  tanarg  24359  advlogexp  24395  logtayllem  24399  logtayl  24400  cxpadd  24419  mulcxp  24425  cxpmul  24428  cxpmul2  24429  cxpmul2z  24431  abscxp  24432  abscxp2  24433  dvcxp2  24476  abscxpbnd  24488  root1eq1  24490  cxpeq  24492  angcan  24526  pythag  24541  ssscongptld  24546  affineequiv  24547  affineequiv2  24548  chordthmlem2  24554  chordthmlem3  24555  chordthmlem4  24556  chordthmlem5  24557  heron  24559  quad2  24560  quad  24561  dcubic1lem  24564  dcubic2  24565  dcubic1  24566  dcubic  24567  mcubic  24568  cubic2  24569  cubic  24570  binom4  24571  dquartlem1  24572  dquartlem2  24573  dquart  24574  quart1cl  24575  quart1lem  24576  quart1  24577  quartlem1  24578  quartlem2  24579  atantayl3  24660  leibpi  24663  birthdaylem2  24673  divsqrtsumo1  24704  cvxcl  24705  jensenlem2  24708  lgamgulmlem2  24750  lgamgulmlem3  24751  lgamgulmlem4  24752  lgamgulmlem5  24753  lgamgulmlem6  24754  lgamgulm2  24756  lgamcvg2  24775  gamcvg  24776  gamcvg2lem  24779  wilthlem2  24789  ftalem1  24793  ftalem2  24794  ftalem4  24796  ftalem5  24797  basellem2  24802  basellem3  24803  basellem8  24808  muinv  24913  fsumdvdsmul  24915  logfacrlim  24943  logexprlim  24944  perfectlem2  24949  bposlem9  25011  gausslemma2dlem4  25088  lgsquad2lem1  25103  2lgslem3b  25116  2lgslem3c  25117  2lgslem3d  25118  2sqlem3  25139  rplogsumlem1  25167  dchrisumlem2  25173  dchrisumlem3  25174  dchrmusum2  25177  dchrvmasumlem1  25178  dchrvmasum2lem  25179  dchrvmasum2if  25180  dchrvmasumlem3  25182  dchrvmasumiflem1  25184  dchrvmasumiflem2  25185  rpvmasum2  25195  dchrisum0lem1  25199  dchrisum0lem2a  25200  dchrisum0lem2  25201  dchrmusumlem  25205  dchrvmasumlem  25206  rplogsum  25210  mudivsum  25213  mulogsumlem  25214  mulogsum  25215  mulog2sumlem1  25217  mulog2sumlem2  25218  mulog2sumlem3  25219  vmalogdivsum  25222  logsqvma  25225  log2sumbnd  25227  selberglem1  25228  selberglem2  25229  selberglem3  25230  selberg  25231  selberg2lem  25233  selberg2  25234  selberg3lem1  25240  selberg3  25242  selberg4lem1  25243  selberg4  25244  pntrsumo1  25248  selbergr  25251  selberg3r  25252  selberg4r  25253  selberg34r  25254  pntsval2  25259  pntrlog2bndlem1  25260  pntrlog2bndlem2  25261  pntrlog2bndlem3  25262  pntrlog2bndlem4  25263  pntrlog2bndlem5  25264  pntrlog2bndlem6  25266  pntrlog2bnd  25267  pntlemb  25280  pntlemf  25288  pntlemo  25290  ostth2lem2  25317  ostth2lem3  25318  ttgcontlem1  25759  brbtwn2  25779  colinearalg  25784  ax5seglem2  25803  ax5seglem9  25811  axeuclidlem  25836  axcontlem2  25839  axcontlem4  25841  axcontlem7  25844  axcontlem8  25845  finsumvtxdg2ssteplem4  26438  ex-ind-dvds  27302  ipval2  27546  dipcl  27551  riesz3i  28905  dpfrac1  29584  bhmafibid1  29629  bhmafibid2  29630  2sqmod  29633  cnre2csqima  29942  rmulccn  29959  indsum  30068  indsumin  30069  dya2icoseg  30324  oddpwdc  30401  eulerpartlems  30407  eulerpartlemsv3  30408  eulerpartlemgs2  30427  signsplypnf  30612  itgexpif  30669  breprexplemc  30695  breprexp  30696  vtscl  30701  vtsprod  30702  circlemeth  30703  logdivsqrle  30713  hgt750lemf  30716  hgt750leme  30721  subfacval2  31154  subfaclim  31155  resconn  31213  subdivcomb1  31597  subdivcomb2  31598  iprodgam  31614  fwddifnp1  32256  knoppndvlem2  32488  knoppndvlem7  32493  knoppndvlem9  32495  knoppndvlem11  32497  knoppndvlem14  32500  knoppndvlem16  32502  knoppndvlem17  32503  bj-subcom  33134  bj-lineq  33138  bj-bary1lem  33140  bj-bary1lem1  33141  bj-bary1  33142  iblmulc2nc  33455  itgmulc2nc  33458  itgabsnc  33459  ftc1cnnclem  33463  ftc1anclem3  33467  dvasin  33476  areacirclem1  33480  areacirclem4  33483  areacirc  33485  cntotbnd  33575  pellexlem1  37219  pellexlem2  37220  pellexlem6  37224  pell1234qrne0  37243  pell1234qrreccl  37244  pell1234qrmulcl  37245  pell1234qrdich  37251  pell14qrdich  37259  pell1qrge1  37260  pell1qrgaplem  37263  rmspecsqrtnq  37296  qirropth  37299  rmxyneg  37311  rmxyadd  37312  rmxm1  37325  rmym1  37326  rmxluc  37327  rmyluc  37328  rmxdbl  37330  rmydbl  37331  jm2.18  37381  jm2.19lem1  37382  jm2.19lem2  37383  jm2.19lem4  37385  jm2.19  37386  jm2.22  37388  jm2.23  37389  jm2.25  37392  jm2.27c  37400  jm3.1lem2  37411  flcidc  37570  itgpowd  37626  areaquad  37628  inductionexd  38279  imo72b2lem0  38291  int-leftdistd  38308  radcnvrat  38339  expgrowth  38360  binomcxplemwb  38373  binomcxplemnn0  38374  binomcxplemfrat  38376  binomcxplemdvbinom  38378  binomcxplemnotnn0  38381  sineq0ALT  38999  mul13d  39310  fperiodmullem  39336  fperiodmul  39337  divcan8d  39346  dmmcand  39347  ltdiv23neg  39436  mulc1cncfg  39627  mccllem  39635  clim1fr1  39639  mullimc  39654  mullimcf  39661  sumnnodd  39668  reclimc  39691  sinmulcos  39845  coskpi2  39846  cosknegpi  39849  dvsinexp  39894  dvasinbx  39904  dvdivf  39906  dvdivbd  39907  dvdivcncf  39911  dvbdfbdioolem2  39913  dvxpaek  39924  dvnxpaek  39926  dvnmul  39927  dvmptfprodlem  39928  dvnprodlem2  39931  itgsinexplem1  39938  itgsinexp  39939  itgcoscmulx  39954  itgsincmulx  39959  itgiccshift  39965  itgperiod  39966  stoweidlem1  39987  stoweidlem11  39997  stoweidlem13  39999  stoweidlem14  40000  stoweidlem17  40003  stoweidlem25  40011  stoweidlem26  40012  stoweidlem42  40028  wallispilem4  40054  wallispilem5  40055  wallispi  40056  wallispi2lem1  40057  wallispi2lem2  40058  wallispi2  40059  stirlinglem1  40060  stirlinglem3  40062  stirlinglem4  40063  stirlinglem5  40064  stirlinglem6  40065  stirlinglem7  40066  stirlinglem8  40067  stirlinglem10  40069  stirlinglem11  40070  stirlinglem12  40071  stirlinglem13  40072  stirlinglem14  40073  stirlinglem15  40074  dirker2re  40078  dirkerdenne0  40079  dirkerper  40082  dirkertrigeqlem1  40084  dirkertrigeqlem2  40085  dirkertrigeqlem3  40086  dirkertrigeq  40087  dirkeritg  40088  dirkercncflem2  40090  dirkercncflem4  40092  fourierdlem26  40119  fourierdlem30  40123  fourierdlem39  40132  fourierdlem42  40135  fourierdlem47  40139  fourierdlem48  40140  fourierdlem56  40148  fourierdlem57  40149  fourierdlem58  40150  fourierdlem62  40154  fourierdlem65  40157  fourierdlem66  40158  fourierdlem68  40160  fourierdlem72  40164  fourierdlem73  40165  fourierdlem76  40168  fourierdlem80  40172  fourierdlem83  40175  fourierdlem85  40177  fourierdlem89  40181  fourierdlem90  40182  fourierdlem91  40183  fourierdlem95  40187  fourierdlem97  40189  fourierdlem101  40193  fourierdlem103  40195  fourierdlem104  40196  fourierdlem111  40203  sqwvfoura  40214  sqwvfourb  40215  fourierswlem  40216  fouriersw  40217  elaa2lem  40219  etransclem8  40228  etransclem18  40238  etransclem20  40240  etransclem21  40241  etransclem23  40243  etransclem24  40244  etransclem31  40251  etransclem33  40253  etransclem35  40255  etransclem45  40265  etransclem46  40266  etransclem47  40267  etransclem48  40268  hoicvrrex  40539  hoidmvlelem2  40579  smfmullem1  40767  sigarim  40809  sigarac  40810  sigaraf  40811  sigarmf  40812  sigarls  40815  sigardiv  40819  sigarcol  40822  cevathlem1  40825  fmtnorec2lem  41225  fmtnorec3  41231  fmtnorec4  41232  fmtnoprmfac1  41248  fmtnoprmfac2  41250  fmtnofac2lem  41251  pwdif  41272  sfprmdvdsmersenne  41291  lighneallem3  41295  opeoALTV  41366  perfectALTVlem2  41402  0nodd  41581  2nodd  41583  2zlidl  41705  2zrngnmlid  41720  altgsumbcALT  41902  fldivmod  42084  nn0sumshdiglemA  42184  nn0sumshdiglemB  42185  nn0sumshdiglem2  42187  nn0mullong  42190  i2linesd  42296  aacllem  42318  amgmwlem  42319  amgmlemALT  42320
  Copyright terms: Public domain W3C validator