Theorem mulridd 11191

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066  1c1 11069   · cmul 11073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-mulcl 11130  ax-mulcom 11132  ax-mulass 11134  ax-distr 11135  ax-1rid 11138  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  muladd11  11344  muls1d  11638  divrec  11853  diveq1  11867  conjmul  11899  divelunit  13455  modid  13858  addmodlteq  13911  expadd  14069  leexp2r  14139  nnlesq  14170  sqoddm1div8  14208  faclbnd  14255  faclbnd2  14256  faclbnd4lem3  14260  faclbnd6  14264  facavg  14266  bcn0  14275  bcn1  14278  hashf1lem2  14421  hashfac  14423  reccn2  15563  iseraltlem2  15649  iseraltlem3  15650  hash2iun1dif1  15790  binom11  15798  harmonic  15825  trireciplem  15828  geoserg  15832  pwdif  15834  pwm1geoser  15835  cvgrat  15849  fprodsplit  15932  fprodle  15962  fsumcube  16026  efzval  16070  tanhlt1  16128  tanaddlem  16134  tanadd  16135  cos01gt0  16159  absef  16165  1dvds  16240  bitsfzo  16405  bitsmod  16406  sqgcd  16532  expgcd  16533  lcm1  16580  coprmdvds  16623  qredeu  16628  phiprmpw  16746  coprimeprodsq  16779  pc2dvds  16850  sumhash  16867  fldivp1  16868  pcfaclem  16869  prmpwdvds  16875  prmreclem1  16887  vdwlem3  16954  vdwlem9  16960  prmop1  17009  sylow2a  19549  odadd  19780  zsssubrg  21342  zringcyg  21379  prmirredlem  21382  mulgrhm2  21388  pzriprnglem6  21396  pzriprnglem12  21402  znrrg  21475  mhppwdeg  22037  icopnfcnv  24840  icopnfhmeo  24841  lebnumii  24865  reparphti  24896  reparphtiOLD  24897  itg2const  25641  itg2monolem3  25653  bddibl  25741  dveflem  25883  mvth  25897  dvlipcn  25899  dvivthlem1  25913  dvfsumle  25926  dvfsumleOLD  25927  dvfsumabs  25929  dvfsumlem2  25933  dvfsumlem2OLD  25934  plyconst  26111  plyeq0lem  26115  plyco  26146  0dgrb  26151  coefv0  26153  vieta1  26220  aaliou3lem2  26251  tayl0  26269  taylply2  26275  taylply2OLD  26276  dvtaylp  26278  taylthlem2  26282  taylthlem2OLD  26283  radcnvlem1  26322  abelthlem1  26341  abelthlem2  26342  abelthlem3  26343  abelthlem7  26348  abelthlem8  26349  abelthlem9  26350  efper  26388  tangtx  26414  eflogeq  26511  logdivlti  26529  logcnlem4  26554  advlogexp  26564  cxpmul2  26598  dvcxp2  26650  cxpaddle  26662  cxpeq  26667  loglesqrt  26671  relogbexp  26690  ang180lem5  26723  isosctrlem2  26729  isosctrlem3  26730  heron  26748  2efiatan  26828  dvatan  26845  leibpi  26852  birthdaylem3  26863  jensenlem2  26898  logdiflbnd  26905  harmonicbnd4  26921  lgamgulmlem2  26940  lgamcvg2  26965  ftalem5  26987  basellem2  26992  basellem5  26995  basellem8  26998  0sgm  27054  muinv  27103  chpub  27131  logfaclbnd  27133  logexprlim  27136  dchrsum2  27179  sumdchr2  27181  bposlem1  27195  bposlem2  27196  bposlem5  27199  lgsquad2lem1  27295  lgsquad3  27298  2sqlem6  27334  2sqlem8  27337  chtppilim  27386  vmadivsum  27393  dchrisumlem1  27400  dchrisum0flblem1  27419  rpvmasum2  27423  dchrisum0re  27424  dchrisum0lem2a  27428  dchrisum0lem3  27430  rpvmasum  27437  mudivsum  27441  mulogsumlem  27442  vmalogdivsum2  27449  pntrsumo1  27476  pntrlog2bndlem2  27489  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntibndlem2  27502  pntlemc  27506  pntlemf  27516  ostth2lem2  27545  ostth2lem3  27546  ostth2lem4  27547  ostth2  27548  ostth3  27549  ttgcontlem1  28812  axpaschlem  28867  axcontlem2  28892  axcontlem4  28894  axcontlem8  28898  nmoub3i  30702  ubthlem2  30800  htthlem  30846  nmcexi  31955  nmopcoadji  32030  branmfn  32034  rearchi  33317  ccfldextdgrr  33667  nn0constr  33751  constrrecl  33759  constrimcl  33760  constrreinvcl  33762  constrinvcl  33763  constrresqrtcl  33767  constrabscl  33768  cos9thpiminplylem1  33772  madjusmdetlem4  33820  ccatmulgnn0dir  34533  ofcccat  34534  itgexpif  34597  hashreprin  34611  circlemeth  34631  lpadlem2  34671  subfacval2  35174  cvmliftlem2  35273  snmlff  35316  sinccvglem  35659  bcprod  35725  faclimlem1  35730  faclimlem2  35731  faclim2  35735  knoppndvlem14  36513  knoppndvlem15  36514  knoppndvlem16  36515  knoppndvlem18  36517  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  poimirlem32  37646  itg2addnclem  37665  areacirclem1  37702  areacirclem4  37705  cntotbnd  37790  lcmineqlem11  42027  lcmineqlem12  42028  aks4d1p1p7  42062  aks4d1p8d2  42073  hashscontpow1  42109  2ap1caineq  42133  sticksstones10  42143  sticksstones12a  42145  aks6d1c6lem1  42158  aks6d1c7lem1  42168  aks6d1c7  42172  oddnumth  42299  oexpreposd  42310  readvrec  42350  frlmvscadiccat  42494  fltnltalem  42650  3cubeslem2  42673  3cubeslem3r  42675  irrapxlem1  42810  irrapxlem4  42813  pell1qrgaplem  42861  reglogexpbas  42885  rmspecfund  42897  rmxy1  42911  rmxp1  42921  rmyp1  42922  rmxm1  42923  jm2.17a  42949  jm2.18  42977  jm2.23  42985  jm2.25  42988  jm2.16nn0  42993  relexpmulnn  43698  int-mul11d  44171  nzprmdif  44308  expgrowthi  44322  expgrowth  44324  binomcxplemdvbinom  44342  binomcxplemnotnn0  44345  sqrlearg  45551  fmul01  45578  fmul01lt1lem1  45582  0ellimcdiv  45647  dvxpaek  45938  dvnxpaek  45940  itgiccshift  45978  itgperiod  45979  itgsbtaddcnst  45980  stoweidlem11  46009  stoweidlem26  46024  stoweidlem38  46036  wallispilem4  46066  stirlinglem1  46072  stirlinglem3  46074  stirlinglem6  46077  stirlinglem7  46078  stirlinglem8  46079  stirlinglem10  46081  stirlinglem12  46083  dirkertrigeqlem3  46098  dirkertrigeq  46099  dirkercncflem1  46101  dirkercncflem2  46102  fourierdlem28  46133  fourierdlem30  46135  fourierdlem39  46144  fourierdlem47  46151  fourierdlem60  46164  fourierdlem61  46165  fourierdlem73  46177  fourierdlem83  46187  fourierdlem87  46191  etransclem14  46246  etransclem24  46256  etransclem25  46257  etransclem35  46267  smfmullem1  46789  deccarry  47312  fpprwppr  47740  fpprwpprb  47741  logblt1b  48553  nn0sumshdiglem2  48611  itcovalpclem2  48660  itcovalt2lem1  48664  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727  line2ylem  48740