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

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  (class class class)co 7135  ℂ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 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  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 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138

This theorem is referenced by:  muladd11  10799  muls1d  11089  divrec  11303  diveq1  11320  conjmul  11346  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  14945  iseraltlem2  15031  iseraltlem3  15032  hash2iun1dif1  15171  binom11  15179  harmonic  15206  trireciplem  15209  geoserg  15213  pwdif  15215  pwm1geoser  15216  cvgrat  15231  fprodsplit  15312  fprodle  15342  fsumcube  15406  efzval  15447  tanhlt1  15505  tanaddlem  15511  tanadd  15512  cos01gt0  15536  absef  15542  1dvds  15616  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  18736  odadd  18963  zsssubrg  20149  zringcyg  20184  prmirredlem  20186  mulgrhm2  20192  znrrg  20257  icopnfcnv  23547  icopnfhmeo  23548  lebnumii  23571  reparphti  23602  itg2const  24344  itg2monolem3  24356  bddibl  24443  dveflem  24582  mvth  24595  dvlipcn  24597  dvivthlem1  24611  dvfsumle  24624  dvfsumabs  24626  dvfsumlem2  24630  plyconst  24803  plyeq0lem  24807  plyco  24838  0dgrb  24843  coefv0  24845  vieta1  24908  aaliou3lem2  24939  tayl0  24957  taylply2  24963  dvtaylp  24965  taylthlem2  24969  radcnvlem1  25008  abelthlem1  25026  abelthlem2  25027  abelthlem3  25028  abelthlem7  25033  abelthlem8  25034  abelthlem9  25035  efper  25072  tangtx  25098  eflogeq  25193  logdivlti  25211  logcnlem4  25236  advlogexp  25246  cxpmul2  25280  dvcxp2  25330  cxpaddle  25341  cxpeq  25346  loglesqrt  25347  relogbexp  25366  ang180lem5  25399  isosctrlem2  25405  isosctrlem3  25406  heron  25424  2efiatan  25504  dvatan  25521  leibpi  25528  birthdaylem3  25539  jensenlem2  25573  logdiflbnd  25580  harmonicbnd4  25596  lgamgulmlem2  25615  lgamcvg2  25640  ftalem5  25662  basellem2  25667  basellem5  25670  basellem8  25673  0sgm  25729  muinv  25778  chpub  25804  logfaclbnd  25806  logexprlim  25809  dchrsum2  25852  sumdchr2  25854  bposlem1  25868  bposlem2  25869  bposlem5  25872  lgsquad2lem1  25968  lgsquad3  25971  2sqlem6  26007  2sqlem8  26010  chtppilim  26059  vmadivsum  26066  dchrisumlem1  26073  dchrisum0flblem1  26092  rpvmasum2  26096  dchrisum0re  26097  dchrisum0lem2a  26101  dchrisum0lem3  26103  rpvmasum  26110  mudivsum  26114  mulogsumlem  26115  vmalogdivsum2  26122  pntrsumo1  26149  pntrlog2bndlem2  26162  pntrlog2bndlem4  26164  pntrlog2bndlem5  26165  pntibndlem2  26175  pntlemc  26179  pntlemf  26189  ostth2lem2  26218  ostth2lem3  26219  ostth2lem4  26220  ostth2  26221  ostth3  26222  ttgcontlem1  26679  axpaschlem  26734  axcontlem2  26759  axcontlem4  26761  axcontlem8  26765  nmoub3i  28556  ubthlem2  28654  htthlem  28700  nmcexi  29809  nmopcoadji  29884  branmfn  29888  rearchi  30966  ccfldextdgrr  31145  madjusmdetlem4  31183  ccatmulgnn0dir  31922  ofcccat  31923  itgexpif  31987  hashreprin  32001  circlemeth  32021  lpadlem2  32061  subfacval2  32547  cvmliftlem2  32646  snmlff  32689  sinccvglem  33028  bcprod  33083  faclimlem1  33088  faclimlem2  33089  faclim2  33093  knoppndvlem14  33977  knoppndvlem15  33978  knoppndvlem16  33979  knoppndvlem18  33981  poimirlem29  35086  poimirlem30  35087  poimirlem31  35088  poimirlem32  35089  itg2addnclem  35108  areacirclem1  35145  areacirclem4  35148  cntotbnd  35234  lcmineqlem11  39327  lcmineqlem12  39328  2ap1caineq  39349  frlmvscadiccat  39440  oexpreposd  39487  expgcd  39491  fltnltalem  39618  3cubeslem2  39626  3cubeslem3r  39628  irrapxlem1  39763  irrapxlem4  39766  pell1qrgaplem  39814  reglogexpbas  39838  rmspecfund  39850  rmxy1  39863  rmxp1  39873  rmyp1  39874  rmxm1  39875  jm2.17a  39901  jm2.18  39929  jm2.23  39937  jm2.25  39940  jm2.16nn0  39945  relexpmulnn  40410  int-mul11d  40888  nzprmdif  41023  expgrowthi  41037  expgrowth  41039  binomcxplemdvbinom  41057  binomcxplemnotnn0  41060  sqrlearg  42190  fmul01  42222  fmul01lt1lem1  42226  0ellimcdiv  42291  dvxpaek  42582  dvnxpaek  42584  itgiccshift  42622  itgperiod  42623  itgsbtaddcnst  42624  stoweidlem11  42653  stoweidlem26  42668  stoweidlem38  42680  wallispilem4  42710  stirlinglem1  42716  stirlinglem3  42718  stirlinglem6  42721  stirlinglem7  42722  stirlinglem8  42723  stirlinglem10  42725  stirlinglem12  42727  dirkertrigeqlem3  42742  dirkertrigeq  42743  dirkercncflem1  42745  dirkercncflem2  42746  fourierdlem28  42777  fourierdlem30  42779  fourierdlem39  42788  fourierdlem47  42795  fourierdlem60  42808  fourierdlem61  42809  fourierdlem73  42821  fourierdlem83  42831  fourierdlem87  42835  etransclem14  42890  etransclem24  42900  etransclem25  42901  etransclem35  42911  smfmullem1  43423  deccarry  43868  fpprwppr  44257  fpprwpprb  44258  logblt1b  44978  nn0sumshdiglem2  45036  itcovalpclem2  45085  itcovalt2lem1  45089  eenglngeehlnmlem1  45151  eenglngeehlnmlem2  45152  line2ylem  45165