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

Theorem mulid1d 9031
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 9014 . 2  |-  ( A  e.  CC  ->  ( A  x.  1 )  =  A )
31, 2syl 16 1  |-  ( ph  ->  ( A  x.  1 )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1717  (class class class)co 6013   CCcc 8914   1c1 8917    x. cmul 8921
This theorem is referenced by:  muladd11  9161  divrec  9619  diveq1  9633  conjmul  9656  modid  11190  expadd  11342  leexp2r  11357  nnlesq  11404  faclbnd  11501  faclbnd2  11502  faclbnd4lem3  11506  faclbnd6  11510  facavg  11512  bcn0  11521  bcn1  11524  hashf1lem2  11625  hashfac  11627  reccn2  12310  iseraltlem2  12396  iseraltlem3  12397  binom11  12531  harmonic  12558  arisum2  12560  trireciplem  12561  geoserg  12565  cvgrat  12580  efzval  12623  tanhlt1  12681  tanaddlem  12687  tanadd  12688  cos01gt0  12712  absef  12718  1dvds  12784  3dvds  12832  bitsfzo  12867  bitsmod  12868  gcdmultiple  12970  sqgcd  12978  coprmdvds  13022  qredeu  13027  phiprmpw  13085  coprimeprodsq  13103  pc2dvds  13172  sumhash  13185  fldivp1  13186  pcfaclem  13187  prmpwdvds  13192  prmreclem1  13204  vdwlem3  13271  vdwlem9  13277  sylow2a  15173  odadd  15385  zsssubrg  16673  zcyg  16688  prmirredlem  16689  mulgrhm2  16704  znrrg  16762  icopnfcnv  18831  icopnfhmeo  18832  lebnumii  18855  reparphti  18886  itg2const  19492  itg2monolem3  19504  bddibl  19591  dveflem  19723  mvth  19736  dvlipcn  19738  dvivthlem1  19752  dvfsumle  19765  dvfsumabs  19767  dvfsumlem2  19771  plyconst  19985  plyeq0lem  19989  plyco  20020  0dgrb  20025  coefv0  20026  vieta1  20089  aaliou3lem2  20120  tayl0  20138  taylply2  20144  dvtaylp  20146  taylthlem2  20150  radcnvlem1  20189  abelthlem1  20207  abelthlem2  20208  abelthlem3  20209  abelthlem7  20214  abelthlem8  20215  abelthlem9  20216  efper  20247  tangtx  20273  eflogeq  20356  logdivlti  20375  logcnlem4  20396  advlogexp  20406  cxpmul2  20440  dvcxp2  20487  cxpaddle  20496  cxpeq  20501  loglesqr  20502  ang180lem5  20515  isosctrlem2  20523  isosctrlem3  20524  2efiatan  20618  dvatan  20635  leibpi  20642  birthdaylem3  20652  jensenlem2  20686  logdiflbnd  20693  harmonicbnd4  20709  wilthlem2  20712  ftalem5  20719  basellem2  20724  basellem5  20727  basellem8  20730  0sgm  20787  muinv  20838  chpub  20864  logfaclbnd  20866  logexprlim  20869  dchrsum2  20912  sumdchr2  20914  bposlem1  20928  bposlem2  20929  bposlem5  20932  lgsquad2lem1  21002  lgsquad3  21005  2sqlem6  21013  2sqlem8  21016  chtppilim  21029  vmadivsum  21036  dchrisumlem1  21043  dchrisum0flblem1  21062  rpvmasum2  21066  dchrisum0re  21067  dchrisum0lem2a  21071  dchrisum0lem3  21073  rpvmasum  21080  mudivsum  21084  mulogsumlem  21085  vmalogdivsum2  21092  pntrsumo1  21119  pntrlog2bndlem2  21132  pntrlog2bndlem4  21134  pntrlog2bndlem5  21135  pntibndlem2  21145  pntlemc  21149  pntlemf  21159  ostth2lem2  21188  ostth2lem3  21189  ostth2lem4  21190  ostth2  21191  ostth3  21192  nmoub3i  22115  ubthlem2  22214  htthlem  22261  nmcexi  23370  nmopcoadji  23445  branmfn  23449  lgamgulmlem2  24586  lgamcvg2  24611  subfacval2  24645  cvmliftlem2  24745  snmlff  24788  sinccvglem  24881  divelunit  24957  muls1d  24985  fprodsplit  25061  faclimlem1  25113  faclimlem2  25114  faclim2  25118  axpaschlem  25586  axcontlem2  25611  axcontlem4  25613  axcontlem8  25617  fsumcube  25813  itg2addnclem  25950  areacirclem2  25975  areacirclem5  25979  cntotbnd  26189  irrapxlem1  26569  irrapxlem4  26572  pell1qrgaplem  26620  reglogexpbas  26644  rmspecsqrnq  26653  rmspecfund  26656  rmxy1  26669  rmxp1  26679  rmyp1  26680  rmxm1  26681  jm2.17a  26709  jm2.18  26743  jm2.23  26751  jm2.25  26754  jm2.16nn0  26759  expgrowthi  27212  expgrowth  27214  fmul01  27371  fmul01lt1lem1  27375  m1expeven  27386  stoweidlem11  27421  stoweidlem26  27436  stoweidlem38  27448  wallispilem4  27478  stirlinglem1  27484  stirlinglem3  27486  stirlinglem6  27489  stirlinglem7  27490  stirlinglem8  27491  stirlinglem10  27493  stirlinglem12  27495
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361  ax-resscn 8973  ax-1cn 8974  ax-icn 8975  ax-addcl 8976  ax-mulcl 8978  ax-mulcom 8980  ax-mulass 8982  ax-distr 8983  ax-1rid 8986  ax-cnre 8989
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ral 2647  df-rex 2648  df-rab 2651  df-v 2894  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-nul 3565  df-if 3676  df-sn 3756  df-pr 3757  df-op 3759  df-uni 3951  df-br 4147  df-iota 5351  df-fv 5395  df-ov 6016
  Copyright terms: Public domain W3C validator