Theorem mulid1d 9061

Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
addcld.1	|- ( ph -> A e. CC )

Assertion

Ref	Expression
mulid1d	|- ( ph -> ( A x. 1 ) = A )

Proof of Theorem mulid1d

Step	Hyp	Ref	Expression
1		addcld.1	. 2 |- ( ph -> A e. CC )
2		mulid1 9044	. 2 |- ( A e. CC -> ( A x. 1 ) = A )
3	1, 2	syl 16	1 |- ( ph -> ( A x. 1 ) = A )

Syntax hints:   -> wi 4   = wceq 1649   e. wcel 1721  (class class class)co 6040   CCcc 8944   1c1 8947   x. cmul 8951

This theorem is referenced by:  muladd11  9192  divrec  9650  diveq1  9664  conjmul  9687  modid  11225  expadd  11377  leexp2r  11392  nnlesq  11439  faclbnd  11536  faclbnd2  11537  faclbnd4lem3  11541  faclbnd6  11545  facavg  11547  bcn0  11556  bcn1  11559  hashf1lem2  11660  hashfac  11662  reccn2  12345  iseraltlem2  12431  iseraltlem3  12432  binom11  12566  harmonic  12593  arisum2  12595  trireciplem  12596  geoserg  12600  cvgrat  12615  efzval  12658  tanhlt1  12716  tanaddlem  12722  tanadd  12723  cos01gt0  12747  absef  12753  1dvds  12819  3dvds  12867  bitsfzo  12902  bitsmod  12903  gcdmultiple  13005  sqgcd  13013  coprmdvds  13057  qredeu  13062  phiprmpw  13120  coprimeprodsq  13138  pc2dvds  13207  sumhash  13220  fldivp1  13221  pcfaclem  13222  prmpwdvds  13227  prmreclem1  13239  vdwlem3  13306  vdwlem9  13312  sylow2a  15208  odadd  15420  zsssubrg  16712  zcyg  16727  prmirredlem  16728  mulgrhm2  16743  znrrg  16801  icopnfcnv  18920  icopnfhmeo  18921  lebnumii  18944  reparphti  18975  itg2const  19585  itg2monolem3  19597  bddibl  19684  dveflem  19816  mvth  19829  dvlipcn  19831  dvivthlem1  19845  dvfsumle  19858  dvfsumabs  19860  dvfsumlem2  19864  plyconst  20078  plyeq0lem  20082  plyco  20113  0dgrb  20118  coefv0  20119  vieta1  20182  aaliou3lem2  20213  tayl0  20231  taylply2  20237  dvtaylp  20239  taylthlem2  20243  radcnvlem1  20282  abelthlem1  20300  abelthlem2  20301  abelthlem3  20302  abelthlem7  20307  abelthlem8  20308  abelthlem9  20309  efper  20340  tangtx  20366  eflogeq  20449  logdivlti  20468  logcnlem4  20489  advlogexp  20499  cxpmul2  20533  dvcxp2  20580  cxpaddle  20589  cxpeq  20594  loglesqr  20595  ang180lem5  20608  isosctrlem2  20616  isosctrlem3  20617  2efiatan  20711  dvatan  20728  leibpi  20735  birthdaylem3  20745  jensenlem2  20779  logdiflbnd  20786  harmonicbnd4  20802  wilthlem2  20805  ftalem5  20812  basellem2  20817  basellem5  20820  basellem8  20823  0sgm  20880  muinv  20931  chpub  20957  logfaclbnd  20959  logexprlim  20962  dchrsum2  21005  sumdchr2  21007  bposlem1  21021  bposlem2  21022  bposlem5  21025  lgsquad2lem1  21095  lgsquad3  21098  2sqlem6  21106  2sqlem8  21109  chtppilim  21122  vmadivsum  21129  dchrisumlem1  21136  dchrisum0flblem1  21155  rpvmasum2  21159  dchrisum0re  21160  dchrisum0lem2a  21164  dchrisum0lem3  21166  rpvmasum  21173  mudivsum  21177  mulogsumlem  21178  vmalogdivsum2  21185  pntrsumo1  21212  pntrlog2bndlem2  21225  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  pntibndlem2  21238  pntlemc  21242  pntlemf  21252  ostth2lem2  21281  ostth2lem3  21282  ostth2lem4  21283  ostth2  21284  ostth3  21285  nmoub3i  22227  ubthlem2  22326  htthlem  22373  nmcexi  23482  nmopcoadji  23557  branmfn  23561  lgamgulmlem2  24767  lgamcvg2  24792  subfacval2  24826  cvmliftlem2  24926  snmlff  24969  sinccvglem  25062  divelunit  25138  muls1d  25166  fprodsplit  25242  faclimlem1  25310  faclimlem2  25311  faclim2  25315  axpaschlem  25783  axcontlem2  25808  axcontlem4  25810  axcontlem8  25814  fsumcube  26010  itg2addnclem  26155  areacirclem2  26181  areacirclem5  26185  cntotbnd  26395  irrapxlem1  26775  irrapxlem4  26778  pell1qrgaplem  26826  reglogexpbas  26850  rmspecsqrnq  26859  rmspecfund  26862  rmxy1  26875  rmxp1  26885  rmyp1  26886  rmxm1  26887  jm2.17a  26915  jm2.18  26949  jm2.23  26957  jm2.25  26960  jm2.16nn0  26965  expgrowthi  27418  expgrowth  27420  fmul01  27577  fmul01lt1lem1  27581  m1expeven  27592  stoweidlem11  27627  stoweidlem26  27642  stoweidlem38  27654  wallispilem4  27684  stirlinglem1  27690  stirlinglem3  27692  stirlinglem6  27695  stirlinglem7  27696  stirlinglem8  27697  stirlinglem10  27699  stirlinglem12  27701

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-mulcl 9008  ax-mulcom 9010  ax-mulass 9012  ax-distr 9013  ax-1rid 9016  ax-cnre 9019

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043