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

Theorem mulid2d 8869
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 8852 . 2  |-  ( A  e.  CC  ->  (
1  x.  A )  =  A )
31, 2syl 15 1  |-  ( ph  ->  ( 1  x.  A
)  =  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:  addid1  9008  mulcand  9417  receu  9429  divdivdiv  9477  divcan5  9478  subrec  9605  ltrec  9653  recp1lt1  9670  nndivtr  9803  gtndiv  10105  lincmb01cmp  10793  iccf1o  10794  modfrac  11000  m1expcl2  11141  expgt1  11156  ltexp2a  11169  leexp2a  11173  binom3  11238  faclbnd  11319  faclbnd4lem4  11325  facavg  11330  bcval5  11346  sqrlem2  11745  absimle  11810  reccn2  12086  iseraltlem2  12171  iseraltlem3  12172  o1fsum  12287  abscvgcvg  12293  ackbijnn  12302  binom1p  12305  binom1dif  12307  incexclem  12311  incexc  12312  climcndslem1  12324  geomulcvg  12348  efcllem  12375  ef01bndlem  12480  efieq1re  12495  eirrlem  12498  iddvds  12558  bitsfzolem  12641  bitsfzo  12642  rpmulgcd  12750  prmind2  12785  isprm5  12807  phiprm  12861  eulerthlem2  12866  fermltl  12868  odzdvds  12876  pythagtriplem4  12888  pcexp  12928  4sqlem18  13025  vdwapun  13037  mulgnnass  14611  odinv  14890  odadd2  15157  pgpfaclem2  15333  abvneg  15615  nrginvrcnlem  18217  nmoid  18267  blcvx  18320  icopnfcnv  18456  reparphti  18511  pcorevlem  18540  itg11  19062  itg2mulc  19118  itg2monolem1  19121  itgcnlem  19160  iblabs  19199  dvexp  19318  dvef  19343  lhop1lem  19376  dvcvx  19383  dvfsumlem1  19389  dvfsumlem2  19390  dvfsumlem4  19392  dvfsum2  19397  plypow  19603  dgrcolem1  19670  vieta1lem2  19707  radcnvlem1  19805  radcnvlem2  19806  dvradcnv  19813  abelthlem2  19824  abelthlem6  19828  abelthlem7  19830  abelth2  19834  sinhalfpip  19876  sinhalfpim  19877  coshalfpip  19878  coshalfpim  19879  tangtx  19889  efif1olem4  19923  logdivlti  19987  advlog  20017  advlogexp  20018  logtayl  20023  cxpaddlelem  20107  cxpaddle  20108  affineequiv  20139  affineequiv2  20140  chordthmlem5  20149  dcubic2  20156  dcubic  20158  mcubic  20159  binom4  20162  dquartlem1  20163  quart1lem  20167  quart1  20168  quartlem1  20169  quart  20173  efiasin  20200  atantayl  20249  cvxcl  20295  scvxcvx  20296  wilthlem1  20322  wilthlem2  20323  basellem9  20342  fsumfldivdiaglem  20445  muinv  20449  chpub  20475  logexprlim  20480  mersenne  20482  perfectlem2  20485  dchrmulid2  20507  dchrptlem1  20519  dchrsum2  20523  sumdchr2  20525  bposlem2  20540  bposlem9  20547  lgsval2lem  20561  lgsval4a  20573  lgsneg1  20575  lgsdir2lem4  20581  lgsdir  20585  lgsdirnn0  20594  lgsdinn0  20595  lgseisenlem1  20604  lgseisenlem2  20605  lgseisenlem4  20607  lgsquad2lem1  20613  2sqlem8  20627  chebbnd1lem3  20636  chpchtlim  20644  rplogsumlem1  20649  rplogsumlem2  20650  rpvmasumlem  20652  dchrmusum2  20659  dchrvmasum2lem  20661  dchrvmasumlem2  20663  dchrvmasumlem3  20664  dchrisum0flblem1  20673  mulog2sumlem2  20700  vmalogdivsum2  20703  2vmadivsumlem  20705  log2sumbnd  20709  selberglem2  20711  chpdifbndlem1  20718  selberg3lem1  20722  selberg4lem1  20725  pntrlog2bndlem2  20743  pntrlog2bndlem5  20746  pntpbnd1  20751  pntpbnd2  20752  pntibndlem2  20756  pntlemb  20762  pntlemr  20767  pntlemk  20771  pntlemo  20772  ablomul  21038  mulid  21039  nvm1  21246  nvpi  21248  nvmtri  21253  ipval2  21296  ipasslem1  21425  ipasslem4  21428  bcs2  21777  lnfnaddi  22639  sqsscirc1  23307  indsum  23621  subfacp1lem6  23731  subfaclim  23734  cvxpcon  23788  cvxscon  23789  rescon  23792  sinccvglem  24020  brbtwn2  24605  colinearalglem4  24609  ax5seglem3  24631  axbtwnid  24639  axpaschlem  24640  axeuclidlem  24662  axcontlem7  24670  axcontlem8  24671  bpolysum  24860  bpolydiflem  24861  bpoly4  24866  itg2addnc  25005  iblabsnc  25015  iblmulc2nc  25016  areacirclem2  25028  mulone  25788  nn0prpwlem  26341  bfplem2  26650  bfp  26651  rrntotbnd  26663  irrapxlem5  27014  pellexlem2  27018  pellexlem6  27022  pellfundex  27074  jm2.19lem3  27187  jm2.25  27195  jm2.27c  27203  jm3.1lem2  27214  flcidc  27482  hashgcdlem  27619  itgsinexp  27852  wallispilem5  27921  wallispi2lem1  27923  wallispi2  27925  stirlinglem1  27926  stirlinglem3  27928  stirlinglem4  27929  stirlinglem5  27930  stirlinglem6  27931  stirlinglem7  27932  stirlinglem10  27935
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