Theorem mulridd 11275

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150  1c1 11153   · cmul 11157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-mulcl 11214  ax-mulcom 11216  ax-mulass 11218  ax-distr 11219  ax-1rid 11222  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433

This theorem is referenced by:  muladd11  11428  muls1d  11720  divrec  11935  diveq1  11949  conjmul  11981  divelunit  13530  modid  13932  addmodlteq  13983  expadd  14141  leexp2r  14210  nnlesq  14240  sqoddm1div8  14278  faclbnd  14325  faclbnd2  14326  faclbnd4lem3  14330  faclbnd6  14334  facavg  14336  bcn0  14345  bcn1  14348  hashf1lem2  14491  hashfac  14493  reccn2  15629  iseraltlem2  15715  iseraltlem3  15716  hash2iun1dif1  15856  binom11  15864  harmonic  15891  trireciplem  15894  geoserg  15898  pwdif  15900  pwm1geoser  15901  cvgrat  15915  fprodsplit  15998  fprodle  16028  fsumcube  16092  efzval  16134  tanhlt1  16192  tanaddlem  16198  tanadd  16199  cos01gt0  16223  absef  16229  1dvds  16304  bitsfzo  16468  bitsmod  16469  sqgcd  16595  expgcd  16596  lcm1  16643  coprmdvds  16686  qredeu  16691  phiprmpw  16809  coprimeprodsq  16841  pc2dvds  16912  sumhash  16929  fldivp1  16930  pcfaclem  16931  prmpwdvds  16937  prmreclem1  16949  vdwlem3  17016  vdwlem9  17022  prmop1  17071  sylow2a  19651  odadd  19882  zsssubrg  21460  zringcyg  21497  prmirredlem  21500  mulgrhm2  21506  pzriprnglem6  21514  pzriprnglem12  21520  znrrg  21601  mhppwdeg  22171  icopnfcnv  24986  icopnfhmeo  24987  lebnumii  25011  reparphti  25042  reparphtiOLD  25043  itg2const  25789  itg2monolem3  25801  bddibl  25889  dveflem  26031  mvth  26045  dvlipcn  26047  dvivthlem1  26061  dvfsumle  26074  dvfsumleOLD  26075  dvfsumabs  26077  dvfsumlem2  26081  dvfsumlem2OLD  26082  plyconst  26259  plyeq0lem  26263  plyco  26294  0dgrb  26299  coefv0  26301  vieta1  26368  aaliou3lem2  26399  tayl0  26417  taylply2  26423  taylply2OLD  26424  dvtaylp  26426  taylthlem2  26430  taylthlem2OLD  26431  radcnvlem1  26470  abelthlem1  26489  abelthlem2  26490  abelthlem3  26491  abelthlem7  26496  abelthlem8  26497  abelthlem9  26498  efper  26535  tangtx  26561  eflogeq  26658  logdivlti  26676  logcnlem4  26701  advlogexp  26711  cxpmul2  26745  dvcxp2  26797  cxpaddle  26809  cxpeq  26814  loglesqrt  26818  relogbexp  26837  ang180lem5  26870  isosctrlem2  26876  isosctrlem3  26877  heron  26895  2efiatan  26975  dvatan  26992  leibpi  26999  birthdaylem3  27010  jensenlem2  27045  logdiflbnd  27052  harmonicbnd4  27068  lgamgulmlem2  27087  lgamcvg2  27112  ftalem5  27134  basellem2  27139  basellem5  27142  basellem8  27145  0sgm  27201  muinv  27250  chpub  27278  logfaclbnd  27280  logexprlim  27283  dchrsum2  27326  sumdchr2  27328  bposlem1  27342  bposlem2  27343  bposlem5  27346  lgsquad2lem1  27442  lgsquad3  27445  2sqlem6  27481  2sqlem8  27484  chtppilim  27533  vmadivsum  27540  dchrisumlem1  27547  dchrisum0flblem1  27566  rpvmasum2  27570  dchrisum0re  27571  dchrisum0lem2a  27575  dchrisum0lem3  27577  rpvmasum  27584  mudivsum  27588  mulogsumlem  27589  vmalogdivsum2  27596  pntrsumo1  27623  pntrlog2bndlem2  27636  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  pntibndlem2  27649  pntlemc  27653  pntlemf  27663  ostth2lem2  27692  ostth2lem3  27693  ostth2lem4  27694  ostth2  27695  ostth3  27696  ttgcontlem1  28913  axpaschlem  28969  axcontlem2  28994  axcontlem4  28996  axcontlem8  29000  nmoub3i  30801  ubthlem2  30899  htthlem  30945  nmcexi  32054  nmopcoadji  32129  branmfn  32133  rearchi  33353  ccfldextdgrr  33696  madjusmdetlem4  33790  ccatmulgnn0dir  34535  ofcccat  34536  itgexpif  34599  hashreprin  34613  circlemeth  34633  lpadlem2  34673  subfacval2  35171  cvmliftlem2  35270  snmlff  35313  sinccvglem  35656  bcprod  35717  faclimlem1  35722  faclimlem2  35723  faclim2  35727  knoppndvlem14  36507  knoppndvlem15  36508  knoppndvlem16  36509  knoppndvlem18  36511  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  poimirlem32  37638  itg2addnclem  37657  areacirclem1  37694  areacirclem4  37697  cntotbnd  37782  lcmineqlem11  42020  lcmineqlem12  42021  aks4d1p1p7  42055  aks4d1p8d2  42066  hashscontpow1  42102  2ap1caineq  42126  sticksstones10  42136  sticksstones12a  42138  aks6d1c6lem1  42151  aks6d1c7lem1  42161  aks6d1c7  42165  oddnumth  42323  oexpreposd  42335  readvrec  42370  frlmvscadiccat  42492  fltnltalem  42648  3cubeslem2  42672  3cubeslem3r  42674  irrapxlem1  42809  irrapxlem4  42812  pell1qrgaplem  42860  reglogexpbas  42884  rmspecfund  42896  rmxy1  42910  rmxp1  42920  rmyp1  42921  rmxm1  42922  jm2.17a  42948  jm2.18  42976  jm2.23  42984  jm2.25  42987  jm2.16nn0  42992  relexpmulnn  43698  int-mul11d  44171  nzprmdif  44314  expgrowthi  44328  expgrowth  44330  binomcxplemdvbinom  44348  binomcxplemnotnn0  44351  sqrlearg  45505  fmul01  45535  fmul01lt1lem1  45539  0ellimcdiv  45604  dvxpaek  45895  dvnxpaek  45897  itgiccshift  45935  itgperiod  45936  itgsbtaddcnst  45937  stoweidlem11  45966  stoweidlem26  45981  stoweidlem38  45993  wallispilem4  46023  stirlinglem1  46029  stirlinglem3  46031  stirlinglem6  46034  stirlinglem7  46035  stirlinglem8  46036  stirlinglem10  46038  stirlinglem12  46040  dirkertrigeqlem3  46055  dirkertrigeq  46056  dirkercncflem1  46058  dirkercncflem2  46059  fourierdlem28  46090  fourierdlem30  46092  fourierdlem39  46101  fourierdlem47  46108  fourierdlem60  46121  fourierdlem61  46122  fourierdlem73  46134  fourierdlem83  46144  fourierdlem87  46148  etransclem14  46203  etransclem24  46213  etransclem25  46214  etransclem35  46224  smfmullem1  46746  deccarry  47260  fpprwppr  47663  fpprwpprb  47664  logblt1b  48413  nn0sumshdiglem2  48471  itcovalpclem2  48520  itcovalt2lem1  48524  eenglngeehlnmlem1  48586  eenglngeehlnmlem2  48587  line2ylem  48600