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

Theorem mulid2d 9098
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 9081 . 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 1652    e. wcel 1725  (class class class)co 6073   CCcc 8980   1c1 8983    x. cmul 8987
This theorem is referenced by:  addid1  9238  mulcand  9647  receu  9659  divdivdiv  9707  divcan5  9708  subrec  9835  ltrec  9883  recp1lt1  9900  nndivtr  10033  gtndiv  10339  lincmb01cmp  11030  iccf1o  11031  modfrac  11253  m1expcl2  11395  expgt1  11410  ltexp2a  11423  leexp2a  11427  binom3  11492  faclbnd  11573  faclbnd4lem4  11579  facavg  11584  bcval5  11601  sqrlem2  12041  absimle  12106  reccn2  12382  iseraltlem2  12468  iseraltlem3  12469  o1fsum  12584  abscvgcvg  12590  ackbijnn  12599  binom1p  12602  binom1dif  12604  incexclem  12608  incexc  12609  climcndslem1  12621  geomulcvg  12645  efcllem  12672  ef01bndlem  12777  efieq1re  12792  eirrlem  12795  iddvds  12855  bitsfzolem  12938  bitsfzo  12939  rpmulgcd  13047  prmind2  13082  isprm5  13104  phiprm  13158  eulerthlem2  13163  fermltl  13165  odzdvds  13173  pythagtriplem4  13185  pcexp  13225  4sqlem18  13322  vdwapun  13334  mulgnnass  14910  odinv  15189  odadd2  15456  pgpfaclem2  15632  abvneg  15914  nrginvrcnlem  18718  nmoid  18768  blcvx  18821  icopnfcnv  18959  reparphti  19014  pcorevlem  19043  itg11  19575  itg2mulc  19631  itg2monolem1  19634  itgcnlem  19673  iblabs  19712  dvexp  19831  dvef  19856  lhop1lem  19889  dvcvx  19896  dvfsumlem1  19902  dvfsumlem2  19903  dvfsumlem4  19905  dvfsum2  19910  plypow  20116  dgrcolem1  20183  vieta1lem2  20220  radcnvlem1  20321  radcnvlem2  20322  dvradcnv  20329  abelthlem2  20340  abelthlem6  20344  abelthlem7  20346  abelth2  20350  sinhalfpip  20392  sinhalfpim  20393  coshalfpip  20394  coshalfpim  20395  tangtx  20405  efif1olem4  20439  abslogle  20505  logdivlti  20507  advlog  20537  advlogexp  20538  logtayl  20543  cxpaddlelem  20627  cxpaddle  20628  affineequiv  20659  affineequiv2  20660  chordthmlem5  20669  dcubic2  20676  dcubic  20678  mcubic  20679  binom4  20682  dquartlem1  20683  quart1lem  20687  quart1  20688  quartlem1  20689  quart  20693  efiasin  20720  atantayl  20769  cvxcl  20815  scvxcvx  20816  wilthlem1  20843  wilthlem2  20844  basellem9  20863  fsumfldivdiaglem  20966  muinv  20970  chpub  20996  logexprlim  21001  mersenne  21003  perfectlem2  21006  dchrmulid2  21028  dchrptlem1  21040  dchrsum2  21044  sumdchr2  21046  bposlem2  21061  bposlem9  21068  lgsval2lem  21082  lgsval4a  21094  lgsneg1  21096  lgsdir2lem4  21102  lgsdir  21106  lgsdirnn0  21115  lgsdinn0  21116  lgseisenlem1  21125  lgseisenlem2  21126  lgseisenlem4  21128  lgsquad2lem1  21134  2sqlem8  21148  chebbnd1lem3  21157  chpchtlim  21165  rplogsumlem1  21170  rplogsumlem2  21171  rpvmasumlem  21173  dchrmusum2  21180  dchrvmasum2lem  21182  dchrvmasumlem2  21184  dchrvmasumlem3  21185  dchrisum0flblem1  21194  mulog2sumlem2  21221  vmalogdivsum2  21224  2vmadivsumlem  21226  log2sumbnd  21230  selberglem2  21232  chpdifbndlem1  21239  selberg3lem1  21243  selberg4lem1  21246  pntrlog2bndlem2  21264  pntrlog2bndlem5  21267  pntpbnd1  21272  pntpbnd2  21273  pntibndlem2  21277  pntlemb  21283  pntlemr  21288  pntlemk  21292  pntlemo  21293  ablomul  21935  mulid  21936  nvm1  22145  nvpi  22147  nvmtri  22152  ipval2  22195  ipasslem1  22324  ipasslem4  22327  bcs2  22676  lnfnaddi  23538  sqsscirc1  24298  indsum  24412  lgamgulmlem5  24809  lgamcvg2  24831  lgam1  24840  subfacp1lem6  24863  subfaclim  24866  cvxpcon  24921  cvxscon  24922  rescon  24925  sinccvglem  25101  fprodsplit  25281  fallrisefac  25333  brbtwn2  25836  colinearalglem4  25840  ax5seglem3  25862  axbtwnid  25870  axpaschlem  25871  axeuclidlem  25893  axcontlem7  25901  axcontlem8  25902  bpolysum  26091  bpolydiflem  26092  bpoly4  26097  mblfinlem2  26235  itg2addnclem3  26248  iblabsnc  26259  iblmulc2nc  26260  ftc1anclem6  26275  ftc1anclem7  26276  ftc1anclem8  26277  areacirclem2  26282  nn0prpwlem  26316  bfplem2  26523  bfp  26524  rrntotbnd  26536  irrapxlem5  26880  pellexlem2  26884  pellexlem6  26888  pellfundex  26940  jm2.19lem3  27053  jm2.25  27061  jm2.27c  27069  jm3.1lem2  27080  flcidc  27347  hashgcdlem  27484  fmul01lt1lem2  27682  itgsinexp  27716  stoweidlem14  27730  stoweidlem26  27742  wallispilem4  27784  wallispilem5  27785  wallispi2lem1  27787  wallispi2  27789  stirlinglem1  27790  stirlinglem3  27792  stirlinglem4  27793  stirlinglem5  27794  stirlinglem6  27795  stirlinglem7  27796  stirlinglem10  27799  ltdifltdiv  28126  modvalp1  28129  modprm0  28194  cshweqrep  28237
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