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

Theorem mulid1d 10646
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 10627 . 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 10523  1c1 10526   · cmul 10530
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 2790  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-mulcl 10587  ax-mulcom 10589  ax-mulass 10591  ax-distr 10592  ax-1rid 10595  ax-cnre 10598
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 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7148
This theorem is referenced by:  muladd11  10798  muls1d  11088  divrec  11302  diveq1  11319  conjmul  11345  divelunit  12868  modid  13252  addmodlteq  13302  expadd  13459  leexp2r  13526  nnlesq  13556  sqoddm1div8  13592  faclbnd  13638  faclbnd2  13639  faclbnd4lem3  13643  faclbnd6  13647  facavg  13649  bcn0  13658  bcn1  13661  hashf1lem2  13802  hashfac  13804  reccn2  14941  iseraltlem2  15027  iseraltlem3  15028  hash2iun1dif1  15167  binom11  15175  harmonic  15202  trireciplem  15205  geoserg  15209  pwdif  15211  pwm1geoser  15212  cvgrat  15227  fprodsplit  15308  fprodle  15338  fsumcube  15402  efzval  15443  tanhlt1  15501  tanaddlem  15507  tanadd  15508  cos01gt0  15532  absef  15538  1dvds  15612  bitsfzo  15772  bitsmod  15773  gcdmultipleOLD  15888  sqgcd  15897  lcm1  15942  coprmdvds  15985  qredeu  15990  phiprmpw  16101  coprimeprodsq  16133  pc2dvds  16203  sumhash  16220  fldivp1  16221  pcfaclem  16222  prmpwdvds  16228  prmreclem1  16240  vdwlem3  16307  vdwlem9  16313  prmop1  16362  sylow2a  18673  odadd  18899  zsssubrg  20531  zringcyg  20566  prmirredlem  20568  mulgrhm2  20574  znrrg  20640  icopnfcnv  23473  icopnfhmeo  23474  lebnumii  23497  reparphti  23528  itg2const  24268  itg2monolem3  24280  bddibl  24367  dveflem  24503  mvth  24516  dvlipcn  24518  dvivthlem1  24532  dvfsumle  24545  dvfsumabs  24547  dvfsumlem2  24551  plyconst  24723  plyeq0lem  24727  plyco  24758  0dgrb  24763  coefv0  24765  vieta1  24828  aaliou3lem2  24859  tayl0  24877  taylply2  24883  dvtaylp  24885  taylthlem2  24889  radcnvlem1  24928  abelthlem1  24946  abelthlem2  24947  abelthlem3  24948  abelthlem7  24953  abelthlem8  24954  abelthlem9  24955  efper  24992  tangtx  25018  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  25447  birthdaylem3  25458  jensenlem2  25492  logdiflbnd  25499  harmonicbnd4  25515  lgamgulmlem2  25534  lgamcvg2  25559  ftalem5  25581  basellem2  25586  basellem5  25589  basellem8  25592  0sgm  25648  muinv  25697  chpub  25723  logfaclbnd  25725  logexprlim  25728  dchrsum2  25771  sumdchr2  25773  bposlem1  25787  bposlem2  25788  bposlem5  25791  lgsquad2lem1  25887  lgsquad3  25890  2sqlem6  25926  2sqlem8  25929  chtppilim  25978  vmadivsum  25985  dchrisumlem1  25992  dchrisum0flblem1  26011  rpvmasum2  26015  dchrisum0re  26016  dchrisum0lem2a  26020  dchrisum0lem3  26022  rpvmasum  26029  mudivsum  26033  mulogsumlem  26034  vmalogdivsum2  26041  pntrsumo1  26068  pntrlog2bndlem2  26081  pntrlog2bndlem4  26083  pntrlog2bndlem5  26084  pntibndlem2  26094  pntlemc  26098  pntlemf  26108  ostth2lem2  26137  ostth2lem3  26138  ostth2lem4  26139  ostth2  26140  ostth3  26141  ttgcontlem1  26598  axpaschlem  26653  axcontlem2  26678  axcontlem4  26680  axcontlem8  26684  nmoub3i  28477  ubthlem2  28575  htthlem  28621  nmcexi  29730  nmopcoadji  29805  branmfn  29809  rearchi  30842  ccfldextdgrr  30956  madjusmdetlem4  30994  ccatmulgnn0dir  31711  ofcccat  31712  itgexpif  31776  hashreprin  31790  circlemeth  31810  lpadlem2  31850  subfacval2  32331  cvmliftlem2  32430  snmlff  32473  sinccvglem  32812  bcprod  32867  faclimlem1  32872  faclimlem2  32873  faclim2  32877  knoppndvlem14  33761  knoppndvlem15  33762  knoppndvlem16  33763  knoppndvlem18  33765  poimirlem29  34802  poimirlem30  34803  poimirlem31  34804  poimirlem32  34805  itg2addnclem  34824  areacirclem1  34863  areacirclem4  34866  cntotbnd  34955  frlmvscadiccat  39023  oexpreposd  39057  expgcd  39061  fltnltalem  39152  3cubeslem2  39160  3cubeslem3r  39162  irrapxlem1  39297  irrapxlem4  39300  pell1qrgaplem  39348  reglogexpbas  39372  rmspecfund  39384  rmxy1  39397  rmxp1  39407  rmyp1  39408  rmxm1  39409  jm2.17a  39435  jm2.18  39463  jm2.23  39471  jm2.25  39474  jm2.16nn0  39479  relexpmulnn  39932  int-mul11d  40413  nzprmdif  40528  expgrowthi  40542  expgrowth  40544  binomcxplemdvbinom  40562  binomcxplemnotnn0  40565  sqrlearg  41705  fmul01  41737  fmul01lt1lem1  41741  0ellimcdiv  41806  dvxpaek  42101  dvnxpaek  42103  itgiccshift  42141  itgperiod  42142  itgsbtaddcnst  42143  stoweidlem11  42173  stoweidlem26  42188  stoweidlem38  42200  wallispilem4  42230  stirlinglem1  42236  stirlinglem3  42238  stirlinglem6  42241  stirlinglem7  42242  stirlinglem8  42243  stirlinglem10  42245  stirlinglem12  42247  dirkertrigeqlem3  42262  dirkertrigeq  42263  dirkercncflem1  42265  dirkercncflem2  42266  fourierdlem28  42297  fourierdlem30  42299  fourierdlem39  42308  fourierdlem47  42315  fourierdlem60  42328  fourierdlem61  42329  fourierdlem73  42341  fourierdlem83  42351  fourierdlem87  42355  etransclem14  42410  etransclem24  42420  etransclem25  42421  etransclem35  42431  smfmullem1  42943  deccarry  43388  fpprwppr  43781  fpprwpprb  43782  logblt1b  44552  nn0sumshdiglem2  44610  eenglngeehlnmlem1  44652  eenglngeehlnmlem2  44653  line2ylem  44666
  Copyright terms: Public domain W3C validator