Theorem mulridd 11307

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7412  ℂcc 11179  1c1 11182   · cmul 11186

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 2147  ax-9 2155  ax-ext 2733  ax-resscn 11238  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-mulcl 11243  ax-mulcom 11245  ax-mulass 11247  ax-distr 11248  ax-1rid 11251  ax-cnre 11254

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 2740  df-cleq 2753  df-clel 2836  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6487  df-fv 6539  df-ov 7415

This theorem is used by:  muladd11  11461  muls1d  11757  divrec  11971  diveq1  11984  conjmul  12015  divelunit  13606  modid  14016  addmodlteq  14069  expadd  14227  leexp2r  14297  nnlesq  14329  sqoddm1div8  14367  faclbnd  14414  faclbnd2  14415  faclbnd4lem3  14419  faclbnd6  14423  facavg  14425  bcn0  14434  bcn1  14437  hashf1lem2  14581  hashfac  14583  reccn2  15744  iseraltlem2  15830  iseraltlem3  15831  fsumconst1  15937  hash2iun1dif1  15971  indsumhash  15976  binom11  15981  harmonic  16008  trireciplem  16011  geoserg  16015  pwdif  16017  pwm1geoser  16018  cvgrat  16032  fprodsplit  16113  fprodle  16143  fsumcube  16206  efzval  16250  tanhlt1  16308  tanaddlem  16314  tanadd  16315  cos01gt0  16339  absef  16345  1dvds  16420  bitsfzo  16585  bitsmod  16586  sqgcd  16716  expgcd  16717  lcm1  16765  coprmdvds  16808  qredeu  16813  phiprmpw  16933  coprimeprodsq  16966  pc2dvds  17037  sumhash  17054  fldivp1  17055  pcfaclem  17056  prmpwdvds  17062  prmreclem1  17074  vdwlem3  17141  vdwlem9  17147  prmop1  17196  sylow2a  19813  odadd  20044  zsssubrg  21711  zringcyg  21755  prmirredlem  21758  mulgrhm2  21764  pzriprnglem6  21772  pzriprnglem12  21778  znrrg  21851  mhppwdeg  22451  icopnfcnv  25243  icopnfhmeo  25244  lebnumii  25267  reparphti  25298  itg2const  26041  itg2monolem3  26053  bddibl  26140  dveflem  26279  mvth  26292  dvlipcn  26294  dvivthlem1  26308  dvfsumle  26321  dvfsumabs  26323  dvfsumlem2  26327  plyconst  26504  plyeq0lem  26509  plyco  26540  0dgrb  26545  coefv0  26547  vieta1  26617  aaliou3lem2  26652  tayl0  26671  taylply2  26677  dvtaylp  26679  taylthlem2  26683  radcnvlem1  26722  abelthlem1  26740  abelthlem2  26741  abelthlem3  26742  abelthlem7  26747  abelthlem8  26748  abelthlem9  26749  efper  26790  tangtx  26816  eflogeq  26912  logdivlti  26930  logcnlem4  26955  advlogexp  26965  cxpmul2  26999  dvcxp2  27051  cxpaddle  27062  cxpeq  27067  loglesqrt  27071  relogbexp  27090  ang180lem5  27123  isosctrlem2  27129  isosctrlem3  27130  heron  27148  2efiatan  27228  dvatan  27245  leibpi  27252  birthdaylem3  27263  jensenlem2  27297  logdiflbnd  27304  harmonicbnd4  27320  lgamgulmlem2  27339  lgamcvg2  27364  ftalem5  27386  basellem2  27391  basellem5  27394  basellem8  27397  0sgm  27453  muinv  27502  chpub  27529  logfaclbnd  27531  logexprlim  27534  dchrsum2  27577  sumdchr2  27579  bposlem1  27593  bposlem2  27594  bposlem5  27597  lgsquad2lem1  27693  lgsquad3  27696  2sqlem6  27732  2sqlem8  27735  chtppilim  27784  vmadivsum  27791  dchrisumlem1  27798  dchrisum0flblem1  27817  rpvmasum2  27821  dchrisum0re  27822  dchrisum0lem2a  27826  dchrisum0lem3  27828  rpvmasum  27835  mudivsum  27839  mulogsumlem  27840  vmalogdivsum2  27847  pntrsumo1  27874  pntrlog2bndlem2  27887  pntrlog2bndlem4  27889  pntrlog2bndlem5  27890  pntibndlem2  27900  pntlemc  27904  pntlemf  27914  ostth2lem2  27943  ostth2lem3  27944  ostth2lem4  27945  ostth2  27946  ostth3  27947  ttgcontlem1  29444  axpaschlem  29500  axcontlem2  29525  axcontlem4  29527  axcontlem8  29531  nmoub3i  31357  ubthlem2  31455  htthlem  31501  nmcexi  32610  nmopcoadji  32685  branmfn  32689  gsumind  33888  rearchi  33889  vietadeg1  34192  ccfldextdgrr  34286  nn0constr  34375  constrrecl  34383  constrimcl  34384  constrreinvcl  34386  constrinvcl  34387  constrresqrtcl  34391  constrabscl  34392  cos9thpiminplylem1  34396  madjusmdetlem4  34444  ccatmulgnn0dir  35157  ofcccat  35158  itgexpif  35218  hashreprin  35232  circlemeth  35252  lpadlem2  35295  subfacval2  35921  cvmliftlem2  36020  snmlff  36063  sinccvglem  36406  bcprod  36472  faclimlem1  36477  faclimlem2  36478  faclim2  36482  knoppndvlem14  37361  knoppndvlem15  37362  knoppndvlem16  37363  knoppndvlem18  37365  poimirlem29  38535  poimirlem30  38536  poimirlem31  38537  poimirlem32  38538  itg2addnclem  38557  areacirclem1  38594  areacirclem4  38597  cntotbnd  38698  lcmineqlem11  43057  lcmineqlem12  43058  aks4d1p1p7  43092  aks4d1p8d2  43103  hashscontpow1  43139  2ap1caineq  43163  sticksstones10  43173  sticksstones12a  43175  aks6d1c6lem1  43188  aks6d1c7lem1  43198  aks6d1c7  43202  oddnumth  43336  oexpreposd  43347  readvrec  43381  frlmvscadiccat  43538  fltnltalem  43627  3cubeslem2  43649  3cubeslem3r  43651  irrapxlem1  43782  irrapxlem4  43785  pell1qrgaplem  43833  reglogexpbas  43857  rmspecfund  43869  rmxy1  43882  rmxp1  43892  rmyp1  43893  rmxm1  43894  jm2.17a  43920  jm2.18  43948  jm2.23  43956  jm2.25  43959  jm2.16nn0  43964  relexpmulnn  44668  int-mul11d  45141  nzprmdif  45262  expgrowthi  45276  expgrowth  45278  binomcxplemdvbinom  45296  binomcxplemnotnn0  45299  sqrlearg  46509  fmul01  46536  fmul01lt1lem1  46540  0ellimcdiv  46603  dvxpaek  46894  dvnxpaek  46896  itgiccshift  46934  itgperiod  46935  itgsbtaddcnst  46936  stoweidlem11  46965  stoweidlem26  46980  stoweidlem38  46992  wallispilem4  47022  stirlinglem1  47028  stirlinglem3  47030  stirlinglem6  47033  stirlinglem7  47034  stirlinglem8  47035  stirlinglem10  47037  stirlinglem12  47039  dirkertrigeqlem3  47054  dirkertrigeq  47055  dirkercncflem1  47057  dirkercncflem2  47058  fourierdlem28  47089  fourierdlem30  47091  fourierdlem39  47100  fourierdlem47  47107  fourierdlem60  47120  fourierdlem61  47121  fourierdlem73  47133  fourierdlem83  47143  fourierdlem87  47147  etransclem14  47202  etransclem24  47212  etransclem25  47213  etransclem35  47223  smfmullem1  47745  sin3t  47861  cos3t  47862  sin5tlem1  47863  deccarry  48325  fpprwppr  48781  fpprwpprb  48782  logblt1b  49620  nn0sumshdiglem2  49678  itcovalpclem2  49727  itcovalt2lem1  49731  eenglngeehlnmlem1  49793  eenglngeehlnmlem2  49794  line2ylem  49807