Theorem mulid1d 10739

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7173  ℂcc 10616  1c1 10619   · cmul 10623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711  ax-resscn 10675  ax-1cn 10676  ax-icn 10677  ax-addcl 10678  ax-mulcl 10680  ax-mulcom 10682  ax-mulass 10684  ax-distr 10685  ax-1rid 10688  ax-cnre 10691

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-ral 3059  df-rex 3060  df-v 3401  df-un 3849  df-in 3851  df-ss 3861  df-sn 4518  df-pr 4520  df-op 4524  df-uni 4798  df-br 5032  df-iota 6298  df-fv 6348  df-ov 7176

This theorem is referenced by:  muladd11  10891  muls1d  11181  divrec  11395  diveq1  11412  conjmul  11438  divelunit  12971  modid  13358  addmodlteq  13408  expadd  13566  leexp2r  13633  nnlesq  13663  sqoddm1div8  13699  faclbnd  13745  faclbnd2  13746  faclbnd4lem3  13750  faclbnd6  13754  facavg  13756  bcn0  13765  bcn1  13768  hashf1lem2  13911  hashfac  13913  reccn2  15047  iseraltlem2  15135  iseraltlem3  15136  hash2iun1dif1  15275  binom11  15283  harmonic  15310  trireciplem  15313  geoserg  15317  pwdif  15319  pwm1geoser  15320  cvgrat  15334  fprodsplit  15415  fprodle  15445  fsumcube  15509  efzval  15550  tanhlt1  15608  tanaddlem  15614  tanadd  15615  cos01gt0  15639  absef  15645  1dvds  15719  bitsfzo  15881  bitsmod  15882  gcdmultipleOLD  15999  sqgcd  16009  lcm1  16054  coprmdvds  16097  qredeu  16102  phiprmpw  16216  coprimeprodsq  16248  pc2dvds  16318  sumhash  16335  fldivp1  16336  pcfaclem  16337  prmpwdvds  16343  prmreclem1  16355  vdwlem3  16422  vdwlem9  16428  prmop1  16477  sylow2a  18865  odadd  19092  zsssubrg  20278  zringcyg  20313  prmirredlem  20316  mulgrhm2  20322  znrrg  20387  mhppwdeg  20947  icopnfcnv  23697  icopnfhmeo  23698  lebnumii  23721  reparphti  23752  itg2const  24496  itg2monolem3  24508  bddibl  24595  dveflem  24734  mvth  24747  dvlipcn  24749  dvivthlem1  24763  dvfsumle  24776  dvfsumabs  24778  dvfsumlem2  24782  plyconst  24958  plyeq0lem  24962  plyco  24993  0dgrb  24998  coefv0  25000  vieta1  25063  aaliou3lem2  25094  tayl0  25112  taylply2  25118  dvtaylp  25120  taylthlem2  25124  radcnvlem1  25163  abelthlem1  25181  abelthlem2  25182  abelthlem3  25183  abelthlem7  25188  abelthlem8  25189  abelthlem9  25190  efper  25227  tangtx  25253  eflogeq  25348  logdivlti  25366  logcnlem4  25391  advlogexp  25401  cxpmul2  25435  dvcxp2  25485  cxpaddle  25496  cxpeq  25501  loglesqrt  25502  relogbexp  25521  ang180lem5  25554  isosctrlem2  25560  isosctrlem3  25561  heron  25579  2efiatan  25659  dvatan  25676  leibpi  25683  birthdaylem3  25694  jensenlem2  25728  logdiflbnd  25735  harmonicbnd4  25751  lgamgulmlem2  25770  lgamcvg2  25795  ftalem5  25817  basellem2  25822  basellem5  25825  basellem8  25828  0sgm  25884  muinv  25933  chpub  25959  logfaclbnd  25961  logexprlim  25964  dchrsum2  26007  sumdchr2  26009  bposlem1  26023  bposlem2  26024  bposlem5  26027  lgsquad2lem1  26123  lgsquad3  26126  2sqlem6  26162  2sqlem8  26165  chtppilim  26214  vmadivsum  26221  dchrisumlem1  26228  dchrisum0flblem1  26247  rpvmasum2  26251  dchrisum0re  26252  dchrisum0lem2a  26256  dchrisum0lem3  26258  rpvmasum  26265  mudivsum  26269  mulogsumlem  26270  vmalogdivsum2  26277  pntrsumo1  26304  pntrlog2bndlem2  26317  pntrlog2bndlem4  26319  pntrlog2bndlem5  26320  pntibndlem2  26330  pntlemc  26334  pntlemf  26344  ostth2lem2  26373  ostth2lem3  26374  ostth2lem4  26375  ostth2  26376  ostth3  26377  ttgcontlem1  26834  axpaschlem  26889  axcontlem2  26914  axcontlem4  26916  axcontlem8  26920  nmoub3i  28711  ubthlem2  28809  htthlem  28855  nmcexi  29964  nmopcoadji  30039  branmfn  30043  rearchi  31121  ccfldextdgrr  31317  madjusmdetlem4  31355  ccatmulgnn0dir  32094  ofcccat  32095  itgexpif  32159  hashreprin  32173  circlemeth  32193  lpadlem2  32233  subfacval2  32723  cvmliftlem2  32822  snmlff  32865  sinccvglem  33204  bcprod  33280  faclimlem1  33285  faclimlem2  33286  faclim2  33290  knoppndvlem14  34351  knoppndvlem15  34352  knoppndvlem16  34353  knoppndvlem18  34355  poimirlem29  35452  poimirlem30  35453  poimirlem31  35454  poimirlem32  35455  itg2addnclem  35474  areacirclem1  35511  areacirclem4  35514  cntotbnd  35600  lcmineqlem11  39690  lcmineqlem12  39691  aks4d1p1p7  39724  2ap1caineq  39730  frlmvscadiccat  39842  oexpreposd  39920  expgcd  39934  fltnltalem  40094  3cubeslem2  40102  3cubeslem3r  40104  irrapxlem1  40239  irrapxlem4  40242  pell1qrgaplem  40290  reglogexpbas  40314  rmspecfund  40326  rmxy1  40339  rmxp1  40349  rmyp1  40350  rmxm1  40351  jm2.17a  40377  jm2.18  40405  jm2.23  40413  jm2.25  40416  jm2.16nn0  40421  relexpmulnn  40886  int-mul11d  41363  nzprmdif  41498  expgrowthi  41512  expgrowth  41514  binomcxplemdvbinom  41532  binomcxplemnotnn0  41535  sqrlearg  42654  fmul01  42686  fmul01lt1lem1  42690  0ellimcdiv  42755  dvxpaek  43046  dvnxpaek  43048  itgiccshift  43086  itgperiod  43087  itgsbtaddcnst  43088  stoweidlem11  43117  stoweidlem26  43132  stoweidlem38  43144  wallispilem4  43174  stirlinglem1  43180  stirlinglem3  43182  stirlinglem6  43185  stirlinglem7  43186  stirlinglem8  43187  stirlinglem10  43189  stirlinglem12  43191  dirkertrigeqlem3  43206  dirkertrigeq  43207  dirkercncflem1  43209  dirkercncflem2  43210  fourierdlem28  43241  fourierdlem30  43243  fourierdlem39  43252  fourierdlem47  43259  fourierdlem60  43272  fourierdlem61  43273  fourierdlem73  43285  fourierdlem83  43295  fourierdlem87  43299  etransclem14  43354  etransclem24  43364  etransclem25  43365  etransclem35  43375  smfmullem1  43887  deccarry  44367  fpprwppr  44755  fpprwpprb  44756  logblt1b  45474  nn0sumshdiglem2  45532  itcovalpclem2  45581  itcovalt2lem1  45585  eenglngeehlnmlem1  45647  eenglngeehlnmlem2  45648  line2ylem  45661