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

Theorem mulcld 10223
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 10183 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
41, 2, 3syl2anc 696 1 (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2127  (class class class)co 6801  cc 10097   · cmul 10104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 10161
This theorem depends on definitions:  df-bi 197  df-an 385
This theorem is referenced by:  mul02lem1  10375  addid1  10379  cnegex  10380  kcnktkm1cn  10624  receu  10835  divrec  10864  divcan3  10874  muldivdir  10883  divdivdiv  10889  divsubdiv  10904  cru  11175  mul2lt0rlt0  12096  lincmb01cmp  12479  iccf1o  12480  flpmodeq  12838  moddiffl  12846  modvalp1  12854  modcyc  12870  modadd1  12872  modmuladdnn0  12879  modmul1  12888  modaddmulmod  12902  mulexpz  13065  expmulz  13071  binom3  13150  bernneq  13155  mulsubdivbinom2  13211  muldivbinom2  13212  remullem  14038  cjreim2  14071  absimle  14219  abstri  14240  sqreulem  14269  sqreu  14270  mulcn2  14496  reccn2  14497  o1rlimmul  14519  isummulc2  14663  fsummulc2  14686  fsumparts  14708  binomlem  14731  binom1dif  14735  incexclem  14738  incexc  14739  incexc2  14740  geomulcvg  14777  mertenslem1  14786  mertens  14788  fprodmul  14860  fprodn0f  14892  iprodmul  14904  binomfallfaclem1  14940  binomfallfaclem2  14941  binomrisefac  14943  bpolycl  14953  bpolysum  14954  bpolydiflem  14955  bpoly4  14960  efaddlem  14993  sinadd  15064  cosadd  15065  tanaddlem  15066  tanadd  15067  addsin  15070  sincossq  15076  sin2t  15077  dvds2ln  15187  oddm1even  15240  pwp1fsum  15287  flodddiv4  15310  sadadd2lem2  15345  bezoutlem2  15430  bezoutlem3  15431  bezoutlem4  15432  lcmgcdlem  15492  phiprmpw  15654  pythagtriplem12  15704  pythagtriplem14  15706  pythagtriplem16  15708  pcpremul  15721  pcaddlem  15765  fldivp1  15774  mul4sqlem  15830  4sqlem14  15835  vdwapun  15851  vdwlem2  15859  vdwlem6  15863  zringlpirlem3  20007  znunit  20085  blcvx  22773  icopnfcnv  22913  cphipipcj  23171  cphipval2  23211  4cphipval2  23212  cphipval  23213  mbfmulc2re  23585  mbfmulc2  23600  itg1addlem4  23636  itg1addlem5  23637  itg1mulc  23641  mbfmul  23663  itgcl  23720  itgcnlem  23726  iblmulc2  23767  itgmulc2  23770  itgabs  23771  itgsplit  23772  dvmulbr  23872  dvcmul  23877  dvcmulf  23878  dvexp  23886  dvmptcmul  23897  dvmptdiv  23907  dvexp3  23911  dvsincos  23914  cmvth  23924  dvlipcn  23927  dvfsumabs  23956  dvfsumlem1  23959  ftc1lem4  23972  itgparts  23980  plyf  24124  ply1termlem  24129  plyeq0lem  24136  plypf1  24138  plyaddlem1  24139  plymullem1  24140  coeeulem  24150  coeidlem  24163  coeid3  24166  plyco  24167  coemullem  24176  coemulhi  24180  coemulc  24181  dgrcolem2  24200  plycjlem  24202  plyrecj  24205  dvply1  24209  vieta1lem2  24236  vieta1  24237  elqaalem3  24246  aareccl  24251  aalioulem1  24257  taylfvallem1  24281  tayl0  24286  dvtaylp  24294  taylthlem2  24298  psergf  24336  radcnvlem1  24337  dvradcnv  24345  psercn2  24347  pserdvlem2  24352  pserdv2  24354  abelthlem4  24358  abelthlem5  24359  abelthlem6  24360  abelthlem7  24362  abelthlem9  24364  tanregt0  24455  efgh  24457  efabl  24466  efsubm  24467  cosargd  24524  abslogle  24534  tanarg  24535  advlogexp  24571  logtayllem  24575  logtayl  24576  cxpadd  24595  mulcxp  24601  cxpmul  24604  cxpmul2  24605  cxpmul2z  24607  abscxp  24608  abscxp2  24609  dvcxp2  24652  abscxpbnd  24664  root1eq1  24666  cxpeq  24668  angcan  24702  pythag  24717  ssscongptld  24722  affineequiv  24723  affineequiv2  24724  chordthmlem2  24730  chordthmlem3  24731  chordthmlem4  24732  chordthmlem5  24733  heron  24735  quad2  24736  quad  24737  dcubic1lem  24740  dcubic2  24741  dcubic1  24742  dcubic  24743  mcubic  24744  cubic2  24745  cubic  24746  binom4  24747  dquartlem1  24748  dquartlem2  24749  dquart  24750  quart1cl  24751  quart1lem  24752  quart1  24753  quartlem1  24754  quartlem2  24755  atantayl3  24836  leibpi  24839  birthdaylem2  24849  divsqrtsumo1  24880  cvxcl  24881  jensenlem2  24884  lgamgulmlem2  24926  lgamgulmlem3  24927  lgamgulmlem4  24928  lgamgulmlem5  24929  lgamgulmlem6  24930  lgamgulm2  24932  lgamcvg2  24951  gamcvg  24952  gamcvg2lem  24955  wilthlem2  24965  ftalem1  24969  ftalem2  24970  ftalem4  24972  ftalem5  24973  basellem2  24978  basellem3  24979  basellem8  24984  muinv  25089  fsumdvdsmul  25091  logfacrlim  25119  logexprlim  25120  perfectlem2  25125  bposlem9  25187  gausslemma2dlem4  25264  lgsquad2lem1  25279  2lgslem3b  25292  2lgslem3c  25293  2lgslem3d  25294  2sqlem3  25315  rplogsumlem1  25343  dchrisumlem2  25349  dchrisumlem3  25350  dchrmusum2  25353  dchrvmasumlem1  25354  dchrvmasum2lem  25355  dchrvmasum2if  25356  dchrvmasumlem3  25358  dchrvmasumiflem1  25360  dchrvmasumiflem2  25361  rpvmasum2  25371  dchrisum0lem1  25375  dchrisum0lem2a  25376  dchrisum0lem2  25377  dchrmusumlem  25381  dchrvmasumlem  25382  rplogsum  25386  mudivsum  25389  mulogsumlem  25390  mulogsum  25391  mulog2sumlem1  25393  mulog2sumlem2  25394  mulog2sumlem3  25395  vmalogdivsum  25398  logsqvma  25401  log2sumbnd  25403  selberglem1  25404  selberglem2  25405  selberglem3  25406  selberg  25407  selberg2lem  25409  selberg2  25410  selberg3lem1  25416  selberg3  25418  selberg4lem1  25419  selberg4  25420  pntrsumo1  25424  selbergr  25427  selberg3r  25428  selberg4r  25429  selberg34r  25430  pntsval2  25435  pntrlog2bndlem1  25436  pntrlog2bndlem2  25437  pntrlog2bndlem3  25438  pntrlog2bndlem4  25439  pntrlog2bndlem5  25440  pntrlog2bndlem6  25442  pntrlog2bnd  25443  pntlemb  25456  pntlemf  25464  pntlemo  25466  ostth2lem2  25493  ostth2lem3  25494  ttgcontlem1  25935  brbtwn2  25955  colinearalg  25960  ax5seglem2  25979  ax5seglem9  25987  axeuclidlem  26012  axcontlem2  26015  axcontlem4  26017  axcontlem7  26020  axcontlem8  26021  finsumvtxdg2ssteplem4  26625  ex-ind-dvds  27600  ipval2  27842  dipcl  27847  riesz3i  29201  dpfrac1  29879  bhmafibid1  29924  bhmafibid2  29925  2sqmod  29928  cnre2csqima  30237  rmulccn  30254  indsum  30363  indsumin  30364  dya2icoseg  30619  oddpwdc  30696  eulerpartlems  30702  eulerpartlemsv3  30703  eulerpartlemgs2  30722  signsplypnf  30907  itgexpif  30964  breprexplemc  30990  breprexp  30991  vtscl  30996  vtsprod  30997  circlemeth  30998  logdivsqrle  31008  hgt750lemf  31011  hgt750leme  31016  subfacval2  31447  subfaclim  31448  resconn  31506  subdivcomb1  31889  subdivcomb2  31890  iprodgam  31906  fwddifnp1  32549  knoppndvlem2  32781  knoppndvlem7  32786  knoppndvlem9  32788  knoppndvlem11  32790  knoppndvlem14  32793  knoppndvlem16  32795  knoppndvlem17  32796  bj-subcom  33436  bj-lineq  33440  bj-bary1lem  33442  bj-bary1lem1  33443  bj-bary1  33444  iblmulc2nc  33757  itgmulc2nc  33760  itgabsnc  33761  ftc1cnnclem  33765  ftc1anclem3  33769  dvasin  33778  areacirclem1  33782  areacirclem4  33785  areacirc  33787  cntotbnd  33877  pellexlem1  37864  pellexlem2  37865  pellexlem6  37869  pell1234qrne0  37888  pell1234qrreccl  37889  pell1234qrmulcl  37890  pell1234qrdich  37896  pell14qrdich  37904  pell1qrge1  37905  pell1qrgaplem  37908  rmspecsqrtnq  37941  qirropth  37944  rmxyneg  37956  rmxyadd  37957  rmxm1  37970  rmym1  37971  rmxluc  37972  rmyluc  37973  rmxdbl  37975  rmydbl  37976  jm2.18  38026  jm2.19lem1  38027  jm2.19lem2  38028  jm2.19lem4  38030  jm2.19  38031  jm2.22  38033  jm2.23  38034  jm2.25  38037  jm2.27c  38045  jm3.1lem2  38056  flcidc  38215  itgpowd  38271  areaquad  38273  inductionexd  38924  imo72b2lem0  38936  int-leftdistd  38953  radcnvrat  38984  expgrowth  39005  binomcxplemwb  39018  binomcxplemnn0  39019  binomcxplemfrat  39021  binomcxplemdvbinom  39023  binomcxplemnotnn0  39026  sineq0ALT  39641  mul13d  39959  fperiodmullem  39985  fperiodmul  39986  divcan8d  39994  dmmcand  39995  ltdiv23neg  40084  mulc1cncfg  40293  mccllem  40301  clim1fr1  40305  mullimc  40320  mullimcf  40327  sumnnodd  40334  reclimc  40357  sinmulcos  40548  coskpi2  40549  cosknegpi  40552  dvsinexp  40597  dvasinbx  40607  dvdivf  40609  dvdivbd  40610  dvdivcncf  40614  dvbdfbdioolem2  40616  dvxpaek  40627  dvnxpaek  40629  dvnmul  40630  dvmptfprodlem  40631  dvnprodlem2  40634  itgsinexplem1  40641  itgsinexp  40642  itgcoscmulx  40657  itgsincmulx  40662  itgiccshift  40668  itgperiod  40669  stoweidlem1  40690  stoweidlem11  40700  stoweidlem13  40702  stoweidlem14  40703  stoweidlem17  40706  stoweidlem25  40714  stoweidlem26  40715  stoweidlem42  40731  wallispilem4  40757  wallispilem5  40758  wallispi  40759  wallispi2lem1  40760  wallispi2lem2  40761  wallispi2  40762  stirlinglem1  40763  stirlinglem3  40765  stirlinglem4  40766  stirlinglem5  40767  stirlinglem6  40768  stirlinglem7  40769  stirlinglem8  40770  stirlinglem10  40772  stirlinglem11  40773  stirlinglem12  40774  stirlinglem13  40775  stirlinglem14  40776  stirlinglem15  40777  dirker2re  40781  dirkerdenne0  40782  dirkerper  40785  dirkertrigeqlem1  40787  dirkertrigeqlem2  40788  dirkertrigeqlem3  40789  dirkertrigeq  40790  dirkeritg  40791  dirkercncflem2  40793  dirkercncflem4  40795  fourierdlem26  40822  fourierdlem30  40826  fourierdlem39  40835  fourierdlem42  40838  fourierdlem47  40842  fourierdlem48  40843  fourierdlem56  40851  fourierdlem57  40852  fourierdlem58  40853  fourierdlem62  40857  fourierdlem65  40860  fourierdlem66  40861  fourierdlem68  40863  fourierdlem72  40867  fourierdlem73  40868  fourierdlem76  40871  fourierdlem80  40875  fourierdlem83  40878  fourierdlem85  40880  fourierdlem89  40884  fourierdlem90  40885  fourierdlem91  40886  fourierdlem95  40890  fourierdlem97  40892  fourierdlem101  40896  fourierdlem103  40898  fourierdlem104  40899  fourierdlem111  40906  sqwvfoura  40917  sqwvfourb  40918  fourierswlem  40919  fouriersw  40920  elaa2lem  40922  etransclem8  40931  etransclem18  40941  etransclem20  40943  etransclem21  40944  etransclem23  40946  etransclem24  40947  etransclem31  40954  etransclem33  40956  etransclem35  40958  etransclem45  40968  etransclem46  40969  etransclem47  40970  etransclem48  40971  hoicvrrex  41245  hoidmvlelem2  41285  smfmullem1  41473  sigarim  41515  sigarac  41516  sigaraf  41517  sigarmf  41518  sigarls  41521  sigardiv  41525  sigarcol  41528  cevathlem1  41531  fmtnorec2lem  41933  fmtnorec3  41939  fmtnorec4  41940  fmtnoprmfac1  41956  fmtnoprmfac2  41958  fmtnofac2lem  41959  pwdif  41980  sfprmdvdsmersenne  41999  lighneallem3  42003  opeoALTV  42074  perfectALTVlem2  42110  0nodd  42289  2nodd  42291  2zlidl  42413  2zrngnmlid  42428  altgsumbcALT  42610  fldivmod  42792  nn0sumshdiglemA  42892  nn0sumshdiglemB  42893  nn0sumshdiglem2  42895  nn0mullong  42898  i2linesd  43007  aacllem  43029  amgmwlem  43030  amgmlemALT  43031
  Copyright terms: Public domain W3C validator