Theorem mulridd 11278

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153  1c1 11156   · cmul 11160

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-mulcl 11217  ax-mulcom 11219  ax-mulass 11221  ax-distr 11222  ax-1rid 11225  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434

This theorem is referenced by:  muladd11  11431  muls1d  11723  divrec  11938  diveq1  11952  conjmul  11984  divelunit  13534  modid  13936  addmodlteq  13987  expadd  14145  leexp2r  14214  nnlesq  14244  sqoddm1div8  14282  faclbnd  14329  faclbnd2  14330  faclbnd4lem3  14334  faclbnd6  14338  facavg  14340  bcn0  14349  bcn1  14352  hashf1lem2  14495  hashfac  14497  reccn2  15633  iseraltlem2  15719  iseraltlem3  15720  hash2iun1dif1  15860  binom11  15868  harmonic  15895  trireciplem  15898  geoserg  15902  pwdif  15904  pwm1geoser  15905  cvgrat  15919  fprodsplit  16002  fprodle  16032  fsumcube  16096  efzval  16138  tanhlt1  16196  tanaddlem  16202  tanadd  16203  cos01gt0  16227  absef  16233  1dvds  16308  bitsfzo  16472  bitsmod  16473  sqgcd  16599  expgcd  16600  lcm1  16647  coprmdvds  16690  qredeu  16695  phiprmpw  16813  coprimeprodsq  16846  pc2dvds  16917  sumhash  16934  fldivp1  16935  pcfaclem  16936  prmpwdvds  16942  prmreclem1  16954  vdwlem3  17021  vdwlem9  17027  prmop1  17076  sylow2a  19637  odadd  19868  zsssubrg  21443  zringcyg  21480  prmirredlem  21483  mulgrhm2  21489  pzriprnglem6  21497  pzriprnglem12  21503  znrrg  21584  mhppwdeg  22154  icopnfcnv  24973  icopnfhmeo  24974  lebnumii  24998  reparphti  25029  reparphtiOLD  25030  itg2const  25775  itg2monolem3  25787  bddibl  25875  dveflem  26017  mvth  26031  dvlipcn  26033  dvivthlem1  26047  dvfsumle  26060  dvfsumleOLD  26061  dvfsumabs  26063  dvfsumlem2  26067  dvfsumlem2OLD  26068  plyconst  26245  plyeq0lem  26249  plyco  26280  0dgrb  26285  coefv0  26287  vieta1  26354  aaliou3lem2  26385  tayl0  26403  taylply2  26409  taylply2OLD  26410  dvtaylp  26412  taylthlem2  26416  taylthlem2OLD  26417  radcnvlem1  26456  abelthlem1  26475  abelthlem2  26476  abelthlem3  26477  abelthlem7  26482  abelthlem8  26483  abelthlem9  26484  efper  26521  tangtx  26547  eflogeq  26644  logdivlti  26662  logcnlem4  26687  advlogexp  26697  cxpmul2  26731  dvcxp2  26783  cxpaddle  26795  cxpeq  26800  loglesqrt  26804  relogbexp  26823  ang180lem5  26856  isosctrlem2  26862  isosctrlem3  26863  heron  26881  2efiatan  26961  dvatan  26978  leibpi  26985  birthdaylem3  26996  jensenlem2  27031  logdiflbnd  27038  harmonicbnd4  27054  lgamgulmlem2  27073  lgamcvg2  27098  ftalem5  27120  basellem2  27125  basellem5  27128  basellem8  27131  0sgm  27187  muinv  27236  chpub  27264  logfaclbnd  27266  logexprlim  27269  dchrsum2  27312  sumdchr2  27314  bposlem1  27328  bposlem2  27329  bposlem5  27332  lgsquad2lem1  27428  lgsquad3  27431  2sqlem6  27467  2sqlem8  27470  chtppilim  27519  vmadivsum  27526  dchrisumlem1  27533  dchrisum0flblem1  27552  rpvmasum2  27556  dchrisum0re  27557  dchrisum0lem2a  27561  dchrisum0lem3  27563  rpvmasum  27570  mudivsum  27574  mulogsumlem  27575  vmalogdivsum2  27582  pntrsumo1  27609  pntrlog2bndlem2  27622  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  pntibndlem2  27635  pntlemc  27639  pntlemf  27649  ostth2lem2  27678  ostth2lem3  27679  ostth2lem4  27680  ostth2  27681  ostth3  27682  ttgcontlem1  28899  axpaschlem  28955  axcontlem2  28980  axcontlem4  28982  axcontlem8  28986  nmoub3i  30792  ubthlem2  30890  htthlem  30936  nmcexi  32045  nmopcoadji  32120  branmfn  32124  rearchi  33374  ccfldextdgrr  33722  madjusmdetlem4  33829  ccatmulgnn0dir  34557  ofcccat  34558  itgexpif  34621  hashreprin  34635  circlemeth  34655  lpadlem2  34695  subfacval2  35192  cvmliftlem2  35291  snmlff  35334  sinccvglem  35677  bcprod  35738  faclimlem1  35743  faclimlem2  35744  faclim2  35748  knoppndvlem14  36526  knoppndvlem15  36527  knoppndvlem16  36528  knoppndvlem18  36530  poimirlem29  37656  poimirlem30  37657  poimirlem31  37658  poimirlem32  37659  itg2addnclem  37678  areacirclem1  37715  areacirclem4  37718  cntotbnd  37803  lcmineqlem11  42040  lcmineqlem12  42041  aks4d1p1p7  42075  aks4d1p8d2  42086  hashscontpow1  42122  2ap1caineq  42146  sticksstones10  42156  sticksstones12a  42158  aks6d1c6lem1  42171  aks6d1c7lem1  42181  aks6d1c7  42185  oddnumth  42345  oexpreposd  42357  readvrec  42392  frlmvscadiccat  42516  fltnltalem  42672  3cubeslem2  42696  3cubeslem3r  42698  irrapxlem1  42833  irrapxlem4  42836  pell1qrgaplem  42884  reglogexpbas  42908  rmspecfund  42920  rmxy1  42934  rmxp1  42944  rmyp1  42945  rmxm1  42946  jm2.17a  42972  jm2.18  43000  jm2.23  43008  jm2.25  43011  jm2.16nn0  43016  relexpmulnn  43722  int-mul11d  44195  nzprmdif  44338  expgrowthi  44352  expgrowth  44354  binomcxplemdvbinom  44372  binomcxplemnotnn0  44375  sqrlearg  45566  fmul01  45595  fmul01lt1lem1  45599  0ellimcdiv  45664  dvxpaek  45955  dvnxpaek  45957  itgiccshift  45995  itgperiod  45996  itgsbtaddcnst  45997  stoweidlem11  46026  stoweidlem26  46041  stoweidlem38  46053  wallispilem4  46083  stirlinglem1  46089  stirlinglem3  46091  stirlinglem6  46094  stirlinglem7  46095  stirlinglem8  46096  stirlinglem10  46098  stirlinglem12  46100  dirkertrigeqlem3  46115  dirkertrigeq  46116  dirkercncflem1  46118  dirkercncflem2  46119  fourierdlem28  46150  fourierdlem30  46152  fourierdlem39  46161  fourierdlem47  46168  fourierdlem60  46181  fourierdlem61  46182  fourierdlem73  46194  fourierdlem83  46204  fourierdlem87  46208  etransclem14  46263  etransclem24  46273  etransclem25  46274  etransclem35  46284  smfmullem1  46806  deccarry  47323  fpprwppr  47726  fpprwpprb  47727  logblt1b  48485  nn0sumshdiglem2  48543  itcovalpclem2  48592  itcovalt2lem1  48596  eenglngeehlnmlem1  48658  eenglngeehlnmlem2  48659  line2ylem  48672