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

Theorem mulid1d 9097
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 9080 . 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 1652    e. wcel 1725  (class class class)co 6073   CCcc 8980   1c1 8983    x. cmul 8987
This theorem is referenced by:  muladd11  9228  divrec  9686  diveq1  9700  conjmul  9723  modid  11262  expadd  11414  leexp2r  11429  nnlesq  11476  faclbnd  11573  faclbnd2  11574  faclbnd4lem3  11578  faclbnd6  11582  facavg  11584  bcn0  11593  bcn1  11596  hashf1lem2  11697  hashfac  11699  reccn2  12382  iseraltlem2  12468  iseraltlem3  12469  binom11  12603  harmonic  12630  arisum2  12632  trireciplem  12633  geoserg  12637  cvgrat  12652  efzval  12695  tanhlt1  12753  tanaddlem  12759  tanadd  12760  cos01gt0  12784  absef  12790  1dvds  12856  3dvds  12904  bitsfzo  12939  bitsmod  12940  gcdmultiple  13042  sqgcd  13050  coprmdvds  13094  qredeu  13099  phiprmpw  13157  coprimeprodsq  13175  pc2dvds  13244  sumhash  13257  fldivp1  13258  pcfaclem  13259  prmpwdvds  13264  prmreclem1  13276  vdwlem3  13343  vdwlem9  13349  sylow2a  15245  odadd  15457  zsssubrg  16749  zcyg  16764  prmirredlem  16765  mulgrhm2  16780  znrrg  16838  icopnfcnv  18959  icopnfhmeo  18960  lebnumii  18983  reparphti  19014  itg2const  19624  itg2monolem3  19636  bddibl  19723  dveflem  19855  mvth  19868  dvlipcn  19870  dvivthlem1  19884  dvfsumle  19897  dvfsumabs  19899  dvfsumlem2  19903  plyconst  20117  plyeq0lem  20121  plyco  20152  0dgrb  20157  coefv0  20158  vieta1  20221  aaliou3lem2  20252  tayl0  20270  taylply2  20276  dvtaylp  20278  taylthlem2  20282  radcnvlem1  20321  abelthlem1  20339  abelthlem2  20340  abelthlem3  20341  abelthlem7  20346  abelthlem8  20347  abelthlem9  20348  efper  20379  tangtx  20405  eflogeq  20488  logdivlti  20507  logcnlem4  20528  advlogexp  20538  cxpmul2  20572  dvcxp2  20619  cxpaddle  20628  cxpeq  20633  loglesqr  20634  ang180lem5  20647  isosctrlem2  20655  isosctrlem3  20656  2efiatan  20750  dvatan  20767  leibpi  20774  birthdaylem3  20784  jensenlem2  20818  logdiflbnd  20825  harmonicbnd4  20841  wilthlem2  20844  ftalem5  20851  basellem2  20856  basellem5  20859  basellem8  20862  0sgm  20919  muinv  20970  chpub  20996  logfaclbnd  20998  logexprlim  21001  dchrsum2  21044  sumdchr2  21046  bposlem1  21060  bposlem2  21061  bposlem5  21064  lgsquad2lem1  21134  lgsquad3  21137  2sqlem6  21145  2sqlem8  21148  chtppilim  21161  vmadivsum  21168  dchrisumlem1  21175  dchrisum0flblem1  21194  rpvmasum2  21198  dchrisum0re  21199  dchrisum0lem2a  21203  dchrisum0lem3  21205  rpvmasum  21212  mudivsum  21216  mulogsumlem  21217  vmalogdivsum2  21224  pntrsumo1  21251  pntrlog2bndlem2  21264  pntrlog2bndlem4  21266  pntrlog2bndlem5  21267  pntibndlem2  21277  pntlemc  21281  pntlemf  21291  ostth2lem2  21320  ostth2lem3  21321  ostth2lem4  21322  ostth2  21323  ostth3  21324  nmoub3i  22266  ubthlem2  22365  htthlem  22412  nmcexi  23521  nmopcoadji  23596  branmfn  23600  lgamgulmlem2  24806  lgamcvg2  24831  subfacval2  24865  cvmliftlem2  24965  snmlff  25008  sinccvglem  25101  divelunit  25177  muls1d  25205  fprodsplit  25281  faclimlem1  25354  faclimlem2  25355  faclim2  25359  axpaschlem  25871  axcontlem2  25896  axcontlem4  25898  axcontlem8  25902  fsumcube  26098  itg2addnclem  26246  areacirclem2  26282  areacirclem5  26286  cntotbnd  26496  irrapxlem1  26876  irrapxlem4  26879  pell1qrgaplem  26927  reglogexpbas  26951  rmspecsqrnq  26960  rmspecfund  26963  rmxy1  26976  rmxp1  26986  rmyp1  26987  rmxm1  26988  jm2.17a  27016  jm2.18  27050  jm2.23  27058  jm2.25  27061  jm2.16nn0  27066  expgrowthi  27518  expgrowth  27520  fmul01  27677  fmul01lt1lem1  27681  m1expeven  27692  stoweidlem11  27727  stoweidlem26  27742  stoweidlem38  27754  wallispilem4  27784  stirlinglem1  27790  stirlinglem3  27792  stirlinglem6  27795  stirlinglem7  27796  stirlinglem8  27797  stirlinglem10  27799  stirlinglem12  27801
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-resscn 9039  ax-1cn 9040  ax-icn 9041  ax-addcl 9042  ax-mulcl 9044  ax-mulcom 9046  ax-mulass 9048  ax-distr 9049  ax-1rid 9052  ax-cnre 9055
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-iota 5410  df-fv 5454  df-ov 6076
  Copyright terms: Public domain W3C validator