Theorem mulid1d 10394

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

Hypothesis

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
mulid1d	⊢ (𝜑 → (𝐴 · 1) = 𝐴)

Proof of Theorem mulid1d

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		mulid1 10374	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 · 1) = 𝐴)

Syntax hints:   → wi 4   = wceq 1601   ∈ wcel 2107  (class class class)co 6922  ℂcc 10270  1c1 10273   · cmul 10277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-mulcl 10334  ax-mulcom 10336  ax-mulass 10338  ax-distr 10339  ax-1rid 10342  ax-cnre 10345

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-iota 6099  df-fv 6143  df-ov 6925

This theorem is referenced by:  muladd11  10546  muls1d  10835  divrec  11049  diveq1  11066  conjmul  11092  divelunit  12631  modid  13014  addmodlteq  13064  expadd  13220  leexp2r  13236  nnlesq  13287  sqoddm1div8  13349  faclbnd  13395  faclbnd2  13396  faclbnd4lem3  13400  faclbnd6  13404  facavg  13406  bcn0  13415  bcn1  13418  hashf1lem2  13554  hashfac  13556  reccn2  14735  iseraltlem2  14821  iseraltlem3  14822  hash2iun1dif1  14960  binom11  14968  harmonic  14995  trireciplem  14998  geoserg  15002  cvgrat  15018  fprodsplit  15099  fprodle  15129  fsumcube  15193  efzval  15234  tanhlt1  15292  tanaddlem  15298  tanadd  15299  cos01gt0  15323  absef  15329  1dvds  15403  bitsfzo  15563  bitsmod  15564  gcdmultiple  15675  sqgcd  15684  lcm1  15729  coprmdvds  15772  qredeu  15777  phiprmpw  15885  coprimeprodsq  15917  pc2dvds  15987  sumhash  16004  fldivp1  16005  pcfaclem  16006  prmpwdvds  16012  prmreclem1  16024  vdwlem3  16091  vdwlem9  16097  prmop1  16146  sylow2a  18418  odadd  18639  zsssubrg  20200  zringcyg  20235  prmirredlem  20237  mulgrhm2  20243  znrrg  20309  icopnfcnv  23149  icopnfhmeo  23150  lebnumii  23173  reparphti  23204  itg2const  23944  itg2monolem3  23956  bddibl  24043  dveflem  24179  mvth  24192  dvlipcn  24194  dvivthlem1  24208  dvfsumle  24221  dvfsumabs  24223  dvfsumlem2  24227  plyconst  24399  plyeq0lem  24403  plyco  24434  0dgrb  24439  coefv0  24441  vieta1  24504  aaliou3lem2  24535  tayl0  24553  taylply2  24559  dvtaylp  24561  taylthlem2  24565  radcnvlem1  24604  abelthlem1  24622  abelthlem2  24623  abelthlem3  24624  abelthlem7  24629  abelthlem8  24630  abelthlem9  24631  efper  24669  tangtx  24695  eflogeq  24785  logdivlti  24803  logcnlem4  24828  advlogexp  24838  cxpmul2  24872  dvcxp2  24922  cxpaddle  24933  cxpeq  24938  loglesqrt  24939  relogbexp  24958  ang180lem5  24991  isosctrlem2  24997  isosctrlem3  24998  heron  25016  2efiatan  25096  dvatan  25113  leibpi  25121  birthdaylem3  25132  jensenlem2  25166  logdiflbnd  25173  harmonicbnd4  25189  lgamgulmlem2  25208  lgamcvg2  25233  wilthlem2  25247  ftalem5  25255  basellem2  25260  basellem5  25263  basellem8  25266  0sgm  25322  muinv  25371  chpub  25397  logfaclbnd  25399  logexprlim  25402  dchrsum2  25445  sumdchr2  25447  bposlem1  25461  bposlem2  25462  bposlem5  25465  lgsquad2lem1  25561  lgsquad3  25564  2sqlem6  25600  2sqlem8  25603  chtppilim  25616  vmadivsum  25623  dchrisumlem1  25630  dchrisum0flblem1  25649  rpvmasum2  25653  dchrisum0re  25654  dchrisum0lem2a  25658  dchrisum0lem3  25660  rpvmasum  25667  mudivsum  25671  mulogsumlem  25672  vmalogdivsum2  25679  pntrsumo1  25706  pntrlog2bndlem2  25719  pntrlog2bndlem4  25721  pntrlog2bndlem5  25722  pntibndlem2  25732  pntlemc  25736  pntlemf  25746  ostth2lem2  25775  ostth2lem3  25776  ostth2lem4  25777  ostth2  25778  ostth3  25779  ttgcontlem1  26234  axpaschlem  26289  axcontlem2  26314  axcontlem4  26316  axcontlem8  26320  nmoub3i  28200  ubthlem2  28299  htthlem  28346  nmcexi  29457  nmopcoadji  29532  branmfn  29536  rearchi  30404  madjusmdetlem4  30494  ccatmulgnn0dir  31219  ofcccat  31220  itgexpif  31286  hashreprin  31300  circlemeth  31320  subfacval2  31768  cvmliftlem2  31867  snmlff  31910  sinccvglem  32163  bcprod  32218  faclimlem1  32223  faclimlem2  32224  faclim2  32228  knoppndvlem14  33098  knoppndvlem15  33099  knoppndvlem16  33100  knoppndvlem18  33102  poimirlem29  34064  poimirlem30  34065  poimirlem31  34066  poimirlem32  34067  itg2addnclem  34086  areacirclem1  34125  areacirclem4  34128  cntotbnd  34219  oexpreposd  38159  expgcd  38163  irrapxlem1  38346  irrapxlem4  38349  pell1qrgaplem  38397  reglogexpbas  38421  rmspecfund  38433  rmxy1  38446  rmxp1  38456  rmyp1  38457  rmxm1  38458  jm2.17a  38486  jm2.18  38514  jm2.23  38522  jm2.25  38525  jm2.16nn0  38530  relexpmulnn  38958  int-mul11d  39441  nzprmdif  39474  expgrowthi  39488  expgrowth  39490  binomcxplemdvbinom  39508  binomcxplemnotnn0  39511  sqrlearg  40688  fmul01  40720  fmul01lt1lem1  40724  0ellimcdiv  40789  dvxpaek  41083  dvnxpaek  41085  itgiccshift  41123  itgperiod  41124  itgsbtaddcnst  41125  stoweidlem11  41155  stoweidlem26  41170  stoweidlem38  41182  wallispilem4  41212  stirlinglem1  41218  stirlinglem3  41220  stirlinglem6  41223  stirlinglem7  41224  stirlinglem8  41225  stirlinglem10  41227  stirlinglem12  41229  dirkertrigeqlem3  41244  dirkertrigeq  41245  dirkercncflem1  41247  dirkercncflem2  41248  fourierdlem28  41279  fourierdlem30  41281  fourierdlem39  41290  fourierdlem47  41297  fourierdlem60  41310  fourierdlem61  41311  fourierdlem73  41323  fourierdlem83  41333  fourierdlem87  41337  etransclem14  41392  etransclem24  41402  etransclem25  41403  etransclem35  41413  smfmullem1  41925  deccarry  42353  pwdif  42522  pwm1geoserALT  42523  logblt1b  43373  nn0sumshdiglem2  43431  eenglngeehlnmlem1  43473  eenglngeehlnmlem2  43474  line2ylem  43487