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

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

Proof of Theorem mulid2d
StepHypRef Expression
1 addcld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 mulid2 9583 . 2  |-  ( A  e.  CC  ->  (
1  x.  A )  =  A )
31, 2syl 16 1  |-  ( ph  ->  ( 1  x.  A
)  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398    e. wcel 1823  (class class class)co 6270   CCcc 9479   1c1 9482    x. cmul 9486
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-mulcl 9543  ax-mulcom 9545  ax-mulass 9547  ax-distr 9548  ax-1rid 9551  ax-cnre 9554
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578  df-ov 6273
This theorem is referenced by:  addid1  9749  mulsubfacd  10012  mulcand  10178  receu  10190  divdivdiv  10241  divcan5  10242  subrec  10369  ltrec  10421  recp1lt1  10438  nndivtr  10573  gtndiv  10936  lincmb01cmp  11666  iccf1o  11667  ltdifltdiv  11948  modfrac  11991  modvalp1  11996  m1expcl2  12170  expgt1  12186  ltexp2a  12199  leexp2a  12203  binom3  12269  faclbnd  12350  faclbnd4lem4  12356  facavg  12361  bcval5  12378  cshweqrep  12780  sqrlem2  13159  absimle  13224  reccn2  13501  iseraltlem2  13587  iseraltlem3  13588  o1fsum  13709  abscvgcvg  13715  ackbijnn  13722  binom1p  13725  binom1dif  13727  incexclem  13730  incexc  13731  climcndslem1  13743  geomulcvg  13767  fprodsplit  13852  efcllem  13895  ef01bndlem  14001  efieq1re  14016  eirrlem  14019  iddvds  14081  bitsfzolem  14168  bitsfzo  14169  rpmulgcd  14277  prmind2  14312  isprm5  14337  phiprm  14391  eulerthlem2  14396  fermltl  14398  odzdvds  14406  powm2modprm  14412  modprm0  14414  pythagtriplem4  14427  pcexp  14467  4sqlem18  14564  vdwapun  14576  mulgnnass  16369  odinv  16782  odadd2  17054  pgpfaclem2  17328  abvneg  17678  nrginvrcnlem  21365  nmoid  21415  blcvx  21469  icopnfcnv  21608  reparphti  21663  pcorevlem  21692  itg11  22264  itg2mulc  22320  itg2monolem1  22323  itgcnlem  22362  iblabs  22401  dvexp  22522  dvef  22547  lhop1lem  22580  dvcvx  22587  dvfsumlem1  22593  dvfsumlem2  22594  dvfsumlem4  22596  dvfsum2  22601  plypow  22768  dgrcolem1  22836  vieta1lem2  22873  radcnvlem1  22974  radcnvlem2  22975  dvradcnv  22982  abelthlem2  22993  abelthlem6  22997  abelthlem7  22999  abelth2  23003  sinhalfpip  23051  sinhalfpim  23052  coshalfpip  23053  coshalfpim  23054  tangtx  23064  efif1olem4  23098  abslogle  23171  logdivlti  23173  advlog  23203  advlogexp  23204  logtayl  23209  cxpaddlelem  23293  cxpaddle  23294  affineequiv  23354  affineequiv2  23355  chordthmlem5  23364  dcubic2  23372  dcubic  23374  mcubic  23375  binom4  23378  dquartlem1  23379  quart1lem  23383  quart1  23384  quartlem1  23385  quart  23389  efiasin  23416  atantayl  23465  cvxcl  23512  scvxcvx  23513  wilthlem1  23540  wilthlem2  23541  basellem9  23560  fsumfldivdiaglem  23663  muinv  23667  chpub  23693  logexprlim  23698  mersenne  23700  perfectlem2  23703  dchrmulid2  23725  dchrptlem1  23737  dchrsum2  23741  sumdchr2  23743  bposlem2  23758  bposlem9  23765  lgsval2lem  23779  lgsval4a  23791  lgsneg1  23793  lgsdir2lem4  23799  lgsdir  23803  lgsdirnn0  23812  lgsdinn0  23813  lgseisenlem1  23822  lgseisenlem2  23823  lgseisenlem4  23825  lgsquad2lem1  23831  2sqlem8  23845  chebbnd1lem3  23854  chpchtlim  23862  rplogsumlem1  23867  rplogsumlem2  23868  rpvmasumlem  23870  dchrmusum2  23877  dchrvmasum2lem  23879  dchrvmasumlem2  23881  dchrvmasumlem3  23882  dchrisum0flblem1  23891  mulog2sumlem2  23918  vmalogdivsum2  23921  2vmadivsumlem  23923  log2sumbnd  23927  selberglem2  23929  chpdifbndlem1  23936  selberg3lem1  23940  selberg4lem1  23943  pntrlog2bndlem2  23961  pntrlog2bndlem5  23964  pntpbnd1  23969  pntpbnd2  23970  pntibndlem2  23974  pntlemb  23980  pntlemr  23985  pntlemk  23989  pntlemo  23990  brbtwn2  24410  colinearalglem4  24414  ax5seglem3  24436  axbtwnid  24444  axpaschlem  24445  axeuclidlem  24467  axcontlem7  24475  axcontlem8  24476  ablomul  25555  mulid  25556  nvm1  25765  nvpi  25767  nvmtri  25772  ipval2  25815  ipasslem1  25944  ipasslem4  25947  bcs2  26297  lnfnaddi  27160  sqsscirc1  28125  indsum  28252  eulerpartlemgs2  28583  plymulx0  28768  lgamgulmlem5  28839  lgamcvg2  28861  lgam1  28870  subfacp1lem6  28893  subfaclim  28896  cvxpcon  28951  cvxscon  28952  rescon  28955  sinccvglem  29302  fallrisefac  29388  bpolysum  30043  bpolydiflem  30044  bpoly4  30049  mblfinlem3  30293  itg2addnclem3  30308  iblabsnc  30319  iblmulc2nc  30320  ftc1anclem6  30335  ftc1anclem7  30336  ftc1anclem8  30337  areacirclem1  30347  nn0prpwlem  30380  bfplem2  30559  bfp  30560  rrntotbnd  30572  irrapxlem5  31001  pellexlem2  31005  pellexlem6  31009  pellfundex  31061  jm2.19lem3  31172  jm2.25  31180  jm2.27c  31188  jm3.1lem2  31199  flcidc  31364  hashgcdlem  31398  cvgdvgrat  31435  bccn1  31490  binomcxplemnotnn0  31502  adddirp1d  31726  fperiodmullem  31742  fmul01lt1lem2  31818  mccllem  31844  reclimc  31898  cosknegpi  31908  dvsinax  31947  dvmptdiv  31953  dvnxpaek  31978  dvnmul  31979  itgsinexp  31992  stoweidlem14  32035  stoweidlem26  32047  wallispilem4  32089  wallispilem5  32090  wallispi2lem1  32092  wallispi2  32094  stirlinglem1  32095  stirlinglem3  32097  stirlinglem4  32098  stirlinglem5  32099  stirlinglem6  32100  stirlinglem7  32101  stirlinglem10  32104  dirkertrigeqlem2  32120  dirkertrigeqlem3  32121  dirkercncflem2  32125  fourierdlem26  32154  fourierdlem41  32169  fourierdlem42  32170  fourierdlem56  32184  fourierdlem57  32185  fourierdlem58  32186  fourierdlem62  32190  fourierdlem64  32192  fourierdlem65  32193  fourierdlem95  32223  sqwvfoura  32250  sqwvfourb  32251  fouriersw  32253  etransclem23  32279  etransclem35  32291  etransclem46  32302  xp1d2m1eqxm1d2  32532  ztprmneprm  33190  altgsumbc  33195  divge1b  33370  divgt1b  33371  bj-bary1lem1  35077  int-mul12d  38456
  Copyright terms: Public domain W3C validator