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

Theorem mulid2d 9062
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 9045 . 2  |-  ( A  e.  CC  ->  (
1  x.  A )  =  A )
31, 2syl 16 1  |-  ( ph  ->  ( 1  x.  A
)  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721  (class class class)co 6040   CCcc 8944   1c1 8947    x. cmul 8951
This theorem is referenced by:  addid1  9202  mulcand  9611  receu  9623  divdivdiv  9671  divcan5  9672  subrec  9799  ltrec  9847  recp1lt1  9864  nndivtr  9997  gtndiv  10303  lincmb01cmp  10994  iccf1o  10995  modfrac  11216  m1expcl2  11358  expgt1  11373  ltexp2a  11386  leexp2a  11390  binom3  11455  faclbnd  11536  faclbnd4lem4  11542  facavg  11547  bcval5  11564  sqrlem2  12004  absimle  12069  reccn2  12345  iseraltlem2  12431  iseraltlem3  12432  o1fsum  12547  abscvgcvg  12553  ackbijnn  12562  binom1p  12565  binom1dif  12567  incexclem  12571  incexc  12572  climcndslem1  12584  geomulcvg  12608  efcllem  12635  ef01bndlem  12740  efieq1re  12755  eirrlem  12758  iddvds  12818  bitsfzolem  12901  bitsfzo  12902  rpmulgcd  13010  prmind2  13045  isprm5  13067  phiprm  13121  eulerthlem2  13126  fermltl  13128  odzdvds  13136  pythagtriplem4  13148  pcexp  13188  4sqlem18  13285  vdwapun  13297  mulgnnass  14873  odinv  15152  odadd2  15419  pgpfaclem2  15595  abvneg  15877  nrginvrcnlem  18679  nmoid  18729  blcvx  18782  icopnfcnv  18920  reparphti  18975  pcorevlem  19004  itg11  19536  itg2mulc  19592  itg2monolem1  19595  itgcnlem  19634  iblabs  19673  dvexp  19792  dvef  19817  lhop1lem  19850  dvcvx  19857  dvfsumlem1  19863  dvfsumlem2  19864  dvfsumlem4  19866  dvfsum2  19871  plypow  20077  dgrcolem1  20144  vieta1lem2  20181  radcnvlem1  20282  radcnvlem2  20283  dvradcnv  20290  abelthlem2  20301  abelthlem6  20305  abelthlem7  20307  abelth2  20311  sinhalfpip  20353  sinhalfpim  20354  coshalfpip  20355  coshalfpim  20356  tangtx  20366  efif1olem4  20400  abslogle  20466  logdivlti  20468  advlog  20498  advlogexp  20499  logtayl  20504  cxpaddlelem  20588  cxpaddle  20589  affineequiv  20620  affineequiv2  20621  chordthmlem5  20630  dcubic2  20637  dcubic  20639  mcubic  20640  binom4  20643  dquartlem1  20644  quart1lem  20648  quart1  20649  quartlem1  20650  quart  20654  efiasin  20681  atantayl  20730  cvxcl  20776  scvxcvx  20777  wilthlem1  20804  wilthlem2  20805  basellem9  20824  fsumfldivdiaglem  20927  muinv  20931  chpub  20957  logexprlim  20962  mersenne  20964  perfectlem2  20967  dchrmulid2  20989  dchrptlem1  21001  dchrsum2  21005  sumdchr2  21007  bposlem2  21022  bposlem9  21029  lgsval2lem  21043  lgsval4a  21055  lgsneg1  21057  lgsdir2lem4  21063  lgsdir  21067  lgsdirnn0  21076  lgsdinn0  21077  lgseisenlem1  21086  lgseisenlem2  21087  lgseisenlem4  21089  lgsquad2lem1  21095  2sqlem8  21109  chebbnd1lem3  21118  chpchtlim  21126  rplogsumlem1  21131  rplogsumlem2  21132  rpvmasumlem  21134  dchrmusum2  21141  dchrvmasum2lem  21143  dchrvmasumlem2  21145  dchrvmasumlem3  21146  dchrisum0flblem1  21155  mulog2sumlem2  21182  vmalogdivsum2  21185  2vmadivsumlem  21187  log2sumbnd  21191  selberglem2  21193  chpdifbndlem1  21200  selberg3lem1  21204  selberg4lem1  21207  pntrlog2bndlem2  21225  pntrlog2bndlem5  21228  pntpbnd1  21233  pntpbnd2  21234  pntibndlem2  21238  pntlemb  21244  pntlemr  21249  pntlemk  21253  pntlemo  21254  ablomul  21896  mulid  21897  nvm1  22106  nvpi  22108  nvmtri  22113  ipval2  22156  ipasslem1  22285  ipasslem4  22288  bcs2  22637  lnfnaddi  23499  sqsscirc1  24259  indsum  24373  lgamgulmlem5  24770  lgamcvg2  24792  lgam1  24801  subfacp1lem6  24824  subfaclim  24827  cvxpcon  24882  cvxscon  24883  rescon  24886  sinccvglem  25062  fprodsplit  25242  fallrisefac  25293  brbtwn2  25748  colinearalglem4  25752  ax5seglem3  25774  axbtwnid  25782  axpaschlem  25783  axeuclidlem  25805  axcontlem7  25813  axcontlem8  25814  bpolysum  26003  bpolydiflem  26004  bpoly4  26009  mblfinlem2  26144  itg2addnclem3  26157  iblabsnc  26168  iblmulc2nc  26169  areacirclem2  26181  nn0prpwlem  26215  bfplem2  26422  bfp  26423  rrntotbnd  26435  irrapxlem5  26779  pellexlem2  26783  pellexlem6  26787  pellfundex  26839  jm2.19lem3  26952  jm2.25  26960  jm2.27c  26968  jm3.1lem2  26979  flcidc  27247  hashgcdlem  27384  fmul01lt1lem2  27582  itgsinexp  27616  stoweidlem14  27630  stoweidlem26  27642  wallispilem4  27684  wallispilem5  27685  wallispi2lem1  27687  wallispi2  27689  stirlinglem1  27690  stirlinglem3  27692  stirlinglem4  27693  stirlinglem5  27694  stirlinglem6  27695  stirlinglem7  27696  stirlinglem10  27699
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-mulcl 9008  ax-mulcom 9010  ax-mulass 9012  ax-distr 9013  ax-1rid 9016  ax-cnre 9019
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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043
  Copyright terms: Public domain W3C validator