Theorem mulridd 11214

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086  1c1 11089   · cmul 11093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-mulcl 11150  ax-mulcom 11152  ax-mulass 11154  ax-distr 11155  ax-1rid 11158  ax-cnre 11161

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533  df-ov 7403

This theorem is referenced by:  muladd11  11368  muls1d  11662  divrec  11876  diveq1  11890  conjmul  11923  divelunit  13512  modid  13920  addmodlteq  13973  expadd  14131  leexp2r  14201  nnlesq  14232  sqoddm1div8  14270  faclbnd  14317  faclbnd2  14318  faclbnd4lem3  14322  faclbnd6  14326  facavg  14328  bcn0  14337  bcn1  14340  hashf1lem2  14483  hashfac  14485  reccn2  15638  iseraltlem2  15724  iseraltlem3  15725  fsumconst1  15832  hash2iun1dif1  15866  indsumhash  15871  binom11  15876  harmonic  15903  trireciplem  15906  geoserg  15910  pwdif  15912  pwm1geoser  15913  cvgrat  15927  fprodsplit  16010  fprodle  16040  fsumcube  16104  efzval  16148  tanhlt1  16206  tanaddlem  16212  tanadd  16213  cos01gt0  16237  absef  16243  1dvds  16318  bitsfzo  16483  bitsmod  16484  sqgcd  16610  expgcd  16611  lcm1  16658  coprmdvds  16701  qredeu  16706  phiprmpw  16825  coprimeprodsq  16858  pc2dvds  16929  sumhash  16946  fldivp1  16947  pcfaclem  16948  prmpwdvds  16954  prmreclem1  16966  vdwlem3  17033  vdwlem9  17039  prmop1  17088  sylow2a  19680  odadd  19911  zsssubrg  21535  zringcyg  21579  prmirredlem  21582  mulgrhm2  21588  pzriprnglem6  21596  pzriprnglem12  21602  znrrg  21675  mhppwdeg  22273  icopnfcnv  25062  icopnfhmeo  25063  lebnumii  25086  reparphti  25117  itg2const  25860  itg2monolem3  25872  bddibl  25960  dveflem  26099  mvth  26112  dvlipcn  26114  dvivthlem1  26128  dvfsumle  26141  dvfsumabs  26143  dvfsumlem2  26147  plyconst  26324  plyeq0lem  26328  plyco  26359  0dgrb  26364  coefv0  26366  vieta1  26434  aaliou3lem2  26465  tayl0  26483  taylply2  26489  dvtaylp  26491  taylthlem2  26495  radcnvlem1  26534  abelthlem1  26552  abelthlem2  26553  abelthlem3  26554  abelthlem7  26559  abelthlem8  26560  abelthlem9  26561  efper  26602  tangtx  26628  eflogeq  26725  logdivlti  26743  logcnlem4  26768  advlogexp  26778  cxpmul2  26812  dvcxp2  26864  cxpaddle  26875  cxpeq  26880  loglesqrt  26884  relogbexp  26903  ang180lem5  26936  isosctrlem2  26942  isosctrlem3  26943  heron  26961  2efiatan  27041  dvatan  27058  leibpi  27065  birthdaylem3  27076  jensenlem2  27110  logdiflbnd  27117  harmonicbnd4  27133  lgamgulmlem2  27152  lgamcvg2  27177  ftalem5  27199  basellem2  27204  basellem5  27207  basellem8  27210  0sgm  27266  muinv  27315  chpub  27342  logfaclbnd  27344  logexprlim  27347  dchrsum2  27390  sumdchr2  27392  bposlem1  27406  bposlem2  27407  bposlem5  27410  lgsquad2lem1  27506  lgsquad3  27509  2sqlem6  27545  2sqlem8  27548  chtppilim  27597  vmadivsum  27604  dchrisumlem1  27611  dchrisum0flblem1  27630  rpvmasum2  27634  dchrisum0re  27635  dchrisum0lem2a  27639  dchrisum0lem3  27641  rpvmasum  27648  mudivsum  27652  mulogsumlem  27653  vmalogdivsum2  27660  pntrsumo1  27687  pntrlog2bndlem2  27700  pntrlog2bndlem4  27702  pntrlog2bndlem5  27703  pntibndlem2  27713  pntlemc  27717  pntlemf  27727  ostth2lem2  27756  ostth2lem3  27757  ostth2lem4  27758  ostth2  27759  ostth3  27760  ttgcontlem1  29143  axpaschlem  29199  axcontlem2  29224  axcontlem4  29226  axcontlem8  29230  nmoub3i  31034  ubthlem2  31132  htthlem  31178  nmcexi  32287  nmopcoadji  32362  branmfn  32366  gsumind  33580  rearchi  33581  vietadeg1  33885  ccfldextdgrr  33979  nn0constr  34068  constrrecl  34076  constrimcl  34077  constrreinvcl  34079  constrinvcl  34080  constrresqrtcl  34084  constrabscl  34085  cos9thpiminplylem1  34089  madjusmdetlem4  34137  ccatmulgnn0dir  34849  ofcccat  34850  itgexpif  34910  hashreprin  34924  circlemeth  34944  lpadlem2  34987  subfacval2  35550  cvmliftlem2  35649  snmlff  35692  sinccvglem  36035  bcprod  36101  faclimlem1  36106  faclimlem2  36107  faclim2  36111  knoppndvlem14  36976  knoppndvlem15  36977  knoppndvlem16  36978  knoppndvlem18  36980  poimirlem29  38160  poimirlem30  38161  poimirlem31  38162  poimirlem32  38163  itg2addnclem  38182  areacirclem1  38219  areacirclem4  38222  cntotbnd  38307  lcmineqlem11  42668  lcmineqlem12  42669  aks4d1p1p7  42703  aks4d1p8d2  42714  hashscontpow1  42750  2ap1caineq  42774  sticksstones10  42784  sticksstones12a  42786  aks6d1c6lem1  42799  aks6d1c7lem1  42809  aks6d1c7  42813  oddnumth  42932  oexpreposd  42943  readvrec  42983  frlmvscadiccat  43140  fltnltalem  43256  3cubeslem2  43278  3cubeslem3r  43280  irrapxlem1  43411  irrapxlem4  43414  pell1qrgaplem  43462  reglogexpbas  43486  rmspecfund  43498  rmxy1  43511  rmxp1  43521  rmyp1  43522  rmxm1  43523  jm2.17a  43549  jm2.18  43577  jm2.23  43585  jm2.25  43588  jm2.16nn0  43593  relexpmulnn  44297  int-mul11d  44770  nzprmdif  44893  expgrowthi  44907  expgrowth  44909  binomcxplemdvbinom  44927  binomcxplemnotnn0  44930  sqrlearg  46127  fmul01  46154  fmul01lt1lem1  46158  0ellimcdiv  46221  dvxpaek  46512  dvnxpaek  46514  itgiccshift  46552  itgperiod  46553  itgsbtaddcnst  46554  stoweidlem11  46583  stoweidlem26  46598  stoweidlem38  46610  wallispilem4  46640  stirlinglem1  46646  stirlinglem3  46648  stirlinglem6  46651  stirlinglem7  46652  stirlinglem8  46653  stirlinglem10  46655  stirlinglem12  46657  dirkertrigeqlem3  46672  dirkertrigeq  46673  dirkercncflem1  46675  dirkercncflem2  46676  fourierdlem28  46707  fourierdlem30  46709  fourierdlem39  46718  fourierdlem47  46725  fourierdlem60  46738  fourierdlem61  46739  fourierdlem73  46751  fourierdlem83  46761  fourierdlem87  46765  etransclem14  46820  etransclem24  46830  etransclem25  46831  etransclem35  46841  smfmullem1  47363  sin3t  47463  cos3t  47464  sin5tlem1  47465  deccarry  47903  fpprwppr  48359  fpprwpprb  48360  logblt1b  49195  nn0sumshdiglem2  49253  itcovalpclem2  49302  itcovalt2lem1  49306  eenglngeehlnmlem1  49368  eenglngeehlnmlem2  49369  line2ylem  49382