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

Theorem mulid2d 9692
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 9672 . 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 1455    e. wcel 1898  (class class class)co 6320   CCcc 9568   1c1 9571    x. cmul 9575
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-mulcl 9632  ax-mulcom 9634  ax-mulass 9636  ax-distr 9637  ax-1rid 9640  ax-cnre 9643
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4419  df-iota 5569  df-fv 5613  df-ov 6323
This theorem is referenced by:  addid1  9844  mulsubfacd  10111  mulcand  10278  receu  10290  divdivdiv  10341  divcan5  10342  subrec  10469  ltrec  10521  recp1lt1  10537  nndivtr  10684  gtndiv  11047  lincmb01cmp  11810  iccf1o  11811  ltdifltdiv  12104  modfrac  12148  modvalp1  12153  negmod  12176  addmodid  12177  m1expcl2  12332  expgt1  12348  ltexp2a  12362  leexp2a  12366  binom3  12431  faclbnd  12513  faclbnd4lem4  12519  facavg  12524  bcval5  12541  cshweqrep  12963  sqrlem2  13362  absimle  13427  reccn2  13715  iseraltlem2  13804  iseraltlem3  13805  o1fsum  13928  abscvgcvg  13934  ackbijnn  13941  binom1p  13944  binom1dif  13946  incexclem  13949  incexc  13950  climcndslem1  13962  geomulcvg  13987  fprodsplit  14075  fallrisefac  14133  bpolysum  14161  bpolydiflem  14162  bpoly4  14167  efcllem  14187  ef01bndlem  14293  efieq1re  14308  eirrlem  14311  iddvds  14371  bitsfzolem  14462  bitsfzolemOLD  14463  bitsfzo  14464  rpmulgcd  14578  prmind2  14690  isprm5  14706  phiprm  14780  eulerthlem2  14785  fermltl  14787  odzdvds  14795  odzdvdsOLD  14801  powm2modprm  14809  modprm0  14811  pythagtriplem4  14824  pcexp  14864  4sqlem18OLD  14961  4sqlem18  14967  vdwapun  14979  mulgnnass  16841  odinv  17267  odadd2  17542  pgpfaclem2  17770  abvneg  18117  nrginvrcnlem  21748  nmoid  21818  blcvx  21871  icopnfcnv  22025  reparphti  22083  pcorevlem  22112  itg11  22705  itg2mulc  22761  itg2monolem1  22764  itgcnlem  22803  iblabs  22842  dvexp  22963  dvef  22988  lhop1lem  23021  dvcvx  23028  dvfsumlem1  23034  dvfsumlem2  23035  dvfsumlem4  23037  dvfsum2  23042  plypow  23215  dgrcolem1  23283  vieta1lem2  23320  radcnvlem1  23424  radcnvlem2  23425  dvradcnv  23432  abelthlem2  23443  abelthlem6  23447  abelthlem7  23449  abelth2  23453  sinhalfpip  23503  sinhalfpim  23504  coshalfpip  23505  coshalfpim  23506  tangtx  23516  efif1olem4  23550  abslogle  23623  logdivlti  23625  advlog  23655  advlogexp  23656  logtayl  23661  cxpaddlelem  23747  cxpaddle  23748  affineequiv  23808  affineequiv2  23809  chordthmlem5  23818  dcubic2  23826  dcubic  23828  mcubic  23829  binom4  23832  dquartlem1  23833  quart1lem  23837  quart1  23838  quartlem1  23839  quart  23843  efiasin  23870  atantayl  23919  cvxcl  23966  scvxcvx  23967  lgamgulmlem5  24014  lgamcvg2  24036  lgam1  24045  wilthlem1  24049  wilthlem2  24050  basellem9  24071  fsumfldivdiaglem  24174  muinv  24178  chpub  24204  logexprlim  24209  mersenne  24211  perfectlem2  24214  dchrmulid2  24236  dchrptlem1  24248  dchrsum2  24252  sumdchr2  24254  bposlem2  24269  bposlem9  24276  lgsval2lem  24290  lgsval4a  24302  lgsneg1  24304  lgsdir2lem4  24310  lgsdir  24314  lgsdirnn0  24323  lgsdinn0  24324  lgseisenlem1  24333  lgseisenlem2  24334  lgseisenlem4  24336  lgsquad2lem1  24342  2sqlem8  24356  chebbnd1lem3  24365  chpchtlim  24373  rplogsumlem1  24378  rplogsumlem2  24379  rpvmasumlem  24381  dchrmusum2  24388  dchrvmasum2lem  24390  dchrvmasumlem2  24392  dchrvmasumlem3  24393  dchrisum0flblem1  24402  mulog2sumlem2  24429  vmalogdivsum2  24432  2vmadivsumlem  24434  log2sumbnd  24438  selberglem2  24440  chpdifbndlem1  24447  selberg3lem1  24451  selberg4lem1  24454  pntrlog2bndlem2  24472  pntrlog2bndlem5  24475  pntpbnd1  24480  pntpbnd2  24481  pntibndlem2  24485  pntlemb  24491  pntlemr  24496  pntlemk  24500  pntlemo  24501  brbtwn2  24991  colinearalglem4  24995  ax5seglem3  25017  axbtwnid  25025  axpaschlem  25026  axeuclidlem  25048  axcontlem7  25056  axcontlem8  25057  ablomul  26139  mulid  26140  nvm1  26349  nvpi  26351  nvmtri  26356  ipval2  26399  ipasslem1  26528  ipasslem4  26531  bcs2  26891  lnfnaddi  27752  sqsscirc1  28765  indsum  28895  eulerpartlemgs2  29263  plymulx0  29486  subfacp1lem6  29958  subfaclim  29961  cvxpcon  30015  cvxscon  30016  rescon  30019  sinccvglem  30366  fwddifn0  30981  nn0prpwlem  31028  bj-bary1lem1  31762  mblfinlem3  32025  itg2addnclem3  32041  iblabsnc  32052  iblmulc2nc  32053  ftc1anclem6  32068  ftc1anclem7  32069  ftc1anclem8  32070  areacirclem1  32078  bfplem2  32201  bfp  32202  rrntotbnd  32214  irrapxlem5  35716  pellexlem2  35720  pellexlem6  35724  pellfundex  35780  jm2.19lem3  35892  jm2.25  35900  jm2.27c  35908  jm3.1lem2  35919  flcidc  36086  hashgcdlem  36120  int-mul12d  36675  cvgdvgrat  36707  bccn1  36738  binomcxplemnotnn0  36750  adddirp1d  37585  fperiodmullem  37596  xralrple2  37652  fmul01lt1lem2  37749  mccllem  37763  reclimc  37820  cosknegpi  37830  dvsinax  37869  dvmptdiv  37875  dvnxpaek  37903  dvnmul  37904  itgsinexp  37917  stoweidlem14  37975  stoweidlem26  37987  wallispilem4  38031  wallispilem5  38032  wallispi2lem1  38034  wallispi2  38036  stirlinglem1  38037  stirlinglem3  38039  stirlinglem4  38040  stirlinglem5  38041  stirlinglem6  38042  stirlinglem7  38043  stirlinglem10  38046  dirkertrigeqlem2  38062  dirkertrigeqlem3  38063  dirkercncflem2  38067  fourierdlem26  38096  fourierdlem41  38112  fourierdlem42  38113  fourierdlem42OLD  38114  fourierdlem56  38127  fourierdlem57  38128  fourierdlem58  38129  fourierdlem62  38133  fourierdlem64  38135  fourierdlem65  38136  fourierdlem95  38166  sqwvfoura  38193  sqwvfourb  38194  fouriersw  38196  etransclem23  38223  etransclem35  38235  etransclem46  38246  xp1d2m1eqxm1d2  38846  m1expoddALTV  38913  perfectALTVlem2  38979  ztprmneprm  40497  altgsumbc  40502  divge1b  40677  divgt1b  40678
  Copyright terms: Public domain W3C validator