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

Theorem mulid1d 10645
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 10626 . 2 (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
31, 2syl 17 1 (𝜑 → (𝐴 · 1) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2115  (class class class)co 7140  cc 10522  1c1 10525   · cmul 10529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-resscn 10581  ax-1cn 10582  ax-icn 10583  ax-addcl 10584  ax-mulcl 10586  ax-mulcom 10588  ax-mulass 10590  ax-distr 10591  ax-1rid 10594  ax-cnre 10597
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3137  df-rex 3138  df-rab 3141  df-v 3481  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-sn 4549  df-pr 4551  df-op 4555  df-uni 4822  df-br 5050  df-iota 6297  df-fv 6346  df-ov 7143
This theorem is referenced by:  muladd11  10797  muls1d  11087  divrec  11301  diveq1  11318  conjmul  11344  divelunit  12872  modid  13259  addmodlteq  13309  expadd  13467  leexp2r  13534  nnlesq  13564  sqoddm1div8  13600  faclbnd  13646  faclbnd2  13647  faclbnd4lem3  13651  faclbnd6  13655  facavg  13657  bcn0  13666  bcn1  13669  hashf1lem2  13810  hashfac  13812  reccn2  14944  iseraltlem2  15030  iseraltlem3  15031  hash2iun1dif1  15170  binom11  15178  harmonic  15205  trireciplem  15208  geoserg  15212  pwdif  15214  pwm1geoser  15215  cvgrat  15230  fprodsplit  15311  fprodle  15341  fsumcube  15405  efzval  15446  tanhlt1  15504  tanaddlem  15510  tanadd  15511  cos01gt0  15535  absef  15541  1dvds  15615  bitsfzo  15773  bitsmod  15774  gcdmultipleOLD  15889  sqgcd  15898  lcm1  15943  coprmdvds  15986  qredeu  15991  phiprmpw  16102  coprimeprodsq  16134  pc2dvds  16204  sumhash  16221  fldivp1  16222  pcfaclem  16223  prmpwdvds  16229  prmreclem1  16241  vdwlem3  16308  vdwlem9  16314  prmop1  16363  sylow2a  18735  odadd  18961  zsssubrg  20591  zringcyg  20626  prmirredlem  20628  mulgrhm2  20634  znrrg  20700  icopnfcnv  23538  icopnfhmeo  23539  lebnumii  23562  reparphti  23593  itg2const  24335  itg2monolem3  24347  bddibl  24434  dveflem  24573  mvth  24586  dvlipcn  24588  dvivthlem1  24602  dvfsumle  24615  dvfsumabs  24617  dvfsumlem2  24621  plyconst  24794  plyeq0lem  24798  plyco  24829  0dgrb  24834  coefv0  24836  vieta1  24899  aaliou3lem2  24930  tayl0  24948  taylply2  24954  dvtaylp  24956  taylthlem2  24960  radcnvlem1  24999  abelthlem1  25017  abelthlem2  25018  abelthlem3  25019  abelthlem7  25024  abelthlem8  25025  abelthlem9  25026  efper  25063  tangtx  25089  eflogeq  25184  logdivlti  25202  logcnlem4  25227  advlogexp  25237  cxpmul2  25271  dvcxp2  25321  cxpaddle  25332  cxpeq  25337  loglesqrt  25338  relogbexp  25357  ang180lem5  25390  isosctrlem2  25396  isosctrlem3  25397  heron  25415  2efiatan  25495  dvatan  25512  leibpi  25519  birthdaylem3  25530  jensenlem2  25564  logdiflbnd  25571  harmonicbnd4  25587  lgamgulmlem2  25606  lgamcvg2  25631  ftalem5  25653  basellem2  25658  basellem5  25661  basellem8  25664  0sgm  25720  muinv  25769  chpub  25795  logfaclbnd  25797  logexprlim  25800  dchrsum2  25843  sumdchr2  25845  bposlem1  25859  bposlem2  25860  bposlem5  25863  lgsquad2lem1  25959  lgsquad3  25962  2sqlem6  25998  2sqlem8  26001  chtppilim  26050  vmadivsum  26057  dchrisumlem1  26064  dchrisum0flblem1  26083  rpvmasum2  26087  dchrisum0re  26088  dchrisum0lem2a  26092  dchrisum0lem3  26094  rpvmasum  26101  mudivsum  26105  mulogsumlem  26106  vmalogdivsum2  26113  pntrsumo1  26140  pntrlog2bndlem2  26153  pntrlog2bndlem4  26155  pntrlog2bndlem5  26156  pntibndlem2  26166  pntlemc  26170  pntlemf  26180  ostth2lem2  26209  ostth2lem3  26210  ostth2lem4  26211  ostth2  26212  ostth3  26213  ttgcontlem1  26670  axpaschlem  26725  axcontlem2  26750  axcontlem4  26752  axcontlem8  26756  nmoub3i  28547  ubthlem2  28645  htthlem  28691  nmcexi  29800  nmopcoadji  29875  branmfn  29879  rearchi  30935  ccfldextdgrr  31080  madjusmdetlem4  31118  ccatmulgnn0dir  31832  ofcccat  31833  itgexpif  31897  hashreprin  31911  circlemeth  31931  lpadlem2  31971  subfacval2  32454  cvmliftlem2  32553  snmlff  32596  sinccvglem  32935  bcprod  32990  faclimlem1  32995  faclimlem2  32996  faclim2  33000  knoppndvlem14  33884  knoppndvlem15  33885  knoppndvlem16  33886  knoppndvlem18  33888  poimirlem29  34991  poimirlem30  34992  poimirlem31  34993  poimirlem32  34994  itg2addnclem  35013  areacirclem1  35050  areacirclem4  35053  cntotbnd  35139  lcmineqlem11  39228  lcmineqlem12  39229  frlmvscadiccat  39311  oexpreposd  39353  expgcd  39357  fltnltalem  39465  3cubeslem2  39473  3cubeslem3r  39475  irrapxlem1  39610  irrapxlem4  39613  pell1qrgaplem  39661  reglogexpbas  39685  rmspecfund  39697  rmxy1  39710  rmxp1  39720  rmyp1  39721  rmxm1  39722  jm2.17a  39748  jm2.18  39776  jm2.23  39784  jm2.25  39787  jm2.16nn0  39792  relexpmulnn  40257  int-mul11d  40738  nzprmdif  40874  expgrowthi  40888  expgrowth  40890  binomcxplemdvbinom  40908  binomcxplemnotnn0  40911  sqrlearg  42047  fmul01  42079  fmul01lt1lem1  42083  0ellimcdiv  42148  dvxpaek  42439  dvnxpaek  42441  itgiccshift  42479  itgperiod  42480  itgsbtaddcnst  42481  stoweidlem11  42510  stoweidlem26  42525  stoweidlem38  42537  wallispilem4  42567  stirlinglem1  42573  stirlinglem3  42575  stirlinglem6  42578  stirlinglem7  42579  stirlinglem8  42580  stirlinglem10  42582  stirlinglem12  42584  dirkertrigeqlem3  42599  dirkertrigeq  42600  dirkercncflem1  42602  dirkercncflem2  42603  fourierdlem28  42634  fourierdlem30  42636  fourierdlem39  42645  fourierdlem47  42652  fourierdlem60  42665  fourierdlem61  42666  fourierdlem73  42678  fourierdlem83  42688  fourierdlem87  42692  etransclem14  42747  etransclem24  42757  etransclem25  42758  etransclem35  42768  smfmullem1  43280  deccarry  43725  fpprwppr  44114  fpprwpprb  44115  logblt1b  44834  nn0sumshdiglem2  44892  itcovalpclem2  44930  itcovalt2lem1  44934  eenglngeehlnmlem1  44996  eenglngeehlnmlem2  44997  line2ylem  45010
  Copyright terms: Public domain W3C validator