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

Theorem mulid2d 9603
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 9583 . 2  |-  ( A  e.  CC  ->  (
1  x.  A )  =  A )
31, 2syl 16 1  |-  ( ph  ->  ( 1  x.  A
)  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1374    e. wcel 1762  (class class class)co 6275   CCcc 9479   1c1 9482    x. cmul 9486
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-mulcl 9543  ax-mulcom 9545  ax-mulass 9547  ax-distr 9548  ax-1rid 9551  ax-cnre 9554
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-iota 5542  df-fv 5587  df-ov 6278
This theorem is referenced by:  addid1  9748  mulsubfacd  10005  mulcand  10171  receu  10183  divdivdiv  10234  divcan5  10235  subrec  10362  ltrec  10415  recp1lt1  10432  nndivtr  10566  gtndiv  10927  lincmb01cmp  11652  iccf1o  11653  ltdifltdiv  11922  modfrac  11965  modvalp1  11970  m1expcl2  12144  expgt1  12159  ltexp2a  12172  leexp2a  12176  binom3  12242  faclbnd  12323  faclbnd4lem4  12329  facavg  12334  bcval5  12351  cshweqrep  12739  sqrlem2  13027  absimle  13092  reccn2  13368  iseraltlem2  13454  iseraltlem3  13455  o1fsum  13576  abscvgcvg  13582  ackbijnn  13592  binom1p  13595  binom1dif  13597  incexclem  13600  incexc  13601  climcndslem1  13613  geomulcvg  13637  efcllem  13664  ef01bndlem  13769  efieq1re  13784  eirrlem  13787  iddvds  13847  bitsfzolem  13932  bitsfzo  13933  rpmulgcd  14041  prmind2  14076  isprm5  14101  phiprm  14155  eulerthlem2  14160  fermltl  14162  odzdvds  14170  powm2modprm  14176  modprm0  14178  pythagtriplem4  14191  pcexp  14231  4sqlem18  14328  vdwapun  14340  mulgnnass  15963  odinv  16372  odadd2  16641  pgpfaclem2  16916  abvneg  17259  nrginvrcnlem  20927  nmoid  20977  blcvx  21031  icopnfcnv  21170  reparphti  21225  pcorevlem  21254  itg11  21826  itg2mulc  21882  itg2monolem1  21885  itgcnlem  21924  iblabs  21963  dvexp  22084  dvef  22109  lhop1lem  22142  dvcvx  22149  dvfsumlem1  22155  dvfsumlem2  22156  dvfsumlem4  22158  dvfsum2  22163  plypow  22330  dgrcolem1  22397  vieta1lem2  22434  radcnvlem1  22535  radcnvlem2  22536  dvradcnv  22543  abelthlem2  22554  abelthlem6  22558  abelthlem7  22560  abelth2  22564  sinhalfpip  22611  sinhalfpim  22612  coshalfpip  22613  coshalfpim  22614  tangtx  22624  efif1olem4  22658  abslogle  22724  logdivlti  22726  advlog  22756  advlogexp  22757  logtayl  22762  cxpaddlelem  22846  cxpaddle  22847  affineequiv  22878  affineequiv2  22879  chordthmlem5  22888  dcubic2  22896  dcubic  22898  mcubic  22899  binom4  22902  dquartlem1  22903  quart1lem  22907  quart1  22908  quartlem1  22909  quart  22913  efiasin  22940  atantayl  22989  cvxcl  23035  scvxcvx  23036  wilthlem1  23063  wilthlem2  23064  basellem9  23083  fsumfldivdiaglem  23186  muinv  23190  chpub  23216  logexprlim  23221  mersenne  23223  perfectlem2  23226  dchrmulid2  23248  dchrptlem1  23260  dchrsum2  23264  sumdchr2  23266  bposlem2  23281  bposlem9  23288  lgsval2lem  23302  lgsval4a  23314  lgsneg1  23316  lgsdir2lem4  23322  lgsdir  23326  lgsdirnn0  23335  lgsdinn0  23336  lgseisenlem1  23345  lgseisenlem2  23346  lgseisenlem4  23348  lgsquad2lem1  23354  2sqlem8  23368  chebbnd1lem3  23377  chpchtlim  23385  rplogsumlem1  23390  rplogsumlem2  23391  rpvmasumlem  23393  dchrmusum2  23400  dchrvmasum2lem  23402  dchrvmasumlem2  23404  dchrvmasumlem3  23405  dchrisum0flblem1  23414  mulog2sumlem2  23441  vmalogdivsum2  23444  2vmadivsumlem  23446  log2sumbnd  23450  selberglem2  23452  chpdifbndlem1  23459  selberg3lem1  23463  selberg4lem1  23466  pntrlog2bndlem2  23484  pntrlog2bndlem5  23487  pntpbnd1  23492  pntpbnd2  23493  pntibndlem2  23497  pntlemb  23503  pntlemr  23508  pntlemk  23512  pntlemo  23513  brbtwn2  23877  colinearalglem4  23881  ax5seglem3  23903  axbtwnid  23911  axpaschlem  23912  axeuclidlem  23934  axcontlem7  23942  axcontlem8  23943  ablomul  24883  mulid  24884  nvm1  25093  nvpi  25095  nvmtri  25100  ipval2  25143  ipasslem1  25272  ipasslem4  25275  bcs2  25625  lnfnaddi  26488  sqsscirc1  27376  indsum  27526  eulerpartlemgs2  27809  plymulx0  27994  lgamgulmlem5  28065  lgamcvg2  28087  lgam1  28096  subfacp1lem6  28119  subfaclim  28122  cvxpcon  28177  cvxscon  28178  rescon  28181  sinccvglem  28363  fprodsplit  28522  fallrisefac  28574  bpolysum  29242  bpolydiflem  29243  bpoly4  29248  mblfinlem3  29481  itg2addnclem3  29496  iblabsnc  29507  iblmulc2nc  29508  ftc1anclem6  29523  ftc1anclem7  29524  ftc1anclem8  29525  areacirclem1  29535  nn0prpwlem  29568  bfplem2  29773  bfp  29774  rrntotbnd  29786  irrapxlem5  30217  pellexlem2  30221  pellexlem6  30225  pellfundex  30277  jm2.19lem3  30390  jm2.25  30398  jm2.27c  30406  jm3.1lem2  30417  flcidc  30581  hashgcdlem  30615  adddirp1d  30882  fperiodmullem  30899  fmul01lt1lem2  30954  reclimc  31014  cosknegpi  31024  dvsinax  31060  dvmptdiv  31066  itgsinexp  31091  stoweidlem14  31133  stoweidlem26  31145  wallispilem4  31187  wallispilem5  31188  wallispi2lem1  31190  wallispi2  31192  stirlinglem1  31193  stirlinglem3  31195  stirlinglem4  31196  stirlinglem5  31197  stirlinglem6  31198  stirlinglem7  31199  stirlinglem10  31202  dirkertrigeqlem2  31218  dirkertrigeqlem3  31219  dirkercncflem2  31223  fourierdlem26  31252  fourierdlem41  31267  fourierdlem42  31268  fourierdlem48  31274  fourierdlem56  31282  fourierdlem57  31283  fourierdlem58  31284  fourierdlem62  31288  fourierdlem64  31290  fourierdlem65  31291  fourierdlem95  31321  sqwvfoura  31348  sqwvfourb  31349  fouriersw  31351  ztprmneprm  31875  altgsumbc  31880  bj-bary1lem1  33627
  Copyright terms: Public domain W3C validator