Theorem mulid1d 10057

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

Syntax hints:   → wi 4   = wceq 1483   ∈ wcel 1990  (class class class)co 6650  ℂcc 9934  1c1 9937   · cmul 9941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-mulcl 9998  ax-mulcom 10000  ax-mulass 10002  ax-distr 10003  ax-1rid 10006  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by:  muladd11  10206  muls1d  10491  divrec  10701  diveq1  10718  conjmul  10742  divelunit  12314  modid  12695  addmodlteq  12745  expadd  12902  leexp2r  12918  nnlesq  12968  sqoddm1div8  13028  faclbnd  13077  faclbnd2  13078  faclbnd4lem3  13082  faclbnd6  13086  facavg  13088  bcn0  13097  bcn1  13100  hashf1lem2  13240  hashfac  13242  reccn2  14327  iseraltlem2  14413  iseraltlem3  14414  hash2iun1dif1  14556  binom11  14564  harmonic  14591  trireciplem  14594  geoserg  14598  cvgrat  14615  fprodsplit  14696  fprodle  14727  fsumcube  14791  efzval  14832  tanhlt1  14890  tanaddlem  14896  tanadd  14897  cos01gt0  14921  absef  14927  1dvds  14996  3dvdsOLD  15053  bitsfzo  15157  bitsmod  15158  gcdmultiple  15269  sqgcd  15278  lcm1  15323  coprmdvds  15366  coprmdvdsOLD  15367  qredeu  15372  phiprmpw  15481  coprimeprodsq  15513  pc2dvds  15583  sumhash  15600  fldivp1  15601  pcfaclem  15602  prmpwdvds  15608  prmreclem1  15620  vdwlem3  15687  vdwlem9  15693  prmop1  15742  sylow2a  18034  odadd  18253  zsssubrg  19804  zringcyg  19839  prmirredlem  19841  mulgrhm2  19847  znrrg  19914  icopnfcnv  22741  icopnfhmeo  22742  lebnumii  22765  reparphti  22797  itg2const  23507  itg2monolem3  23519  bddibl  23606  dveflem  23742  mvth  23755  dvlipcn  23757  dvivthlem1  23771  dvfsumle  23784  dvfsumabs  23786  dvfsumlem2  23790  plyconst  23962  plyeq0lem  23966  plyco  23997  0dgrb  24002  coefv0  24004  vieta1  24067  aaliou3lem2  24098  tayl0  24116  taylply2  24122  dvtaylp  24124  taylthlem2  24128  radcnvlem1  24167  abelthlem1  24185  abelthlem2  24186  abelthlem3  24187  abelthlem7  24192  abelthlem8  24193  abelthlem9  24194  efper  24231  tangtx  24257  eflogeq  24348  logdivlti  24366  logcnlem4  24391  advlogexp  24401  cxpmul2  24435  dvcxp2  24482  cxpaddle  24493  cxpeq  24498  loglesqrt  24499  relogbexp  24518  ang180lem5  24543  isosctrlem2  24549  isosctrlem3  24550  heron  24565  2efiatan  24645  dvatan  24662  leibpi  24669  birthdaylem3  24680  jensenlem2  24714  logdiflbnd  24721  harmonicbnd4  24737  lgamgulmlem2  24756  lgamcvg2  24781  wilthlem2  24795  ftalem5  24803  basellem2  24808  basellem5  24811  basellem8  24814  0sgm  24870  muinv  24919  chpub  24945  logfaclbnd  24947  logexprlim  24950  dchrsum2  24993  sumdchr2  24995  bposlem1  25009  bposlem2  25010  bposlem5  25013  lgsquad2lem1  25109  lgsquad3  25112  2sqlem6  25148  2sqlem8  25151  chtppilim  25164  vmadivsum  25171  dchrisumlem1  25178  dchrisum0flblem1  25197  rpvmasum2  25201  dchrisum0re  25202  dchrisum0lem2a  25206  dchrisum0lem3  25208  rpvmasum  25215  mudivsum  25219  mulogsumlem  25220  vmalogdivsum2  25227  pntrsumo1  25254  pntrlog2bndlem2  25267  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntibndlem2  25280  pntlemc  25284  pntlemf  25294  ostth2lem2  25323  ostth2lem3  25324  ostth2lem4  25325  ostth2  25326  ostth3  25327  ttgcontlem1  25765  axpaschlem  25820  axcontlem2  25845  axcontlem4  25847  axcontlem8  25851  nmoub3i  27628  ubthlem2  27727  htthlem  27774  nmcexi  28885  nmopcoadji  28960  branmfn  28964  rearchi  29842  madjusmdetlem4  29896  ccatmulgnn0dir  30619  ofcccat  30620  itgexpif  30684  hashreprin  30698  circlemeth  30718  subfacval2  31169  cvmliftlem2  31268  snmlff  31311  sinccvglem  31566  bcprod  31624  faclimlem1  31629  faclimlem2  31630  faclim2  31634  knoppndvlem14  32516  knoppndvlem15  32517  knoppndvlem16  32518  knoppndvlem18  32520  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  itg2addnclem  33461  areacirclem1  33500  areacirclem4  33503  cntotbnd  33595  irrapxlem1  37386  irrapxlem4  37389  pell1qrgaplem  37437  reglogexpbas  37461  rmspecsqrtnqOLD  37471  rmspecfund  37474  rmxy1  37487  rmxp1  37497  rmyp1  37498  rmxm1  37499  jm2.17a  37527  jm2.18  37555  jm2.23  37563  jm2.25  37566  jm2.16nn0  37571  relexpmulnn  38001  int-mul11d  38485  nzprmdif  38518  expgrowthi  38532  expgrowth  38534  binomcxplemdvbinom  38552  binomcxplemnotnn0  38555  sqrlearg  39780  fmul01  39812  fmul01lt1lem1  39816  0ellimcdiv  39881  dvxpaek  40155  dvnxpaek  40157  itgiccshift  40196  itgperiod  40197  itgsbtaddcnst  40198  stoweidlem11  40228  stoweidlem26  40243  stoweidlem38  40255  wallispilem4  40285  stirlinglem1  40291  stirlinglem3  40293  stirlinglem6  40296  stirlinglem7  40297  stirlinglem8  40298  stirlinglem10  40300  stirlinglem12  40302  dirkertrigeqlem3  40317  dirkertrigeq  40318  dirkercncflem1  40320  dirkercncflem2  40321  fourierdlem28  40352  fourierdlem30  40354  fourierdlem39  40363  fourierdlem47  40370  fourierdlem60  40383  fourierdlem61  40384  fourierdlem73  40396  fourierdlem83  40406  fourierdlem87  40410  etransclem14  40465  etransclem24  40475  etransclem25  40476  etransclem35  40486  smfmullem1  40998  deccarry  41321  pwdif  41501  pwm1geoserALT  41502  logblt1b  42358  nn0sumshdiglem2  42416