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

Theorem mulid2d 9612
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 9592 . 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 1381    e. wcel 1802  (class class class)co 6277   CCcc 9488   1c1 9491    x. cmul 9495
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-mulcl 9552  ax-mulcom 9554  ax-mulass 9556  ax-distr 9557  ax-1rid 9560  ax-cnre 9563
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-iota 5537  df-fv 5582  df-ov 6280
This theorem is referenced by:  addid1  9758  mulsubfacd  10017  mulcand  10183  receu  10195  divdivdiv  10246  divcan5  10247  subrec  10374  ltrec  10427  recp1lt1  10444  nndivtr  10578  gtndiv  10941  lincmb01cmp  11667  iccf1o  11668  ltdifltdiv  11940  modfrac  11983  modvalp1  11988  m1expcl2  12162  expgt1  12178  ltexp2a  12191  leexp2a  12195  binom3  12261  faclbnd  12342  faclbnd4lem4  12348  facavg  12353  bcval5  12370  cshweqrep  12763  sqrlem2  13051  absimle  13116  reccn2  13393  iseraltlem2  13479  iseraltlem3  13480  o1fsum  13601  abscvgcvg  13607  ackbijnn  13614  binom1p  13617  binom1dif  13619  incexclem  13622  incexc  13623  climcndslem1  13635  geomulcvg  13659  efcllem  13686  ef01bndlem  13791  efieq1re  13806  eirrlem  13809  iddvds  13869  bitsfzolem  13956  bitsfzo  13957  rpmulgcd  14065  prmind2  14100  isprm5  14125  phiprm  14179  eulerthlem2  14184  fermltl  14186  odzdvds  14194  powm2modprm  14200  modprm0  14202  pythagtriplem4  14215  pcexp  14255  4sqlem18  14352  vdwapun  14364  mulgnnass  16039  odinv  16452  odadd2  16724  pgpfaclem2  17001  abvneg  17351  nrginvrcnlem  21065  nmoid  21115  blcvx  21169  icopnfcnv  21308  reparphti  21363  pcorevlem  21392  itg11  21964  itg2mulc  22020  itg2monolem1  22023  itgcnlem  22062  iblabs  22101  dvexp  22222  dvef  22247  lhop1lem  22280  dvcvx  22287  dvfsumlem1  22293  dvfsumlem2  22294  dvfsumlem4  22296  dvfsum2  22301  plypow  22468  dgrcolem1  22535  vieta1lem2  22572  radcnvlem1  22673  radcnvlem2  22674  dvradcnv  22681  abelthlem2  22692  abelthlem6  22696  abelthlem7  22698  abelth2  22702  sinhalfpip  22750  sinhalfpim  22751  coshalfpip  22752  coshalfpim  22753  tangtx  22763  efif1olem4  22797  abslogle  22868  logdivlti  22870  advlog  22900  advlogexp  22901  logtayl  22906  cxpaddlelem  22990  cxpaddle  22991  affineequiv  23022  affineequiv2  23023  chordthmlem5  23032  dcubic2  23040  dcubic  23042  mcubic  23043  binom4  23046  dquartlem1  23047  quart1lem  23051  quart1  23052  quartlem1  23053  quart  23057  efiasin  23084  atantayl  23133  cvxcl  23179  scvxcvx  23180  wilthlem1  23207  wilthlem2  23208  basellem9  23227  fsumfldivdiaglem  23330  muinv  23334  chpub  23360  logexprlim  23365  mersenne  23367  perfectlem2  23370  dchrmulid2  23392  dchrptlem1  23404  dchrsum2  23408  sumdchr2  23410  bposlem2  23425  bposlem9  23432  lgsval2lem  23446  lgsval4a  23458  lgsneg1  23460  lgsdir2lem4  23466  lgsdir  23470  lgsdirnn0  23479  lgsdinn0  23480  lgseisenlem1  23489  lgseisenlem2  23490  lgseisenlem4  23492  lgsquad2lem1  23498  2sqlem8  23512  chebbnd1lem3  23521  chpchtlim  23529  rplogsumlem1  23534  rplogsumlem2  23535  rpvmasumlem  23537  dchrmusum2  23544  dchrvmasum2lem  23546  dchrvmasumlem2  23548  dchrvmasumlem3  23549  dchrisum0flblem1  23558  mulog2sumlem2  23585  vmalogdivsum2  23588  2vmadivsumlem  23590  log2sumbnd  23594  selberglem2  23596  chpdifbndlem1  23603  selberg3lem1  23607  selberg4lem1  23610  pntrlog2bndlem2  23628  pntrlog2bndlem5  23631  pntpbnd1  23636  pntpbnd2  23637  pntibndlem2  23641  pntlemb  23647  pntlemr  23652  pntlemk  23656  pntlemo  23657  brbtwn2  24073  colinearalglem4  24077  ax5seglem3  24099  axbtwnid  24107  axpaschlem  24108  axeuclidlem  24130  axcontlem7  24138  axcontlem8  24139  ablomul  25222  mulid  25223  nvm1  25432  nvpi  25434  nvmtri  25439  ipval2  25482  ipasslem1  25611  ipasslem4  25614  bcs2  25964  lnfnaddi  26827  sqsscirc1  27756  indsum  27902  eulerpartlemgs2  28185  plymulx0  28370  lgamgulmlem5  28441  lgamcvg2  28463  lgam1  28472  subfacp1lem6  28495  subfaclim  28498  cvxpcon  28553  cvxscon  28554  rescon  28557  sinccvglem  28904  fprodsplit  29063  fallrisefac  29115  bpolysum  29783  bpolydiflem  29784  bpoly4  29789  mblfinlem3  30021  itg2addnclem3  30036  iblabsnc  30047  iblmulc2nc  30048  ftc1anclem6  30063  ftc1anclem7  30064  ftc1anclem8  30065  areacirclem1  30075  nn0prpwlem  30108  bfplem2  30287  bfp  30288  rrntotbnd  30300  irrapxlem5  30730  pellexlem2  30734  pellexlem6  30738  pellfundex  30790  jm2.19lem3  30901  jm2.25  30909  jm2.27c  30917  jm3.1lem2  30928  flcidc  31092  hashgcdlem  31126  cvgdvgrat  31163  adddirp1d  31431  fperiodmullem  31448  fmul01lt1lem2  31503  reclimc  31563  cosknegpi  31572  dvsinax  31608  dvmptdiv  31614  itgsinexp  31639  stoweidlem14  31681  stoweidlem26  31693  wallispilem4  31735  wallispilem5  31736  wallispi2lem1  31738  wallispi2  31740  stirlinglem1  31741  stirlinglem3  31743  stirlinglem4  31744  stirlinglem5  31745  stirlinglem6  31746  stirlinglem7  31747  stirlinglem10  31750  dirkertrigeqlem2  31766  dirkertrigeqlem3  31767  dirkercncflem2  31771  fourierdlem26  31800  fourierdlem41  31815  fourierdlem42  31816  fourierdlem56  31830  fourierdlem57  31831  fourierdlem58  31832  fourierdlem62  31836  fourierdlem64  31838  fourierdlem65  31839  fourierdlem95  31869  sqwvfoura  31896  sqwvfourb  31897  fouriersw  31899  ztprmneprm  32644  altgsumbc  32649  bj-bary1lem1  34382
  Copyright terms: Public domain W3C validator