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

Theorem mulid1d 8852
Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
addcld.1  |-  ( ph  ->  A  e.  CC )
Assertion
Ref Expression
mulid1d  |-  ( ph  ->  ( A  x.  1 )  =  A )

Proof of Theorem mulid1d
StepHypRef Expression
1 addcld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 mulid1 8835 . 2  |-  ( A  e.  CC  ->  ( A  x.  1 )  =  A )
31, 2syl 15 1  |-  ( ph  ->  ( A  x.  1 )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684  (class class class)co 5858   CCcc 8735   1c1 8738    x. cmul 8742
This theorem is referenced by:  muladd11  8982  divrec  9440  diveq1  9454  conjmul  9477  modid  10993  expadd  11144  leexp2r  11159  nnlesq  11206  faclbnd  11303  faclbnd2  11304  faclbnd4lem3  11308  faclbnd6  11312  facavg  11314  bcn0  11323  bcn1  11325  hashf1lem2  11394  hashfac  11396  reccn2  12070  iseraltlem2  12155  iseraltlem3  12156  binom11  12290  harmonic  12317  arisum2  12319  trireciplem  12320  geoserg  12324  cvgrat  12339  efzval  12382  tanhlt1  12440  tanaddlem  12446  tanadd  12447  cos01gt0  12471  absef  12477  1dvds  12543  3dvds  12591  bitsfzo  12626  bitsmod  12627  gcdmultiple  12729  sqgcd  12737  coprmdvds  12781  qredeu  12786  phiprmpw  12844  coprimeprodsq  12862  pc2dvds  12931  sumhash  12944  fldivp1  12945  pcfaclem  12946  prmpwdvds  12951  prmreclem1  12963  vdwlem3  13030  vdwlem9  13036  sylow2a  14930  odadd  15142  zsssubrg  16430  zcyg  16445  prmirredlem  16446  mulgrhm2  16461  znrrg  16519  icopnfcnv  18440  icopnfhmeo  18441  lebnumii  18464  reparphti  18495  itg2const  19095  itg2monolem3  19107  bddibl  19194  dveflem  19326  mvth  19339  dvlipcn  19341  dvivthlem1  19355  dvfsumle  19368  dvfsumabs  19370  dvfsumlem2  19374  plyconst  19588  plyeq0lem  19592  plyco  19623  0dgrb  19628  coefv0  19629  vieta1  19692  aaliou3lem2  19723  tayl0  19741  taylply2  19747  dvtaylp  19749  taylthlem2  19753  radcnvlem1  19789  abelthlem1  19807  abelthlem2  19808  abelthlem3  19809  abelthlem7  19814  abelthlem8  19815  abelthlem9  19816  efper  19847  tangtx  19873  eflogeq  19955  logdivlti  19971  logcnlem4  19992  advlogexp  20002  cxpmul2  20036  dvcxp2  20083  cxpaddle  20092  cxpeq  20097  loglesqr  20098  ang180lem5  20111  isosctrlem2  20119  isosctrlem3  20120  2efiatan  20214  dvatan  20231  leibpi  20238  birthdaylem3  20248  jensenlem2  20282  harmonicbnd4  20304  wilthlem2  20307  ftalem5  20314  basellem2  20319  basellem5  20322  basellem8  20325  0sgm  20382  muinv  20433  chpub  20459  logfaclbnd  20461  logexprlim  20464  dchrsum2  20507  sumdchr2  20509  bposlem1  20523  bposlem2  20524  bposlem5  20527  lgsquad2lem1  20597  lgsquad3  20600  2sqlem6  20608  2sqlem8  20611  chtppilim  20624  vmadivsum  20631  dchrisumlem1  20638  dchrisum0flblem1  20657  rpvmasum2  20661  dchrisum0re  20662  dchrisum0lem2a  20666  dchrisum0lem3  20668  rpvmasum  20675  mudivsum  20679  mulogsumlem  20680  vmalogdivsum2  20687  pntrsumo1  20714  pntrlog2bndlem2  20727  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  pntibndlem2  20740  pntlemc  20744  pntlemf  20754  ostth2lem2  20783  ostth2lem3  20784  ostth2lem4  20785  ostth2  20786  ostth3  20787  nmoub3i  21351  ubthlem2  21450  htthlem  21497  nmcexi  22606  nmopcoadji  22681  branmfn  22685  subfacval2  23718  cvmliftlem2  23817  snmlff  23912  sinccvglem  24005  divelunit  24080  axpaschlem  24568  axcontlem2  24593  axcontlem4  24595  axcontlem8  24599  areacirclem2  24925  areacirclem5  24929  cntotbnd  26520  irrapxlem1  26907  irrapxlem4  26910  pell1qrgaplem  26958  reglogexpbas  26982  rmspecsqrnq  26991  rmspecfund  26994  rmxy1  27007  rmxp1  27017  rmyp1  27018  rmxm1  27019  jm2.17a  27047  jm2.18  27081  jm2.23  27089  jm2.25  27092  jm2.16nn0  27097  expgrowthi  27550  expgrowth  27552  m1expeven  27725  wallispilem4  27817  stirlinglem1  27823  stirlinglem3  27825  stirlinglem6  27828  stirlinglem7  27829  stirlinglem8  27830  stirlinglem10  27832  stirlinglem12  27834
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-mulcl 8799  ax-mulcom 8801  ax-mulass 8803  ax-distr 8804  ax-1rid 8807  ax-cnre 8810
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861
  Copyright terms: Public domain W3C validator