Theorem mulridd 11162

Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
mulridd	⊢ (𝜑 → (𝐴 · 1) = 𝐴)

Proof of Theorem mulridd

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036  1c1 11039   · cmul 11043

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-mulcom 11102  ax-mulass 11104  ax-distr 11105  ax-1rid 11108  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370

This theorem is referenced by:  muladd11  11316  muls1d  11610  divrec  11825  diveq1  11839  conjmul  11872  divelunit  13447  modid  13855  addmodlteq  13908  expadd  14066  leexp2r  14136  nnlesq  14167  sqoddm1div8  14205  faclbnd  14252  faclbnd2  14253  faclbnd4lem3  14257  faclbnd6  14261  facavg  14263  bcn0  14272  bcn1  14275  hashf1lem2  14418  hashfac  14420  reccn2  15559  iseraltlem2  15645  iseraltlem3  15646  fsumconst1  15753  hash2iun1dif1  15787  indsumhash  15792  binom11  15797  harmonic  15824  trireciplem  15827  geoserg  15831  pwdif  15833  pwm1geoser  15834  cvgrat  15848  fprodsplit  15931  fprodle  15961  fsumcube  16025  efzval  16069  tanhlt1  16127  tanaddlem  16133  tanadd  16134  cos01gt0  16158  absef  16164  1dvds  16239  bitsfzo  16404  bitsmod  16405  sqgcd  16531  expgcd  16532  lcm1  16579  coprmdvds  16622  qredeu  16627  phiprmpw  16746  coprimeprodsq  16779  pc2dvds  16850  sumhash  16867  fldivp1  16868  pcfaclem  16869  prmpwdvds  16875  prmreclem1  16887  vdwlem3  16954  vdwlem9  16960  prmop1  17009  sylow2a  19594  odadd  19825  zsssubrg  21405  zringcyg  21449  prmirredlem  21452  mulgrhm2  21458  pzriprnglem6  21466  pzriprnglem12  21472  znrrg  21545  mhppwdeg  22116  icopnfcnv  24909  icopnfhmeo  24910  lebnumii  24933  reparphti  24964  itg2const  25707  itg2monolem3  25719  bddibl  25807  dveflem  25946  mvth  25959  dvlipcn  25961  dvivthlem1  25975  dvfsumle  25988  dvfsumabs  25990  dvfsumlem2  25994  plyconst  26171  plyeq0lem  26175  plyco  26206  0dgrb  26211  coefv0  26213  vieta1  26278  aaliou3lem2  26309  tayl0  26327  taylply2  26333  dvtaylp  26335  taylthlem2  26339  radcnvlem1  26378  abelthlem1  26396  abelthlem2  26397  abelthlem3  26398  abelthlem7  26403  abelthlem8  26404  abelthlem9  26405  efper  26443  tangtx  26469  eflogeq  26566  logdivlti  26584  logcnlem4  26609  advlogexp  26619  cxpmul2  26653  dvcxp2  26705  cxpaddle  26716  cxpeq  26721  loglesqrt  26725  relogbexp  26744  ang180lem5  26777  isosctrlem2  26783  isosctrlem3  26784  heron  26802  2efiatan  26882  dvatan  26899  leibpi  26906  birthdaylem3  26917  jensenlem2  26951  logdiflbnd  26958  harmonicbnd4  26974  lgamgulmlem2  26993  lgamcvg2  27018  ftalem5  27040  basellem2  27045  basellem5  27048  basellem8  27051  0sgm  27107  muinv  27156  chpub  27183  logfaclbnd  27185  logexprlim  27188  dchrsum2  27231  sumdchr2  27233  bposlem1  27247  bposlem2  27248  bposlem5  27251  lgsquad2lem1  27347  lgsquad3  27350  2sqlem6  27386  2sqlem8  27389  chtppilim  27438  vmadivsum  27445  dchrisumlem1  27452  dchrisum0flblem1  27471  rpvmasum2  27475  dchrisum0re  27476  dchrisum0lem2a  27480  dchrisum0lem3  27482  rpvmasum  27489  mudivsum  27493  mulogsumlem  27494  vmalogdivsum2  27501  pntrsumo1  27528  pntrlog2bndlem2  27541  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntibndlem2  27554  pntlemc  27558  pntlemf  27568  ostth2lem2  27597  ostth2lem3  27598  ostth2lem4  27599  ostth2  27600  ostth3  27601  ttgcontlem1  28953  axpaschlem  29009  axcontlem2  29034  axcontlem4  29036  axcontlem8  29040  nmoub3i  30844  ubthlem2  30942  htthlem  30988  nmcexi  32097  nmopcoadji  32172  branmfn  32176  gsumind  33405  rearchi  33406  vietadeg1  33722  ccfldextdgrr  33816  nn0constr  33905  constrrecl  33913  constrimcl  33914  constrreinvcl  33916  constrinvcl  33917  constrresqrtcl  33921  constrabscl  33922  cos9thpiminplylem1  33926  madjusmdetlem4  33974  ccatmulgnn0dir  34686  ofcccat  34687  itgexpif  34750  hashreprin  34764  circlemeth  34784  lpadlem2  34824  subfacval2  35369  cvmliftlem2  35468  snmlff  35511  sinccvglem  35854  bcprod  35920  faclimlem1  35925  faclimlem2  35926  faclim2  35930  knoppndvlem14  36785  knoppndvlem15  36786  knoppndvlem16  36787  knoppndvlem18  36789  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  itg2addnclem  37992  areacirclem1  38029  areacirclem4  38032  cntotbnd  38117  lcmineqlem11  42478  lcmineqlem12  42479  aks4d1p1p7  42513  aks4d1p8d2  42524  hashscontpow1  42560  2ap1caineq  42584  sticksstones10  42594  sticksstones12a  42596  aks6d1c6lem1  42609  aks6d1c7lem1  42619  aks6d1c7  42623  oddnumth  42743  oexpreposd  42754  readvrec  42794  frlmvscadiccat  42951  fltnltalem  43095  3cubeslem2  43117  3cubeslem3r  43119  irrapxlem1  43250  irrapxlem4  43253  pell1qrgaplem  43301  reglogexpbas  43325  rmspecfund  43337  rmxy1  43350  rmxp1  43360  rmyp1  43361  rmxm1  43362  jm2.17a  43388  jm2.18  43416  jm2.23  43424  jm2.25  43427  jm2.16nn0  43432  relexpmulnn  44136  int-mul11d  44609  nzprmdif  44746  expgrowthi  44760  expgrowth  44762  binomcxplemdvbinom  44780  binomcxplemnotnn0  44783  sqrlearg  45983  fmul01  46010  fmul01lt1lem1  46014  0ellimcdiv  46077  dvxpaek  46368  dvnxpaek  46370  itgiccshift  46408  itgperiod  46409  itgsbtaddcnst  46410  stoweidlem11  46439  stoweidlem26  46454  stoweidlem38  46466  wallispilem4  46496  stirlinglem1  46502  stirlinglem3  46504  stirlinglem6  46507  stirlinglem7  46508  stirlinglem8  46509  stirlinglem10  46511  stirlinglem12  46513  dirkertrigeqlem3  46528  dirkertrigeq  46529  dirkercncflem1  46531  dirkercncflem2  46532  fourierdlem28  46563  fourierdlem30  46565  fourierdlem39  46574  fourierdlem47  46581  fourierdlem60  46594  fourierdlem61  46595  fourierdlem73  46607  fourierdlem83  46617  fourierdlem87  46621  etransclem14  46676  etransclem24  46686  etransclem25  46687  etransclem35  46697  smfmullem1  47219  sin3t  47319  cos3t  47320  sin5tlem1  47321  deccarry  47759  fpprwppr  48215  fpprwpprb  48216  logblt1b  49040  nn0sumshdiglem2  49098  itcovalpclem2  49147  itcovalt2lem1  49151  eenglngeehlnmlem1  49213  eenglngeehlnmlem2  49214  line2ylem  49227