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

Theorem mulid1d 11173
Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
addcld.1 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
Assertion
Ref Expression
mulid1d (๐œ‘ โ†’ (๐ด ยท 1) = ๐ด)

Proof of Theorem mulid1d
StepHypRef Expression
1 addcld.1 . 2 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
2 mulid1 11154 . 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 7358  โ„‚cc 11050  1c1 11053   ยท cmul 11057
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 2708  ax-resscn 11109  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-mulcl 11114  ax-mulcom 11116  ax-mulass 11118  ax-distr 11119  ax-1rid 11122  ax-cnre 11125
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 2715  df-cleq 2729  df-clel 2815  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361
This theorem is referenced by:  muladd11  11326  muls1d  11616  divrec  11830  diveq1  11847  conjmul  11873  divelunit  13412  modid  13802  addmodlteq  13852  expadd  14011  leexp2r  14080  nnlesq  14110  sqoddm1div8  14147  faclbnd  14191  faclbnd2  14192  faclbnd4lem3  14196  faclbnd6  14200  facavg  14202  bcn0  14211  bcn1  14214  hashf1lem2  14356  hashfac  14358  reccn2  15480  iseraltlem2  15568  iseraltlem3  15569  hash2iun1dif1  15710  binom11  15718  harmonic  15745  trireciplem  15748  geoserg  15752  pwdif  15754  pwm1geoser  15755  cvgrat  15769  fprodsplit  15850  fprodle  15880  fsumcube  15944  efzval  15985  tanhlt1  16043  tanaddlem  16049  tanadd  16050  cos01gt0  16074  absef  16080  1dvds  16154  bitsfzo  16316  bitsmod  16317  sqgcd  16442  lcm1  16487  coprmdvds  16530  qredeu  16535  phiprmpw  16649  coprimeprodsq  16681  pc2dvds  16752  sumhash  16769  fldivp1  16770  pcfaclem  16771  prmpwdvds  16777  prmreclem1  16789  vdwlem3  16856  vdwlem9  16862  prmop1  16911  sylow2a  19402  odadd  19629  zsssubrg  20858  zringcyg  20893  prmirredlem  20896  mulgrhm2  20902  znrrg  20975  mhppwdeg  21543  icopnfcnv  24308  icopnfhmeo  24309  lebnumii  24332  reparphti  24363  itg2const  25108  itg2monolem3  25120  bddibl  25207  dveflem  25346  mvth  25359  dvlipcn  25361  dvivthlem1  25375  dvfsumle  25388  dvfsumabs  25390  dvfsumlem2  25394  plyconst  25570  plyeq0lem  25574  plyco  25605  0dgrb  25610  coefv0  25612  vieta1  25675  aaliou3lem2  25706  tayl0  25724  taylply2  25730  dvtaylp  25732  taylthlem2  25736  radcnvlem1  25775  abelthlem1  25793  abelthlem2  25794  abelthlem3  25795  abelthlem7  25800  abelthlem8  25801  abelthlem9  25802  efper  25839  tangtx  25865  eflogeq  25960  logdivlti  25978  logcnlem4  26003  advlogexp  26013  cxpmul2  26047  dvcxp2  26097  cxpaddle  26108  cxpeq  26113  loglesqrt  26114  relogbexp  26133  ang180lem5  26166  isosctrlem2  26172  isosctrlem3  26173  heron  26191  2efiatan  26271  dvatan  26288  leibpi  26295  birthdaylem3  26306  jensenlem2  26340  logdiflbnd  26347  harmonicbnd4  26363  lgamgulmlem2  26382  lgamcvg2  26407  ftalem5  26429  basellem2  26434  basellem5  26437  basellem8  26440  0sgm  26496  muinv  26545  chpub  26571  logfaclbnd  26573  logexprlim  26576  dchrsum2  26619  sumdchr2  26621  bposlem1  26635  bposlem2  26636  bposlem5  26639  lgsquad2lem1  26735  lgsquad3  26738  2sqlem6  26774  2sqlem8  26777  chtppilim  26826  vmadivsum  26833  dchrisumlem1  26840  dchrisum0flblem1  26859  rpvmasum2  26863  dchrisum0re  26864  dchrisum0lem2a  26868  dchrisum0lem3  26870  rpvmasum  26877  mudivsum  26881  mulogsumlem  26882  vmalogdivsum2  26889  pntrsumo1  26916  pntrlog2bndlem2  26929  pntrlog2bndlem4  26931  pntrlog2bndlem5  26932  pntibndlem2  26942  pntlemc  26946  pntlemf  26956  ostth2lem2  26985  ostth2lem3  26986  ostth2lem4  26987  ostth2  26988  ostth3  26989  ttgcontlem1  27836  axpaschlem  27892  axcontlem2  27917  axcontlem4  27919  axcontlem8  27923  nmoub3i  29718  ubthlem2  29816  htthlem  29862  nmcexi  30971  nmopcoadji  31046  branmfn  31050  rearchi  32141  ccfldextdgrr  32359  madjusmdetlem4  32414  ccatmulgnn0dir  33157  ofcccat  33158  itgexpif  33222  hashreprin  33236  circlemeth  33256  lpadlem2  33296  subfacval2  33784  cvmliftlem2  33883  snmlff  33926  sinccvglem  34263  bcprod  34314  faclimlem1  34319  faclimlem2  34320  faclim2  34324  knoppndvlem14  34991  knoppndvlem15  34992  knoppndvlem16  34993  knoppndvlem18  34995  poimirlem29  36110  poimirlem30  36111  poimirlem31  36112  poimirlem32  36113  itg2addnclem  36132  areacirclem1  36169  areacirclem4  36172  cntotbnd  36258  lcmineqlem11  40499  lcmineqlem12  40500  aks4d1p1p7  40534  aks4d1p8d2  40545  2ap1caineq  40556  sticksstones10  40566  sticksstones12a  40568  frlmvscadiccat  40684  oexpreposd  40810  expgcd  40823  fltnltalem  41003  3cubeslem2  41011  3cubeslem3r  41013  irrapxlem1  41148  irrapxlem4  41151  pell1qrgaplem  41199  reglogexpbas  41223  rmspecfund  41235  rmxy1  41249  rmxp1  41259  rmyp1  41260  rmxm1  41261  jm2.17a  41287  jm2.18  41315  jm2.23  41323  jm2.25  41326  jm2.16nn0  41331  relexpmulnn  41988  int-mul11d  42462  nzprmdif  42606  expgrowthi  42620  expgrowth  42622  binomcxplemdvbinom  42640  binomcxplemnotnn0  42643  sqrlearg  43798  fmul01  43828  fmul01lt1lem1  43832  0ellimcdiv  43897  dvxpaek  44188  dvnxpaek  44190  itgiccshift  44228  itgperiod  44229  itgsbtaddcnst  44230  stoweidlem11  44259  stoweidlem26  44274  stoweidlem38  44286  wallispilem4  44316  stirlinglem1  44322  stirlinglem3  44324  stirlinglem6  44327  stirlinglem7  44328  stirlinglem8  44329  stirlinglem10  44331  stirlinglem12  44333  dirkertrigeqlem3  44348  dirkertrigeq  44349  dirkercncflem1  44351  dirkercncflem2  44352  fourierdlem28  44383  fourierdlem30  44385  fourierdlem39  44394  fourierdlem47  44401  fourierdlem60  44414  fourierdlem61  44415  fourierdlem73  44427  fourierdlem83  44437  fourierdlem87  44441  etransclem14  44496  etransclem24  44506  etransclem25  44507  etransclem35  44517  smfmullem1  45039  deccarry  45550  fpprwppr  45938  fpprwpprb  45939  logblt1b  46657  nn0sumshdiglem2  46715  itcovalpclem2  46764  itcovalt2lem1  46768  eenglngeehlnmlem1  46830  eenglngeehlnmlem2  46831  line2ylem  46844
  Copyright terms: Public domain W3C validator