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

Theorem mulcld 9913
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 9873 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
41, 2, 3syl2anc 690 1 (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  (class class class)co 6524  cc 9787   · cmul 9794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 9851
This theorem depends on definitions:  df-bi 195  df-an 384
This theorem is referenced by:  mul02lem1  10060  addid1  10064  cnegex  10065  kcnktkm1cn  10309  receu  10518  divrec  10547  divcan3  10557  muldivdir  10566  divdivdiv  10572  divsubdiv  10587  cru  10856  mul2lt0rlt0  11761  lincmb01cmp  12139  iccf1o  12140  flpmodeq  12487  moddiffl  12495  modvalp1  12503  modcyc  12519  modadd1  12521  modmuladdnn0  12528  modmul1  12537  modaddmulmod  12551  mulexpz  12714  expmulz  12720  binom3  12799  bernneq  12804  mulsubdivbinom2  12860  muldivbinom2  12861  remullem  13659  cjreim2  13692  absimle  13840  abstri  13861  sqreulem  13890  sqreu  13891  mulcn2  14117  reccn2  14118  o1rlimmul  14140  isummulc2  14278  fsummulc2  14301  fsumparts  14322  binomlem  14343  binom1dif  14347  incexclem  14350  incexc  14351  incexc2  14352  geomulcvg  14389  mertenslem1  14398  mertens  14400  fprodmul  14472  fprodn0f  14504  iprodmul  14516  binomfallfaclem1  14552  binomfallfaclem2  14553  binomrisefac  14555  bpolycl  14565  bpolysum  14566  bpolydiflem  14567  bpoly4  14572  efaddlem  14605  sinadd  14676  cosadd  14677  tanaddlem  14678  tanadd  14679  addsin  14682  sincossq  14688  sin2t  14689  dvds2ln  14795  oddm1even  14848  pwp1fsum  14895  flodddiv4  14918  sadadd2lem2  14953  bezoutlem2  15038  bezoutlem3  15039  bezoutlem4  15040  lcmgcdlem  15100  phiprmpw  15262  pythagtriplem12  15312  pythagtriplem14  15314  pythagtriplem16  15316  pcpremul  15329  pcaddlem  15373  fldivp1  15382  mul4sqlem  15438  4sqlem14  15443  vdwapun  15459  vdwlem2  15467  vdwlem6  15471  zringlpirlem3  19596  znunit  19673  blcvx  22338  icopnfcnv  22477  mbfmulc2re  23135  mbfmulc2  23150  itg1addlem4  23186  itg1addlem5  23187  itg1mulc  23191  mbfmul  23213  itgcl  23270  itgcnlem  23276  iblmulc2  23317  itgmulc2  23320  itgabs  23321  itgsplit  23322  dvmulbr  23422  dvcmul  23427  dvcmulf  23428  dvexp  23436  dvmptcmul  23447  dvexp3  23459  dvsincos  23462  cmvth  23472  dvlipcn  23475  dvfsumabs  23504  dvfsumlem1  23507  ftc1lem4  23520  itgparts  23528  plyf  23672  ply1termlem  23677  plyeq0lem  23684  plypf1  23686  plyaddlem1  23687  plymullem1  23688  coeeulem  23698  coeidlem  23711  coeid3  23714  plyco  23715  coemullem  23724  coemulhi  23728  coemulc  23729  dgrcolem2  23748  plycjlem  23750  plyrecj  23753  dvply1  23757  vieta1lem2  23784  vieta1  23785  elqaalem3  23794  aareccl  23799  aalioulem1  23805  taylfvallem1  23829  tayl0  23834  dvtaylp  23842  taylthlem2  23846  psergf  23884  radcnvlem1  23885  dvradcnv  23893  psercn2  23895  pserdvlem2  23900  pserdv2  23902  abelthlem4  23906  abelthlem5  23907  abelthlem6  23908  abelthlem7  23910  abelthlem9  23912  tanregt0  24003  efgh  24005  efabl  24014  efsubm  24015  cosargd  24072  abslogle  24082  tanarg  24083  advlogexp  24115  logtayllem  24119  logtayl  24120  cxpadd  24139  mulcxp  24145  cxpmul  24148  cxpmul2  24149  cxpmul2z  24151  abscxp  24152  abscxp2  24153  dvcxp2  24196  abscxpbnd  24208  root1eq1  24210  cxpeq  24212  angcan  24246  pythag  24261  ssscongptld  24266  affineequiv  24267  affineequiv2  24268  chordthmlem2  24274  chordthmlem3  24275  chordthmlem4  24276  chordthmlem5  24277  heron  24279  quad2  24280  quad  24281  dcubic1lem  24284  dcubic2  24285  dcubic1  24286  dcubic  24287  mcubic  24288  cubic2  24289  cubic  24290  binom4  24291  dquartlem1  24292  dquartlem2  24293  dquart  24294  quart1cl  24295  quart1lem  24296  quart1  24297  quartlem1  24298  quartlem2  24299  atantayl3  24380  leibpi  24383  birthdaylem2  24393  divsqrtsumo1  24424  cvxcl  24425  jensenlem2  24428  lgamgulmlem2  24470  lgamgulmlem3  24471  lgamgulmlem4  24472  lgamgulmlem5  24473  lgamgulmlem6  24474  lgamgulm2  24476  lgamcvg2  24495  gamcvg  24496  gamcvg2lem  24499  wilthlem2  24509  ftalem1  24513  ftalem2  24514  ftalem4  24516  ftalem5  24517  basellem2  24522  basellem3  24523  basellem8  24528  muinv  24633  fsumdvdsmul  24635  logfacrlim  24663  logexprlim  24664  perfectlem2  24669  bposlem9  24731  gausslemma2dlem4  24808  lgsquad2lem1  24823  2lgslem3b  24836  2lgslem3c  24837  2lgslem3d  24838  2sqlem3  24859  rplogsumlem1  24887  dchrisumlem2  24893  dchrisumlem3  24894  dchrmusum2  24897  dchrvmasumlem1  24898  dchrvmasum2lem  24899  dchrvmasum2if  24900  dchrvmasumlem3  24902  dchrvmasumiflem1  24904  dchrvmasumiflem2  24905  rpvmasum2  24915  dchrisum0lem1  24919  dchrisum0lem2a  24920  dchrisum0lem2  24921  dchrmusumlem  24925  dchrvmasumlem  24926  rplogsum  24930  mudivsum  24933  mulogsumlem  24934  mulogsum  24935  mulog2sumlem1  24937  mulog2sumlem2  24938  mulog2sumlem3  24939  vmalogdivsum  24942  logsqvma  24945  log2sumbnd  24947  selberglem1  24948  selberglem2  24949  selberglem3  24950  selberg  24951  selberg2lem  24953  selberg2  24954  selberg3lem1  24960  selberg3  24962  selberg4lem1  24963  selberg4  24964  pntrsumo1  24968  selbergr  24971  selberg3r  24972  selberg4r  24973  selberg34r  24974  pntsval2  24979  pntrlog2bndlem1  24980  pntrlog2bndlem2  24981  pntrlog2bndlem3  24982  pntrlog2bndlem4  24983  pntrlog2bndlem5  24984  pntrlog2bndlem6  24986  pntrlog2bnd  24987  pntlemb  25000  pntlemf  25008  pntlemo  25010  ostth2lem2  25037  ostth2lem3  25038  ttgcontlem1  25480  brbtwn2  25500  colinearalg  25505  ax5seglem2  25524  ax5seglem9  25532  axeuclidlem  25557  axcontlem2  25560  axcontlem4  25562  axcontlem7  25565  axcontlem8  25566  ex-ind-dvds  26473  ipval2  26744  dipcl  26752  riesz3i  28108  bhmafibid1  28778  bhmafibid2  28779  2sqmod  28782  cnre2csqima  29088  rmulccn  29105  indsum  29215  dya2icoseg  29469  oddpwdc  29546  eulerpartlems  29552  eulerpartlemsv3  29553  eulerpartlemgs2  29572  signsplypnf  29756  subfacval2  30226  subfaclim  30227  rescon  30285  subdivcomb1  30667  subdivcomb2  30668  iprodgam  30684  fwddifnp1  31245  knoppndvlem2  31477  knoppndvlem7  31482  knoppndvlem9  31484  knoppndvlem11  31486  knoppndvlem14  31489  knoppndvlem16  31491  knoppndvlem17  31492  bj-subcom  32131  bj-lineq  32135  bj-bary1lem  32137  bj-bary1lem1  32138  bj-bary1  32139  iblmulc2nc  32445  itgmulc2nc  32448  itgabsnc  32449  ftc1cnnclem  32453  ftc1anclem3  32457  dvasin  32466  areacirclem1  32470  areacirclem4  32473  areacirc  32475  cntotbnd  32565  pellexlem1  36211  pellexlem2  36212  pellexlem6  36216  pell1234qrne0  36235  pell1234qrreccl  36236  pell1234qrmulcl  36237  pell1234qrdich  36243  pell14qrdich  36251  pell1qrge1  36252  pell1qrgaplem  36255  rmspecsqrtnq  36288  qirropth  36291  rmxyneg  36303  rmxyadd  36304  rmxm1  36317  rmym1  36318  rmxluc  36319  rmyluc  36320  rmxdbl  36322  rmydbl  36323  jm2.18  36373  jm2.19lem1  36374  jm2.19lem2  36375  jm2.19lem4  36377  jm2.19  36378  jm2.22  36380  jm2.23  36381  jm2.25  36384  jm2.27c  36392  jm3.1lem2  36403  flcidc  36563  itgpowd  36619  areaquad  36621  inductionexd  37273  imo72b2lem0  37287  int-leftdistd  37304  radcnvrat  37335  expgrowth  37356  binomcxplemwb  37369  binomcxplemnn0  37370  binomcxplemfrat  37372  binomcxplemdvbinom  37374  binomcxplemnotnn0  37377  sineq0ALT  37995  mul13d  38232  fperiodmullem  38258  fperiodmul  38259  divcan8d  38269  dmmcand  38270  ltdiv23neg  38359  mulc1cncfg  38457  mccllem  38465  clim1fr1  38469  mullimc  38484  mullimcf  38491  sumnnodd  38498  reclimc  38521  sinmulcos  38549  coskpi2  38550  cosknegpi  38553  dvsinexp  38599  dvmptdiv  38608  dvasinbx  38611  dvdivf  38613  dvdivbd  38614  dvdivcncf  38618  dvbdfbdioolem2  38620  dvxpaek  38631  dvnxpaek  38633  dvnmul  38634  dvmptfprodlem  38635  dvnprodlem2  38638  itgsinexplem1  38646  itgsinexp  38647  itgcoscmulx  38662  itgsincmulx  38667  itgiccshift  38673  itgperiod  38674  stoweidlem1  38695  stoweidlem11  38705  stoweidlem13  38707  stoweidlem14  38708  stoweidlem17  38711  stoweidlem25  38719  stoweidlem26  38720  stoweidlem42  38736  wallispilem4  38762  wallispilem5  38763  wallispi  38764  wallispi2lem1  38765  wallispi2lem2  38766  wallispi2  38767  stirlinglem1  38768  stirlinglem3  38770  stirlinglem4  38771  stirlinglem5  38772  stirlinglem6  38773  stirlinglem7  38774  stirlinglem8  38775  stirlinglem10  38777  stirlinglem11  38778  stirlinglem12  38779  stirlinglem13  38780  stirlinglem14  38781  stirlinglem15  38782  dirker2re  38786  dirkerdenne0  38787  dirkerper  38790  dirkertrigeqlem1  38792  dirkertrigeqlem2  38793  dirkertrigeqlem3  38794  dirkertrigeq  38795  dirkeritg  38796  dirkercncflem2  38798  dirkercncflem4  38800  fourierdlem26  38827  fourierdlem30  38831  fourierdlem39  38840  fourierdlem42  38843  fourierdlem47  38847  fourierdlem48  38848  fourierdlem56  38856  fourierdlem57  38857  fourierdlem58  38858  fourierdlem62  38862  fourierdlem65  38865  fourierdlem66  38866  fourierdlem68  38868  fourierdlem72  38872  fourierdlem73  38873  fourierdlem76  38876  fourierdlem80  38880  fourierdlem83  38883  fourierdlem85  38885  fourierdlem89  38889  fourierdlem90  38890  fourierdlem91  38891  fourierdlem95  38895  fourierdlem97  38897  fourierdlem101  38901  fourierdlem103  38903  fourierdlem104  38904  fourierdlem111  38911  sqwvfoura  38922  sqwvfourb  38923  fourierswlem  38924  fouriersw  38925  elaa2lem  38927  etransclem8  38936  etransclem18  38946  etransclem20  38948  etransclem21  38949  etransclem23  38951  etransclem24  38952  etransclem31  38959  etransclem33  38961  etransclem35  38963  etransclem45  38973  etransclem46  38974  etransclem47  38975  etransclem48  38976  hoicvrrex  39247  hoidmvlelem2  39287  smfmullem1  39477  sigarim  39490  sigarac  39491  sigaraf  39492  sigarmf  39493  sigarls  39496  sigardiv  39500  sigarcol  39503  cevathlem1  39506  fmtnorec2lem  39794  fmtnorec3  39800  fmtnorec4  39801  fmtnoprmfac1  39817  fmtnoprmfac2  39819  fmtnofac2lem  39820  pwdif  39841  sfprmdvdsmersenne  39860  lighneallem3  39864  opeoALTV  39935  perfectALTVlem2  39967  0nodd  41599  2nodd  41601  2zlidl  41723  2zrngnmlid  41738  altgsumbcALT  41923  fldivmod  42106  nn0sumshdiglemA  42210  nn0sumshdiglemB  42211  nn0sumshdiglem2  42213  nn0mullong  42216  dpfrac1  42272  i2linesd  42294  aacllem  42316  amgmwlem  42317  amgmlemALT  42318
  Copyright terms: Public domain W3C validator