Theorem mullidd 11140

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7355  ℂcc 11014  1c1 11017   · cmul 11021

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-resscn 11073  ax-1cn 11074  ax-icn 11075  ax-addcl 11076  ax-mulcl 11078  ax-mulcom 11080  ax-mulass 11082  ax-distr 11083  ax-1rid 11086  ax-cnre 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-ov 7358

This theorem is referenced by:  adddirp1d  11148  addrid  11303  mulsubfacd  11588  mulcand  11760  receu  11772  divdivdiv  11832  divcan5  11833  subrecd  11960  ltrec  12014  recp1lt1  12030  nndivtr  12182  subhalfhalf  12365  xp1d2m1eqxm1d2  12385  gtndiv  12560  ge2halflem1  13017  lincmb01cmp  13405  iccf1o  13406  ltdifltdiv  13748  modfrac  13798  negmod  13833  addmodid  13836  m1expcl2  14002  expgt1  14017  ltexp2a  14083  leexp2a  14089  binom3  14141  faclbnd  14207  faclbnd4lem4  14213  facavg  14218  bcval5  14235  cshweqrep  14738  01sqrexlem2  15160  absimle  15226  reccn2  15514  iseraltlem2  15600  iseraltlem3  15601  o1fsum  15730  abscvgcvg  15736  ackbijnn  15745  binom1p  15748  binom1dif  15750  incexclem  15753  incexc  15754  climcndslem1  15766  pwdif  15785  geomulcvg  15793  fprodsplit  15883  fallrisefac  15942  bpolysum  15970  bpolydiflem  15971  bpoly4  15976  efcllem  15994  ef01bndlem  16103  efieq1re  16118  eirrlem  16123  iddvds  16190  pwp1fsum  16312  oddpwp1fsum  16313  bitsfzolem  16355  bitsfzo  16356  rpmulgcd  16478  prmind2  16606  isprm5  16628  phiprm  16698  eulerthlem2  16703  fermltl  16705  hashgcdlem  16709  odzdvds  16717  powm2modprm  16725  modprm0  16727  pythagtriplem4  16741  4sqlem18  16884  vdwapun  16896  mulgnnass  19032  odinv  19483  odadd2  19771  pgpfaclem2  20006  abvneg  20751  pzriprnglem6  21433  pzriprnglem12  21439  nrginvrcnlem  24616  nmoid  24667  blcvx  24723  icopnfcnv  24877  reparphti  24933  reparphtiOLD  24934  pcorevlem  24963  ncvsm1  25091  ncvspi  25093  cphipval2  25178  cphipval  25180  itg11  25629  itg2mulc  25685  itg2monolem1  25688  itgcnlem  25728  iblabs  25767  dvexp  25894  dvmptdiv  25915  dvef  25921  lhop1lem  25955  dvcvx  25962  dvfsumlem1  25969  dvfsumlem2  25970  dvfsumlem2OLD  25971  dvfsumlem4  25973  dvfsum2  25978  plypow  26147  dgrcolem1  26216  vieta1lem2  26256  radcnvlem1  26359  radcnvlem2  26360  dvradcnv  26367  abelthlem6  26383  abelthlem7  26385  abelth2  26389  sinhalfpip  26438  sinhalfpim  26439  coshalfpip  26440  coshalfpim  26441  tangtx  26451  efif1olem4  26491  abslogle  26564  logdivlti  26566  advlog  26600  advlogexp  26601  logtayl  26606  cxpaddlelem  26698  cxpaddle  26699  affineequiv  26770  affineequiv2  26771  chordthmlem5  26783  dcubic2  26791  dcubic  26793  mcubic  26794  binom4  26797  dquartlem1  26798  quart1lem  26802  quart1  26803  quartlem1  26804  quart  26808  efiasin  26835  atantayl  26884  cvxcl  26932  scvxcvx  26933  lgamgulmlem5  26980  lgamcvg2  27002  lgam1  27011  wilthlem1  27015  wilthlem2  27016  basellem9  27036  fsumfldivdiaglem  27136  muinv  27140  chpub  27168  logexprlim  27173  mersenne  27175  perfectlem2  27178  dchrmullid  27200  dchrptlem1  27212  dchrsum2  27216  sumdchr2  27218  bposlem2  27233  bposlem9  27240  lgsval2lem  27255  lgsval4a  27267  lgsneg1  27270  lgsdir2lem4  27276  lgsdir  27280  lgsmulsqcoprm  27291  lgsdirnn0  27292  lgsdinn0  27293  gausslemma2dlem1a  27313  gausslemma2dlem4  27317  gausslemma2dlem7  27321  gausslemma2d  27322  lgseisenlem1  27323  lgseisenlem2  27324  lgseisenlem4  27326  lgsquad2lem1  27332  2sqlem8  27374  chebbnd1lem3  27419  chpchtlim  27427  rplogsumlem1  27432  rplogsumlem2  27433  rpvmasumlem  27435  dchrmusum2  27442  dchrvmasum2lem  27444  dchrvmasumlem2  27446  dchrvmasumlem3  27447  dchrisum0flblem1  27456  mulog2sumlem2  27483  vmalogdivsum2  27486  2vmadivsumlem  27488  log2sumbnd  27492  selberglem2  27494  selberg3lem1  27505  selberg4lem1  27508  pntrlog2bndlem2  27526  pntrlog2bndlem5  27529  pntpbnd1  27534  pntpbnd2  27535  pntibndlem2  27539  pntlemb  27545  pntlemr  27550  pntlemk  27554  pntlemo  27555  brbtwn2  28894  colinearalglem4  28898  ax5seglem3  28920  axbtwnid  28928  axpaschlem  28929  axeuclidlem  28951  axcontlem7  28959  axcontlem8  28960  elntg2  28974  nvm1  30656  nvpi  30658  nvmtri  30662  ipval2  30698  ipasslem1  30822  ipasslem4  30825  bcs2  31173  lnfnaddi  32034  nnmulge  32733  quad3d  32744  2exple2exp  32839  indsum  32853  indsumin  32854  ccfldsrarelvec  33695  constrfin  33770  constrremulcl  33791  constrrecl  33793  constrimcl  33794  constrmulcl  33795  constrreinvcl  33796  2sqr3minply  33804  cos9thpiminplylem2  33807  sqsscirc1  33932  eulerpartlemgs2  34404  plymulx0  34571  logdivsqrle  34674  subfacp1lem6  35240  subfaclim  35243  cvxpconn  35297  cvxsconn  35298  resconn  35301  sinccvglem  35727  fwddifn0  36219  nn0prpwlem  36377  knoppndvlem9  36575  knoppndvlem14  36580  bj-bary1lem1  37366  mblfinlem3  37709  itg2addnclem3  37723  iblabsnc  37734  iblmulc2nc  37735  ftc1anclem6  37748  ftc1anclem7  37749  ftc1anclem8  37750  areacirclem1  37758  bfplem2  37873  bfp  37874  rrntotbnd  37886  lcmineqlem1  42132  lcmineqlem12  42143  lcmineqlem18  42149  aks4d1p1p7  42177  aks4d1p8  42190  primrootscoprmpow  42202  posbezout  42203  aks6d1c2lem4  42230  3rdpwhole  42400  fltnlta  42771  3cubeslem2  42792  3cubeslem3r  42794  irrapxlem5  42933  pellexlem2  42937  pellexlem6  42941  pellfundex  42993  jm2.19lem3  43098  jm2.25  43106  jm2.27c  43114  jm3.1lem2  43125  flcidc  43277  reabssgn  43743  sqrtcval  43748  int-mul12d  44290  cvgdvgrat  44420  bccn1  44451  binomcxplemnotnn0  44463  fperiodmullem  45418  xralrple2  45467  fmul01lt1lem2  45699  mccllem  45711  reclimc  45765  cosknegpi  45981  dvsinax  46025  dvnxpaek  46054  dvnmul  46055  itgsinexp  46067  stoweidlem14  46126  stoweidlem26  46138  wallispilem4  46180  wallispilem5  46181  wallispi2lem1  46183  wallispi2  46185  stirlinglem1  46186  stirlinglem3  46188  stirlinglem4  46189  stirlinglem5  46190  stirlinglem6  46191  stirlinglem7  46192  stirlinglem10  46195  dirkertrigeqlem2  46211  dirkertrigeqlem3  46212  dirkercncflem2  46216  fourierdlem26  46245  fourierdlem41  46260  fourierdlem42  46261  fourierdlem56  46274  fourierdlem57  46275  fourierdlem58  46276  fourierdlem62  46280  fourierdlem64  46282  fourierdlem65  46283  fourierdlem95  46313  sqwvfoura  46340  sqwvfourb  46341  fouriersw  46343  etransclem23  46369  etransclem35  46381  etransclem46  46392  fmtnorec2lem  47656  fmtnorec3  47662  m1expoddALTV  47762  perfectALTVlem2  47836  ztprmneprm  48461  altgsumbc  48466  divge1b  48627  divgt1b  48628  ackval1  48796  affineid  48819  1subrec1sub  48820  rrx2vlinest  48856  line2x  48869