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

Theorem mulid1d 10647
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 10628 . 2 (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
31, 2syl 17 1 (𝜑 → (𝐴 · 1) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  (class class class)co 7145  cc 10524  1c1 10527   · cmul 10531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-mulcom 10590  ax-mulass 10592  ax-distr 10593  ax-1rid 10596  ax-cnre 10599
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-iota 6308  df-fv 6357  df-ov 7148
This theorem is referenced by:  muladd11  10799  muls1d  11089  divrec  11303  diveq1  11320  conjmul  11346  divelunit  12870  modid  13254  addmodlteq  13304  expadd  13461  leexp2r  13528  nnlesq  13558  sqoddm1div8  13594  faclbnd  13640  faclbnd2  13641  faclbnd4lem3  13645  faclbnd6  13649  facavg  13651  bcn0  13660  bcn1  13663  hashf1lem2  13804  hashfac  13806  reccn2  14943  iseraltlem2  15029  iseraltlem3  15030  hash2iun1dif1  15169  binom11  15177  harmonic  15204  trireciplem  15207  geoserg  15211  pwdif  15213  pwm1geoser  15214  cvgrat  15229  fprodsplit  15310  fprodle  15340  fsumcube  15404  efzval  15445  tanhlt1  15503  tanaddlem  15509  tanadd  15510  cos01gt0  15534  absef  15540  1dvds  15614  bitsfzo  15774  bitsmod  15775  gcdmultipleOLD  15890  sqgcd  15899  lcm1  15944  coprmdvds  15987  qredeu  15992  phiprmpw  16103  coprimeprodsq  16135  pc2dvds  16205  sumhash  16222  fldivp1  16223  pcfaclem  16224  prmpwdvds  16230  prmreclem1  16242  vdwlem3  16309  vdwlem9  16315  prmop1  16364  sylow2a  18675  odadd  18901  zsssubrg  20533  zringcyg  20568  prmirredlem  20570  mulgrhm2  20576  znrrg  20642  icopnfcnv  23475  icopnfhmeo  23476  lebnumii  23499  reparphti  23530  itg2const  24270  itg2monolem3  24282  bddibl  24369  dveflem  24505  mvth  24518  dvlipcn  24520  dvivthlem1  24534  dvfsumle  24547  dvfsumabs  24549  dvfsumlem2  24553  plyconst  24725  plyeq0lem  24729  plyco  24760  0dgrb  24765  coefv0  24767  vieta1  24830  aaliou3lem2  24861  tayl0  24879  taylply2  24885  dvtaylp  24887  taylthlem2  24891  radcnvlem1  24930  abelthlem1  24948  abelthlem2  24949  abelthlem3  24950  abelthlem7  24955  abelthlem8  24956  abelthlem9  24957  efper  24994  tangtx  25020  eflogeq  25112  logdivlti  25130  logcnlem4  25155  advlogexp  25165  cxpmul2  25199  dvcxp2  25249  cxpaddle  25260  cxpeq  25265  loglesqrt  25266  relogbexp  25285  ang180lem5  25318  isosctrlem2  25324  isosctrlem3  25325  heron  25343  2efiatan  25423  dvatan  25440  leibpi  25448  birthdaylem3  25459  jensenlem2  25493  logdiflbnd  25500  harmonicbnd4  25516  lgamgulmlem2  25535  lgamcvg2  25560  ftalem5  25582  basellem2  25587  basellem5  25590  basellem8  25593  0sgm  25649  muinv  25698  chpub  25724  logfaclbnd  25726  logexprlim  25729  dchrsum2  25772  sumdchr2  25774  bposlem1  25788  bposlem2  25789  bposlem5  25792  lgsquad2lem1  25888  lgsquad3  25891  2sqlem6  25927  2sqlem8  25930  chtppilim  25979  vmadivsum  25986  dchrisumlem1  25993  dchrisum0flblem1  26012  rpvmasum2  26016  dchrisum0re  26017  dchrisum0lem2a  26021  dchrisum0lem3  26023  rpvmasum  26030  mudivsum  26034  mulogsumlem  26035  vmalogdivsum2  26042  pntrsumo1  26069  pntrlog2bndlem2  26082  pntrlog2bndlem4  26084  pntrlog2bndlem5  26085  pntibndlem2  26095  pntlemc  26099  pntlemf  26109  ostth2lem2  26138  ostth2lem3  26139  ostth2lem4  26140  ostth2  26141  ostth3  26142  ttgcontlem1  26599  axpaschlem  26654  axcontlem2  26679  axcontlem4  26681  axcontlem8  26685  nmoub3i  28478  ubthlem2  28576  htthlem  28622  nmcexi  29731  nmopcoadji  29806  branmfn  29810  rearchi  30843  ccfldextdgrr  30957  madjusmdetlem4  30995  ccatmulgnn0dir  31712  ofcccat  31713  itgexpif  31777  hashreprin  31791  circlemeth  31811  lpadlem2  31851  subfacval2  32332  cvmliftlem2  32431  snmlff  32474  sinccvglem  32813  bcprod  32868  faclimlem1  32873  faclimlem2  32874  faclim2  32878  knoppndvlem14  33762  knoppndvlem15  33763  knoppndvlem16  33764  knoppndvlem18  33766  poimirlem29  34803  poimirlem30  34804  poimirlem31  34805  poimirlem32  34806  itg2addnclem  34825  areacirclem1  34864  areacirclem4  34867  cntotbnd  34957  frlmvscadiccat  39025  oexpreposd  39059  expgcd  39063  fltnltalem  39154  3cubeslem2  39162  3cubeslem3r  39164  irrapxlem1  39299  irrapxlem4  39302  pell1qrgaplem  39350  reglogexpbas  39374  rmspecfund  39386  rmxy1  39399  rmxp1  39409  rmyp1  39410  rmxm1  39411  jm2.17a  39437  jm2.18  39465  jm2.23  39473  jm2.25  39476  jm2.16nn0  39481  relexpmulnn  39934  int-mul11d  40416  nzprmdif  40531  expgrowthi  40545  expgrowth  40547  binomcxplemdvbinom  40565  binomcxplemnotnn0  40568  sqrlearg  41709  fmul01  41741  fmul01lt1lem1  41745  0ellimcdiv  41810  dvxpaek  42105  dvnxpaek  42107  itgiccshift  42145  itgperiod  42146  itgsbtaddcnst  42147  stoweidlem11  42177  stoweidlem26  42192  stoweidlem38  42204  wallispilem4  42234  stirlinglem1  42240  stirlinglem3  42242  stirlinglem6  42245  stirlinglem7  42246  stirlinglem8  42247  stirlinglem10  42249  stirlinglem12  42251  dirkertrigeqlem3  42266  dirkertrigeq  42267  dirkercncflem1  42269  dirkercncflem2  42270  fourierdlem28  42301  fourierdlem30  42303  fourierdlem39  42312  fourierdlem47  42319  fourierdlem60  42332  fourierdlem61  42333  fourierdlem73  42345  fourierdlem83  42355  fourierdlem87  42359  etransclem14  42414  etransclem24  42424  etransclem25  42425  etransclem35  42435  smfmullem1  42947  deccarry  43392  fpprwppr  43751  fpprwpprb  43752  logblt1b  44522  nn0sumshdiglem2  44580  eenglngeehlnmlem1  44622  eenglngeehlnmlem2  44623  line2ylem  44636
  Copyright terms: Public domain W3C validator