Theorem mulridd 11238

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2105  (class class class)co 7412  ℂcc 11114  1c1 11117   · cmul 11121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-resscn 11173  ax-1cn 11174  ax-icn 11175  ax-addcl 11176  ax-mulcl 11178  ax-mulcom 11180  ax-mulass 11182  ax-distr 11183  ax-1rid 11186  ax-cnre 11189

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7415

This theorem is referenced by:  muladd11  11391  muls1d  11681  divrec  11895  diveq1  11912  conjmul  11938  divelunit  13478  modid  13868  addmodlteq  13918  expadd  14077  leexp2r  14146  nnlesq  14176  sqoddm1div8  14213  faclbnd  14257  faclbnd2  14258  faclbnd4lem3  14262  faclbnd6  14266  facavg  14268  bcn0  14277  bcn1  14280  hashf1lem2  14424  hashfac  14426  reccn2  15548  iseraltlem2  15636  iseraltlem3  15637  hash2iun1dif1  15777  binom11  15785  harmonic  15812  trireciplem  15815  geoserg  15819  pwdif  15821  pwm1geoser  15822  cvgrat  15836  fprodsplit  15917  fprodle  15947  fsumcube  16011  efzval  16052  tanhlt1  16110  tanaddlem  16116  tanadd  16117  cos01gt0  16141  absef  16147  1dvds  16221  bitsfzo  16383  bitsmod  16384  sqgcd  16509  lcm1  16554  coprmdvds  16597  qredeu  16602  phiprmpw  16716  coprimeprodsq  16748  pc2dvds  16819  sumhash  16836  fldivp1  16837  pcfaclem  16838  prmpwdvds  16844  prmreclem1  16856  vdwlem3  16923  vdwlem9  16929  prmop1  16978  sylow2a  19535  odadd  19766  zsssubrg  21292  zringcyg  21329  prmirredlem  21332  mulgrhm2  21338  pzriprnglem6  21346  pzriprnglem12  21352  znrrg  21431  mhppwdeg  22002  icopnfcnv  24787  icopnfhmeo  24788  lebnumii  24812  reparphti  24843  reparphtiOLD  24844  itg2const  25590  itg2monolem3  25602  bddibl  25689  dveflem  25831  mvth  25845  dvlipcn  25847  dvivthlem1  25861  dvfsumle  25874  dvfsumleOLD  25875  dvfsumabs  25877  dvfsumlem2  25881  dvfsumlem2OLD  25882  plyconst  26058  plyeq0lem  26062  plyco  26093  0dgrb  26098  coefv0  26100  vieta1  26164  aaliou3lem2  26195  tayl0  26213  taylply2  26219  dvtaylp  26221  taylthlem2  26225  radcnvlem1  26264  abelthlem1  26283  abelthlem2  26284  abelthlem3  26285  abelthlem7  26290  abelthlem8  26291  abelthlem9  26292  efper  26329  tangtx  26355  eflogeq  26450  logdivlti  26468  logcnlem4  26493  advlogexp  26503  cxpmul2  26537  dvcxp2  26589  cxpaddle  26601  cxpeq  26606  loglesqrt  26607  relogbexp  26626  ang180lem5  26659  isosctrlem2  26665  isosctrlem3  26666  heron  26684  2efiatan  26764  dvatan  26781  leibpi  26788  birthdaylem3  26799  jensenlem2  26834  logdiflbnd  26841  harmonicbnd4  26857  lgamgulmlem2  26876  lgamcvg2  26901  ftalem5  26923  basellem2  26928  basellem5  26931  basellem8  26934  0sgm  26990  muinv  27039  chpub  27067  logfaclbnd  27069  logexprlim  27072  dchrsum2  27115  sumdchr2  27117  bposlem1  27131  bposlem2  27132  bposlem5  27135  lgsquad2lem1  27231  lgsquad3  27234  2sqlem6  27270  2sqlem8  27273  chtppilim  27322  vmadivsum  27329  dchrisumlem1  27336  dchrisum0flblem1  27355  rpvmasum2  27359  dchrisum0re  27360  dchrisum0lem2a  27364  dchrisum0lem3  27366  rpvmasum  27373  mudivsum  27377  mulogsumlem  27378  vmalogdivsum2  27385  pntrsumo1  27412  pntrlog2bndlem2  27425  pntrlog2bndlem4  27427  pntrlog2bndlem5  27428  pntibndlem2  27438  pntlemc  27442  pntlemf  27452  ostth2lem2  27481  ostth2lem3  27482  ostth2lem4  27483  ostth2  27484  ostth3  27485  ttgcontlem1  28576  axpaschlem  28632  axcontlem2  28657  axcontlem4  28659  axcontlem8  28663  nmoub3i  30460  ubthlem2  30558  htthlem  30604  nmcexi  31713  nmopcoadji  31788  branmfn  31792  rearchi  32898  ccfldextdgrr  33202  madjusmdetlem4  33275  ccatmulgnn0dir  34018  ofcccat  34019  itgexpif  34083  hashreprin  34097  circlemeth  34117  lpadlem2  34157  subfacval2  34643  cvmliftlem2  34742  snmlff  34785  sinccvglem  35122  bcprod  35179  faclimlem1  35184  faclimlem2  35185  faclim2  35189  gg-taylthlem2  35633  knoppndvlem14  35867  knoppndvlem15  35868  knoppndvlem16  35869  knoppndvlem18  35871  poimirlem29  36983  poimirlem30  36984  poimirlem31  36985  poimirlem32  36986  itg2addnclem  37005  areacirclem1  37042  areacirclem4  37045  cntotbnd  37130  lcmineqlem11  41373  lcmineqlem12  41374  aks4d1p1p7  41408  aks4d1p8d2  41419  2ap1caineq  41430  sticksstones10  41440  sticksstones12a  41442  frlmvscadiccat  41549  oddnumth  41674  oexpreposd  41677  expgcd  41690  fltnltalem  41869  3cubeslem2  41888  3cubeslem3r  41890  irrapxlem1  42025  irrapxlem4  42028  pell1qrgaplem  42076  reglogexpbas  42100  rmspecfund  42112  rmxy1  42126  rmxp1  42136  rmyp1  42137  rmxm1  42138  jm2.17a  42164  jm2.18  42192  jm2.23  42200  jm2.25  42203  jm2.16nn0  42208  relexpmulnn  42925  int-mul11d  43399  nzprmdif  43543  expgrowthi  43557  expgrowth  43559  binomcxplemdvbinom  43577  binomcxplemnotnn0  43580  sqrlearg  44727  fmul01  44757  fmul01lt1lem1  44761  0ellimcdiv  44826  dvxpaek  45117  dvnxpaek  45119  itgiccshift  45157  itgperiod  45158  itgsbtaddcnst  45159  stoweidlem11  45188  stoweidlem26  45203  stoweidlem38  45215  wallispilem4  45245  stirlinglem1  45251  stirlinglem3  45253  stirlinglem6  45256  stirlinglem7  45257  stirlinglem8  45258  stirlinglem10  45260  stirlinglem12  45262  dirkertrigeqlem3  45277  dirkertrigeq  45278  dirkercncflem1  45280  dirkercncflem2  45281  fourierdlem28  45312  fourierdlem30  45314  fourierdlem39  45323  fourierdlem47  45330  fourierdlem60  45343  fourierdlem61  45344  fourierdlem73  45356  fourierdlem83  45366  fourierdlem87  45370  etransclem14  45425  etransclem24  45435  etransclem25  45436  etransclem35  45446  smfmullem1  45968  deccarry  46480  fpprwppr  46868  fpprwpprb  46869  logblt1b  47414  nn0sumshdiglem2  47472  itcovalpclem2  47521  itcovalt2lem1  47525  eenglngeehlnmlem1  47587  eenglngeehlnmlem2  47588  line2ylem  47601