Theorem mulid1d 10923

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800  1c1 10803   · cmul 10807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-mulcl 10864  ax-mulcom 10866  ax-mulass 10868  ax-distr 10869  ax-1rid 10872  ax-cnre 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258

This theorem is referenced by:  muladd11  11075  muls1d  11365  divrec  11579  diveq1  11596  conjmul  11622  divelunit  13155  modid  13544  addmodlteq  13594  expadd  13753  leexp2r  13820  nnlesq  13850  sqoddm1div8  13886  faclbnd  13932  faclbnd2  13933  faclbnd4lem3  13937  faclbnd6  13941  facavg  13943  bcn0  13952  bcn1  13955  hashf1lem2  14098  hashfac  14100  reccn2  15234  iseraltlem2  15322  iseraltlem3  15323  hash2iun1dif1  15464  binom11  15472  harmonic  15499  trireciplem  15502  geoserg  15506  pwdif  15508  pwm1geoser  15509  cvgrat  15523  fprodsplit  15604  fprodle  15634  fsumcube  15698  efzval  15739  tanhlt1  15797  tanaddlem  15803  tanadd  15804  cos01gt0  15828  absef  15834  1dvds  15908  bitsfzo  16070  bitsmod  16071  gcdmultipleOLD  16188  sqgcd  16198  lcm1  16243  coprmdvds  16286  qredeu  16291  phiprmpw  16405  coprimeprodsq  16437  pc2dvds  16508  sumhash  16525  fldivp1  16526  pcfaclem  16527  prmpwdvds  16533  prmreclem1  16545  vdwlem3  16612  vdwlem9  16618  prmop1  16667  sylow2a  19139  odadd  19366  zsssubrg  20568  zringcyg  20603  prmirredlem  20606  mulgrhm2  20612  znrrg  20685  mhppwdeg  21250  icopnfcnv  24011  icopnfhmeo  24012  lebnumii  24035  reparphti  24066  itg2const  24810  itg2monolem3  24822  bddibl  24909  dveflem  25048  mvth  25061  dvlipcn  25063  dvivthlem1  25077  dvfsumle  25090  dvfsumabs  25092  dvfsumlem2  25096  plyconst  25272  plyeq0lem  25276  plyco  25307  0dgrb  25312  coefv0  25314  vieta1  25377  aaliou3lem2  25408  tayl0  25426  taylply2  25432  dvtaylp  25434  taylthlem2  25438  radcnvlem1  25477  abelthlem1  25495  abelthlem2  25496  abelthlem3  25497  abelthlem7  25502  abelthlem8  25503  abelthlem9  25504  efper  25541  tangtx  25567  eflogeq  25662  logdivlti  25680  logcnlem4  25705  advlogexp  25715  cxpmul2  25749  dvcxp2  25799  cxpaddle  25810  cxpeq  25815  loglesqrt  25816  relogbexp  25835  ang180lem5  25868  isosctrlem2  25874  isosctrlem3  25875  heron  25893  2efiatan  25973  dvatan  25990  leibpi  25997  birthdaylem3  26008  jensenlem2  26042  logdiflbnd  26049  harmonicbnd4  26065  lgamgulmlem2  26084  lgamcvg2  26109  ftalem5  26131  basellem2  26136  basellem5  26139  basellem8  26142  0sgm  26198  muinv  26247  chpub  26273  logfaclbnd  26275  logexprlim  26278  dchrsum2  26321  sumdchr2  26323  bposlem1  26337  bposlem2  26338  bposlem5  26341  lgsquad2lem1  26437  lgsquad3  26440  2sqlem6  26476  2sqlem8  26479  chtppilim  26528  vmadivsum  26535  dchrisumlem1  26542  dchrisum0flblem1  26561  rpvmasum2  26565  dchrisum0re  26566  dchrisum0lem2a  26570  dchrisum0lem3  26572  rpvmasum  26579  mudivsum  26583  mulogsumlem  26584  vmalogdivsum2  26591  pntrsumo1  26618  pntrlog2bndlem2  26631  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  pntibndlem2  26644  pntlemc  26648  pntlemf  26658  ostth2lem2  26687  ostth2lem3  26688  ostth2lem4  26689  ostth2  26690  ostth3  26691  ttgcontlem1  27155  axpaschlem  27211  axcontlem2  27236  axcontlem4  27238  axcontlem8  27242  nmoub3i  29036  ubthlem2  29134  htthlem  29180  nmcexi  30289  nmopcoadji  30364  branmfn  30368  rearchi  31448  ccfldextdgrr  31644  madjusmdetlem4  31682  ccatmulgnn0dir  32421  ofcccat  32422  itgexpif  32486  hashreprin  32500  circlemeth  32520  lpadlem2  32560  subfacval2  33049  cvmliftlem2  33148  snmlff  33191  sinccvglem  33530  bcprod  33610  faclimlem1  33615  faclimlem2  33616  faclim2  33620  knoppndvlem14  34632  knoppndvlem15  34633  knoppndvlem16  34634  knoppndvlem18  34636  poimirlem29  35733  poimirlem30  35734  poimirlem31  35735  poimirlem32  35736  itg2addnclem  35755  areacirclem1  35792  areacirclem4  35795  cntotbnd  35881  lcmineqlem11  39975  lcmineqlem12  39976  aks4d1p1p7  40010  aks4d1p8d2  40021  2ap1caineq  40029  sticksstones10  40039  sticksstones12a  40041  frlmvscadiccat  40163  oexpreposd  40242  expgcd  40255  fltnltalem  40415  3cubeslem2  40423  3cubeslem3r  40425  irrapxlem1  40560  irrapxlem4  40563  pell1qrgaplem  40611  reglogexpbas  40635  rmspecfund  40647  rmxy1  40660  rmxp1  40670  rmyp1  40671  rmxm1  40672  jm2.17a  40698  jm2.18  40726  jm2.23  40734  jm2.25  40737  jm2.16nn0  40742  relexpmulnn  41206  int-mul11d  41682  nzprmdif  41826  expgrowthi  41840  expgrowth  41842  binomcxplemdvbinom  41860  binomcxplemnotnn0  41863  sqrlearg  42981  fmul01  43011  fmul01lt1lem1  43015  0ellimcdiv  43080  dvxpaek  43371  dvnxpaek  43373  itgiccshift  43411  itgperiod  43412  itgsbtaddcnst  43413  stoweidlem11  43442  stoweidlem26  43457  stoweidlem38  43469  wallispilem4  43499  stirlinglem1  43505  stirlinglem3  43507  stirlinglem6  43510  stirlinglem7  43511  stirlinglem8  43512  stirlinglem10  43514  stirlinglem12  43516  dirkertrigeqlem3  43531  dirkertrigeq  43532  dirkercncflem1  43534  dirkercncflem2  43535  fourierdlem28  43566  fourierdlem30  43568  fourierdlem39  43577  fourierdlem47  43584  fourierdlem60  43597  fourierdlem61  43598  fourierdlem73  43610  fourierdlem83  43620  fourierdlem87  43624  etransclem14  43679  etransclem24  43689  etransclem25  43690  etransclem35  43700  smfmullem1  44212  deccarry  44691  fpprwppr  45079  fpprwpprb  45080  logblt1b  45798  nn0sumshdiglem2  45856  itcovalpclem2  45905  itcovalt2lem1  45909  eenglngeehlnmlem1  45971  eenglngeehlnmlem2  45972  line2ylem  45985