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  12511  lincmb01cmp  13341  iccf1o  13342  ltdifltdiv  13668  modfrac  13718  negmod  13750  addmodid  13753  m1expcl2  13918  expgt1  13935  ltexp2a  13998  leexp2a  14004  binom3  14053  faclbnd  14118  faclbnd4lem4  14124  facavg  14129  bcval5  14146  cshweqrep  14641  sqrlem2  15063  absimle  15129  reccn2  15414  iseraltlem2  15502  iseraltlem3  15503  o1fsum  15633  abscvgcvg  15639  ackbijnn  15648  binom1p  15651  binom1dif  15653  incexclem  15656  incexc  15657  climcndslem1  15669  pwdif  15688  geomulcvg  15696  fprodsplit  15784  fallrisefac  15843  bpolysum  15871  bpolydiflem  15872  bpoly4  15877  efcllem  15895  ef01bndlem  16001  efieq1re  16016  eirrlem  16021  iddvds  16087  pwp1fsum  16208  oddpwp1fsum  16209  bitsfzolem  16249  bitsfzo  16250  rpmulgcd  16372  prmind2  16496  isprm5  16518  phiprm  16584  eulerthlem2  16589  fermltl  16591  hashgcdlem  16595  odzdvds  16602  powm2modprm  16610  modprm0  16612  pythagtriplem4  16626  4sqlem18  16769  vdwapun  16781  mulgnnass  18844  odinv  19275  odadd2  19557  pgpfaclem2  19791  abvneg  20217  nrginvrcnlem  23978  nmoid  24029  blcvx  24084  icopnfcnv  24228  reparphti  24283  pcorevlem  24312  ncvsm1  24441  ncvspi  24443  cphipval2  24528  cphipval  24530  itg11  24978  itg2mulc  25035  itg2monolem1  25038  itgcnlem  25077  iblabs  25116  dvexp  25240  dvmptdiv  25261  dvef  25267  lhop1lem  25300  dvcvx  25307  dvfsumlem1  25313  dvfsumlem2  25314  dvfsumlem4  25316  dvfsum2  25321  plypow  25489  dgrcolem1  25557  vieta1lem2  25594  radcnvlem1  25695  radcnvlem2  25696  dvradcnv  25703  abelthlem6  25718  abelthlem7  25720  abelth2  25724  sinhalfpip  25772  sinhalfpim  25773  coshalfpip  25774  coshalfpim  25775  tangtx  25785  efif1olem4  25824  abslogle  25896  logdivlti  25898  advlog  25932  advlogexp  25933  logtayl  25938  cxpaddlelem  26027  cxpaddle  26028  affineequiv  26096  affineequiv2  26097  chordthmlem5  26109  dcubic2  26117  dcubic  26119  mcubic  26120  binom4  26123  dquartlem1  26124  quart1lem  26128  quart1  26129  quartlem1  26130  quart  26134  efiasin  26161  atantayl  26210  cvxcl  26257  scvxcvx  26258  lgamgulmlem5  26305  lgamcvg2  26327  lgam1  26336  wilthlem1  26340  wilthlem2  26341  basellem9  26361  fsumfldivdiaglem  26461  muinv  26465  chpub  26491  logexprlim  26496  mersenne  26498  perfectlem2  26501  dchrmulid2  26523  dchrptlem1  26535  dchrsum2  26539  sumdchr2  26541  bposlem2  26556  bposlem9  26563  lgsval2lem  26578  lgsval4a  26590  lgsneg1  26593  lgsdir2lem4  26599  lgsdir  26603  lgsmulsqcoprm  26614  lgsdirnn0  26615  lgsdinn0  26616  gausslemma2dlem1a  26636  gausslemma2dlem4  26640  gausslemma2dlem7  26644  gausslemma2d  26645  lgseisenlem1  26646  lgseisenlem2  26647  lgseisenlem4  26649  lgsquad2lem1  26655  2sqlem8  26697  chebbnd1lem3  26742  chpchtlim  26750  rplogsumlem1  26755  rplogsumlem2  26756  rpvmasumlem  26758  dchrmusum2  26765  dchrvmasum2lem  26767  dchrvmasumlem2  26769  dchrvmasumlem3  26770  dchrisum0flblem1  26779  mulog2sumlem2  26806  vmalogdivsum2  26809  2vmadivsumlem  26811  log2sumbnd  26815  selberglem2  26817  selberg3lem1  26828  selberg4lem1  26831  pntrlog2bndlem2  26849  pntrlog2bndlem5  26852  pntpbnd1  26857  pntpbnd2  26858  pntibndlem2  26862  pntlemb  26868  pntlemr  26873  pntlemk  26877  pntlemo  26878  brbtwn2  27653  colinearalglem4  27657  ax5seglem3  27679  axbtwnid  27687  axpaschlem  27688  axeuclidlem  27710  axcontlem7  27718  axcontlem8  27719  elntg2  27733  nvm1  29406  nvpi  29408  nvmtri  29412  ipval2  29448  ipasslem1  29572  ipasslem4  29575  bcs2  29923  lnfnaddi  30784  nnmulge  31450  ccfldsrarelvec  32139  sqsscirc1  32263  indsum  32394  indsumin  32395  eulerpartlemgs2  32754  plymulx0  32933  logdivsqrle  33037  subfacp1lem6  33553  subfaclim  33556  cvxpconn  33610  cvxsconn  33611  resconn  33614  sinccvglem  34036  fwddifn0  34645  nn0prpwlem  34690  knoppndvlem9  34879  knoppndvlem14  34884  bj-bary1lem1  35678  mblfinlem3  36013  itg2addnclem3  36027  iblabsnc  36038  iblmulc2nc  36039  ftc1anclem6  36052  ftc1anclem7  36053  ftc1anclem8  36054  areacirclem1  36062  bfplem2  36178  bfp  36179  rrntotbnd  36191  lcmineqlem1  40382  lcmineqlem12  40393  lcmineqlem18  40399  aks4d1p1p7  40427  aks4d1p8  40440  fltnlta  40867  3cubeslem2  40874  3cubeslem3r  40876  irrapxlem5  41015  pellexlem2  41019  pellexlem6  41023  pellfundex  41075  jm2.19lem3  41181  jm2.25  41189  jm2.27c  41197  jm3.1lem2  41208  flcidc  41367  reabssgn  41671  sqrtcval  41676  int-mul12d  42221  cvgdvgrat  42358  bccn1  42389  binomcxplemnotnn0  42401  fperiodmullem  43296  xralrple2  43347  fmul01lt1lem2  43581  mccllem  43593  reclimc  43649  cosknegpi  43865  dvsinax  43909  dvnxpaek  43938  dvnmul  43939  itgsinexp  43951  stoweidlem14  44010  stoweidlem26  44022  wallispilem4  44064  wallispilem5  44065  wallispi2lem1  44067  wallispi2  44069  stirlinglem1  44070  stirlinglem3  44072  stirlinglem4  44073  stirlinglem5  44074  stirlinglem6  44075  stirlinglem7  44076  stirlinglem10  44079  dirkertrigeqlem2  44095  dirkertrigeqlem3  44096  dirkercncflem2  44100  fourierdlem26  44129  fourierdlem41  44144  fourierdlem42  44145  fourierdlem56  44158  fourierdlem57  44159  fourierdlem58  44160  fourierdlem62  44164  fourierdlem64  44166  fourierdlem65  44167  fourierdlem95  44197  sqwvfoura  44224  sqwvfourb  44225  fouriersw  44227  etransclem23  44253  etransclem35  44265  etransclem46  44276  fmtnorec2lem  45489  fmtnorec3  45495  m1expoddALTV  45595  perfectALTVlem2  45669  ztprmneprm  46178  altgsumbc  46183  divge1b  46348  divgt1b  46349  ackval1  46522  affineid  46545  1subrec1sub  46546  rrx2vlinest  46582  line2x  46595
  Copyright terms: Public domain W3C validator