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

Theorem mulid2d 9915
Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
addcld.1 (𝜑𝐴 ∈ ℂ)
Assertion
Ref Expression
mulid2d (𝜑 → (1 · 𝐴) = 𝐴)

Proof of Theorem mulid2d
StepHypRef Expression
1 addcld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 mulid2 9895 . 2 (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
31, 2syl 17 1 (𝜑 → (1 · 𝐴) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wcel 1977  (class class class)co 6527  cc 9791  1c1 9794   · cmul 9798
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-mulcl 9855  ax-mulcom 9857  ax-mulass 9859  ax-distr 9860  ax-1rid 9863  ax-cnre 9866
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4368  df-br 4579  df-iota 5754  df-fv 5798  df-ov 6530
This theorem is referenced by:  adddirp1d  9923  addid1  10068  mulsubfacd  10344  mulcand  10512  receu  10524  divdivdiv  10578  divcan5  10579  subrec  10706  ltrec  10757  recp1lt1  10773  nndivtr  10912  subhalfhalf  11116  xp1d2m1eqxm1d2  11136  gtndiv  11289  lincmb01cmp  12145  iccf1o  12146  ltdifltdiv  12455  modfrac  12503  modvalp1  12509  negmod  12535  addmodid  12538  m1expcl2  12702  expgt1  12718  ltexp2a  12732  leexp2a  12736  binom3  12805  faclbnd  12897  faclbnd4lem4  12903  facavg  12908  bcval5  12925  cshweqrep  13367  sqrlem2  13781  absimle  13846  reccn2  14124  iseraltlem2  14210  iseraltlem3  14211  o1fsum  14335  abscvgcvg  14341  ackbijnn  14348  binom1p  14351  binom1dif  14353  incexclem  14356  incexc  14357  climcndslem1  14369  geomulcvg  14395  fprodsplit  14484  fallrisefac  14544  bpolysum  14572  bpolydiflem  14573  bpoly4  14578  efcllem  14596  ef01bndlem  14702  efieq1re  14717  eirrlem  14720  iddvds  14782  pwp1fsum  14901  oddpwp1fsum  14902  bitsfzolem  14943  bitsfzo  14944  rpmulgcd  15062  prmind2  15185  isprm5  15206  phiprm  15269  eulerthlem2  15274  fermltl  15276  hashgcdlem  15280  odzdvds  15287  powm2modprm  15295  modprm0  15297  pythagtriplem4  15311  pcexp  15351  4sqlem18  15453  vdwapun  15465  mulgnnass  17348  mulgnnassOLD  17349  odinv  17750  odadd2  18024  pgpfaclem2  18253  abvneg  18606  nrginvrcnlem  22253  nmoid  22304  blcvx  22357  icopnfcnv  22497  reparphti  22553  pcorevlem  22582  ncvsm1  22707  ncvspi  22709  cphipval2  22793  cphipval  22795  itg11  23209  itg2mulc  23265  itg2monolem1  23268  itgcnlem  23307  iblabs  23346  dvexp  23467  dvef  23492  lhop1lem  23525  dvcvx  23532  dvfsumlem1  23538  dvfsumlem2  23539  dvfsumlem4  23541  dvfsum2  23546  plypow  23710  dgrcolem1  23778  vieta1lem2  23815  radcnvlem1  23916  radcnvlem2  23917  dvradcnv  23924  abelthlem2  23935  abelthlem6  23939  abelthlem7  23941  abelth2  23945  sinhalfpip  23993  sinhalfpim  23994  coshalfpip  23995  coshalfpim  23996  tangtx  24006  efif1olem4  24040  abslogle  24113  logdivlti  24115  advlog  24145  advlogexp  24146  logtayl  24151  cxpaddlelem  24237  cxpaddle  24238  affineequiv  24298  affineequiv2  24299  chordthmlem5  24308  dcubic2  24316  dcubic  24318  mcubic  24319  binom4  24322  dquartlem1  24323  quart1lem  24327  quart1  24328  quartlem1  24329  quart  24333  efiasin  24360  atantayl  24409  cvxcl  24456  scvxcvx  24457  lgamgulmlem5  24504  lgamcvg2  24526  lgam1  24535  wilthlem1  24539  wilthlem2  24540  basellem9  24560  fsumfldivdiaglem  24660  muinv  24664  chpub  24690  logexprlim  24695  mersenne  24697  perfectlem2  24700  dchrmulid2  24722  dchrptlem1  24734  dchrsum2  24738  sumdchr2  24740  bposlem2  24755  bposlem9  24762  lgsval2lem  24777  lgsval4a  24789  lgsneg1  24792  lgsdir2lem4  24798  lgsdir  24802  lgsmulsqcoprm  24813  lgsdirnn0  24814  lgsdinn0  24815  gausslemma2dlem1a  24835  gausslemma2dlem4  24839  gausslemma2dlem7  24843  gausslemma2d  24844  lgseisenlem1  24845  lgseisenlem2  24846  lgseisenlem4  24848  lgsquad2lem1  24854  2sqlem8  24896  chebbnd1lem3  24905  chpchtlim  24913  rplogsumlem1  24918  rplogsumlem2  24919  rpvmasumlem  24921  dchrmusum2  24928  dchrvmasum2lem  24930  dchrvmasumlem2  24932  dchrvmasumlem3  24933  dchrisum0flblem1  24942  mulog2sumlem2  24969  vmalogdivsum2  24972  2vmadivsumlem  24974  log2sumbnd  24978  selberglem2  24980  chpdifbndlem1  24987  selberg3lem1  24991  selberg4lem1  24994  pntrlog2bndlem2  25012  pntrlog2bndlem5  25015  pntpbnd1  25020  pntpbnd2  25021  pntibndlem2  25025  pntlemb  25031  pntlemr  25036  pntlemk  25040  pntlemo  25041  brbtwn2  25531  colinearalglem4  25535  ax5seglem3  25557  axbtwnid  25565  axpaschlem  25566  axeuclidlem  25588  axcontlem7  25596  axcontlem8  25597  nvm1  26698  nvpi  26700  nvmtri  26704  ipval2  26740  ipasslem1  26864  ipasslem4  26867  bcs2  27217  lnfnaddi  28080  sqsscirc1  29076  indsum  29206  eulerpartlemgs2  29563  plymulx0  29744  subfacp1lem6  30215  subfaclim  30218  cvxpcon  30272  cvxscon  30273  rescon  30276  sinccvglem  30614  fwddifn0  31235  nn0prpwlem  31281  knoppndvlem9  31475  knoppndvlem14  31480  bj-bary1lem1  32132  mblfinlem3  32412  itg2addnclem3  32427  iblabsnc  32438  iblmulc2nc  32439  ftc1anclem6  32454  ftc1anclem7  32455  ftc1anclem8  32456  areacirclem1  32464  bfplem2  32586  bfp  32587  rrntotbnd  32599  irrapxlem5  36202  pellexlem2  36206  pellexlem6  36210  pellfundex  36262  jm2.19lem3  36370  jm2.25  36378  jm2.27c  36386  jm3.1lem2  36397  flcidc  36557  int-mul12d  37302  cvgdvgrat  37328  bccn1  37359  binomcxplemnotnn0  37371  fperiodmullem  38252  xralrple2  38305  fmul01lt1lem2  38446  mccllem  38458  reclimc  38514  cosknegpi  38546  dvsinax  38595  dvmptdiv  38601  dvnxpaek  38626  dvnmul  38627  itgsinexp  38640  stoweidlem14  38701  stoweidlem26  38713  wallispilem4  38755  wallispilem5  38756  wallispi2lem1  38758  wallispi2  38760  stirlinglem1  38761  stirlinglem3  38763  stirlinglem4  38764  stirlinglem5  38765  stirlinglem6  38766  stirlinglem7  38767  stirlinglem10  38770  dirkertrigeqlem2  38786  dirkertrigeqlem3  38787  dirkercncflem2  38791  fourierdlem26  38820  fourierdlem41  38835  fourierdlem42  38836  fourierdlem56  38849  fourierdlem57  38850  fourierdlem58  38851  fourierdlem62  38855  fourierdlem64  38857  fourierdlem65  38858  fourierdlem95  38888  sqwvfoura  38915  sqwvfourb  38916  fouriersw  38918  etransclem23  38944  etransclem35  38956  etransclem46  38967  fmtnorec2lem  39787  fmtnorec3  39793  pwdif  39834  m1expoddALTV  39894  perfectALTVlem2  39960  ztprmneprm  41910  altgsumbc  41915  divge1b  42088  divgt1b  42089
  Copyright terms: Public domain W3C validator