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

Theorem mulcld 9609
Description: Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1  |-  ( ph  ->  A  e.  CC )
addcld.2  |-  ( ph  ->  B  e.  CC )
Assertion
Ref Expression
mulcld  |-  ( ph  ->  ( A  x.  B
)  e.  CC )

Proof of Theorem mulcld
StepHypRef Expression
1 addcld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addcld.2 . 2  |-  ( ph  ->  B  e.  CC )
3 mulcl 9569 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
41, 2, 3syl2anc 665 1  |-  ( ph  ->  ( A  x.  B
)  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1872  (class class class)co 6244   CCcc 9483    x. cmul 9490
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 9547
This theorem depends on definitions:  df-bi 188  df-an 372
This theorem is referenced by:  mul02lem1  9755  addid1  9759  cnegex  9760  kcnktkm1cn  9996  receu  10203  divrec  10232  divcan3  10240  divdivdiv  10254  divsubdiv  10269  cru  10547  mul2lt0rlt0  11344  lincmb01cmp  11721  iccf1o  11722  flpmodeq  12046  moddiffl  12053  modvalp1  12060  modcyc  12077  modadd1  12079  modmul1  12088  modaddmulmod  12101  mulexpz  12257  expmulz  12263  binom3  12338  bernneq  12343  remullem  13130  cjreim2  13163  absimle  13311  abstri  13332  sqreulem  13361  sqreu  13362  mulcn2  13597  reccn2  13598  o1rlimmul  13620  isummulc2  13761  fsummulc2  13783  fsumparts  13804  binomlem  13825  binom1dif  13829  incexclem  13832  incexc  13833  incexc2  13834  geomulcvg  13870  mertenslem1  13878  mertens  13880  fprodmul  13952  fprodn0f  13983  iprodmul  13994  binomfallfaclem1  14030  binomfallfaclem2  14031  binomrisefac  14033  bpolycl  14043  bpolysum  14044  bpolydiflem  14045  bpoly4  14050  efaddlem  14085  sinadd  14156  cosadd  14157  tanaddlem  14158  tanadd  14159  addsin  14162  sincossq  14168  sin2t  14169  dvds2ln  14271  oddm1even  14304  sadadd2lem2  14362  bezoutlem2OLD  14442  bezoutlem3OLD  14443  bezoutlem4OLD  14444  bezoutlem2  14445  bezoutlem3  14446  bezoutlem4  14447  lcmgcdlem  14509  phiprmpw  14662  pythagtriplem12  14714  pythagtriplem14  14716  pythagtriplem16  14718  pcpremul  14731  pcaddlem  14771  fldivp1  14780  mul4sqlem  14835  4sqlem14OLD  14840  4sqlem14  14846  vdwapun  14862  vdwlem2  14870  vdwlem6  14874  zringlpirlem3OLD  18992  zringlpirlem3  18994  znunit  19071  blcvx  21753  icopnfcnv  21907  mbfmulc2re  22541  mbfmulc2  22556  itg1addlem4  22594  itg1addlem5  22595  itg1mulc  22599  mbfmul  22621  itgcl  22678  itgcnlem  22684  iblmulc2  22725  itgmulc2  22728  itgabs  22729  itgsplit  22730  dvmulbr  22830  dvcmul  22835  dvcmulf  22836  dvexp  22844  dvmptcmul  22855  dvexp3  22867  dvsincos  22870  cmvth  22880  dvlipcn  22883  dvfsumabs  22912  dvfsumlem1  22915  ftc1lem4  22928  itgparts  22936  plyf  23089  ply1termlem  23094  plyeq0lem  23101  plypf1  23103  plyaddlem1  23104  plymullem1  23105  coeeulem  23115  coeidlem  23128  coeid3  23131  plyco  23132  coemullem  23141  coemulhi  23145  coemulc  23146  dgrcolem2  23165  plycjlem  23167  plyrecj  23170  dvply1  23174  vieta1lem2  23201  vieta1  23202  elqaalem3  23211  elqaalem3OLD  23214  aareccl  23219  aalioulem1  23225  taylfvallem1  23249  tayl0  23254  dvtaylp  23262  taylthlem2  23266  psergf  23304  radcnvlem1  23305  dvradcnv  23313  psercn2  23315  pserdvlem2  23320  pserdv2  23322  abelthlem4  23326  abelthlem5  23327  abelthlem6  23328  abelthlem7  23330  abelthlem9  23332  tanregt0  23425  efgh  23427  efabl  23436  efsubm  23437  cosargd  23494  abslogle  23504  tanarg  23505  advlogexp  23537  logtayllem  23541  logtayl  23542  cxpadd  23561  mulcxp  23567  cxpmul  23570  cxpmul2  23571  cxpmul2z  23573  abscxp  23574  abscxp2  23575  dvcxp2  23618  abscxpbnd  23630  root1eq1  23632  cxpeq  23634  angcan  23668  pythag  23683  ssscongptld  23688  affineequiv  23689  affineequiv2  23690  chordthmlem2  23696  chordthmlem3  23697  chordthmlem4  23698  chordthmlem5  23699  heron  23701  quad2  23702  quad  23703  dcubic1lem  23706  dcubic2  23707  dcubic1  23708  dcubic  23709  mcubic  23710  cubic2  23711  cubic  23712  binom4  23713  dquartlem1  23714  dquartlem2  23715  dquart  23716  quart1cl  23717  quart1lem  23718  quart1  23719  quartlem1  23720  quartlem2  23721  atantayl3  23802  leibpi  23805  birthdaylem2  23815  divsqrtsumo1  23846  cvxcl  23847  jensenlem2  23850  lgamgulmlem2  23892  lgamgulmlem3  23893  lgamgulmlem4  23894  lgamgulmlem5  23895  lgamgulmlem6  23896  lgamgulm2  23898  lgamcvg2  23917  gamcvg  23918  gamcvg2lem  23921  wilthlem2  23931  ftalem1  23934  ftalem2  23935  ftalem4  23937  ftalem5  23938  ftalem4OLD  23939  ftalem5OLD  23940  basellem2  23945  basellem3  23946  basellem8  23951  muinv  24059  fsumdvdsmul  24061  logfacrlim  24089  logexprlim  24090  perfectlem2  24095  bposlem9  24157  lgsquad2lem1  24223  2sqlem3  24231  rplogsumlem1  24259  dchrisumlem2  24265  dchrisumlem3  24266  dchrmusum2  24269  dchrvmasumlem1  24270  dchrvmasum2lem  24271  dchrvmasum2if  24272  dchrvmasumlem3  24274  dchrvmasumiflem1  24276  dchrvmasumiflem2  24277  rpvmasum2  24287  dchrisum0lem1  24291  dchrisum0lem2a  24292  dchrisum0lem2  24293  dchrmusumlem  24297  dchrvmasumlem  24298  rplogsum  24302  mudivsum  24305  mulogsumlem  24306  mulogsum  24307  mulog2sumlem1  24309  mulog2sumlem2  24310  mulog2sumlem3  24311  vmalogdivsum  24314  logsqvma  24317  log2sumbnd  24319  selberglem1  24320  selberglem2  24321  selberglem3  24322  selberg  24323  selberg2lem  24325  selberg2  24326  selberg3lem1  24332  selberg3  24334  selberg4lem1  24335  selberg4  24336  pntrsumo1  24340  selbergr  24343  selberg3r  24344  selberg4r  24345  selberg34r  24346  pntsval2  24351  pntrlog2bndlem1  24352  pntrlog2bndlem2  24353  pntrlog2bndlem3  24354  pntrlog2bndlem4  24355  pntrlog2bndlem5  24356  pntrlog2bndlem6  24358  pntrlog2bnd  24359  pntlemb  24372  pntlemf  24380  pntlemo  24382  ostth2lem2  24409  ostth2lem3  24410  ttgcontlem1  24852  brbtwn2  24872  colinearalg  24877  ax5seglem2  24896  ax5seglem9  24904  axeuclidlem  24929  axcontlem2  24932  axcontlem4  24934  axcontlem7  24937  axcontlem8  24938  ex-ind-dvds  25836  ipval2  26280  dipcl  26288  riesz3i  27652  bhmafibid1  28351  bhmafibid2  28352  2sqmod  28355  cnre2csqima  28664  rmulccn  28681  indsum  28791  dya2icoseg  29046  oddpwdc  29134  eulerpartlems  29140  eulerpartlemsv3  29141  eulerpartlemgs2  29160  signsplypnf  29386  subfacval2  29857  subfaclim  29858  rescon  29916  subdivcomb1  30306  subdivcomb2  30307  iprodgam  30324  fwddifnp1  30876  bj-subcom  31616  bj-lineq  31620  bj-bary1lem  31622  bj-bary1lem1  31623  bj-bary1  31624  iblmulc2nc  31914  itgmulc2nc  31917  itgabsnc  31918  ftc1cnnclem  31922  ftc1anclem3  31926  dvasin  31935  areacirclem1  31939  areacirclem4  31942  areacirc  31944  cntotbnd  32035  pellexlem1  35586  pellexlem2  35587  pellexlem6  35591  pell1234qrne0  35612  pell1234qrreccl  35613  pell1234qrmulcl  35614  pell1234qrdich  35620  pell14qrdich  35628  pell1qrge1  35629  pell1qrgaplem  35632  qirropth  35669  rmxyneg  35681  rmxyadd  35682  rmxm1  35695  rmym1  35696  rmxluc  35697  rmyluc  35698  rmxdbl  35700  rmydbl  35701  jm2.18  35756  jm2.19lem1  35757  jm2.19lem2  35758  jm2.19lem4  35760  jm2.19  35761  jm2.22  35763  jm2.23  35764  jm2.25  35767  jm2.27c  35775  jm3.1lem2  35786  flcidc  35953  itgpowd  36012  areaquad  36014  inductionexd  36506  imo72b2lem0  36521  int-leftdistd  36539  radcnvrat  36576  expgrowth  36597  binomcxplemwb  36610  binomcxplemnn0  36611  binomcxplemfrat  36613  binomcxplemdvbinom  36615  binomcxplemnotnn0  36618  sineq0ALT  37250  mul13d  37386  fperiodmullem  37418  fperiodmul  37419  divcan8d  37429  dmmcand  37431  mulc1cncfg  37550  mccllem  37560  clim1fr1  37562  mullimc  37579  mullimcf  37586  sumnnodd  37593  reclimc  37617  sinmulcos  37623  coskpi2  37624  cosknegpi  37627  dvsinexp  37663  dvmptdiv  37672  dvasinbx  37675  dvdivf  37677  dvdivbd  37678  dvdivcncf  37682  dvbdfbdioolem2  37684  dvxpaek  37698  dvnxpaek  37700  dvnmul  37701  dvmptfprodlem  37702  dvnprodlem2  37705  itgsinexplem1  37713  itgsinexp  37714  itgcoscmulx  37729  itgsincmulx  37734  itgiccshift  37740  itgperiod  37741  stoweidlem1  37744  stoweidlem11  37754  stoweidlem13  37756  stoweidlem14  37757  stoweidlem17  37760  stoweidlem25  37768  stoweidlem26  37769  stoweidlem42  37786  wallispilem4  37813  wallispilem5  37814  wallispi  37815  wallispi2lem1  37816  wallispi2lem2  37817  wallispi2  37818  stirlinglem1  37819  stirlinglem3  37821  stirlinglem4  37822  stirlinglem5  37823  stirlinglem6  37824  stirlinglem7  37825  stirlinglem8  37826  stirlinglem10  37828  stirlinglem11  37829  stirlinglem12  37830  stirlinglem13  37831  stirlinglem14  37832  stirlinglem15  37833  dirker2re  37837  dirkerdenne0  37838  dirkerper  37841  dirkertrigeqlem1  37843  dirkertrigeqlem2  37844  dirkertrigeqlem3  37845  dirkertrigeq  37846  dirkeritg  37847  dirkercncflem2  37849  dirkercncflem4  37851  fourierdlem26  37878  fourierdlem30  37882  fourierdlem39  37892  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem47  37900  fourierdlem48  37901  fourierdlem56  37909  fourierdlem57  37910  fourierdlem58  37911  fourierdlem62  37915  fourierdlem65  37918  fourierdlem66  37919  fourierdlem68  37921  fourierdlem72  37925  fourierdlem73  37926  fourierdlem76  37929  fourierdlem80  37933  fourierdlem83  37936  fourierdlem85  37938  fourierdlem89  37942  fourierdlem90  37943  fourierdlem91  37944  fourierdlem95  37948  fourierdlem97  37950  fourierdlem101  37954  fourierdlem103  37956  fourierdlem104  37957  fourierdlem111  37964  sqwvfoura  37975  sqwvfourb  37976  fourierswlem  37977  fouriersw  37978  elaa2lem  37980  elaa2lemOLD  37981  etransclem8  37990  etransclem18  38000  etransclem20  38002  etransclem21  38003  etransclem23  38005  etransclem24  38006  etransclem31  38013  etransclem33  38015  etransclem35  38017  etransclem45  38027  etransclem46  38028  etransclem47  38029  etransclem48OLD  38030  etransclem48  38031  hoicvrrex  38225  hoidmvlelem2  38265  sigarim  38274  sigarac  38275  sigaraf  38276  sigarmf  38277  sigarls  38280  sigardiv  38284  sigarcol  38287  cevathlem1  38290  deccarry  38528  opeoALTV  38626  perfectALTVlem2  38657  0nodd  39401  2nodd  39403  2zlidl  39525  2zrngnmlid  39540  altgsumbcALT  39727  fldivmod  39914  nn0sumshdiglemA  40023  nn0sumshdiglemB  40024  nn0sumshdiglem2  40026  nn0mullong  40029  i2linesd  40111  aacllem  40133
  Copyright terms: Public domain W3C validator