Theorem mulid1d 10652

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2110  (class class class)co 7150  ℂcc 10529  1c1 10532   · cmul 10536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-mulcl 10593  ax-mulcom 10595  ax-mulass 10597  ax-distr 10598  ax-1rid 10601  ax-cnre 10604

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-iota 6308  df-fv 6357  df-ov 7153

This theorem is referenced by:  muladd11  10804  muls1d  11094  divrec  11308  diveq1  11325  conjmul  11351  divelunit  12874  modid  13258  addmodlteq  13308  expadd  13465  leexp2r  13532  nnlesq  13562  sqoddm1div8  13598  faclbnd  13644  faclbnd2  13645  faclbnd4lem3  13649  faclbnd6  13653  facavg  13655  bcn0  13664  bcn1  13667  hashf1lem2  13808  hashfac  13810  reccn2  14947  iseraltlem2  15033  iseraltlem3  15034  hash2iun1dif1  15173  binom11  15181  harmonic  15208  trireciplem  15211  geoserg  15215  pwdif  15217  pwm1geoser  15218  cvgrat  15233  fprodsplit  15314  fprodle  15344  fsumcube  15408  efzval  15449  tanhlt1  15507  tanaddlem  15513  tanadd  15514  cos01gt0  15538  absef  15544  1dvds  15618  bitsfzo  15778  bitsmod  15779  gcdmultipleOLD  15894  sqgcd  15903  lcm1  15948  coprmdvds  15991  qredeu  15996  phiprmpw  16107  coprimeprodsq  16139  pc2dvds  16209  sumhash  16226  fldivp1  16227  pcfaclem  16228  prmpwdvds  16234  prmreclem1  16246  vdwlem3  16313  vdwlem9  16319  prmop1  16368  sylow2a  18738  odadd  18964  zsssubrg  20597  zringcyg  20632  prmirredlem  20634  mulgrhm2  20640  znrrg  20706  icopnfcnv  23540  icopnfhmeo  23541  lebnumii  23564  reparphti  23595  itg2const  24335  itg2monolem3  24347  bddibl  24434  dveflem  24570  mvth  24583  dvlipcn  24585  dvivthlem1  24599  dvfsumle  24612  dvfsumabs  24614  dvfsumlem2  24618  plyconst  24790  plyeq0lem  24794  plyco  24825  0dgrb  24830  coefv0  24832  vieta1  24895  aaliou3lem2  24926  tayl0  24944  taylply2  24950  dvtaylp  24952  taylthlem2  24956  radcnvlem1  24995  abelthlem1  25013  abelthlem2  25014  abelthlem3  25015  abelthlem7  25020  abelthlem8  25021  abelthlem9  25022  efper  25059  tangtx  25085  eflogeq  25179  logdivlti  25197  logcnlem4  25222  advlogexp  25232  cxpmul2  25266  dvcxp2  25316  cxpaddle  25327  cxpeq  25332  loglesqrt  25333  relogbexp  25352  ang180lem5  25385  isosctrlem2  25391  isosctrlem3  25392  heron  25410  2efiatan  25490  dvatan  25507  leibpi  25514  birthdaylem3  25525  jensenlem2  25559  logdiflbnd  25566  harmonicbnd4  25582  lgamgulmlem2  25601  lgamcvg2  25626  ftalem5  25648  basellem2  25653  basellem5  25656  basellem8  25659  0sgm  25715  muinv  25764  chpub  25790  logfaclbnd  25792  logexprlim  25795  dchrsum2  25838  sumdchr2  25840  bposlem1  25854  bposlem2  25855  bposlem5  25858  lgsquad2lem1  25954  lgsquad3  25957  2sqlem6  25993  2sqlem8  25996  chtppilim  26045  vmadivsum  26052  dchrisumlem1  26059  dchrisum0flblem1  26078  rpvmasum2  26082  dchrisum0re  26083  dchrisum0lem2a  26087  dchrisum0lem3  26089  rpvmasum  26096  mudivsum  26100  mulogsumlem  26101  vmalogdivsum2  26108  pntrsumo1  26135  pntrlog2bndlem2  26148  pntrlog2bndlem4  26150  pntrlog2bndlem5  26151  pntibndlem2  26161  pntlemc  26165  pntlemf  26175  ostth2lem2  26204  ostth2lem3  26205  ostth2lem4  26206  ostth2  26207  ostth3  26208  ttgcontlem1  26665  axpaschlem  26720  axcontlem2  26745  axcontlem4  26747  axcontlem8  26751  nmoub3i  28544  ubthlem2  28642  htthlem  28688  nmcexi  29797  nmopcoadji  29872  branmfn  29876  rearchi  30910  ccfldextdgrr  31052  madjusmdetlem4  31090  ccatmulgnn0dir  31807  ofcccat  31808  itgexpif  31872  hashreprin  31886  circlemeth  31906  lpadlem2  31946  subfacval2  32429  cvmliftlem2  32528  snmlff  32571  sinccvglem  32910  bcprod  32965  faclimlem1  32970  faclimlem2  32971  faclim2  32975  knoppndvlem14  33859  knoppndvlem15  33860  knoppndvlem16  33861  knoppndvlem18  33863  poimirlem29  34915  poimirlem30  34916  poimirlem31  34917  poimirlem32  34918  itg2addnclem  34937  areacirclem1  34976  areacirclem4  34979  cntotbnd  35068  frlmvscadiccat  39138  oexpreposd  39172  expgcd  39176  fltnltalem  39267  3cubeslem2  39275  3cubeslem3r  39277  irrapxlem1  39412  irrapxlem4  39415  pell1qrgaplem  39463  reglogexpbas  39487  rmspecfund  39499  rmxy1  39512  rmxp1  39522  rmyp1  39523  rmxm1  39524  jm2.17a  39550  jm2.18  39578  jm2.23  39586  jm2.25  39589  jm2.16nn0  39594  relexpmulnn  40047  int-mul11d  40528  nzprmdif  40644  expgrowthi  40658  expgrowth  40660  binomcxplemdvbinom  40678  binomcxplemnotnn0  40681  sqrlearg  41822  fmul01  41854  fmul01lt1lem1  41858  0ellimcdiv  41923  dvxpaek  42218  dvnxpaek  42220  itgiccshift  42258  itgperiod  42259  itgsbtaddcnst  42260  stoweidlem11  42290  stoweidlem26  42305  stoweidlem38  42317  wallispilem4  42347  stirlinglem1  42353  stirlinglem3  42355  stirlinglem6  42358  stirlinglem7  42359  stirlinglem8  42360  stirlinglem10  42362  stirlinglem12  42364  dirkertrigeqlem3  42379  dirkertrigeq  42380  dirkercncflem1  42382  dirkercncflem2  42383  fourierdlem28  42414  fourierdlem30  42416  fourierdlem39  42425  fourierdlem47  42432  fourierdlem60  42445  fourierdlem61  42446  fourierdlem73  42458  fourierdlem83  42468  fourierdlem87  42472  etransclem14  42527  etransclem24  42537  etransclem25  42538  etransclem35  42548  smfmullem1  43060  deccarry  43505  fpprwppr  43898  fpprwpprb  43899  logblt1b  44618  nn0sumshdiglem2  44676  eenglngeehlnmlem1  44718  eenglngeehlnmlem2  44719  line2ylem  44732