Theorem mulridd 11136

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7352  ℂcc 11011  1c1 11014   · cmul 11018

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-resscn 11070  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-mulcl 11075  ax-mulcom 11077  ax-mulass 11079  ax-distr 11080  ax-1rid 11083  ax-cnre 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6442  df-fv 6494  df-ov 7355

This theorem is referenced by:  muladd11  11290  muls1d  11584  divrec  11799  diveq1  11813  conjmul  11845  divelunit  13396  modid  13802  addmodlteq  13855  expadd  14013  leexp2r  14083  nnlesq  14114  sqoddm1div8  14152  faclbnd  14199  faclbnd2  14200  faclbnd4lem3  14204  faclbnd6  14208  facavg  14210  bcn0  14219  bcn1  14222  hashf1lem2  14365  hashfac  14367  reccn2  15506  iseraltlem2  15592  iseraltlem3  15593  hash2iun1dif1  15733  binom11  15741  harmonic  15768  trireciplem  15771  geoserg  15775  pwdif  15777  pwm1geoser  15778  cvgrat  15792  fprodsplit  15875  fprodle  15905  fsumcube  15969  efzval  16013  tanhlt1  16071  tanaddlem  16077  tanadd  16078  cos01gt0  16102  absef  16108  1dvds  16183  bitsfzo  16348  bitsmod  16349  sqgcd  16475  expgcd  16476  lcm1  16523  coprmdvds  16566  qredeu  16571  phiprmpw  16689  coprimeprodsq  16722  pc2dvds  16793  sumhash  16810  fldivp1  16811  pcfaclem  16812  prmpwdvds  16818  prmreclem1  16830  vdwlem3  16897  vdwlem9  16903  prmop1  16952  sylow2a  19533  odadd  19764  zsssubrg  21364  zringcyg  21408  prmirredlem  21411  mulgrhm2  21417  pzriprnglem6  21425  pzriprnglem12  21431  znrrg  21504  mhppwdeg  22066  icopnfcnv  24868  icopnfhmeo  24869  lebnumii  24893  reparphti  24924  reparphtiOLD  24925  itg2const  25669  itg2monolem3  25681  bddibl  25769  dveflem  25911  mvth  25925  dvlipcn  25927  dvivthlem1  25941  dvfsumle  25954  dvfsumleOLD  25955  dvfsumabs  25957  dvfsumlem2  25961  dvfsumlem2OLD  25962  plyconst  26139  plyeq0lem  26143  plyco  26174  0dgrb  26179  coefv0  26181  vieta1  26248  aaliou3lem2  26279  tayl0  26297  taylply2  26303  taylply2OLD  26304  dvtaylp  26306  taylthlem2  26310  taylthlem2OLD  26311  radcnvlem1  26350  abelthlem1  26369  abelthlem2  26370  abelthlem3  26371  abelthlem7  26376  abelthlem8  26377  abelthlem9  26378  efper  26416  tangtx  26442  eflogeq  26539  logdivlti  26557  logcnlem4  26582  advlogexp  26592  cxpmul2  26626  dvcxp2  26678  cxpaddle  26690  cxpeq  26695  loglesqrt  26699  relogbexp  26718  ang180lem5  26751  isosctrlem2  26757  isosctrlem3  26758  heron  26776  2efiatan  26856  dvatan  26873  leibpi  26880  birthdaylem3  26891  jensenlem2  26926  logdiflbnd  26933  harmonicbnd4  26949  lgamgulmlem2  26968  lgamcvg2  26993  ftalem5  27015  basellem2  27020  basellem5  27023  basellem8  27026  0sgm  27082  muinv  27131  chpub  27159  logfaclbnd  27161  logexprlim  27164  dchrsum2  27207  sumdchr2  27209  bposlem1  27223  bposlem2  27224  bposlem5  27227  lgsquad2lem1  27323  lgsquad3  27326  2sqlem6  27362  2sqlem8  27365  chtppilim  27414  vmadivsum  27421  dchrisumlem1  27428  dchrisum0flblem1  27447  rpvmasum2  27451  dchrisum0re  27452  dchrisum0lem2a  27456  dchrisum0lem3  27458  rpvmasum  27465  mudivsum  27469  mulogsumlem  27470  vmalogdivsum2  27477  pntrsumo1  27504  pntrlog2bndlem2  27517  pntrlog2bndlem4  27519  pntrlog2bndlem5  27520  pntibndlem2  27530  pntlemc  27534  pntlemf  27544  ostth2lem2  27573  ostth2lem3  27574  ostth2lem4  27575  ostth2  27576  ostth3  27577  ttgcontlem1  28864  axpaschlem  28920  axcontlem2  28945  axcontlem4  28947  axcontlem8  28951  nmoub3i  30755  ubthlem2  30853  htthlem  30899  nmcexi  32008  nmopcoadji  32083  branmfn  32087  gsumind  33317  rearchi  33318  ccfldextdgrr  33706  nn0constr  33795  constrrecl  33803  constrimcl  33804  constrreinvcl  33806  constrinvcl  33807  constrresqrtcl  33811  constrabscl  33812  cos9thpiminplylem1  33816  madjusmdetlem4  33864  ccatmulgnn0dir  34576  ofcccat  34577  itgexpif  34640  hashreprin  34654  circlemeth  34674  lpadlem2  34714  subfacval2  35252  cvmliftlem2  35351  snmlff  35394  sinccvglem  35737  bcprod  35803  faclimlem1  35808  faclimlem2  35809  faclim2  35813  knoppndvlem14  36590  knoppndvlem15  36591  knoppndvlem16  36592  knoppndvlem18  36594  poimirlem29  37709  poimirlem30  37710  poimirlem31  37711  poimirlem32  37712  itg2addnclem  37731  areacirclem1  37768  areacirclem4  37771  cntotbnd  37856  lcmineqlem11  42152  lcmineqlem12  42153  aks4d1p1p7  42187  aks4d1p8d2  42198  hashscontpow1  42234  2ap1caineq  42258  sticksstones10  42268  sticksstones12a  42270  aks6d1c6lem1  42283  aks6d1c7lem1  42293  aks6d1c7  42297  oddnumth  42429  oexpreposd  42440  readvrec  42480  frlmvscadiccat  42624  fltnltalem  42780  3cubeslem2  42802  3cubeslem3r  42804  irrapxlem1  42939  irrapxlem4  42942  pell1qrgaplem  42990  reglogexpbas  43014  rmspecfund  43026  rmxy1  43039  rmxp1  43049  rmyp1  43050  rmxm1  43051  jm2.17a  43077  jm2.18  43105  jm2.23  43113  jm2.25  43116  jm2.16nn0  43121  relexpmulnn  43826  int-mul11d  44299  nzprmdif  44436  expgrowthi  44450  expgrowth  44452  binomcxplemdvbinom  44470  binomcxplemnotnn0  44473  sqrlearg  45677  fmul01  45704  fmul01lt1lem1  45708  0ellimcdiv  45771  dvxpaek  46062  dvnxpaek  46064  itgiccshift  46102  itgperiod  46103  itgsbtaddcnst  46104  stoweidlem11  46133  stoweidlem26  46148  stoweidlem38  46160  wallispilem4  46190  stirlinglem1  46196  stirlinglem3  46198  stirlinglem6  46201  stirlinglem7  46202  stirlinglem8  46203  stirlinglem10  46205  stirlinglem12  46207  dirkertrigeqlem3  46222  dirkertrigeq  46223  dirkercncflem1  46225  dirkercncflem2  46226  fourierdlem28  46257  fourierdlem30  46259  fourierdlem39  46268  fourierdlem47  46275  fourierdlem60  46288  fourierdlem61  46289  fourierdlem73  46301  fourierdlem83  46311  fourierdlem87  46315  etransclem14  46370  etransclem24  46380  etransclem25  46381  etransclem35  46391  smfmullem1  46913  deccarry  47435  fpprwppr  47863  fpprwpprb  47864  logblt1b  48689  nn0sumshdiglem2  48747  itcovalpclem2  48796  itcovalt2lem1  48800  eenglngeehlnmlem1  48862  eenglngeehlnmlem2  48863  line2ylem  48876