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

Theorem mulid2d 9660
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 9640 . 2  |-  ( A  e.  CC  ->  (
1  x.  A )  =  A )
31, 2syl 17 1  |-  ( ph  ->  ( 1  x.  A
)  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1870  (class class class)co 6305   CCcc 9536   1c1 9539    x. cmul 9543
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-resscn 9595  ax-1cn 9596  ax-icn 9597  ax-addcl 9598  ax-mulcl 9600  ax-mulcom 9602  ax-mulass 9604  ax-distr 9605  ax-1rid 9608  ax-cnre 9611
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-iota 5565  df-fv 5609  df-ov 6308
This theorem is referenced by:  addid1  9812  mulsubfacd  10077  mulcand  10244  receu  10256  divdivdiv  10307  divcan5  10308  subrec  10435  ltrec  10487  recp1lt1  10504  nndivtr  10651  gtndiv  11013  lincmb01cmp  11773  iccf1o  11774  ltdifltdiv  12063  modfrac  12107  modvalp1  12112  negmod  12135  addmodid  12136  m1expcl2  12291  expgt1  12307  ltexp2a  12321  leexp2a  12325  binom3  12390  faclbnd  12472  faclbnd4lem4  12478  facavg  12483  bcval5  12500  cshweqrep  12905  sqrlem2  13286  absimle  13351  reccn2  13638  iseraltlem2  13727  iseraltlem3  13728  o1fsum  13851  abscvgcvg  13857  ackbijnn  13864  binom1p  13867  binom1dif  13869  incexclem  13872  incexc  13873  climcndslem1  13885  geomulcvg  13910  fprodsplit  13998  fallrisefac  14056  bpolysum  14084  bpolydiflem  14085  bpoly4  14090  efcllem  14110  ef01bndlem  14216  efieq1re  14231  eirrlem  14234  iddvds  14294  bitsfzolem  14382  bitsfzo  14383  rpmulgcd  14494  prmind2  14606  isprm5  14622  phiprm  14694  eulerthlem2  14699  fermltl  14701  odzdvds  14709  powm2modprm  14717  modprm0  14719  pythagtriplem4  14732  pcexp  14772  4sqlem18OLD  14869  4sqlem18  14875  vdwapun  14887  mulgnnass  16737  odinv  17150  odadd2  17422  pgpfaclem2  17650  abvneg  17997  nrginvrcnlem  21624  nmoid  21674  blcvx  21727  icopnfcnv  21866  reparphti  21921  pcorevlem  21950  itg11  22526  itg2mulc  22582  itg2monolem1  22585  itgcnlem  22624  iblabs  22663  dvexp  22784  dvef  22809  lhop1lem  22842  dvcvx  22849  dvfsumlem1  22855  dvfsumlem2  22856  dvfsumlem4  22858  dvfsum2  22863  plypow  23027  dgrcolem1  23095  vieta1lem2  23132  radcnvlem1  23233  radcnvlem2  23234  dvradcnv  23241  abelthlem2  23252  abelthlem6  23256  abelthlem7  23258  abelth2  23262  sinhalfpip  23312  sinhalfpim  23313  coshalfpip  23314  coshalfpim  23315  tangtx  23325  efif1olem4  23359  abslogle  23432  logdivlti  23434  advlog  23464  advlogexp  23465  logtayl  23470  cxpaddlelem  23556  cxpaddle  23557  affineequiv  23617  affineequiv2  23618  chordthmlem5  23627  dcubic2  23635  dcubic  23637  mcubic  23638  binom4  23641  dquartlem1  23642  quart1lem  23646  quart1  23647  quartlem1  23648  quart  23652  efiasin  23679  atantayl  23728  cvxcl  23775  scvxcvx  23776  lgamgulmlem5  23823  lgamcvg2  23845  lgam1  23854  wilthlem1  23858  wilthlem2  23859  basellem9  23878  fsumfldivdiaglem  23981  muinv  23985  chpub  24011  logexprlim  24016  mersenne  24018  perfectlem2  24021  dchrmulid2  24043  dchrptlem1  24055  dchrsum2  24059  sumdchr2  24061  bposlem2  24076  bposlem9  24083  lgsval2lem  24097  lgsval4a  24109  lgsneg1  24111  lgsdir2lem4  24117  lgsdir  24121  lgsdirnn0  24130  lgsdinn0  24131  lgseisenlem1  24140  lgseisenlem2  24141  lgseisenlem4  24143  lgsquad2lem1  24149  2sqlem8  24163  chebbnd1lem3  24172  chpchtlim  24180  rplogsumlem1  24185  rplogsumlem2  24186  rpvmasumlem  24188  dchrmusum2  24195  dchrvmasum2lem  24197  dchrvmasumlem2  24199  dchrvmasumlem3  24200  dchrisum0flblem1  24209  mulog2sumlem2  24236  vmalogdivsum2  24239  2vmadivsumlem  24241  log2sumbnd  24245  selberglem2  24247  chpdifbndlem1  24254  selberg3lem1  24258  selberg4lem1  24261  pntrlog2bndlem2  24279  pntrlog2bndlem5  24282  pntpbnd1  24287  pntpbnd2  24288  pntibndlem2  24292  pntlemb  24298  pntlemr  24303  pntlemk  24307  pntlemo  24308  brbtwn2  24781  colinearalglem4  24785  ax5seglem3  24807  axbtwnid  24815  axpaschlem  24816  axeuclidlem  24838  axcontlem7  24846  axcontlem8  24847  ablomul  25928  mulid  25929  nvm1  26138  nvpi  26140  nvmtri  26145  ipval2  26188  ipasslem1  26317  ipasslem4  26320  bcs2  26670  lnfnaddi  27531  sqsscirc1  28553  indsum  28683  eulerpartlemgs2  29039  plymulx0  29224  subfacp1lem6  29696  subfaclim  29699  cvxpcon  29753  cvxscon  29754  rescon  29757  sinccvglem  30104  fwddifn0  30716  nn0prpwlem  30763  bj-bary1lem1  31461  mblfinlem3  31683  itg2addnclem3  31699  iblabsnc  31710  iblmulc2nc  31711  ftc1anclem6  31726  ftc1anclem7  31727  ftc1anclem8  31728  areacirclem1  31736  bfplem2  31859  bfp  31860  rrntotbnd  31872  irrapxlem5  35380  pellexlem2  35384  pellexlem6  35388  pellfundex  35440  jm2.19lem3  35552  jm2.25  35560  jm2.27c  35568  jm3.1lem2  35579  flcidc  35739  hashgcdlem  35773  int-mul12d  36267  cvgdvgrat  36299  bccn1  36330  binomcxplemnotnn0  36342  adddirp1d  37119  fperiodmullem  37130  fmul01lt1lem2  37235  mccllem  37249  reclimc  37306  cosknegpi  37316  dvsinax  37355  dvmptdiv  37361  dvnxpaek  37386  dvnmul  37387  itgsinexp  37400  stoweidlem14  37443  stoweidlem26  37455  wallispilem4  37499  wallispilem5  37500  wallispi2lem1  37502  wallispi2  37504  stirlinglem1  37505  stirlinglem3  37507  stirlinglem4  37508  stirlinglem5  37509  stirlinglem6  37510  stirlinglem7  37511  stirlinglem10  37514  dirkertrigeqlem2  37530  dirkertrigeqlem3  37531  dirkercncflem2  37535  fourierdlem26  37564  fourierdlem41  37579  fourierdlem42  37580  fourierdlem56  37594  fourierdlem57  37595  fourierdlem58  37596  fourierdlem62  37600  fourierdlem64  37602  fourierdlem65  37603  fourierdlem95  37633  sqwvfoura  37660  sqwvfourb  37661  fouriersw  37663  etransclem23  37689  etransclem35  37701  etransclem46  37712  xp1d2m1eqxm1d2  38101  m1expoddALTV  38168  perfectALTVlem2  38234  ztprmneprm  38888  altgsumbc  38893  divge1b  39068  divgt1b  39069
  Copyright terms: Public domain W3C validator