Theorem mullidd 11199

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073  1c1 11076   · cmul 11080

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-mulcl 11137  ax-mulcom 11139  ax-mulass 11141  ax-distr 11142  ax-1rid 11145  ax-cnre 11148

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  adddirp1d  11207  addrid  11361  mulsubfacd  11646  mulcand  11818  receu  11830  divdivdiv  11890  divcan5  11891  subrecd  12018  ltrec  12072  recp1lt1  12088  nndivtr  12240  subhalfhalf  12423  xp1d2m1eqxm1d2  12443  gtndiv  12618  ge2halflem1  13075  lincmb01cmp  13463  iccf1o  13464  ltdifltdiv  13803  modfrac  13853  negmod  13888  addmodid  13891  m1expcl2  14057  expgt1  14072  ltexp2a  14138  leexp2a  14144  binom3  14196  faclbnd  14262  faclbnd4lem4  14268  facavg  14273  bcval5  14290  cshweqrep  14793  01sqrexlem2  15216  absimle  15282  reccn2  15570  iseraltlem2  15656  iseraltlem3  15657  o1fsum  15786  abscvgcvg  15792  ackbijnn  15801  binom1p  15804  binom1dif  15806  incexclem  15809  incexc  15810  climcndslem1  15822  pwdif  15841  geomulcvg  15849  fprodsplit  15939  fallrisefac  15998  bpolysum  16026  bpolydiflem  16027  bpoly4  16032  efcllem  16050  ef01bndlem  16159  efieq1re  16174  eirrlem  16179  iddvds  16246  pwp1fsum  16368  oddpwp1fsum  16369  bitsfzolem  16411  bitsfzo  16412  rpmulgcd  16534  prmind2  16662  isprm5  16684  phiprm  16754  eulerthlem2  16759  fermltl  16761  hashgcdlem  16765  odzdvds  16773  powm2modprm  16781  modprm0  16783  pythagtriplem4  16797  4sqlem18  16940  vdwapun  16952  mulgnnass  19048  odinv  19498  odadd2  19786  pgpfaclem2  20021  abvneg  20742  pzriprnglem6  21403  pzriprnglem12  21409  nrginvrcnlem  24586  nmoid  24637  blcvx  24693  icopnfcnv  24847  reparphti  24903  reparphtiOLD  24904  pcorevlem  24933  ncvsm1  25061  ncvspi  25063  cphipval2  25148  cphipval  25150  itg11  25599  itg2mulc  25655  itg2monolem1  25658  itgcnlem  25698  iblabs  25737  dvexp  25864  dvmptdiv  25885  dvef  25891  lhop1lem  25925  dvcvx  25932  dvfsumlem1  25939  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsumlem4  25943  dvfsum2  25948  plypow  26117  dgrcolem1  26186  vieta1lem2  26226  radcnvlem1  26329  radcnvlem2  26330  dvradcnv  26337  abelthlem6  26353  abelthlem7  26355  abelth2  26359  sinhalfpip  26408  sinhalfpim  26409  coshalfpip  26410  coshalfpim  26411  tangtx  26421  efif1olem4  26461  abslogle  26534  logdivlti  26536  advlog  26570  advlogexp  26571  logtayl  26576  cxpaddlelem  26668  cxpaddle  26669  affineequiv  26740  affineequiv2  26741  chordthmlem5  26753  dcubic2  26761  dcubic  26763  mcubic  26764  binom4  26767  dquartlem1  26768  quart1lem  26772  quart1  26773  quartlem1  26774  quart  26778  efiasin  26805  atantayl  26854  cvxcl  26902  scvxcvx  26903  lgamgulmlem5  26950  lgamcvg2  26972  lgam1  26981  wilthlem1  26985  wilthlem2  26986  basellem9  27006  fsumfldivdiaglem  27106  muinv  27110  chpub  27138  logexprlim  27143  mersenne  27145  perfectlem2  27148  dchrmullid  27170  dchrptlem1  27182  dchrsum2  27186  sumdchr2  27188  bposlem2  27203  bposlem9  27210  lgsval2lem  27225  lgsval4a  27237  lgsneg1  27240  lgsdir2lem4  27246  lgsdir  27250  lgsmulsqcoprm  27261  lgsdirnn0  27262  lgsdinn0  27263  gausslemma2dlem1a  27283  gausslemma2dlem4  27287  gausslemma2dlem7  27291  gausslemma2d  27292  lgseisenlem1  27293  lgseisenlem2  27294  lgseisenlem4  27296  lgsquad2lem1  27302  2sqlem8  27344  chebbnd1lem3  27389  chpchtlim  27397  rplogsumlem1  27402  rplogsumlem2  27403  rpvmasumlem  27405  dchrmusum2  27412  dchrvmasum2lem  27414  dchrvmasumlem2  27416  dchrvmasumlem3  27417  dchrisum0flblem1  27426  mulog2sumlem2  27453  vmalogdivsum2  27456  2vmadivsumlem  27458  log2sumbnd  27462  selberglem2  27464  selberg3lem1  27475  selberg4lem1  27478  pntrlog2bndlem2  27496  pntrlog2bndlem5  27499  pntpbnd1  27504  pntpbnd2  27505  pntibndlem2  27509  pntlemb  27515  pntlemr  27520  pntlemk  27524  pntlemo  27525  brbtwn2  28839  colinearalglem4  28843  ax5seglem3  28865  axbtwnid  28873  axpaschlem  28874  axeuclidlem  28896  axcontlem7  28904  axcontlem8  28905  elntg2  28919  nvm1  30601  nvpi  30603  nvmtri  30607  ipval2  30643  ipasslem1  30767  ipasslem4  30770  bcs2  31118  lnfnaddi  31979  nnmulge  32669  quad3d  32680  2exple2exp  32777  indsum  32791  indsumin  32792  ccfldsrarelvec  33673  constrfin  33743  constrremulcl  33764  constrrecl  33766  constrimcl  33767  constrmulcl  33768  constrreinvcl  33769  2sqr3minply  33777  cos9thpiminplylem2  33780  sqsscirc1  33905  eulerpartlemgs2  34378  plymulx0  34545  logdivsqrle  34648  subfacp1lem6  35179  subfaclim  35182  cvxpconn  35236  cvxsconn  35237  resconn  35240  sinccvglem  35666  fwddifn0  36159  nn0prpwlem  36317  knoppndvlem9  36515  knoppndvlem14  36520  bj-bary1lem1  37306  mblfinlem3  37660  itg2addnclem3  37674  iblabsnc  37685  iblmulc2nc  37686  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anclem8  37701  areacirclem1  37709  bfplem2  37824  bfp  37825  rrntotbnd  37837  lcmineqlem1  42024  lcmineqlem12  42035  lcmineqlem18  42041  aks4d1p1p7  42069  aks4d1p8  42082  primrootscoprmpow  42094  posbezout  42095  aks6d1c2lem4  42122  3rdpwhole  42287  fltnlta  42658  3cubeslem2  42680  3cubeslem3r  42682  irrapxlem5  42821  pellexlem2  42825  pellexlem6  42829  pellfundex  42881  jm2.19lem3  42987  jm2.25  42995  jm2.27c  43003  jm3.1lem2  43014  flcidc  43166  reabssgn  43632  sqrtcval  43637  int-mul12d  44179  cvgdvgrat  44309  bccn1  44340  binomcxplemnotnn0  44352  fperiodmullem  45308  xralrple2  45357  fmul01lt1lem2  45590  mccllem  45602  reclimc  45658  cosknegpi  45874  dvsinax  45918  dvnxpaek  45947  dvnmul  45948  itgsinexp  45960  stoweidlem14  46019  stoweidlem26  46031  wallispilem4  46073  wallispilem5  46074  wallispi2lem1  46076  wallispi2  46078  stirlinglem1  46079  stirlinglem3  46081  stirlinglem4  46082  stirlinglem5  46083  stirlinglem6  46084  stirlinglem7  46085  stirlinglem10  46088  dirkertrigeqlem2  46104  dirkertrigeqlem3  46105  dirkercncflem2  46109  fourierdlem26  46138  fourierdlem41  46153  fourierdlem42  46154  fourierdlem56  46167  fourierdlem57  46168  fourierdlem58  46169  fourierdlem62  46173  fourierdlem64  46175  fourierdlem65  46176  fourierdlem95  46206  sqwvfoura  46233  sqwvfourb  46234  fouriersw  46236  etransclem23  46262  etransclem35  46274  etransclem46  46285  fmtnorec2lem  47547  fmtnorec3  47553  m1expoddALTV  47653  perfectALTVlem2  47727  ztprmneprm  48339  altgsumbc  48344  divge1b  48505  divgt1b  48506  ackval1  48674  affineid  48697  1subrec1sub  48698  rrx2vlinest  48734  line2x  48747