Theorem mullidd 11152

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 7356  ℂ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 2707  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 2714  df-cleq 2727  df-clel 2810  df-rex 3060  df-rab 3388  df-v 3429  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-iota 6443  df-fv 6495  df-ov 7359

This theorem is referenced by:  adddirp1d  11160  addrid  11315  mulsubfacd  11600  mulcand  11772  receu  11784  divdivdiv  11845  divcan5  11846  subrecd  11973  ltrec  12027  recp1lt1  12043  nndivtr  12213  subhalfhalf  12400  xp1d2m1eqxm1d2  12420  gtndiv  12595  ge2halflem1  13048  lincmb01cmp  13437  iccf1o  13438  ltdifltdiv  13782  modfrac  13832  negmod  13867  addmodid  13870  m1expcl2  14036  expgt1  14051  ltexp2a  14117  leexp2a  14123  binom3  14175  faclbnd  14241  faclbnd4lem4  14247  facavg  14252  bcval5  14269  cshweqrep  14772  01sqrexlem2  15194  absimle  15260  reccn2  15548  iseraltlem2  15634  iseraltlem3  15635  o1fsum  15765  abscvgcvg  15771  indsum  15780  ackbijnn  15782  binom1p  15785  binom1dif  15787  incexclem  15790  incexc  15791  climcndslem1  15803  pwdif  15822  geomulcvg  15830  fprodsplit  15920  fallrisefac  15979  bpolysum  16007  bpolydiflem  16008  bpoly4  16013  efcllem  16031  ef01bndlem  16140  efieq1re  16155  eirrlem  16160  iddvds  16227  pwp1fsum  16349  oddpwp1fsum  16350  bitsfzolem  16392  bitsfzo  16393  rpmulgcd  16515  prmind2  16643  isprm5  16666  phiprm  16736  eulerthlem2  16741  fermltl  16743  hashgcdlem  16747  odzdvds  16755  powm2modprm  16763  modprm0  16765  pythagtriplem4  16779  4sqlem18  16922  vdwapun  16934  mulgnnass  19074  odinv  19525  odadd2  19813  pgpfaclem2  20048  abvneg  20792  pzriprnglem6  21455  pzriprnglem12  21461  nrginvrcnlem  24644  nmoid  24695  blcvx  24751  icopnfcnv  24897  reparphti  24952  pcorevlem  24981  ncvsm1  25109  ncvspi  25111  cphipval2  25196  cphipval  25198  itg11  25646  itg2mulc  25702  itg2monolem1  25705  itgcnlem  25745  iblabs  25784  dvexp  25908  dvmptdiv  25929  dvef  25935  lhop1lem  25968  dvcvx  25975  dvfsumlem1  25981  dvfsumlem2  25982  dvfsumlem4  25984  dvfsum2  25989  plypow  26158  dgrcolem1  26226  vieta1lem2  26265  radcnvlem1  26366  radcnvlem2  26367  dvradcnv  26374  abelthlem6  26389  abelthlem7  26391  abelth2  26395  sinhalfpip  26444  sinhalfpim  26445  coshalfpip  26446  coshalfpim  26447  tangtx  26457  efif1olem4  26497  abslogle  26570  logdivlti  26572  advlog  26606  advlogexp  26607  logtayl  26612  cxpaddlelem  26703  cxpaddle  26704  affineequiv  26775  affineequiv2  26776  chordthmlem5  26788  dcubic2  26796  dcubic  26798  mcubic  26799  binom4  26802  dquartlem1  26803  quart1lem  26807  quart1  26808  quartlem1  26809  quart  26813  efiasin  26840  atantayl  26889  cvxcl  26936  scvxcvx  26937  lgamgulmlem5  26984  lgamcvg2  27006  lgam1  27015  wilthlem1  27019  wilthlem2  27020  basellem9  27040  fsumfldivdiaglem  27140  muinv  27144  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  30724  nvpi  30726  nvmtri  30730  ipval2  30766  ipasslem1  30890  ipasslem4  30893  bcs2  31241  lnfnaddi  32102  nnmulge  32800  quad3d  32810  2exple2exp  32906  indsumin  32909  ccfldsrarelvec  33803  constrfin  33878  constrremulcl  33899  constrrecl  33901  constrimcl  33902  constrmulcl  33903  constrreinvcl  33904  2sqr3minply  33912  cos9thpiminplylem2  33915  sqsscirc1  34040  eulerpartlemgs2  34512  plymulx0  34679  logdivsqrle  34782  subfacp1lem6  35355  subfaclim  35358  cvxpconn  35412  cvxsconn  35413  resconn  35416  sinccvglem  35842  fwddifn0  36334  nn0prpwlem  36492  knoppndvlem9  36768  knoppndvlem14  36773  bj-bary1lem1  37613  mblfinlem3  37968  itg2addnclem3  37982  iblabsnc  37993  iblmulc2nc  37994  ftc1anclem6  38007  ftc1anclem7  38008  ftc1anclem8  38009  areacirclem1  38017  bfplem2  38132  bfp  38133  rrntotbnd  38145  lcmineqlem1  42456  lcmineqlem12  42467  lcmineqlem18  42473  aks4d1p1p7  42501  aks4d1p8  42514  primrootscoprmpow  42526  posbezout  42527  aks6d1c2lem4  42554  3rdpwhole  42712  fltnlta  43084  3cubeslem2  43105  3cubeslem3r  43107  irrapxlem5  43242  pellexlem2  43246  pellexlem6  43250  pellfundex  43302  jm2.19lem3  43407  jm2.25  43415  jm2.27c  43423  jm3.1lem2  43434  flcidc  43586  reabssgn  44051  sqrtcval  44056  int-mul12d  44598  cvgdvgrat  44728  bccn1  44759  binomcxplemnotnn0  44771  fperiodmullem  45724  xralrple2  45772  fmul01lt1lem2  46003  mccllem  46015  reclimc  46069  cosknegpi  46285  dvsinax  46329  dvnxpaek  46358  dvnmul  46359  itgsinexp  46371  stoweidlem14  46430  stoweidlem26  46442  wallispilem4  46484  wallispilem5  46485  wallispi2lem1  46487  wallispi2  46489  stirlinglem1  46490  stirlinglem3  46492  stirlinglem4  46493  stirlinglem5  46494  stirlinglem6  46495  stirlinglem7  46496  stirlinglem10  46499  dirkertrigeqlem2  46515  dirkertrigeqlem3  46516  dirkercncflem2  46520  fourierdlem26  46549  fourierdlem41  46564  fourierdlem42  46565  fourierdlem56  46578  fourierdlem57  46579  fourierdlem58  46580  fourierdlem62  46584  fourierdlem64  46586  fourierdlem65  46587  fourierdlem95  46617  sqwvfoura  46644  sqwvfourb  46645  fouriersw  46647  etransclem23  46673  etransclem35  46685  etransclem46  46696  sin5tlem1  47309  sin5tlem2  47310  fmtnorec2lem  47993  fmtnorec3  47999  m1expoddALTV  48112  perfectALTVlem2  48186  ztprmneprm  48811  altgsumbc  48816  divge1b  48976  divgt1b  48977  ackval1  49145  affineid  49168  1subrec1sub  49169  rrx2vlinest  49205  line2x  49218