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

Theorem mulid2d 11107
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 11088 . 2 (๐ด โˆˆ โ„‚ โ†’ (1 ยท ๐ด) = ๐ด)
31, 2syl 17 1 (๐œ‘ โ†’ (1 ยท ๐ด) = ๐ด)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   = wceq 1542   โˆˆ wcel 2107  (class class class)co 7350  โ„‚cc 10983  1c1 10986   ยท cmul 10990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709  ax-resscn 11042  ax-1cn 11043  ax-icn 11044  ax-addcl 11045  ax-mulcl 11047  ax-mulcom 11049  ax-mulass 11051  ax-distr 11052  ax-1rid 11055  ax-cnre 11058
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-rex 3073  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-iota 6444  df-fv 6500  df-ov 7353
This theorem is referenced by:  adddirp1d  11115  addid1  11269  mulsubfacd  11550  mulcand  11722  receu  11734  divdivdiv  11790  divcan5  11791  subrec  11918  ltrec  11971  recp1lt1  11987  nndivtr  12134  subhalfhalf  12321  xp1d2m1eqxm1d2  12341  gtndiv  12514  lincmb01cmp  13342  iccf1o  13343  ltdifltdiv  13669  modfrac  13719  negmod  13751  addmodid  13754  m1expcl2  13919  expgt1  13936  ltexp2a  13999  leexp2a  14005  binom3  14054  faclbnd  14119  faclbnd4lem4  14125  facavg  14130  bcval5  14147  cshweqrep  14642  sqrlem2  15064  absimle  15130  reccn2  15415  iseraltlem2  15503  iseraltlem3  15504  o1fsum  15634  abscvgcvg  15640  ackbijnn  15649  binom1p  15652  binom1dif  15654  incexclem  15657  incexc  15658  climcndslem1  15670  pwdif  15689  geomulcvg  15697  fprodsplit  15785  fallrisefac  15844  bpolysum  15872  bpolydiflem  15873  bpoly4  15878  efcllem  15896  ef01bndlem  16002  efieq1re  16017  eirrlem  16022  iddvds  16088  pwp1fsum  16209  oddpwp1fsum  16210  bitsfzolem  16250  bitsfzo  16251  rpmulgcd  16373  prmind2  16497  isprm5  16519  phiprm  16585  eulerthlem2  16590  fermltl  16592  hashgcdlem  16596  odzdvds  16603  powm2modprm  16611  modprm0  16613  pythagtriplem4  16627  4sqlem18  16770  vdwapun  16782  mulgnnass  18846  odinv  19278  odadd2  19562  pgpfaclem2  19796  abvneg  20222  nrginvrcnlem  23983  nmoid  24034  blcvx  24089  icopnfcnv  24233  reparphti  24288  pcorevlem  24317  ncvsm1  24446  ncvspi  24448  cphipval2  24533  cphipval  24535  itg11  24983  itg2mulc  25040  itg2monolem1  25043  itgcnlem  25082  iblabs  25121  dvexp  25245  dvmptdiv  25266  dvef  25272  lhop1lem  25305  dvcvx  25312  dvfsumlem1  25318  dvfsumlem2  25319  dvfsumlem4  25321  dvfsum2  25326  plypow  25494  dgrcolem1  25562  vieta1lem2  25599  radcnvlem1  25700  radcnvlem2  25701  dvradcnv  25708  abelthlem6  25723  abelthlem7  25725  abelth2  25729  sinhalfpip  25777  sinhalfpim  25778  coshalfpip  25779  coshalfpim  25780  tangtx  25790  efif1olem4  25829  abslogle  25901  logdivlti  25903  advlog  25937  advlogexp  25938  logtayl  25943  cxpaddlelem  26032  cxpaddle  26033  affineequiv  26101  affineequiv2  26102  chordthmlem5  26114  dcubic2  26122  dcubic  26124  mcubic  26125  binom4  26128  dquartlem1  26129  quart1lem  26133  quart1  26134  quartlem1  26135  quart  26139  efiasin  26166  atantayl  26215  cvxcl  26262  scvxcvx  26263  lgamgulmlem5  26310  lgamcvg2  26332  lgam1  26341  wilthlem1  26345  wilthlem2  26346  basellem9  26366  fsumfldivdiaglem  26466  muinv  26470  chpub  26496  logexprlim  26501  mersenne  26503  perfectlem2  26506  dchrmulid2  26528  dchrptlem1  26540  dchrsum2  26544  sumdchr2  26546  bposlem2  26561  bposlem9  26568  lgsval2lem  26583  lgsval4a  26595  lgsneg1  26598  lgsdir2lem4  26604  lgsdir  26608  lgsmulsqcoprm  26619  lgsdirnn0  26620  lgsdinn0  26621  gausslemma2dlem1a  26641  gausslemma2dlem4  26645  gausslemma2dlem7  26649  gausslemma2d  26650  lgseisenlem1  26651  lgseisenlem2  26652  lgseisenlem4  26654  lgsquad2lem1  26660  2sqlem8  26702  chebbnd1lem3  26747  chpchtlim  26755  rplogsumlem1  26760  rplogsumlem2  26761  rpvmasumlem  26763  dchrmusum2  26770  dchrvmasum2lem  26772  dchrvmasumlem2  26774  dchrvmasumlem3  26775  dchrisum0flblem1  26784  mulog2sumlem2  26811  vmalogdivsum2  26814  2vmadivsumlem  26816  log2sumbnd  26820  selberglem2  26822  selberg3lem1  26833  selberg4lem1  26836  pntrlog2bndlem2  26854  pntrlog2bndlem5  26857  pntpbnd1  26862  pntpbnd2  26863  pntibndlem2  26867  pntlemb  26873  pntlemr  26878  pntlemk  26882  pntlemo  26883  brbtwn2  27659  colinearalglem4  27663  ax5seglem3  27685  axbtwnid  27693  axpaschlem  27694  axeuclidlem  27716  axcontlem7  27724  axcontlem8  27725  elntg2  27739  nvm1  29412  nvpi  29414  nvmtri  29418  ipval2  29454  ipasslem1  29578  ipasslem4  29581  bcs2  29929  lnfnaddi  30790  nnmulge  31456  ccfldsrarelvec  32145  sqsscirc1  32269  indsum  32400  indsumin  32401  eulerpartlemgs2  32760  plymulx0  32939  logdivsqrle  33043  subfacp1lem6  33559  subfaclim  33562  cvxpconn  33616  cvxsconn  33617  resconn  33620  sinccvglem  34042  fwddifn0  34680  nn0prpwlem  34725  knoppndvlem9  34914  knoppndvlem14  34919  bj-bary1lem1  35713  mblfinlem3  36048  itg2addnclem3  36062  iblabsnc  36073  iblmulc2nc  36074  ftc1anclem6  36087  ftc1anclem7  36088  ftc1anclem8  36089  areacirclem1  36097  bfplem2  36213  bfp  36214  rrntotbnd  36226  lcmineqlem1  40417  lcmineqlem12  40428  lcmineqlem18  40434  aks4d1p1p7  40462  aks4d1p8  40475  fltnlta  40903  3cubeslem2  40910  3cubeslem3r  40912  irrapxlem5  41051  pellexlem2  41055  pellexlem6  41059  pellfundex  41111  jm2.19lem3  41217  jm2.25  41225  jm2.27c  41233  jm3.1lem2  41244  flcidc  41403  reabssgn  41707  sqrtcval  41712  int-mul12d  42257  cvgdvgrat  42394  bccn1  42425  binomcxplemnotnn0  42437  fperiodmullem  43332  xralrple2  43383  fmul01lt1lem2  43617  mccllem  43629  reclimc  43685  cosknegpi  43901  dvsinax  43945  dvnxpaek  43974  dvnmul  43975  itgsinexp  43987  stoweidlem14  44046  stoweidlem26  44058  wallispilem4  44100  wallispilem5  44101  wallispi2lem1  44103  wallispi2  44105  stirlinglem1  44106  stirlinglem3  44108  stirlinglem4  44109  stirlinglem5  44110  stirlinglem6  44111  stirlinglem7  44112  stirlinglem10  44115  dirkertrigeqlem2  44131  dirkertrigeqlem3  44132  dirkercncflem2  44136  fourierdlem26  44165  fourierdlem41  44180  fourierdlem42  44181  fourierdlem56  44194  fourierdlem57  44195  fourierdlem58  44196  fourierdlem62  44200  fourierdlem64  44202  fourierdlem65  44203  fourierdlem95  44233  sqwvfoura  44260  sqwvfourb  44261  fouriersw  44263  etransclem23  44289  etransclem35  44301  etransclem46  44312  fmtnorec2lem  45525  fmtnorec3  45531  m1expoddALTV  45631  perfectALTVlem2  45705  ztprmneprm  46214  altgsumbc  46219  divge1b  46384  divgt1b  46385  ackval1  46558  affineid  46581  1subrec1sub  46582  rrx2vlinest  46618  line2x  46631
  Copyright terms: Public domain W3C validator