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

Theorem mulid2d 9668
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 9648 . 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 1872  (class class class)co 6305   CCcc 9544   1c1 9547    x. cmul 9551
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-resscn 9603  ax-1cn 9604  ax-icn 9605  ax-addcl 9606  ax-mulcl 9608  ax-mulcom 9610  ax-mulass 9612  ax-distr 9613  ax-1rid 9616  ax-cnre 9619
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-iota 5565  df-fv 5609  df-ov 6308
This theorem is referenced by:  addid1  9820  mulsubfacd  10085  mulcand  10252  receu  10264  divdivdiv  10315  divcan5  10316  subrec  10443  ltrec  10495  recp1lt1  10511  nndivtr  10658  gtndiv  11020  lincmb01cmp  11782  iccf1o  11783  ltdifltdiv  12072  modfrac  12116  modvalp1  12121  negmod  12144  addmodid  12145  m1expcl2  12300  expgt1  12316  ltexp2a  12330  leexp2a  12334  binom3  12399  faclbnd  12481  faclbnd4lem4  12487  facavg  12492  bcval5  12509  cshweqrep  12922  sqrlem2  13307  absimle  13372  reccn2  13659  iseraltlem2  13748  iseraltlem3  13749  o1fsum  13872  abscvgcvg  13878  ackbijnn  13885  binom1p  13888  binom1dif  13890  incexclem  13893  incexc  13894  climcndslem1  13906  geomulcvg  13931  fprodsplit  14019  fallrisefac  14077  bpolysum  14105  bpolydiflem  14106  bpoly4  14111  efcllem  14131  ef01bndlem  14237  efieq1re  14252  eirrlem  14255  iddvds  14315  bitsfzolem  14406  bitsfzolemOLD  14407  bitsfzo  14408  rpmulgcd  14522  prmind2  14634  isprm5  14650  phiprm  14724  eulerthlem2  14729  fermltl  14731  odzdvds  14739  odzdvdsOLD  14745  powm2modprm  14753  modprm0  14755  pythagtriplem4  14768  pcexp  14808  4sqlem18OLD  14905  4sqlem18  14911  vdwapun  14923  mulgnnass  16785  odinv  17211  odadd2  17486  pgpfaclem2  17714  abvneg  18061  nrginvrcnlem  21691  nmoid  21761  blcvx  21814  icopnfcnv  21968  reparphti  22026  pcorevlem  22055  itg11  22647  itg2mulc  22703  itg2monolem1  22706  itgcnlem  22745  iblabs  22784  dvexp  22905  dvef  22930  lhop1lem  22963  dvcvx  22970  dvfsumlem1  22976  dvfsumlem2  22977  dvfsumlem4  22979  dvfsum2  22984  plypow  23157  dgrcolem1  23225  vieta1lem2  23262  radcnvlem1  23366  radcnvlem2  23367  dvradcnv  23374  abelthlem2  23385  abelthlem6  23389  abelthlem7  23391  abelth2  23395  sinhalfpip  23445  sinhalfpim  23446  coshalfpip  23447  coshalfpim  23448  tangtx  23458  efif1olem4  23492  abslogle  23565  logdivlti  23567  advlog  23597  advlogexp  23598  logtayl  23603  cxpaddlelem  23689  cxpaddle  23690  affineequiv  23750  affineequiv2  23751  chordthmlem5  23760  dcubic2  23768  dcubic  23770  mcubic  23771  binom4  23774  dquartlem1  23775  quart1lem  23779  quart1  23780  quartlem1  23781  quart  23785  efiasin  23812  atantayl  23861  cvxcl  23908  scvxcvx  23909  lgamgulmlem5  23956  lgamcvg2  23978  lgam1  23987  wilthlem1  23991  wilthlem2  23992  basellem9  24013  fsumfldivdiaglem  24116  muinv  24120  chpub  24146  logexprlim  24151  mersenne  24153  perfectlem2  24156  dchrmulid2  24178  dchrptlem1  24190  dchrsum2  24194  sumdchr2  24196  bposlem2  24211  bposlem9  24218  lgsval2lem  24232  lgsval4a  24244  lgsneg1  24246  lgsdir2lem4  24252  lgsdir  24256  lgsdirnn0  24265  lgsdinn0  24266  lgseisenlem1  24275  lgseisenlem2  24276  lgseisenlem4  24278  lgsquad2lem1  24284  2sqlem8  24298  chebbnd1lem3  24307  chpchtlim  24315  rplogsumlem1  24320  rplogsumlem2  24321  rpvmasumlem  24323  dchrmusum2  24330  dchrvmasum2lem  24332  dchrvmasumlem2  24334  dchrvmasumlem3  24335  dchrisum0flblem1  24344  mulog2sumlem2  24371  vmalogdivsum2  24374  2vmadivsumlem  24376  log2sumbnd  24380  selberglem2  24382  chpdifbndlem1  24389  selberg3lem1  24393  selberg4lem1  24396  pntrlog2bndlem2  24414  pntrlog2bndlem5  24417  pntpbnd1  24422  pntpbnd2  24423  pntibndlem2  24427  pntlemb  24433  pntlemr  24438  pntlemk  24442  pntlemo  24443  brbtwn2  24933  colinearalglem4  24937  ax5seglem3  24959  axbtwnid  24967  axpaschlem  24968  axeuclidlem  24990  axcontlem7  24998  axcontlem8  24999  ablomul  26081  mulid  26082  nvm1  26291  nvpi  26293  nvmtri  26298  ipval2  26341  ipasslem1  26470  ipasslem4  26473  bcs2  26833  lnfnaddi  27694  sqsscirc1  28722  indsum  28852  eulerpartlemgs2  29221  plymulx0  29444  subfacp1lem6  29916  subfaclim  29919  cvxpcon  29973  cvxscon  29974  rescon  29977  sinccvglem  30324  fwddifn0  30936  nn0prpwlem  30983  bj-bary1lem1  31680  mblfinlem3  31943  itg2addnclem3  31959  iblabsnc  31970  iblmulc2nc  31971  ftc1anclem6  31986  ftc1anclem7  31987  ftc1anclem8  31988  areacirclem1  31996  bfplem2  32119  bfp  32120  rrntotbnd  32132  irrapxlem5  35640  pellexlem2  35644  pellexlem6  35648  pellfundex  35704  jm2.19lem3  35816  jm2.25  35824  jm2.27c  35832  jm3.1lem2  35843  flcidc  36010  hashgcdlem  36044  int-mul12d  36600  cvgdvgrat  36632  bccn1  36663  binomcxplemnotnn0  36675  adddirp1d  37464  fperiodmullem  37475  xralrple2  37531  fmul01lt1lem2  37603  mccllem  37617  reclimc  37674  cosknegpi  37684  dvsinax  37723  dvmptdiv  37729  dvnxpaek  37757  dvnmul  37758  itgsinexp  37771  stoweidlem14  37814  stoweidlem26  37826  wallispilem4  37870  wallispilem5  37871  wallispi2lem1  37873  wallispi2  37875  stirlinglem1  37876  stirlinglem3  37878  stirlinglem4  37879  stirlinglem5  37880  stirlinglem6  37881  stirlinglem7  37882  stirlinglem10  37885  dirkertrigeqlem2  37901  dirkertrigeqlem3  37902  dirkercncflem2  37906  fourierdlem26  37935  fourierdlem41  37951  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem56  37966  fourierdlem57  37967  fourierdlem58  37968  fourierdlem62  37972  fourierdlem64  37974  fourierdlem65  37975  fourierdlem95  38005  sqwvfoura  38032  sqwvfourb  38033  fouriersw  38035  etransclem23  38062  etransclem35  38074  etransclem46  38085  xp1d2m1eqxm1d2  38581  m1expoddALTV  38648  perfectALTVlem2  38714  ztprmneprm  39749  altgsumbc  39754  divge1b  39929  divgt1b  39930
  Copyright terms: Public domain W3C validator