Theorem mulid1d 9936

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

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		mulid1 9916	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 · 1) = 𝐴)

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813  1c1 9816   · cmul 9820

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-mulcl 9877  ax-mulcom 9879  ax-mulass 9881  ax-distr 9882  ax-1rid 9885  ax-cnre 9888

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552

This theorem is referenced by:  muladd11  10085  muls1d  10370  divrec  10580  diveq1  10597  conjmul  10621  divelunit  12185  modid  12557  addmodlteq  12607  expadd  12764  leexp2r  12780  nnlesq  12830  sqoddm1div8  12890  faclbnd  12939  faclbnd2  12940  faclbnd4lem3  12944  faclbnd6  12948  facavg  12950  bcn0  12959  bcn1  12962  hashf1lem2  13097  hashfac  13099  reccn2  14175  iseraltlem2  14261  iseraltlem3  14262  binom11  14403  harmonic  14430  trireciplem  14433  geoserg  14437  cvgrat  14454  fprodsplit  14535  fprodle  14566  fsumcube  14630  efzval  14671  tanhlt1  14729  tanaddlem  14735  tanadd  14736  cos01gt0  14760  absef  14766  1dvds  14834  3dvdsOLD  14891  bitsfzo  14995  bitsmod  14996  gcdmultiple  15107  sqgcd  15116  lcm1  15161  coprmdvds  15204  coprmdvdsOLD  15205  qredeu  15210  phiprmpw  15319  coprimeprodsq  15351  pc2dvds  15421  sumhash  15438  fldivp1  15439  pcfaclem  15440  prmpwdvds  15446  prmreclem1  15458  vdwlem3  15525  vdwlem9  15531  prmop1  15580  sylow2a  17857  odadd  18076  zsssubrg  19623  zringcyg  19658  prmirredlem  19660  mulgrhm2  19666  znrrg  19733  icopnfcnv  22549  icopnfhmeo  22550  lebnumii  22573  reparphti  22605  itg2const  23313  itg2monolem3  23325  bddibl  23412  dveflem  23546  mvth  23559  dvlipcn  23561  dvivthlem1  23575  dvfsumle  23588  dvfsumabs  23590  dvfsumlem2  23594  plyconst  23766  plyeq0lem  23770  plyco  23801  0dgrb  23806  coefv0  23808  vieta1  23871  aaliou3lem2  23902  tayl0  23920  taylply2  23926  dvtaylp  23928  taylthlem2  23932  radcnvlem1  23971  abelthlem1  23989  abelthlem2  23990  abelthlem3  23991  abelthlem7  23996  abelthlem8  23997  abelthlem9  23998  efper  24035  tangtx  24061  eflogeq  24152  logdivlti  24170  logcnlem4  24191  advlogexp  24201  cxpmul2  24235  dvcxp2  24282  cxpaddle  24293  cxpeq  24298  loglesqrt  24299  relogbexp  24318  ang180lem5  24343  isosctrlem2  24349  isosctrlem3  24350  heron  24365  2efiatan  24445  dvatan  24462  leibpi  24469  birthdaylem3  24480  jensenlem2  24514  logdiflbnd  24521  harmonicbnd4  24537  lgamgulmlem2  24556  lgamcvg2  24581  wilthlem2  24595  ftalem5  24603  basellem2  24608  basellem5  24611  basellem8  24614  0sgm  24670  muinv  24719  chpub  24745  logfaclbnd  24747  logexprlim  24750  dchrsum2  24793  sumdchr2  24795  bposlem1  24809  bposlem2  24810  bposlem5  24813  lgsquad2lem1  24909  lgsquad3  24912  2sqlem6  24948  2sqlem8  24951  chtppilim  24964  vmadivsum  24971  dchrisumlem1  24978  dchrisum0flblem1  24997  rpvmasum2  25001  dchrisum0re  25002  dchrisum0lem2a  25006  dchrisum0lem3  25008  rpvmasum  25015  mudivsum  25019  mulogsumlem  25020  vmalogdivsum2  25027  pntrsumo1  25054  pntrlog2bndlem2  25067  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntibndlem2  25080  pntlemc  25084  pntlemf  25094  ostth2lem2  25123  ostth2lem3  25124  ostth2lem4  25125  ostth2  25126  ostth3  25127  ttgcontlem1  25565  axpaschlem  25620  axcontlem2  25645  axcontlem4  25647  axcontlem8  25651  nmoub3i  27012  ubthlem2  27111  htthlem  27158  nmcexi  28269  nmopcoadji  28344  branmfn  28348  rearchi  29173  madjusmdetlem4  29224  ccatmulgnn0dir  29945  ofcccat  29946  subfacval2  30423  cvmliftlem2  30522  snmlff  30565  sinccvglem  30820  bcprod  30877  faclimlem1  30882  faclimlem2  30883  faclim2  30887  knoppndvlem14  31686  knoppndvlem15  31687  knoppndvlem16  31688  knoppndvlem18  31690  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  itg2addnclem  32631  areacirclem1  32670  areacirclem4  32673  cntotbnd  32765  irrapxlem1  36404  irrapxlem4  36407  pell1qrgaplem  36455  reglogexpbas  36479  rmspecsqrtnqOLD  36489  rmspecfund  36492  rmxy1  36505  rmxp1  36515  rmyp1  36516  rmxm1  36517  jm2.17a  36545  jm2.18  36573  jm2.23  36581  jm2.25  36584  jm2.16nn0  36589  relexpmulnn  37020  int-mul11d  37507  nzprmdif  37540  expgrowthi  37554  expgrowth  37556  binomcxplemdvbinom  37574  binomcxplemnotnn0  37577  sqrlearg  38627  fmul01  38647  fmul01lt1lem1  38651  0ellimcdiv  38716  dvxpaek  38830  dvnxpaek  38832  itgiccshift  38872  itgperiod  38873  itgsbtaddcnst  38874  stoweidlem11  38904  stoweidlem26  38919  stoweidlem38  38931  wallispilem4  38961  stirlinglem1  38967  stirlinglem3  38969  stirlinglem6  38972  stirlinglem7  38973  stirlinglem8  38974  stirlinglem10  38976  stirlinglem12  38978  dirkertrigeqlem3  38993  dirkertrigeq  38994  dirkercncflem1  38996  dirkercncflem2  38997  fourierdlem28  39028  fourierdlem30  39030  fourierdlem39  39039  fourierdlem47  39046  fourierdlem60  39059  fourierdlem61  39060  fourierdlem73  39072  fourierdlem83  39082  fourierdlem87  39086  etransclem14  39141  etransclem24  39151  etransclem25  39152  etransclem35  39162  smfmullem1  39676  deccarry  39941  pwdif  40039  pwm1geoserALT  40040  logblt1b  42156  nn0sumshdiglem2  42214