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

Theorem mulid2d 9040
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 9023 . 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 1717  (class class class)co 6021   CCcc 8922   1c1 8925    x. cmul 8929
This theorem is referenced by:  addid1  9179  mulcand  9588  receu  9600  divdivdiv  9648  divcan5  9649  subrec  9776  ltrec  9824  recp1lt1  9841  nndivtr  9974  gtndiv  10280  lincmb01cmp  10971  iccf1o  10972  modfrac  11189  m1expcl2  11331  expgt1  11346  ltexp2a  11359  leexp2a  11363  binom3  11428  faclbnd  11509  faclbnd4lem4  11515  facavg  11520  bcval5  11537  sqrlem2  11977  absimle  12042  reccn2  12318  iseraltlem2  12404  iseraltlem3  12405  o1fsum  12520  abscvgcvg  12526  ackbijnn  12535  binom1p  12538  binom1dif  12540  incexclem  12544  incexc  12545  climcndslem1  12557  geomulcvg  12581  efcllem  12608  ef01bndlem  12713  efieq1re  12728  eirrlem  12731  iddvds  12791  bitsfzolem  12874  bitsfzo  12875  rpmulgcd  12983  prmind2  13018  isprm5  13040  phiprm  13094  eulerthlem2  13099  fermltl  13101  odzdvds  13109  pythagtriplem4  13121  pcexp  13161  4sqlem18  13258  vdwapun  13270  mulgnnass  14846  odinv  15125  odadd2  15392  pgpfaclem2  15568  abvneg  15850  nrginvrcnlem  18598  nmoid  18648  blcvx  18701  icopnfcnv  18839  reparphti  18894  pcorevlem  18923  itg11  19451  itg2mulc  19507  itg2monolem1  19510  itgcnlem  19549  iblabs  19588  dvexp  19707  dvef  19732  lhop1lem  19765  dvcvx  19772  dvfsumlem1  19778  dvfsumlem2  19779  dvfsumlem4  19781  dvfsum2  19786  plypow  19992  dgrcolem1  20059  vieta1lem2  20096  radcnvlem1  20197  radcnvlem2  20198  dvradcnv  20205  abelthlem2  20216  abelthlem6  20220  abelthlem7  20222  abelth2  20226  sinhalfpip  20268  sinhalfpim  20269  coshalfpip  20270  coshalfpim  20271  tangtx  20281  efif1olem4  20315  abslogle  20381  logdivlti  20383  advlog  20413  advlogexp  20414  logtayl  20419  cxpaddlelem  20503  cxpaddle  20504  affineequiv  20535  affineequiv2  20536  chordthmlem5  20545  dcubic2  20552  dcubic  20554  mcubic  20555  binom4  20558  dquartlem1  20559  quart1lem  20563  quart1  20564  quartlem1  20565  quart  20569  efiasin  20596  atantayl  20645  cvxcl  20691  scvxcvx  20692  wilthlem1  20719  wilthlem2  20720  basellem9  20739  fsumfldivdiaglem  20842  muinv  20846  chpub  20872  logexprlim  20877  mersenne  20879  perfectlem2  20882  dchrmulid2  20904  dchrptlem1  20916  dchrsum2  20920  sumdchr2  20922  bposlem2  20937  bposlem9  20944  lgsval2lem  20958  lgsval4a  20970  lgsneg1  20972  lgsdir2lem4  20978  lgsdir  20982  lgsdirnn0  20991  lgsdinn0  20992  lgseisenlem1  21001  lgseisenlem2  21002  lgseisenlem4  21004  lgsquad2lem1  21010  2sqlem8  21024  chebbnd1lem3  21033  chpchtlim  21041  rplogsumlem1  21046  rplogsumlem2  21047  rpvmasumlem  21049  dchrmusum2  21056  dchrvmasum2lem  21058  dchrvmasumlem2  21060  dchrvmasumlem3  21061  dchrisum0flblem1  21070  mulog2sumlem2  21097  vmalogdivsum2  21100  2vmadivsumlem  21102  log2sumbnd  21106  selberglem2  21108  chpdifbndlem1  21115  selberg3lem1  21119  selberg4lem1  21122  pntrlog2bndlem2  21140  pntrlog2bndlem5  21143  pntpbnd1  21148  pntpbnd2  21149  pntibndlem2  21153  pntlemb  21159  pntlemr  21164  pntlemk  21168  pntlemo  21169  ablomul  21792  mulid  21793  nvm1  22002  nvpi  22004  nvmtri  22009  ipval2  22052  ipasslem1  22181  ipasslem4  22184  bcs2  22533  lnfnaddi  23395  sqsscirc1  24111  indsum  24217  lgamgulmlem5  24597  lgamcvg2  24619  lgam1  24628  subfacp1lem6  24651  subfaclim  24654  cvxpcon  24709  cvxscon  24710  rescon  24713  sinccvglem  24889  fprodsplit  25069  fallrisefac  25110  brbtwn2  25559  colinearalglem4  25563  ax5seglem3  25585  axbtwnid  25593  axpaschlem  25594  axeuclidlem  25616  axcontlem7  25624  axcontlem8  25625  bpolysum  25814  bpolydiflem  25815  bpoly4  25820  itg2addnc  25960  iblabsnc  25970  iblmulc2nc  25971  areacirclem2  25983  nn0prpwlem  26017  bfplem2  26224  bfp  26225  rrntotbnd  26237  irrapxlem5  26581  pellexlem2  26585  pellexlem6  26589  pellfundex  26641  jm2.19lem3  26754  jm2.25  26762  jm2.27c  26770  jm3.1lem2  26781  flcidc  27049  hashgcdlem  27186  fmul01lt1lem2  27384  itgsinexp  27418  stoweidlem14  27432  stoweidlem26  27444  wallispilem4  27486  wallispilem5  27487  wallispi2lem1  27489  wallispi2  27491  stirlinglem1  27492  stirlinglem3  27494  stirlinglem4  27495  stirlinglem5  27496  stirlinglem6  27497  stirlinglem7  27498  stirlinglem10  27501
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-resscn 8981  ax-1cn 8982  ax-icn 8983  ax-addcl 8984  ax-mulcl 8986  ax-mulcom 8988  ax-mulass 8990  ax-distr 8991  ax-1rid 8994  ax-cnre 8997
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 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ral 2655  df-rex 2656  df-rab 2659  df-v 2902  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-sn 3764  df-pr 3765  df-op 3767  df-uni 3959  df-br 4155  df-iota 5359  df-fv 5403  df-ov 6024
  Copyright terms: Public domain W3C validator