Theorem mulridd 11151

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026  1c1 11029   · cmul 11033

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 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-mulcl 11090  ax-mulcom 11092  ax-mulass 11094  ax-distr 11095  ax-1rid 11098  ax-cnre 11101

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356

This theorem is referenced by:  muladd11  11304  muls1d  11598  divrec  11813  diveq1  11827  conjmul  11859  divelunit  13415  modid  13818  addmodlteq  13871  expadd  14029  leexp2r  14099  nnlesq  14130  sqoddm1div8  14168  faclbnd  14215  faclbnd2  14216  faclbnd4lem3  14220  faclbnd6  14224  facavg  14226  bcn0  14235  bcn1  14238  hashf1lem2  14381  hashfac  14383  reccn2  15522  iseraltlem2  15608  iseraltlem3  15609  hash2iun1dif1  15749  binom11  15757  harmonic  15784  trireciplem  15787  geoserg  15791  pwdif  15793  pwm1geoser  15794  cvgrat  15808  fprodsplit  15891  fprodle  15921  fsumcube  15985  efzval  16029  tanhlt1  16087  tanaddlem  16093  tanadd  16094  cos01gt0  16118  absef  16124  1dvds  16199  bitsfzo  16364  bitsmod  16365  sqgcd  16491  expgcd  16492  lcm1  16539  coprmdvds  16582  qredeu  16587  phiprmpw  16705  coprimeprodsq  16738  pc2dvds  16809  sumhash  16826  fldivp1  16827  pcfaclem  16828  prmpwdvds  16834  prmreclem1  16846  vdwlem3  16913  vdwlem9  16919  prmop1  16968  sylow2a  19516  odadd  19747  zsssubrg  21350  zringcyg  21394  prmirredlem  21397  mulgrhm2  21403  pzriprnglem6  21411  pzriprnglem12  21417  znrrg  21490  mhppwdeg  22053  icopnfcnv  24856  icopnfhmeo  24857  lebnumii  24881  reparphti  24912  reparphtiOLD  24913  itg2const  25657  itg2monolem3  25669  bddibl  25757  dveflem  25899  mvth  25913  dvlipcn  25915  dvivthlem1  25929  dvfsumle  25942  dvfsumleOLD  25943  dvfsumabs  25945  dvfsumlem2  25949  dvfsumlem2OLD  25950  plyconst  26127  plyeq0lem  26131  plyco  26162  0dgrb  26167  coefv0  26169  vieta1  26236  aaliou3lem2  26267  tayl0  26285  taylply2  26291  taylply2OLD  26292  dvtaylp  26294  taylthlem2  26298  taylthlem2OLD  26299  radcnvlem1  26338  abelthlem1  26357  abelthlem2  26358  abelthlem3  26359  abelthlem7  26364  abelthlem8  26365  abelthlem9  26366  efper  26404  tangtx  26430  eflogeq  26527  logdivlti  26545  logcnlem4  26570  advlogexp  26580  cxpmul2  26614  dvcxp2  26666  cxpaddle  26678  cxpeq  26683  loglesqrt  26687  relogbexp  26706  ang180lem5  26739  isosctrlem2  26745  isosctrlem3  26746  heron  26764  2efiatan  26844  dvatan  26861  leibpi  26868  birthdaylem3  26879  jensenlem2  26914  logdiflbnd  26921  harmonicbnd4  26937  lgamgulmlem2  26956  lgamcvg2  26981  ftalem5  27003  basellem2  27008  basellem5  27011  basellem8  27014  0sgm  27070  muinv  27119  chpub  27147  logfaclbnd  27149  logexprlim  27152  dchrsum2  27195  sumdchr2  27197  bposlem1  27211  bposlem2  27212  bposlem5  27215  lgsquad2lem1  27311  lgsquad3  27314  2sqlem6  27350  2sqlem8  27353  chtppilim  27402  vmadivsum  27409  dchrisumlem1  27416  dchrisum0flblem1  27435  rpvmasum2  27439  dchrisum0re  27440  dchrisum0lem2a  27444  dchrisum0lem3  27446  rpvmasum  27453  mudivsum  27457  mulogsumlem  27458  vmalogdivsum2  27465  pntrsumo1  27492  pntrlog2bndlem2  27505  pntrlog2bndlem4  27507  pntrlog2bndlem5  27508  pntibndlem2  27518  pntlemc  27522  pntlemf  27532  ostth2lem2  27561  ostth2lem3  27562  ostth2lem4  27563  ostth2  27564  ostth3  27565  ttgcontlem1  28848  axpaschlem  28903  axcontlem2  28928  axcontlem4  28930  axcontlem8  28934  nmoub3i  30735  ubthlem2  30833  htthlem  30879  nmcexi  31988  nmopcoadji  32063  branmfn  32067  rearchi  33293  ccfldextdgrr  33643  nn0constr  33727  constrrecl  33735  constrimcl  33736  constrreinvcl  33738  constrinvcl  33739  constrresqrtcl  33743  constrabscl  33744  cos9thpiminplylem1  33748  madjusmdetlem4  33796  ccatmulgnn0dir  34509  ofcccat  34510  itgexpif  34573  hashreprin  34587  circlemeth  34607  lpadlem2  34647  subfacval2  35159  cvmliftlem2  35258  snmlff  35301  sinccvglem  35644  bcprod  35710  faclimlem1  35715  faclimlem2  35716  faclim2  35720  knoppndvlem14  36498  knoppndvlem15  36499  knoppndvlem16  36500  knoppndvlem18  36502  poimirlem29  37628  poimirlem30  37629  poimirlem31  37630  poimirlem32  37631  itg2addnclem  37650  areacirclem1  37687  areacirclem4  37690  cntotbnd  37775  lcmineqlem11  42012  lcmineqlem12  42013  aks4d1p1p7  42047  aks4d1p8d2  42058  hashscontpow1  42094  2ap1caineq  42118  sticksstones10  42128  sticksstones12a  42130  aks6d1c6lem1  42143  aks6d1c7lem1  42153  aks6d1c7  42157  oddnumth  42284  oexpreposd  42295  readvrec  42335  frlmvscadiccat  42479  fltnltalem  42635  3cubeslem2  42658  3cubeslem3r  42660  irrapxlem1  42795  irrapxlem4  42798  pell1qrgaplem  42846  reglogexpbas  42870  rmspecfund  42882  rmxy1  42895  rmxp1  42905  rmyp1  42906  rmxm1  42907  jm2.17a  42933  jm2.18  42961  jm2.23  42969  jm2.25  42972  jm2.16nn0  42977  relexpmulnn  43682  int-mul11d  44155  nzprmdif  44292  expgrowthi  44306  expgrowth  44308  binomcxplemdvbinom  44326  binomcxplemnotnn0  44329  sqrlearg  45535  fmul01  45562  fmul01lt1lem1  45566  0ellimcdiv  45631  dvxpaek  45922  dvnxpaek  45924  itgiccshift  45962  itgperiod  45963  itgsbtaddcnst  45964  stoweidlem11  45993  stoweidlem26  46008  stoweidlem38  46020  wallispilem4  46050  stirlinglem1  46056  stirlinglem3  46058  stirlinglem6  46061  stirlinglem7  46062  stirlinglem8  46063  stirlinglem10  46065  stirlinglem12  46067  dirkertrigeqlem3  46082  dirkertrigeq  46083  dirkercncflem1  46085  dirkercncflem2  46086  fourierdlem28  46117  fourierdlem30  46119  fourierdlem39  46128  fourierdlem47  46135  fourierdlem60  46148  fourierdlem61  46149  fourierdlem73  46161  fourierdlem83  46171  fourierdlem87  46175  etransclem14  46230  etransclem24  46240  etransclem25  46241  etransclem35  46251  smfmullem1  46773  deccarry  47296  fpprwppr  47724  fpprwpprb  47725  logblt1b  48550  nn0sumshdiglem2  48608  itcovalpclem2  48657  itcovalt2lem1  48661  eenglngeehlnmlem1  48723  eenglngeehlnmlem2  48724  line2ylem  48737