Theorem mulridd 11244

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  (class class class)co 7423  ℂcc 11116  1c1 11119   · cmul 11123

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-resscn 11175  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-mulcl 11180  ax-mulcom 11182  ax-mulass 11184  ax-distr 11185  ax-1rid 11188  ax-cnre 11191

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426

This theorem is used by:  muladd11  11398  muls1d  11692  divrec  11906  diveq1  11919  conjmul  11950  divelunit  13539  modid  13949  addmodlteq  14002  expadd  14160  leexp2r  14230  nnlesq  14261  sqoddm1div8  14299  faclbnd  14346  faclbnd2  14347  faclbnd4lem3  14351  faclbnd6  14355  facavg  14357  bcn0  14366  bcn1  14369  hashf1lem2  14513  hashfac  14515  reccn2  15674  iseraltlem2  15760  iseraltlem3  15761  fsumconst1  15868  hash2iun1dif1  15902  indsumhash  15907  binom11  15912  harmonic  15939  trireciplem  15942  geoserg  15946  pwdif  15948  pwm1geoser  15949  cvgrat  15963  fprodsplit  16046  fprodle  16076  fsumcube  16139  efzval  16183  tanhlt1  16241  tanaddlem  16247  tanadd  16248  cos01gt0  16272  absef  16278  1dvds  16353  bitsfzo  16518  bitsmod  16519  sqgcd  16645  expgcd  16646  lcm1  16693  coprmdvds  16736  qredeu  16741  phiprmpw  16860  coprimeprodsq  16893  pc2dvds  16964  sumhash  16981  fldivp1  16982  pcfaclem  16983  prmpwdvds  16989  prmreclem1  17001  vdwlem3  17068  vdwlem9  17074  prmop1  17123  sylow2a  19720  odadd  19951  zsssubrg  21612  zringcyg  21656  prmirredlem  21659  mulgrhm2  21665  pzriprnglem6  21673  pzriprnglem12  21679  znrrg  21752  mhppwdeg  22350  icopnfcnv  25138  icopnfhmeo  25139  lebnumii  25162  reparphti  25193  itg2const  25936  itg2monolem3  25948  bddibl  26036  dveflem  26175  mvth  26188  dvlipcn  26190  dvivthlem1  26204  dvfsumle  26217  dvfsumabs  26219  dvfsumlem2  26223  plyconst  26400  plyeq0lem  26404  plyco  26435  0dgrb  26440  coefv0  26442  vieta1  26510  aaliou3lem2  26543  tayl0  26562  taylply2  26568  dvtaylp  26570  taylthlem2  26574  radcnvlem1  26613  abelthlem1  26631  abelthlem2  26632  abelthlem3  26633  abelthlem7  26638  abelthlem8  26639  abelthlem9  26640  efper  26681  tangtx  26707  eflogeq  26804  logdivlti  26822  logcnlem4  26847  advlogexp  26857  cxpmul2  26891  dvcxp2  26943  cxpaddle  26954  cxpeq  26959  loglesqrt  26963  relogbexp  26982  ang180lem5  27015  isosctrlem2  27021  isosctrlem3  27022  heron  27040  2efiatan  27120  dvatan  27137  leibpi  27144  birthdaylem3  27155  jensenlem2  27189  logdiflbnd  27196  harmonicbnd4  27212  lgamgulmlem2  27231  lgamcvg2  27256  ftalem5  27278  basellem2  27283  basellem5  27286  basellem8  27289  0sgm  27345  muinv  27394  chpub  27421  logfaclbnd  27423  logexprlim  27426  dchrsum2  27469  sumdchr2  27471  bposlem1  27485  bposlem2  27486  bposlem5  27489  lgsquad2lem1  27585  lgsquad3  27588  2sqlem6  27624  2sqlem8  27627  chtppilim  27676  vmadivsum  27683  dchrisumlem1  27690  dchrisum0flblem1  27709  rpvmasum2  27713  dchrisum0re  27714  dchrisum0lem2a  27718  dchrisum0lem3  27720  rpvmasum  27727  mudivsum  27731  mulogsumlem  27732  vmalogdivsum2  27739  pntrsumo1  27766  pntrlog2bndlem2  27779  pntrlog2bndlem4  27781  pntrlog2bndlem5  27782  pntibndlem2  27792  pntlemc  27796  pntlemf  27806  ostth2lem2  27835  ostth2lem3  27836  ostth2lem4  27837  ostth2  27838  ostth3  27839  ttgcontlem1  29271  axpaschlem  29327  axcontlem2  29352  axcontlem4  29354  axcontlem8  29358  nmoub3i  31162  ubthlem2  31260  htthlem  31306  nmcexi  32415  nmopcoadji  32490  branmfn  32494  gsumind  33696  rearchi  33697  vietadeg1  33999  ccfldextdgrr  34093  nn0constr  34182  constrrecl  34190  constrimcl  34191  constrreinvcl  34193  constrinvcl  34194  constrresqrtcl  34198  constrabscl  34199  cos9thpiminplylem1  34203  madjusmdetlem4  34251  ccatmulgnn0dir  34963  ofcccat  34964  itgexpif  35024  hashreprin  35038  circlemeth  35058  lpadlem2  35101  subfacval2  35699  cvmliftlem2  35798  snmlff  35841  sinccvglem  36184  bcprod  36250  faclimlem1  36255  faclimlem2  36256  faclim2  36260  knoppndvlem14  37154  knoppndvlem15  37155  knoppndvlem16  37156  knoppndvlem18  37158  poimirlem29  38340  poimirlem30  38341  poimirlem31  38342  poimirlem32  38343  itg2addnclem  38362  areacirclem1  38399  areacirclem4  38402  cntotbnd  38487  lcmineqlem11  42846  lcmineqlem12  42847  aks4d1p1p7  42881  aks4d1p8d2  42892  hashscontpow1  42928  2ap1caineq  42952  sticksstones10  42962  sticksstones12a  42964  aks6d1c6lem1  42977  aks6d1c7lem1  42987  aks6d1c7  42991  oddnumth  43112  oexpreposd  43123  readvrec  43163  frlmvscadiccat  43320  fltnltalem  43434  3cubeslem2  43456  3cubeslem3r  43458  irrapxlem1  43589  irrapxlem4  43592  pell1qrgaplem  43640  reglogexpbas  43664  rmspecfund  43676  rmxy1  43689  rmxp1  43699  rmyp1  43700  rmxm1  43701  jm2.17a  43727  jm2.18  43755  jm2.23  43763  jm2.25  43766  jm2.16nn0  43771  relexpmulnn  44475  int-mul11d  44948  nzprmdif  45069  expgrowthi  45083  expgrowth  45085  binomcxplemdvbinom  45103  binomcxplemnotnn0  45106  sqrlearg  46309  fmul01  46336  fmul01lt1lem1  46340  0ellimcdiv  46403  dvxpaek  46694  dvnxpaek  46696  itgiccshift  46734  itgperiod  46735  itgsbtaddcnst  46736  stoweidlem11  46765  stoweidlem26  46780  stoweidlem38  46792  wallispilem4  46822  stirlinglem1  46828  stirlinglem3  46830  stirlinglem6  46833  stirlinglem7  46834  stirlinglem8  46835  stirlinglem10  46837  stirlinglem12  46839  dirkertrigeqlem3  46854  dirkertrigeq  46855  dirkercncflem1  46857  dirkercncflem2  46858  fourierdlem28  46889  fourierdlem30  46891  fourierdlem39  46900  fourierdlem47  46907  fourierdlem60  46920  fourierdlem61  46921  fourierdlem73  46933  fourierdlem83  46943  fourierdlem87  46947  etransclem14  47002  etransclem24  47012  etransclem25  47013  etransclem35  47023  smfmullem1  47545  sin3t  47648  cos3t  47649  sin5tlem1  47650  deccarry  48088  fpprwppr  48544  fpprwpprb  48545  logblt1b  49384  nn0sumshdiglem2  49442  itcovalpclem2  49491  itcovalt2lem1  49495  eenglngeehlnmlem1  49557  eenglngeehlnmlem2  49558  line2ylem  49571