Theorem mulridd 11198

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073  1c1 11076   · cmul 11080

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 2702  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-mulcl 11137  ax-mulcom 11139  ax-mulass 11141  ax-distr 11142  ax-1rid 11145  ax-cnre 11148

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 2709  df-cleq 2722  df-clel 2804  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  muladd11  11351  muls1d  11645  divrec  11860  diveq1  11874  conjmul  11906  divelunit  13462  modid  13865  addmodlteq  13918  expadd  14076  leexp2r  14146  nnlesq  14177  sqoddm1div8  14215  faclbnd  14262  faclbnd2  14263  faclbnd4lem3  14267  faclbnd6  14271  facavg  14273  bcn0  14282  bcn1  14285  hashf1lem2  14428  hashfac  14430  reccn2  15570  iseraltlem2  15656  iseraltlem3  15657  hash2iun1dif1  15797  binom11  15805  harmonic  15832  trireciplem  15835  geoserg  15839  pwdif  15841  pwm1geoser  15842  cvgrat  15856  fprodsplit  15939  fprodle  15969  fsumcube  16033  efzval  16077  tanhlt1  16135  tanaddlem  16141  tanadd  16142  cos01gt0  16166  absef  16172  1dvds  16247  bitsfzo  16412  bitsmod  16413  sqgcd  16539  expgcd  16540  lcm1  16587  coprmdvds  16630  qredeu  16635  phiprmpw  16753  coprimeprodsq  16786  pc2dvds  16857  sumhash  16874  fldivp1  16875  pcfaclem  16876  prmpwdvds  16882  prmreclem1  16894  vdwlem3  16961  vdwlem9  16967  prmop1  17016  sylow2a  19556  odadd  19787  zsssubrg  21349  zringcyg  21386  prmirredlem  21389  mulgrhm2  21395  pzriprnglem6  21403  pzriprnglem12  21409  znrrg  21482  mhppwdeg  22044  icopnfcnv  24847  icopnfhmeo  24848  lebnumii  24872  reparphti  24903  reparphtiOLD  24904  itg2const  25648  itg2monolem3  25660  bddibl  25748  dveflem  25890  mvth  25904  dvlipcn  25906  dvivthlem1  25920  dvfsumle  25933  dvfsumleOLD  25934  dvfsumabs  25936  dvfsumlem2  25940  dvfsumlem2OLD  25941  plyconst  26118  plyeq0lem  26122  plyco  26153  0dgrb  26158  coefv0  26160  vieta1  26227  aaliou3lem2  26258  tayl0  26276  taylply2  26282  taylply2OLD  26283  dvtaylp  26285  taylthlem2  26289  taylthlem2OLD  26290  radcnvlem1  26329  abelthlem1  26348  abelthlem2  26349  abelthlem3  26350  abelthlem7  26355  abelthlem8  26356  abelthlem9  26357  efper  26395  tangtx  26421  eflogeq  26518  logdivlti  26536  logcnlem4  26561  advlogexp  26571  cxpmul2  26605  dvcxp2  26657  cxpaddle  26669  cxpeq  26674  loglesqrt  26678  relogbexp  26697  ang180lem5  26730  isosctrlem2  26736  isosctrlem3  26737  heron  26755  2efiatan  26835  dvatan  26852  leibpi  26859  birthdaylem3  26870  jensenlem2  26905  logdiflbnd  26912  harmonicbnd4  26928  lgamgulmlem2  26947  lgamcvg2  26972  ftalem5  26994  basellem2  26999  basellem5  27002  basellem8  27005  0sgm  27061  muinv  27110  chpub  27138  logfaclbnd  27140  logexprlim  27143  dchrsum2  27186  sumdchr2  27188  bposlem1  27202  bposlem2  27203  bposlem5  27206  lgsquad2lem1  27302  lgsquad3  27305  2sqlem6  27341  2sqlem8  27344  chtppilim  27393  vmadivsum  27400  dchrisumlem1  27407  dchrisum0flblem1  27426  rpvmasum2  27430  dchrisum0re  27431  dchrisum0lem2a  27435  dchrisum0lem3  27437  rpvmasum  27444  mudivsum  27448  mulogsumlem  27449  vmalogdivsum2  27456  pntrsumo1  27483  pntrlog2bndlem2  27496  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  pntibndlem2  27509  pntlemc  27513  pntlemf  27523  ostth2lem2  27552  ostth2lem3  27553  ostth2lem4  27554  ostth2  27555  ostth3  27556  ttgcontlem1  28819  axpaschlem  28874  axcontlem2  28899  axcontlem4  28901  axcontlem8  28905  nmoub3i  30709  ubthlem2  30807  htthlem  30853  nmcexi  31962  nmopcoadji  32037  branmfn  32041  rearchi  33324  ccfldextdgrr  33674  nn0constr  33758  constrrecl  33766  constrimcl  33767  constrreinvcl  33769  constrinvcl  33770  constrresqrtcl  33774  constrabscl  33775  cos9thpiminplylem1  33779  madjusmdetlem4  33827  ccatmulgnn0dir  34540  ofcccat  34541  itgexpif  34604  hashreprin  34618  circlemeth  34638  lpadlem2  34678  subfacval2  35181  cvmliftlem2  35280  snmlff  35323  sinccvglem  35666  bcprod  35732  faclimlem1  35737  faclimlem2  35738  faclim2  35742  knoppndvlem14  36520  knoppndvlem15  36521  knoppndvlem16  36522  knoppndvlem18  36524  poimirlem29  37650  poimirlem30  37651  poimirlem31  37652  poimirlem32  37653  itg2addnclem  37672  areacirclem1  37709  areacirclem4  37712  cntotbnd  37797  lcmineqlem11  42034  lcmineqlem12  42035  aks4d1p1p7  42069  aks4d1p8d2  42080  hashscontpow1  42116  2ap1caineq  42140  sticksstones10  42150  sticksstones12a  42152  aks6d1c6lem1  42165  aks6d1c7lem1  42175  aks6d1c7  42179  oddnumth  42306  oexpreposd  42317  readvrec  42357  frlmvscadiccat  42501  fltnltalem  42657  3cubeslem2  42680  3cubeslem3r  42682  irrapxlem1  42817  irrapxlem4  42820  pell1qrgaplem  42868  reglogexpbas  42892  rmspecfund  42904  rmxy1  42918  rmxp1  42928  rmyp1  42929  rmxm1  42930  jm2.17a  42956  jm2.18  42984  jm2.23  42992  jm2.25  42995  jm2.16nn0  43000  relexpmulnn  43705  int-mul11d  44178  nzprmdif  44315  expgrowthi  44329  expgrowth  44331  binomcxplemdvbinom  44349  binomcxplemnotnn0  44352  sqrlearg  45558  fmul01  45585  fmul01lt1lem1  45589  0ellimcdiv  45654  dvxpaek  45945  dvnxpaek  45947  itgiccshift  45985  itgperiod  45986  itgsbtaddcnst  45987  stoweidlem11  46016  stoweidlem26  46031  stoweidlem38  46043  wallispilem4  46073  stirlinglem1  46079  stirlinglem3  46081  stirlinglem6  46084  stirlinglem7  46085  stirlinglem8  46086  stirlinglem10  46088  stirlinglem12  46090  dirkertrigeqlem3  46105  dirkertrigeq  46106  dirkercncflem1  46108  dirkercncflem2  46109  fourierdlem28  46140  fourierdlem30  46142  fourierdlem39  46151  fourierdlem47  46158  fourierdlem60  46171  fourierdlem61  46172  fourierdlem73  46184  fourierdlem83  46194  fourierdlem87  46198  etransclem14  46253  etransclem24  46263  etransclem25  46264  etransclem35  46274  smfmullem1  46796  deccarry  47316  fpprwppr  47744  fpprwpprb  47745  logblt1b  48557  nn0sumshdiglem2  48615  itcovalpclem2  48664  itcovalt2lem1  48668  eenglngeehlnmlem1  48730  eenglngeehlnmlem2  48731  line2ylem  48744