Theorem mullidd 11154

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11028  1c1 11031   · cmul 11035

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 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-mulcl 11092  ax-mulcom 11094  ax-mulass 11096  ax-distr 11097  ax-1rid 11100  ax-cnre 11103

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 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6449  df-fv 6501  df-ov 7363

This theorem is referenced by:  adddirp1d  11162  addrid  11317  mulsubfacd  11602  mulcand  11774  receu  11786  divdivdiv  11846  divcan5  11847  subrecd  11974  ltrec  12028  recp1lt1  12044  nndivtr  12196  subhalfhalf  12379  xp1d2m1eqxm1d2  12399  gtndiv  12573  ge2halflem1  13026  lincmb01cmp  13415  iccf1o  13416  ltdifltdiv  13758  modfrac  13808  negmod  13843  addmodid  13846  m1expcl2  14012  expgt1  14027  ltexp2a  14093  leexp2a  14099  binom3  14151  faclbnd  14217  faclbnd4lem4  14223  facavg  14228  bcval5  14245  cshweqrep  14748  01sqrexlem2  15170  absimle  15236  reccn2  15524  iseraltlem2  15610  iseraltlem3  15611  o1fsum  15740  abscvgcvg  15746  ackbijnn  15755  binom1p  15758  binom1dif  15760  incexclem  15763  incexc  15764  climcndslem1  15776  pwdif  15795  geomulcvg  15803  fprodsplit  15893  fallrisefac  15952  bpolysum  15980  bpolydiflem  15981  bpoly4  15986  efcllem  16004  ef01bndlem  16113  efieq1re  16128  eirrlem  16133  iddvds  16200  pwp1fsum  16322  oddpwp1fsum  16323  bitsfzolem  16365  bitsfzo  16366  rpmulgcd  16488  prmind2  16616  isprm5  16638  phiprm  16708  eulerthlem2  16713  fermltl  16715  hashgcdlem  16719  odzdvds  16727  powm2modprm  16735  modprm0  16737  pythagtriplem4  16751  4sqlem18  16894  vdwapun  16906  mulgnnass  19043  odinv  19494  odadd2  19782  pgpfaclem2  20017  abvneg  20763  pzriprnglem6  21445  pzriprnglem12  21451  nrginvrcnlem  24639  nmoid  24690  blcvx  24746  icopnfcnv  24900  reparphti  24956  reparphtiOLD  24957  pcorevlem  24986  ncvsm1  25114  ncvspi  25116  cphipval2  25201  cphipval  25203  itg11  25652  itg2mulc  25708  itg2monolem1  25711  itgcnlem  25751  iblabs  25790  dvexp  25917  dvmptdiv  25938  dvef  25944  lhop1lem  25978  dvcvx  25985  dvfsumlem1  25992  dvfsumlem2  25993  dvfsumlem2OLD  25994  dvfsumlem4  25996  dvfsum2  26001  plypow  26170  dgrcolem1  26239  vieta1lem2  26279  radcnvlem1  26382  radcnvlem2  26383  dvradcnv  26390  abelthlem6  26406  abelthlem7  26408  abelth2  26412  sinhalfpip  26461  sinhalfpim  26462  coshalfpip  26463  coshalfpim  26464  tangtx  26474  efif1olem4  26514  abslogle  26587  logdivlti  26589  advlog  26623  advlogexp  26624  logtayl  26629  cxpaddlelem  26721  cxpaddle  26722  affineequiv  26793  affineequiv2  26794  chordthmlem5  26806  dcubic2  26814  dcubic  26816  mcubic  26817  binom4  26820  dquartlem1  26821  quart1lem  26825  quart1  26826  quartlem1  26827  quart  26831  efiasin  26858  atantayl  26907  cvxcl  26955  scvxcvx  26956  lgamgulmlem5  27003  lgamcvg2  27025  lgam1  27034  wilthlem1  27038  wilthlem2  27039  basellem9  27059  fsumfldivdiaglem  27159  muinv  27163  chpub  27191  logexprlim  27196  mersenne  27198  perfectlem2  27201  dchrmullid  27223  dchrptlem1  27235  dchrsum2  27239  sumdchr2  27241  bposlem2  27256  bposlem9  27263  lgsval2lem  27278  lgsval4a  27290  lgsneg1  27293  lgsdir2lem4  27299  lgsdir  27303  lgsmulsqcoprm  27314  lgsdirnn0  27315  lgsdinn0  27316  gausslemma2dlem1a  27336  gausslemma2dlem4  27340  gausslemma2dlem7  27344  gausslemma2d  27345  lgseisenlem1  27346  lgseisenlem2  27347  lgseisenlem4  27349  lgsquad2lem1  27355  2sqlem8  27397  chebbnd1lem3  27442  chpchtlim  27450  rplogsumlem1  27455  rplogsumlem2  27456  rpvmasumlem  27458  dchrmusum2  27465  dchrvmasum2lem  27467  dchrvmasumlem2  27469  dchrvmasumlem3  27470  dchrisum0flblem1  27479  mulog2sumlem2  27506  vmalogdivsum2  27509  2vmadivsumlem  27511  log2sumbnd  27515  selberglem2  27517  selberg3lem1  27528  selberg4lem1  27531  pntrlog2bndlem2  27549  pntrlog2bndlem5  27552  pntpbnd1  27557  pntpbnd2  27558  pntibndlem2  27562  pntlemb  27568  pntlemr  27573  pntlemk  27577  pntlemo  27578  brbtwn2  28961  colinearalglem4  28965  ax5seglem3  28987  axbtwnid  28995  axpaschlem  28996  axeuclidlem  29018  axcontlem7  29026  axcontlem8  29027  elntg2  29041  nvm1  30723  nvpi  30725  nvmtri  30729  ipval2  30765  ipasslem1  30889  ipasslem4  30892  bcs2  31240  lnfnaddi  32101  nnmulge  32799  quad3d  32810  2exple2exp  32907  indsum  32923  indsumin  32924  ccfldsrarelvec  33809  constrfin  33884  constrremulcl  33905  constrrecl  33907  constrimcl  33908  constrmulcl  33909  constrreinvcl  33910  2sqr3minply  33918  cos9thpiminplylem2  33921  sqsscirc1  34046  eulerpartlemgs2  34518  plymulx0  34685  logdivsqrle  34788  subfacp1lem6  35360  subfaclim  35363  cvxpconn  35417  cvxsconn  35418  resconn  35421  sinccvglem  35847  fwddifn0  36339  nn0prpwlem  36497  knoppndvlem9  36695  knoppndvlem14  36700  bj-bary1lem1  37487  mblfinlem3  37831  itg2addnclem3  37845  iblabsnc  37856  iblmulc2nc  37857  ftc1anclem6  37870  ftc1anclem7  37871  ftc1anclem8  37872  areacirclem1  37880  bfplem2  37995  bfp  37996  rrntotbnd  38008  lcmineqlem1  42320  lcmineqlem12  42331  lcmineqlem18  42337  aks4d1p1p7  42365  aks4d1p8  42378  primrootscoprmpow  42390  posbezout  42391  aks6d1c2lem4  42418  3rdpwhole  42583  fltnlta  42942  3cubeslem2  42963  3cubeslem3r  42965  irrapxlem5  43104  pellexlem2  43108  pellexlem6  43112  pellfundex  43164  jm2.19lem3  43269  jm2.25  43277  jm2.27c  43285  jm3.1lem2  43296  flcidc  43448  reabssgn  43913  sqrtcval  43918  int-mul12d  44460  cvgdvgrat  44590  bccn1  44621  binomcxplemnotnn0  44633  fperiodmullem  45587  xralrple2  45635  fmul01lt1lem2  45867  mccllem  45879  reclimc  45933  cosknegpi  46149  dvsinax  46193  dvnxpaek  46222  dvnmul  46223  itgsinexp  46235  stoweidlem14  46294  stoweidlem26  46306  wallispilem4  46348  wallispilem5  46349  wallispi2lem1  46351  wallispi2  46353  stirlinglem1  46354  stirlinglem3  46356  stirlinglem4  46357  stirlinglem5  46358  stirlinglem6  46359  stirlinglem7  46360  stirlinglem10  46363  dirkertrigeqlem2  46379  dirkertrigeqlem3  46380  dirkercncflem2  46384  fourierdlem26  46413  fourierdlem41  46428  fourierdlem42  46429  fourierdlem56  46442  fourierdlem57  46443  fourierdlem58  46444  fourierdlem62  46448  fourierdlem64  46450  fourierdlem65  46451  fourierdlem95  46481  sqwvfoura  46508  sqwvfourb  46509  fouriersw  46511  etransclem23  46537  etransclem35  46549  etransclem46  46560  fmtnorec2lem  47824  fmtnorec3  47830  m1expoddALTV  47930  perfectALTVlem2  48004  ztprmneprm  48629  altgsumbc  48634  divge1b  48794  divgt1b  48795  ackval1  48963  affineid  48986  1subrec1sub  48987  rrx2vlinest  49023  line2x  49036