Theorem mulridd 11227

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099  1c1 11102   · cmul 11106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-mulcl 11163  ax-mulcom 11165  ax-mulass 11167  ax-distr 11168  ax-1rid 11171  ax-cnre 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415

This theorem is referenced by:  muladd11  11381  muls1d  11675  divrec  11889  diveq1  11902  conjmul  11933  divelunit  13522  modid  13931  addmodlteq  13984  expadd  14142  leexp2r  14212  nnlesq  14243  sqoddm1div8  14281  faclbnd  14328  faclbnd2  14329  faclbnd4lem3  14333  faclbnd6  14337  facavg  14339  bcn0  14348  bcn1  14351  hashf1lem2  14495  hashfac  14497  reccn2  15650  iseraltlem2  15736  iseraltlem3  15737  fsumconst1  15844  hash2iun1dif1  15878  indsumhash  15883  binom11  15888  harmonic  15915  trireciplem  15918  geoserg  15922  pwdif  15924  pwm1geoser  15925  cvgrat  15939  fprodsplit  16022  fprodle  16052  fsumcube  16115  efzval  16159  tanhlt1  16217  tanaddlem  16223  tanadd  16224  cos01gt0  16248  absef  16254  1dvds  16329  bitsfzo  16494  bitsmod  16495  sqgcd  16621  expgcd  16622  lcm1  16669  coprmdvds  16712  qredeu  16717  phiprmpw  16836  coprimeprodsq  16869  pc2dvds  16940  sumhash  16957  fldivp1  16958  pcfaclem  16959  prmpwdvds  16965  prmreclem1  16977  vdwlem3  17044  vdwlem9  17050  prmop1  17099  sylow2a  19690  odadd  19921  zsssubrg  21556  zringcyg  21600  prmirredlem  21603  mulgrhm2  21609  pzriprnglem6  21617  pzriprnglem12  21623  znrrg  21696  mhppwdeg  22294  icopnfcnv  25082  icopnfhmeo  25083  lebnumii  25106  reparphti  25137  itg2const  25880  itg2monolem3  25892  bddibl  25980  dveflem  26119  mvth  26132  dvlipcn  26134  dvivthlem1  26148  dvfsumle  26161  dvfsumabs  26163  dvfsumlem2  26167  plyconst  26344  plyeq0lem  26348  plyco  26379  0dgrb  26384  coefv0  26386  vieta1  26454  aaliou3lem2  26485  tayl0  26503  taylply2  26509  dvtaylp  26511  taylthlem2  26515  radcnvlem1  26554  abelthlem1  26572  abelthlem2  26573  abelthlem3  26574  abelthlem7  26579  abelthlem8  26580  abelthlem9  26581  efper  26622  tangtx  26648  eflogeq  26745  logdivlti  26763  logcnlem4  26788  advlogexp  26798  cxpmul2  26832  dvcxp2  26884  cxpaddle  26895  cxpeq  26900  loglesqrt  26904  relogbexp  26923  ang180lem5  26956  isosctrlem2  26962  isosctrlem3  26963  heron  26981  2efiatan  27061  dvatan  27078  leibpi  27085  birthdaylem3  27096  jensenlem2  27130  logdiflbnd  27137  harmonicbnd4  27153  lgamgulmlem2  27172  lgamcvg2  27197  ftalem5  27219  basellem2  27224  basellem5  27227  basellem8  27230  0sgm  27286  muinv  27335  chpub  27362  logfaclbnd  27364  logexprlim  27367  dchrsum2  27410  sumdchr2  27412  bposlem1  27426  bposlem2  27427  bposlem5  27430  lgsquad2lem1  27526  lgsquad3  27529  2sqlem6  27565  2sqlem8  27568  chtppilim  27617  vmadivsum  27624  dchrisumlem1  27631  dchrisum0flblem1  27650  rpvmasum2  27654  dchrisum0re  27655  dchrisum0lem2a  27659  dchrisum0lem3  27661  rpvmasum  27668  mudivsum  27672  mulogsumlem  27673  vmalogdivsum2  27680  pntrsumo1  27707  pntrlog2bndlem2  27720  pntrlog2bndlem4  27722  pntrlog2bndlem5  27723  pntibndlem2  27733  pntlemc  27737  pntlemf  27747  ostth2lem2  27776  ostth2lem3  27777  ostth2lem4  27778  ostth2  27779  ostth3  27780  ttgcontlem1  29212  axpaschlem  29268  axcontlem2  29293  axcontlem4  29295  axcontlem8  29299  nmoub3i  31103  ubthlem2  31201  htthlem  31247  nmcexi  32356  nmopcoadji  32431  branmfn  32435  gsumind  33643  rearchi  33644  vietadeg1  33946  ccfldextdgrr  34040  nn0constr  34129  constrrecl  34137  constrimcl  34138  constrreinvcl  34140  constrinvcl  34141  constrresqrtcl  34145  constrabscl  34146  cos9thpiminplylem1  34150  madjusmdetlem4  34198  ccatmulgnn0dir  34910  ofcccat  34911  itgexpif  34971  hashreprin  34985  circlemeth  35005  lpadlem2  35048  subfacval2  35657  cvmliftlem2  35756  snmlff  35799  sinccvglem  36142  bcprod  36208  faclimlem1  36213  faclimlem2  36214  faclim2  36218  knoppndvlem14  37092  knoppndvlem15  37093  knoppndvlem16  37094  knoppndvlem18  37096  poimirlem29  38278  poimirlem30  38279  poimirlem31  38280  poimirlem32  38281  itg2addnclem  38300  areacirclem1  38337  areacirclem4  38340  cntotbnd  38425  lcmineqlem11  42784  lcmineqlem12  42785  aks4d1p1p7  42819  aks4d1p8d2  42830  hashscontpow1  42866  2ap1caineq  42890  sticksstones10  42900  sticksstones12a  42902  aks6d1c6lem1  42915  aks6d1c7lem1  42925  aks6d1c7  42929  oddnumth  43050  oexpreposd  43061  readvrec  43101  frlmvscadiccat  43258  fltnltalem  43374  3cubeslem2  43396  3cubeslem3r  43398  irrapxlem1  43529  irrapxlem4  43532  pell1qrgaplem  43580  reglogexpbas  43604  rmspecfund  43616  rmxy1  43629  rmxp1  43639  rmyp1  43640  rmxm1  43641  jm2.17a  43667  jm2.18  43695  jm2.23  43703  jm2.25  43706  jm2.16nn0  43711  relexpmulnn  44415  int-mul11d  44888  nzprmdif  45009  expgrowthi  45023  expgrowth  45025  binomcxplemdvbinom  45043  binomcxplemnotnn0  45046  sqrlearg  46249  fmul01  46276  fmul01lt1lem1  46280  0ellimcdiv  46343  dvxpaek  46634  dvnxpaek  46636  itgiccshift  46674  itgperiod  46675  itgsbtaddcnst  46676  stoweidlem11  46705  stoweidlem26  46720  stoweidlem38  46732  wallispilem4  46762  stirlinglem1  46768  stirlinglem3  46770  stirlinglem6  46773  stirlinglem7  46774  stirlinglem8  46775  stirlinglem10  46777  stirlinglem12  46779  dirkertrigeqlem3  46794  dirkertrigeq  46795  dirkercncflem1  46797  dirkercncflem2  46798  fourierdlem28  46829  fourierdlem30  46831  fourierdlem39  46840  fourierdlem47  46847  fourierdlem60  46860  fourierdlem61  46861  fourierdlem73  46873  fourierdlem83  46883  fourierdlem87  46887  etransclem14  46942  etransclem24  46952  etransclem25  46953  etransclem35  46963  smfmullem1  47485  sin3t  47585  cos3t  47586  sin5tlem1  47587  deccarry  48025  fpprwppr  48481  fpprwpprb  48482  logblt1b  49321  nn0sumshdiglem2  49379  itcovalpclem2  49428  itcovalt2lem1  49432  eenglngeehlnmlem1  49494  eenglngeehlnmlem2  49495  line2ylem  49508