Theorem mulridd 11232

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  (class class class)co 7404  ℂcc 11107  1c1 11110   · cmul 11114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-mulcl 11171  ax-mulcom 11173  ax-mulass 11175  ax-distr 11176  ax-1rid 11179  ax-cnre 11182

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-rex 3065  df-rab 3427  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-iota 6488  df-fv 6544  df-ov 7407

This theorem is referenced by:  muladd11  11385  muls1d  11675  divrec  11889  diveq1  11906  conjmul  11932  divelunit  13474  modid  13864  addmodlteq  13914  expadd  14072  leexp2r  14141  nnlesq  14171  sqoddm1div8  14208  faclbnd  14252  faclbnd2  14253  faclbnd4lem3  14257  faclbnd6  14261  facavg  14263  bcn0  14272  bcn1  14275  hashf1lem2  14420  hashfac  14422  reccn2  15544  iseraltlem2  15632  iseraltlem3  15633  hash2iun1dif1  15773  binom11  15781  harmonic  15808  trireciplem  15811  geoserg  15815  pwdif  15817  pwm1geoser  15818  cvgrat  15832  fprodsplit  15913  fprodle  15943  fsumcube  16007  efzval  16049  tanhlt1  16107  tanaddlem  16113  tanadd  16114  cos01gt0  16138  absef  16144  1dvds  16218  bitsfzo  16380  bitsmod  16381  sqgcd  16506  lcm1  16551  coprmdvds  16594  qredeu  16599  phiprmpw  16715  coprimeprodsq  16747  pc2dvds  16818  sumhash  16835  fldivp1  16836  pcfaclem  16837  prmpwdvds  16843  prmreclem1  16855  vdwlem3  16922  vdwlem9  16928  prmop1  16977  sylow2a  19536  odadd  19767  zsssubrg  21314  zringcyg  21351  prmirredlem  21354  mulgrhm2  21360  pzriprnglem6  21368  pzriprnglem12  21374  znrrg  21455  mhppwdeg  22028  icopnfcnv  24817  icopnfhmeo  24818  lebnumii  24842  reparphti  24873  reparphtiOLD  24874  itg2const  25620  itg2monolem3  25632  bddibl  25719  dveflem  25861  mvth  25875  dvlipcn  25877  dvivthlem1  25891  dvfsumle  25904  dvfsumleOLD  25905  dvfsumabs  25907  dvfsumlem2  25911  dvfsumlem2OLD  25912  plyconst  26090  plyeq0lem  26094  plyco  26125  0dgrb  26130  coefv0  26132  vieta1  26197  aaliou3lem2  26228  tayl0  26246  taylply2  26252  taylply2OLD  26253  dvtaylp  26255  taylthlem2  26259  taylthlem2OLD  26260  radcnvlem1  26299  abelthlem1  26318  abelthlem2  26319  abelthlem3  26320  abelthlem7  26325  abelthlem8  26326  abelthlem9  26327  efper  26364  tangtx  26390  eflogeq  26486  logdivlti  26504  logcnlem4  26529  advlogexp  26539  cxpmul2  26573  dvcxp2  26625  cxpaddle  26637  cxpeq  26642  loglesqrt  26643  relogbexp  26662  ang180lem5  26695  isosctrlem2  26701  isosctrlem3  26702  heron  26720  2efiatan  26800  dvatan  26817  leibpi  26824  birthdaylem3  26835  jensenlem2  26870  logdiflbnd  26877  harmonicbnd4  26893  lgamgulmlem2  26912  lgamcvg2  26937  ftalem5  26959  basellem2  26964  basellem5  26967  basellem8  26970  0sgm  27026  muinv  27075  chpub  27103  logfaclbnd  27105  logexprlim  27108  dchrsum2  27151  sumdchr2  27153  bposlem1  27167  bposlem2  27168  bposlem5  27171  lgsquad2lem1  27267  lgsquad3  27270  2sqlem6  27306  2sqlem8  27309  chtppilim  27358  vmadivsum  27365  dchrisumlem1  27372  dchrisum0flblem1  27391  rpvmasum2  27395  dchrisum0re  27396  dchrisum0lem2a  27400  dchrisum0lem3  27402  rpvmasum  27409  mudivsum  27413  mulogsumlem  27414  vmalogdivsum2  27421  pntrsumo1  27448  pntrlog2bndlem2  27461  pntrlog2bndlem4  27463  pntrlog2bndlem5  27464  pntibndlem2  27474  pntlemc  27478  pntlemf  27488  ostth2lem2  27517  ostth2lem3  27518  ostth2lem4  27519  ostth2  27520  ostth3  27521  ttgcontlem1  28645  axpaschlem  28701  axcontlem2  28726  axcontlem4  28728  axcontlem8  28732  nmoub3i  30530  ubthlem2  30628  htthlem  30674  nmcexi  31783  nmopcoadji  31858  branmfn  31862  rearchi  32963  ccfldextdgrr  33264  madjusmdetlem4  33339  ccatmulgnn0dir  34082  ofcccat  34083  itgexpif  34146  hashreprin  34160  circlemeth  34180  lpadlem2  34220  subfacval2  34705  cvmliftlem2  34804  snmlff  34847  sinccvglem  35184  bcprod  35240  faclimlem1  35245  faclimlem2  35246  faclim2  35250  knoppndvlem14  35908  knoppndvlem15  35909  knoppndvlem16  35910  knoppndvlem18  35912  poimirlem29  37029  poimirlem30  37030  poimirlem31  37031  poimirlem32  37032  itg2addnclem  37051  areacirclem1  37088  areacirclem4  37091  cntotbnd  37176  lcmineqlem11  41419  lcmineqlem12  41420  aks4d1p1p7  41454  aks4d1p8d2  41465  hashscontpow1  41497  2ap1caineq  41504  sticksstones10  41514  sticksstones12a  41516  frlmvscadiccat  41623  oddnumth  41749  oexpreposd  41759  expgcd  41772  fltnltalem  41964  3cubeslem2  41983  3cubeslem3r  41985  irrapxlem1  42120  irrapxlem4  42123  pell1qrgaplem  42171  reglogexpbas  42195  rmspecfund  42207  rmxy1  42221  rmxp1  42231  rmyp1  42232  rmxm1  42233  jm2.17a  42259  jm2.18  42287  jm2.23  42295  jm2.25  42298  jm2.16nn0  42303  relexpmulnn  43018  int-mul11d  43492  nzprmdif  43636  expgrowthi  43650  expgrowth  43652  binomcxplemdvbinom  43670  binomcxplemnotnn0  43673  sqrlearg  44820  fmul01  44850  fmul01lt1lem1  44854  0ellimcdiv  44919  dvxpaek  45210  dvnxpaek  45212  itgiccshift  45250  itgperiod  45251  itgsbtaddcnst  45252  stoweidlem11  45281  stoweidlem26  45296  stoweidlem38  45308  wallispilem4  45338  stirlinglem1  45344  stirlinglem3  45346  stirlinglem6  45349  stirlinglem7  45350  stirlinglem8  45351  stirlinglem10  45353  stirlinglem12  45355  dirkertrigeqlem3  45370  dirkertrigeq  45371  dirkercncflem1  45373  dirkercncflem2  45374  fourierdlem28  45405  fourierdlem30  45407  fourierdlem39  45416  fourierdlem47  45423  fourierdlem60  45436  fourierdlem61  45437  fourierdlem73  45449  fourierdlem83  45459  fourierdlem87  45463  etransclem14  45518  etransclem24  45528  etransclem25  45529  etransclem35  45539  smfmullem1  46061  deccarry  46573  fpprwppr  46961  fpprwpprb  46962  logblt1b  47507  nn0sumshdiglem2  47565  itcovalpclem2  47614  itcovalt2lem1  47618  eenglngeehlnmlem1  47680  eenglngeehlnmlem2  47681  line2ylem  47694