Theorem mulridd 11269

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  (class class class)co 7426  ℂcc 11144  1c1 11147   · cmul 11151

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 2699  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-mulcl 11208  ax-mulcom 11210  ax-mulass 11212  ax-distr 11213  ax-1rid 11216  ax-cnre 11219

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-rex 3068  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-iota 6505  df-fv 6561  df-ov 7429

This theorem is referenced by:  muladd11  11422  muls1d  11712  divrec  11926  diveq1  11943  conjmul  11969  divelunit  13511  modid  13901  addmodlteq  13951  expadd  14109  leexp2r  14178  nnlesq  14208  sqoddm1div8  14245  faclbnd  14289  faclbnd2  14290  faclbnd4lem3  14294  faclbnd6  14298  facavg  14300  bcn0  14309  bcn1  14312  hashf1lem2  14457  hashfac  14459  reccn2  15581  iseraltlem2  15669  iseraltlem3  15670  hash2iun1dif1  15810  binom11  15818  harmonic  15845  trireciplem  15848  geoserg  15852  pwdif  15854  pwm1geoser  15855  cvgrat  15869  fprodsplit  15950  fprodle  15980  fsumcube  16044  efzval  16086  tanhlt1  16144  tanaddlem  16150  tanadd  16151  cos01gt0  16175  absef  16181  1dvds  16255  bitsfzo  16417  bitsmod  16418  sqgcd  16543  lcm1  16588  coprmdvds  16631  qredeu  16636  phiprmpw  16752  coprimeprodsq  16784  pc2dvds  16855  sumhash  16872  fldivp1  16873  pcfaclem  16874  prmpwdvds  16880  prmreclem1  16892  vdwlem3  16959  vdwlem9  16965  prmop1  17014  sylow2a  19581  odadd  19812  zsssubrg  21365  zringcyg  21402  prmirredlem  21405  mulgrhm2  21411  pzriprnglem6  21419  pzriprnglem12  21425  znrrg  21506  mhppwdeg  22081  icopnfcnv  24887  icopnfhmeo  24888  lebnumii  24912  reparphti  24943  reparphtiOLD  24944  itg2const  25690  itg2monolem3  25702  bddibl  25789  dveflem  25931  mvth  25945  dvlipcn  25947  dvivthlem1  25961  dvfsumle  25974  dvfsumleOLD  25975  dvfsumabs  25977  dvfsumlem2  25981  dvfsumlem2OLD  25982  plyconst  26160  plyeq0lem  26164  plyco  26195  0dgrb  26200  coefv0  26202  vieta1  26267  aaliou3lem2  26298  tayl0  26316  taylply2  26322  taylply2OLD  26323  dvtaylp  26325  taylthlem2  26329  taylthlem2OLD  26330  radcnvlem1  26369  abelthlem1  26388  abelthlem2  26389  abelthlem3  26390  abelthlem7  26395  abelthlem8  26396  abelthlem9  26397  efper  26434  tangtx  26460  eflogeq  26556  logdivlti  26574  logcnlem4  26599  advlogexp  26609  cxpmul2  26643  dvcxp2  26695  cxpaddle  26707  cxpeq  26712  loglesqrt  26713  relogbexp  26732  ang180lem5  26765  isosctrlem2  26771  isosctrlem3  26772  heron  26790  2efiatan  26870  dvatan  26887  leibpi  26894  birthdaylem3  26905  jensenlem2  26940  logdiflbnd  26947  harmonicbnd4  26963  lgamgulmlem2  26982  lgamcvg2  27007  ftalem5  27029  basellem2  27034  basellem5  27037  basellem8  27040  0sgm  27096  muinv  27145  chpub  27173  logfaclbnd  27175  logexprlim  27178  dchrsum2  27221  sumdchr2  27223  bposlem1  27237  bposlem2  27238  bposlem5  27241  lgsquad2lem1  27337  lgsquad3  27340  2sqlem6  27376  2sqlem8  27379  chtppilim  27428  vmadivsum  27435  dchrisumlem1  27442  dchrisum0flblem1  27461  rpvmasum2  27465  dchrisum0re  27466  dchrisum0lem2a  27470  dchrisum0lem3  27472  rpvmasum  27479  mudivsum  27483  mulogsumlem  27484  vmalogdivsum2  27491  pntrsumo1  27518  pntrlog2bndlem2  27531  pntrlog2bndlem4  27533  pntrlog2bndlem5  27534  pntibndlem2  27544  pntlemc  27548  pntlemf  27558  ostth2lem2  27587  ostth2lem3  27588  ostth2lem4  27589  ostth2  27590  ostth3  27591  ttgcontlem1  28715  axpaschlem  28771  axcontlem2  28796  axcontlem4  28798  axcontlem8  28802  nmoub3i  30603  ubthlem2  30701  htthlem  30747  nmcexi  31856  nmopcoadji  31931  branmfn  31935  rearchi  33082  ccfldextdgrr  33393  madjusmdetlem4  33464  ccatmulgnn0dir  34207  ofcccat  34208  itgexpif  34271  hashreprin  34285  circlemeth  34305  lpadlem2  34345  subfacval2  34830  cvmliftlem2  34929  snmlff  34972  sinccvglem  35309  bcprod  35365  faclimlem1  35370  faclimlem2  35371  faclim2  35375  knoppndvlem14  36033  knoppndvlem15  36034  knoppndvlem16  36035  knoppndvlem18  36037  poimirlem29  37155  poimirlem30  37156  poimirlem31  37157  poimirlem32  37158  itg2addnclem  37177  areacirclem1  37214  areacirclem4  37217  cntotbnd  37302  lcmineqlem11  41542  lcmineqlem12  41543  aks4d1p1p7  41577  aks4d1p8d2  41588  hashscontpow1  41624  2ap1caineq  41649  sticksstones10  41659  sticksstones12a  41661  aks6d1c6lem1  41674  aks6d1c7lem1  41684  aks6d1c7  41688  frlmvscadiccat  41777  oddnumth  41902  oexpreposd  41912  expgcd  41925  fltnltalem  42117  3cubeslem2  42136  3cubeslem3r  42138  irrapxlem1  42273  irrapxlem4  42276  pell1qrgaplem  42324  reglogexpbas  42348  rmspecfund  42360  rmxy1  42374  rmxp1  42384  rmyp1  42385  rmxm1  42386  jm2.17a  42412  jm2.18  42440  jm2.23  42448  jm2.25  42451  jm2.16nn0  42456  relexpmulnn  43170  int-mul11d  43643  nzprmdif  43787  expgrowthi  43801  expgrowth  43803  binomcxplemdvbinom  43821  binomcxplemnotnn0  43824  sqrlearg  44967  fmul01  44997  fmul01lt1lem1  45001  0ellimcdiv  45066  dvxpaek  45357  dvnxpaek  45359  itgiccshift  45397  itgperiod  45398  itgsbtaddcnst  45399  stoweidlem11  45428  stoweidlem26  45443  stoweidlem38  45455  wallispilem4  45485  stirlinglem1  45491  stirlinglem3  45493  stirlinglem6  45496  stirlinglem7  45497  stirlinglem8  45498  stirlinglem10  45500  stirlinglem12  45502  dirkertrigeqlem3  45517  dirkertrigeq  45518  dirkercncflem1  45520  dirkercncflem2  45521  fourierdlem28  45552  fourierdlem30  45554  fourierdlem39  45563  fourierdlem47  45570  fourierdlem60  45583  fourierdlem61  45584  fourierdlem73  45596  fourierdlem83  45606  fourierdlem87  45610  etransclem14  45665  etransclem24  45675  etransclem25  45676  etransclem35  45686  smfmullem1  46208  deccarry  46720  fpprwppr  47108  fpprwpprb  47109  logblt1b  47715  nn0sumshdiglem2  47773  itcovalpclem2  47822  itcovalt2lem1  47826  eenglngeehlnmlem1  47888  eenglngeehlnmlem2  47889  line2ylem  47902