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

Theorem mulid1d 8868
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 8851 . 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 1632    e. wcel 1696  (class class class)co 5874   CCcc 8751   1c1 8754    x. cmul 8758
This theorem is referenced by:  muladd11  8998  divrec  9456  diveq1  9470  conjmul  9493  modid  11009  expadd  11160  leexp2r  11175  nnlesq  11222  faclbnd  11319  faclbnd2  11320  faclbnd4lem3  11324  faclbnd6  11328  facavg  11330  bcn0  11339  bcn1  11341  hashf1lem2  11410  hashfac  11412  reccn2  12086  iseraltlem2  12171  iseraltlem3  12172  binom11  12306  harmonic  12333  arisum2  12335  trireciplem  12336  geoserg  12340  cvgrat  12355  efzval  12398  tanhlt1  12456  tanaddlem  12462  tanadd  12463  cos01gt0  12487  absef  12493  1dvds  12559  3dvds  12607  bitsfzo  12642  bitsmod  12643  gcdmultiple  12745  sqgcd  12753  coprmdvds  12797  qredeu  12802  phiprmpw  12860  coprimeprodsq  12878  pc2dvds  12947  sumhash  12960  fldivp1  12961  pcfaclem  12962  prmpwdvds  12967  prmreclem1  12979  vdwlem3  13046  vdwlem9  13052  sylow2a  14946  odadd  15158  zsssubrg  16446  zcyg  16461  prmirredlem  16462  mulgrhm2  16477  znrrg  16535  icopnfcnv  18456  icopnfhmeo  18457  lebnumii  18480  reparphti  18511  itg2const  19111  itg2monolem3  19123  bddibl  19210  dveflem  19342  mvth  19355  dvlipcn  19357  dvivthlem1  19371  dvfsumle  19384  dvfsumabs  19386  dvfsumlem2  19390  plyconst  19604  plyeq0lem  19608  plyco  19639  0dgrb  19644  coefv0  19645  vieta1  19708  aaliou3lem2  19739  tayl0  19757  taylply2  19763  dvtaylp  19765  taylthlem2  19769  radcnvlem1  19805  abelthlem1  19823  abelthlem2  19824  abelthlem3  19825  abelthlem7  19830  abelthlem8  19831  abelthlem9  19832  efper  19863  tangtx  19889  eflogeq  19971  logdivlti  19987  logcnlem4  20008  advlogexp  20018  cxpmul2  20052  dvcxp2  20099  cxpaddle  20108  cxpeq  20113  loglesqr  20114  ang180lem5  20127  isosctrlem2  20135  isosctrlem3  20136  2efiatan  20230  dvatan  20247  leibpi  20254  birthdaylem3  20264  jensenlem2  20298  harmonicbnd4  20320  wilthlem2  20323  ftalem5  20330  basellem2  20335  basellem5  20338  basellem8  20341  0sgm  20398  muinv  20449  chpub  20475  logfaclbnd  20477  logexprlim  20480  dchrsum2  20523  sumdchr2  20525  bposlem1  20539  bposlem2  20540  bposlem5  20543  lgsquad2lem1  20613  lgsquad3  20616  2sqlem6  20624  2sqlem8  20627  chtppilim  20640  vmadivsum  20647  dchrisumlem1  20654  dchrisum0flblem1  20673  rpvmasum2  20677  dchrisum0re  20678  dchrisum0lem2a  20682  dchrisum0lem3  20684  rpvmasum  20691  mudivsum  20695  mulogsumlem  20696  vmalogdivsum2  20703  pntrsumo1  20730  pntrlog2bndlem2  20743  pntrlog2bndlem4  20745  pntrlog2bndlem5  20746  pntibndlem2  20756  pntlemc  20760  pntlemf  20770  ostth2lem2  20799  ostth2lem3  20800  ostth2lem4  20801  ostth2  20802  ostth3  20803  nmoub3i  21367  ubthlem2  21466  htthlem  21513  nmcexi  22622  nmopcoadji  22697  branmfn  22701  subfacval2  23733  cvmliftlem2  23832  snmlff  23927  sinccvglem  24020  divelunit  24095  faclimlem5  24121  axpaschlem  24640  axcontlem2  24665  axcontlem4  24667  axcontlem8  24671  itg2addnclem  25003  areacirclem2  25028  areacirclem5  25032  cntotbnd  26623  irrapxlem1  27010  irrapxlem4  27013  pell1qrgaplem  27061  reglogexpbas  27085  rmspecsqrnq  27094  rmspecfund  27097  rmxy1  27110  rmxp1  27120  rmyp1  27121  rmxm1  27122  jm2.17a  27150  jm2.18  27184  jm2.23  27192  jm2.25  27195  jm2.16nn0  27200  expgrowthi  27653  expgrowth  27655  m1expeven  27828  wallispilem4  27920  stirlinglem1  27926  stirlinglem3  27928  stirlinglem6  27931  stirlinglem7  27932  stirlinglem8  27933  stirlinglem10  27935  stirlinglem12  27937
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-resscn 8810  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-mulcl 8815  ax-mulcom 8817  ax-mulass 8819  ax-distr 8820  ax-1rid 8823  ax-cnre 8826
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877
  Copyright terms: Public domain W3C validator