Theorem mullidd 11151

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

Hypothesis

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

Assertion

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

Proof of Theorem mullidd

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7358  ℂcc 11025  1c1 11028   · cmul 11032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-mulcl 11089  ax-mulcom 11091  ax-mulass 11093  ax-distr 11094  ax-1rid 11097  ax-cnre 11100

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6446  df-fv 6498  df-ov 7361

This theorem is referenced by:  adddirp1d  11159  addrid  11314  mulsubfacd  11599  mulcand  11771  receu  11783  divdivdiv  11843  divcan5  11844  subrecd  11971  ltrec  12025  recp1lt1  12041  nndivtr  12193  subhalfhalf  12376  xp1d2m1eqxm1d2  12396  gtndiv  12570  ge2halflem1  13023  lincmb01cmp  13412  iccf1o  13413  ltdifltdiv  13755  modfrac  13805  negmod  13840  addmodid  13843  m1expcl2  14009  expgt1  14024  ltexp2a  14090  leexp2a  14096  binom3  14148  faclbnd  14214  faclbnd4lem4  14220  facavg  14225  bcval5  14242  cshweqrep  14745  01sqrexlem2  15167  absimle  15233  reccn2  15521  iseraltlem2  15607  iseraltlem3  15608  o1fsum  15737  abscvgcvg  15743  ackbijnn  15752  binom1p  15755  binom1dif  15757  incexclem  15760  incexc  15761  climcndslem1  15773  pwdif  15792  geomulcvg  15800  fprodsplit  15890  fallrisefac  15949  bpolysum  15977  bpolydiflem  15978  bpoly4  15983  efcllem  16001  ef01bndlem  16110  efieq1re  16125  eirrlem  16130  iddvds  16197  pwp1fsum  16319  oddpwp1fsum  16320  bitsfzolem  16362  bitsfzo  16363  rpmulgcd  16485  prmind2  16613  isprm5  16635  phiprm  16705  eulerthlem2  16710  fermltl  16712  hashgcdlem  16716  odzdvds  16724  powm2modprm  16732  modprm0  16734  pythagtriplem4  16748  4sqlem18  16891  vdwapun  16903  mulgnnass  19043  odinv  19494  odadd2  19782  pgpfaclem2  20017  abvneg  20761  pzriprnglem6  21443  pzriprnglem12  21449  nrginvrcnlem  24634  nmoid  24685  blcvx  24741  icopnfcnv  24887  reparphti  24942  pcorevlem  24971  ncvsm1  25099  ncvspi  25101  cphipval2  25186  cphipval  25188  itg11  25636  itg2mulc  25692  itg2monolem1  25695  itgcnlem  25735  iblabs  25774  dvexp  25898  dvmptdiv  25919  dvef  25925  lhop1lem  25959  dvcvx  25966  dvfsumlem1  25973  dvfsumlem2  25974  dvfsumlem2OLD  25975  dvfsumlem4  25977  dvfsum2  25982  plypow  26151  dgrcolem1  26219  vieta1lem2  26259  radcnvlem1  26362  radcnvlem2  26363  dvradcnv  26370  abelthlem6  26386  abelthlem7  26388  abelth2  26392  sinhalfpip  26441  sinhalfpim  26442  coshalfpip  26443  coshalfpim  26444  tangtx  26454  efif1olem4  26494  abslogle  26567  logdivlti  26569  advlog  26603  advlogexp  26604  logtayl  26609  cxpaddlelem  26701  cxpaddle  26702  affineequiv  26773  affineequiv2  26774  chordthmlem5  26786  dcubic2  26794  dcubic  26796  mcubic  26797  binom4  26800  dquartlem1  26801  quart1lem  26805  quart1  26806  quartlem1  26807  quart  26811  efiasin  26838  atantayl  26887  cvxcl  26935  scvxcvx  26936  lgamgulmlem5  26983  lgamcvg2  27005  lgam1  27014  wilthlem1  27018  wilthlem2  27019  basellem9  27039  fsumfldivdiaglem  27139  muinv  27143  chpub  27171  logexprlim  27176  mersenne  27178  perfectlem2  27181  dchrmullid  27203  dchrptlem1  27215  dchrsum2  27219  sumdchr2  27221  bposlem2  27236  bposlem9  27243  lgsval2lem  27258  lgsval4a  27270  lgsneg1  27273  lgsdir2lem4  27279  lgsdir  27283  lgsmulsqcoprm  27294  lgsdirnn0  27295  lgsdinn0  27296  gausslemma2dlem1a  27316  gausslemma2dlem4  27320  gausslemma2dlem7  27324  gausslemma2d  27325  lgseisenlem1  27326  lgseisenlem2  27327  lgseisenlem4  27329  lgsquad2lem1  27335  2sqlem8  27377  chebbnd1lem3  27422  chpchtlim  27430  rplogsumlem1  27435  rplogsumlem2  27436  rpvmasumlem  27438  dchrmusum2  27445  dchrvmasum2lem  27447  dchrvmasumlem2  27449  dchrvmasumlem3  27450  dchrisum0flblem1  27459  mulog2sumlem2  27486  vmalogdivsum2  27489  2vmadivsumlem  27491  log2sumbnd  27495  selberglem2  27497  selberg3lem1  27508  selberg4lem1  27511  pntrlog2bndlem2  27529  pntrlog2bndlem5  27532  pntpbnd1  27537  pntpbnd2  27538  pntibndlem2  27542  pntlemb  27548  pntlemr  27553  pntlemk  27557  pntlemo  27558  brbtwn2  28962  colinearalglem4  28966  ax5seglem3  28988  axbtwnid  28996  axpaschlem  28997  axeuclidlem  29019  axcontlem7  29027  axcontlem8  29028  elntg2  29042  nvm1  30725  nvpi  30727  nvmtri  30731  ipval2  30767  ipasslem1  30891  ipasslem4  30894  bcs2  31242  lnfnaddi  32103  nnmulge  32801  quad3d  32812  2exple2exp  32909  indsum  32925  indsumin  32926  ccfldsrarelvec  33821  constrfin  33896  constrremulcl  33917  constrrecl  33919  constrimcl  33920  constrmulcl  33921  constrreinvcl  33922  2sqr3minply  33930  cos9thpiminplylem2  33933  sqsscirc1  34058  eulerpartlemgs2  34530  plymulx0  34697  logdivsqrle  34800  subfacp1lem6  35373  subfaclim  35376  cvxpconn  35430  cvxsconn  35431  resconn  35434  sinccvglem  35860  fwddifn0  36352  nn0prpwlem  36510  knoppndvlem9  36778  knoppndvlem14  36783  bj-bary1lem1  37623  mblfinlem3  37971  itg2addnclem3  37985  iblabsnc  37996  iblmulc2nc  37997  ftc1anclem6  38010  ftc1anclem7  38011  ftc1anclem8  38012  areacirclem1  38020  bfplem2  38135  bfp  38136  rrntotbnd  38148  lcmineqlem1  42460  lcmineqlem12  42471  lcmineqlem18  42477  aks4d1p1p7  42505  aks4d1p8  42518  primrootscoprmpow  42530  posbezout  42531  aks6d1c2lem4  42558  3rdpwhole  42723  fltnlta  43095  3cubeslem2  43116  3cubeslem3r  43118  irrapxlem5  43257  pellexlem2  43261  pellexlem6  43265  pellfundex  43317  jm2.19lem3  43422  jm2.25  43430  jm2.27c  43438  jm3.1lem2  43449  flcidc  43601  reabssgn  44066  sqrtcval  44071  int-mul12d  44613  cvgdvgrat  44743  bccn1  44774  binomcxplemnotnn0  44786  fperiodmullem  45739  xralrple2  45787  fmul01lt1lem2  46019  mccllem  46031  reclimc  46085  cosknegpi  46301  dvsinax  46345  dvnxpaek  46374  dvnmul  46375  itgsinexp  46387  stoweidlem14  46446  stoweidlem26  46458  wallispilem4  46500  wallispilem5  46501  wallispi2lem1  46503  wallispi2  46505  stirlinglem1  46506  stirlinglem3  46508  stirlinglem4  46509  stirlinglem5  46510  stirlinglem6  46511  stirlinglem7  46512  stirlinglem10  46515  dirkertrigeqlem2  46531  dirkertrigeqlem3  46532  dirkercncflem2  46536  fourierdlem26  46565  fourierdlem41  46580  fourierdlem42  46581  fourierdlem56  46594  fourierdlem57  46595  fourierdlem58  46596  fourierdlem62  46600  fourierdlem64  46602  fourierdlem65  46603  fourierdlem95  46633  sqwvfoura  46660  sqwvfourb  46661  fouriersw  46663  etransclem23  46689  etransclem35  46701  etransclem46  46712  fmtnorec2lem  47976  fmtnorec3  47982  m1expoddALTV  48082  perfectALTVlem2  48156  ztprmneprm  48781  altgsumbc  48786  divge1b  48946  divgt1b  48947  ackval1  49115  affineid  49138  1subrec1sub  49139  rrx2vlinest  49175  line2x  49188