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

Theorem mulid2d 9111
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 9094 . 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 1653    e. wcel 1726  (class class class)co 6084   CCcc 8993   1c1 8996    x. cmul 9000
This theorem is referenced by:  addid1  9251  mulcand  9660  receu  9672  divdivdiv  9720  divcan5  9721  subrec  9848  ltrec  9896  recp1lt1  9913  nndivtr  10046  gtndiv  10352  lincmb01cmp  11043  iccf1o  11044  modfrac  11266  m1expcl2  11408  expgt1  11423  ltexp2a  11436  leexp2a  11440  binom3  11505  faclbnd  11586  faclbnd4lem4  11592  facavg  11597  bcval5  11614  sqrlem2  12054  absimle  12119  reccn2  12395  iseraltlem2  12481  iseraltlem3  12482  o1fsum  12597  abscvgcvg  12603  ackbijnn  12612  binom1p  12615  binom1dif  12617  incexclem  12621  incexc  12622  climcndslem1  12634  geomulcvg  12658  efcllem  12685  ef01bndlem  12790  efieq1re  12805  eirrlem  12808  iddvds  12868  bitsfzolem  12951  bitsfzo  12952  rpmulgcd  13060  prmind2  13095  isprm5  13117  phiprm  13171  eulerthlem2  13176  fermltl  13178  odzdvds  13186  pythagtriplem4  13198  pcexp  13238  4sqlem18  13335  vdwapun  13347  mulgnnass  14923  odinv  15202  odadd2  15469  pgpfaclem2  15645  abvneg  15927  nrginvrcnlem  18731  nmoid  18781  blcvx  18834  icopnfcnv  18972  reparphti  19027  pcorevlem  19056  itg11  19586  itg2mulc  19642  itg2monolem1  19645  itgcnlem  19684  iblabs  19723  dvexp  19844  dvef  19869  lhop1lem  19902  dvcvx  19909  dvfsumlem1  19915  dvfsumlem2  19916  dvfsumlem4  19918  dvfsum2  19923  plypow  20129  dgrcolem1  20196  vieta1lem2  20233  radcnvlem1  20334  radcnvlem2  20335  dvradcnv  20342  abelthlem2  20353  abelthlem6  20357  abelthlem7  20359  abelth2  20363  sinhalfpip  20405  sinhalfpim  20406  coshalfpip  20407  coshalfpim  20408  tangtx  20418  efif1olem4  20452  abslogle  20518  logdivlti  20520  advlog  20550  advlogexp  20551  logtayl  20556  cxpaddlelem  20640  cxpaddle  20641  affineequiv  20672  affineequiv2  20673  chordthmlem5  20682  dcubic2  20689  dcubic  20691  mcubic  20692  binom4  20695  dquartlem1  20696  quart1lem  20700  quart1  20701  quartlem1  20702  quart  20706  efiasin  20733  atantayl  20782  cvxcl  20828  scvxcvx  20829  wilthlem1  20856  wilthlem2  20857  basellem9  20876  fsumfldivdiaglem  20979  muinv  20983  chpub  21009  logexprlim  21014  mersenne  21016  perfectlem2  21019  dchrmulid2  21041  dchrptlem1  21053  dchrsum2  21057  sumdchr2  21059  bposlem2  21074  bposlem9  21081  lgsval2lem  21095  lgsval4a  21107  lgsneg1  21109  lgsdir2lem4  21115  lgsdir  21119  lgsdirnn0  21128  lgsdinn0  21129  lgseisenlem1  21138  lgseisenlem2  21139  lgseisenlem4  21141  lgsquad2lem1  21147  2sqlem8  21161  chebbnd1lem3  21170  chpchtlim  21178  rplogsumlem1  21183  rplogsumlem2  21184  rpvmasumlem  21186  dchrmusum2  21193  dchrvmasum2lem  21195  dchrvmasumlem2  21197  dchrvmasumlem3  21198  dchrisum0flblem1  21207  mulog2sumlem2  21234  vmalogdivsum2  21237  2vmadivsumlem  21239  log2sumbnd  21243  selberglem2  21245  chpdifbndlem1  21252  selberg3lem1  21256  selberg4lem1  21259  pntrlog2bndlem2  21277  pntrlog2bndlem5  21280  pntpbnd1  21285  pntpbnd2  21286  pntibndlem2  21290  pntlemb  21296  pntlemr  21301  pntlemk  21305  pntlemo  21306  ablomul  21948  mulid  21949  nvm1  22158  nvpi  22160  nvmtri  22165  ipval2  22208  ipasslem1  22337  ipasslem4  22340  bcs2  22689  lnfnaddi  23551  sqsscirc1  24311  indsum  24425  lgamgulmlem5  24822  lgamcvg2  24844  lgam1  24853  subfacp1lem6  24876  subfaclim  24879  cvxpcon  24934  cvxscon  24935  rescon  24938  sinccvglem  25114  fprodsplit  25294  fallrisefac  25346  brbtwn2  25849  colinearalglem4  25853  ax5seglem3  25875  axbtwnid  25883  axpaschlem  25884  axeuclidlem  25906  axcontlem7  25914  axcontlem8  25915  bpolysum  26104  bpolydiflem  26105  bpoly4  26110  mblfinlem3  26257  itg2addnclem3  26272  iblabsnc  26283  iblmulc2nc  26284  ftc1anclem6  26299  ftc1anclem7  26300  ftc1anclem8  26301  areacirclem1  26306  nn0prpwlem  26339  bfplem2  26546  bfp  26547  rrntotbnd  26559  irrapxlem5  26903  pellexlem2  26907  pellexlem6  26911  pellfundex  26963  jm2.19lem3  27076  jm2.25  27084  jm2.27c  27092  jm3.1lem2  27103  flcidc  27370  hashgcdlem  27507  fmul01lt1lem2  27705  itgsinexp  27739  stoweidlem14  27753  stoweidlem26  27765  wallispilem4  27807  wallispilem5  27808  wallispi2lem1  27810  wallispi2  27812  stirlinglem1  27813  stirlinglem3  27815  stirlinglem4  27816  stirlinglem5  27817  stirlinglem6  27818  stirlinglem7  27819  stirlinglem10  27822  ltdifltdiv  28171  modvalp1  28174  modprm0  28262  cshweqrep  28308
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-resscn 9052  ax-1cn 9053  ax-icn 9054  ax-addcl 9055  ax-mulcl 9057  ax-mulcom 9059  ax-mulass 9061  ax-distr 9062  ax-1rid 9065  ax-cnre 9068
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-iota 5421  df-fv 5465  df-ov 6087
  Copyright terms: Public domain W3C validator