Theorem mulid1d 11001

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 10982	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 · 1) = 𝐴)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  (class class class)co 7284  ℂcc 10878  1c1 10881   · cmul 10885

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 2710  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-mulcl 10942  ax-mulcom 10944  ax-mulass 10946  ax-distr 10947  ax-1rid 10950  ax-cnre 10953

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287

This theorem is referenced by:  muladd11  11154  muls1d  11444  divrec  11658  diveq1  11675  conjmul  11701  divelunit  13235  modid  13625  addmodlteq  13675  expadd  13834  leexp2r  13901  nnlesq  13931  sqoddm1div8  13967  faclbnd  14013  faclbnd2  14014  faclbnd4lem3  14018  faclbnd6  14022  facavg  14024  bcn0  14033  bcn1  14036  hashf1lem2  14179  hashfac  14181  reccn2  15315  iseraltlem2  15403  iseraltlem3  15404  hash2iun1dif1  15545  binom11  15553  harmonic  15580  trireciplem  15583  geoserg  15587  pwdif  15589  pwm1geoser  15590  cvgrat  15604  fprodsplit  15685  fprodle  15715  fsumcube  15779  efzval  15820  tanhlt1  15878  tanaddlem  15884  tanadd  15885  cos01gt0  15909  absef  15915  1dvds  15989  bitsfzo  16151  bitsmod  16152  gcdmultipleOLD  16269  sqgcd  16279  lcm1  16324  coprmdvds  16367  qredeu  16372  phiprmpw  16486  coprimeprodsq  16518  pc2dvds  16589  sumhash  16606  fldivp1  16607  pcfaclem  16608  prmpwdvds  16614  prmreclem1  16626  vdwlem3  16693  vdwlem9  16699  prmop1  16748  sylow2a  19233  odadd  19460  zsssubrg  20665  zringcyg  20700  prmirredlem  20703  mulgrhm2  20709  znrrg  20782  mhppwdeg  21349  icopnfcnv  24114  icopnfhmeo  24115  lebnumii  24138  reparphti  24169  itg2const  24914  itg2monolem3  24926  bddibl  25013  dveflem  25152  mvth  25165  dvlipcn  25167  dvivthlem1  25181  dvfsumle  25194  dvfsumabs  25196  dvfsumlem2  25200  plyconst  25376  plyeq0lem  25380  plyco  25411  0dgrb  25416  coefv0  25418  vieta1  25481  aaliou3lem2  25512  tayl0  25530  taylply2  25536  dvtaylp  25538  taylthlem2  25542  radcnvlem1  25581  abelthlem1  25599  abelthlem2  25600  abelthlem3  25601  abelthlem7  25606  abelthlem8  25607  abelthlem9  25608  efper  25645  tangtx  25671  eflogeq  25766  logdivlti  25784  logcnlem4  25809  advlogexp  25819  cxpmul2  25853  dvcxp2  25903  cxpaddle  25914  cxpeq  25919  loglesqrt  25920  relogbexp  25939  ang180lem5  25972  isosctrlem2  25978  isosctrlem3  25979  heron  25997  2efiatan  26077  dvatan  26094  leibpi  26101  birthdaylem3  26112  jensenlem2  26146  logdiflbnd  26153  harmonicbnd4  26169  lgamgulmlem2  26188  lgamcvg2  26213  ftalem5  26235  basellem2  26240  basellem5  26243  basellem8  26246  0sgm  26302  muinv  26351  chpub  26377  logfaclbnd  26379  logexprlim  26382  dchrsum2  26425  sumdchr2  26427  bposlem1  26441  bposlem2  26442  bposlem5  26445  lgsquad2lem1  26541  lgsquad3  26544  2sqlem6  26580  2sqlem8  26583  chtppilim  26632  vmadivsum  26639  dchrisumlem1  26646  dchrisum0flblem1  26665  rpvmasum2  26669  dchrisum0re  26670  dchrisum0lem2a  26674  dchrisum0lem3  26676  rpvmasum  26683  mudivsum  26687  mulogsumlem  26688  vmalogdivsum2  26695  pntrsumo1  26722  pntrlog2bndlem2  26735  pntrlog2bndlem4  26737  pntrlog2bndlem5  26738  pntibndlem2  26748  pntlemc  26752  pntlemf  26762  ostth2lem2  26791  ostth2lem3  26792  ostth2lem4  26793  ostth2  26794  ostth3  26795  ttgcontlem1  27261  axpaschlem  27317  axcontlem2  27342  axcontlem4  27344  axcontlem8  27348  nmoub3i  29144  ubthlem2  29242  htthlem  29288  nmcexi  30397  nmopcoadji  30472  branmfn  30476  rearchi  31555  ccfldextdgrr  31751  madjusmdetlem4  31789  ccatmulgnn0dir  32530  ofcccat  32531  itgexpif  32595  hashreprin  32609  circlemeth  32629  lpadlem2  32669  subfacval2  33158  cvmliftlem2  33257  snmlff  33300  sinccvglem  33639  bcprod  33713  faclimlem1  33718  faclimlem2  33719  faclim2  33723  knoppndvlem14  34714  knoppndvlem15  34715  knoppndvlem16  34716  knoppndvlem18  34718  poimirlem29  35815  poimirlem30  35816  poimirlem31  35817  poimirlem32  35818  itg2addnclem  35837  areacirclem1  35874  areacirclem4  35877  cntotbnd  35963  lcmineqlem11  40054  lcmineqlem12  40055  aks4d1p1p7  40089  aks4d1p8d2  40100  2ap1caineq  40108  sticksstones10  40118  sticksstones12a  40120  frlmvscadiccat  40244  oexpreposd  40328  expgcd  40341  fltnltalem  40506  3cubeslem2  40514  3cubeslem3r  40516  irrapxlem1  40651  irrapxlem4  40654  pell1qrgaplem  40702  reglogexpbas  40726  rmspecfund  40738  rmxy1  40751  rmxp1  40761  rmyp1  40762  rmxm1  40763  jm2.17a  40789  jm2.18  40817  jm2.23  40825  jm2.25  40828  jm2.16nn0  40833  relexpmulnn  41324  int-mul11d  41800  nzprmdif  41944  expgrowthi  41958  expgrowth  41960  binomcxplemdvbinom  41978  binomcxplemnotnn0  41981  sqrlearg  43098  fmul01  43128  fmul01lt1lem1  43132  0ellimcdiv  43197  dvxpaek  43488  dvnxpaek  43490  itgiccshift  43528  itgperiod  43529  itgsbtaddcnst  43530  stoweidlem11  43559  stoweidlem26  43574  stoweidlem38  43586  wallispilem4  43616  stirlinglem1  43622  stirlinglem3  43624  stirlinglem6  43627  stirlinglem7  43628  stirlinglem8  43629  stirlinglem10  43631  stirlinglem12  43633  dirkertrigeqlem3  43648  dirkertrigeq  43649  dirkercncflem1  43651  dirkercncflem2  43652  fourierdlem28  43683  fourierdlem30  43685  fourierdlem39  43694  fourierdlem47  43701  fourierdlem60  43714  fourierdlem61  43715  fourierdlem73  43727  fourierdlem83  43737  fourierdlem87  43741  etransclem14  43796  etransclem24  43806  etransclem25  43807  etransclem35  43817  smfmullem1  44336  deccarry  44814  fpprwppr  45202  fpprwpprb  45203  logblt1b  45921  nn0sumshdiglem2  45979  itcovalpclem2  46028  itcovalt2lem1  46032  eenglngeehlnmlem1  46094  eenglngeehlnmlem2  46095  line2ylem  46108