Theorem mullidd 11163

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036  1c1 11039   · cmul 11043

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 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-mulcom 11102  ax-mulass 11104  ax-distr 11105  ax-1rid 11108  ax-cnre 11111

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 6455  df-fv 6507  df-ov 7370

This theorem is referenced by:  adddirp1d  11171  addrid  11326  mulsubfacd  11611  mulcand  11783  receu  11795  divdivdiv  11856  divcan5  11857  subrecd  11984  ltrec  12038  recp1lt1  12054  nndivtr  12224  subhalfhalf  12411  xp1d2m1eqxm1d2  12431  gtndiv  12606  ge2halflem1  13059  lincmb01cmp  13448  iccf1o  13449  ltdifltdiv  13793  modfrac  13843  negmod  13878  addmodid  13881  m1expcl2  14047  expgt1  14062  ltexp2a  14128  leexp2a  14134  binom3  14186  faclbnd  14252  faclbnd4lem4  14258  facavg  14263  bcval5  14280  cshweqrep  14783  01sqrexlem2  15205  absimle  15271  reccn2  15559  iseraltlem2  15645  iseraltlem3  15646  o1fsum  15776  abscvgcvg  15782  indsum  15791  ackbijnn  15793  binom1p  15796  binom1dif  15798  incexclem  15801  incexc  15802  climcndslem1  15814  pwdif  15833  geomulcvg  15841  fprodsplit  15931  fallrisefac  15990  bpolysum  16018  bpolydiflem  16019  bpoly4  16024  efcllem  16042  ef01bndlem  16151  efieq1re  16166  eirrlem  16171  iddvds  16238  pwp1fsum  16360  oddpwp1fsum  16361  bitsfzolem  16403  bitsfzo  16404  rpmulgcd  16526  prmind2  16654  isprm5  16677  phiprm  16747  eulerthlem2  16752  fermltl  16754  hashgcdlem  16758  odzdvds  16766  powm2modprm  16774  modprm0  16776  pythagtriplem4  16790  4sqlem18  16933  vdwapun  16945  mulgnnass  19085  odinv  19536  odadd2  19824  pgpfaclem2  20059  abvneg  20803  pzriprnglem6  21466  pzriprnglem12  21472  nrginvrcnlem  24656  nmoid  24707  blcvx  24763  icopnfcnv  24909  reparphti  24964  pcorevlem  24993  ncvsm1  25121  ncvspi  25123  cphipval2  25208  cphipval  25210  itg11  25658  itg2mulc  25714  itg2monolem1  25717  itgcnlem  25757  iblabs  25796  dvexp  25920  dvmptdiv  25941  dvef  25947  lhop1lem  25980  dvcvx  25987  dvfsumlem1  25993  dvfsumlem2  25994  dvfsumlem4  25996  dvfsum2  26001  plypow  26170  dgrcolem1  26238  vieta1lem2  26277  radcnvlem1  26378  radcnvlem2  26379  dvradcnv  26386  abelthlem6  26401  abelthlem7  26403  abelth2  26407  sinhalfpip  26456  sinhalfpim  26457  coshalfpip  26458  coshalfpim  26459  tangtx  26469  efif1olem4  26509  abslogle  26582  logdivlti  26584  advlog  26618  advlogexp  26619  logtayl  26624  cxpaddlelem  26715  cxpaddle  26716  affineequiv  26787  affineequiv2  26788  chordthmlem5  26800  dcubic2  26808  dcubic  26810  mcubic  26811  binom4  26814  dquartlem1  26815  quart1lem  26819  quart1  26820  quartlem1  26821  quart  26825  efiasin  26852  atantayl  26901  cvxcl  26948  scvxcvx  26949  lgamgulmlem5  26996  lgamcvg2  27018  lgam1  27027  wilthlem1  27031  wilthlem2  27032  basellem9  27052  fsumfldivdiaglem  27152  muinv  27156  chpub  27183  logexprlim  27188  mersenne  27190  perfectlem2  27193  dchrmullid  27215  dchrptlem1  27227  dchrsum2  27231  sumdchr2  27233  bposlem2  27248  bposlem9  27255  lgsval2lem  27270  lgsval4a  27282  lgsneg1  27285  lgsdir2lem4  27291  lgsdir  27295  lgsmulsqcoprm  27306  lgsdirnn0  27307  lgsdinn0  27308  gausslemma2dlem1a  27328  gausslemma2dlem4  27332  gausslemma2dlem7  27336  gausslemma2d  27337  lgseisenlem1  27338  lgseisenlem2  27339  lgseisenlem4  27341  lgsquad2lem1  27347  2sqlem8  27389  chebbnd1lem3  27434  chpchtlim  27442  rplogsumlem1  27447  rplogsumlem2  27448  rpvmasumlem  27450  dchrmusum2  27457  dchrvmasum2lem  27459  dchrvmasumlem2  27461  dchrvmasumlem3  27462  dchrisum0flblem1  27471  mulog2sumlem2  27498  vmalogdivsum2  27501  2vmadivsumlem  27503  log2sumbnd  27507  selberglem2  27509  selberg3lem1  27520  selberg4lem1  27523  pntrlog2bndlem2  27541  pntrlog2bndlem5  27544  pntpbnd1  27549  pntpbnd2  27550  pntibndlem2  27554  pntlemb  27560  pntlemr  27565  pntlemk  27569  pntlemo  27570  brbtwn2  28974  colinearalglem4  28978  ax5seglem3  29000  axbtwnid  29008  axpaschlem  29009  axeuclidlem  29031  axcontlem7  29039  axcontlem8  29040  elntg2  29054  nvm1  30736  nvpi  30738  nvmtri  30742  ipval2  30778  ipasslem1  30902  ipasslem4  30905  bcs2  31253  lnfnaddi  32114  nnmulge  32812  quad3d  32822  2exple2exp  32918  indsumin  32921  ccfldsrarelvec  33815  constrfin  33890  constrremulcl  33911  constrrecl  33913  constrimcl  33914  constrmulcl  33915  constrreinvcl  33916  2sqr3minply  33924  cos9thpiminplylem2  33927  sqsscirc1  34052  eulerpartlemgs2  34524  plymulx0  34691  logdivsqrle  34794  subfacp1lem6  35367  subfaclim  35370  cvxpconn  35424  cvxsconn  35425  resconn  35428  sinccvglem  35854  fwddifn0  36346  nn0prpwlem  36504  knoppndvlem9  36780  knoppndvlem14  36785  bj-bary1lem1  37625  mblfinlem3  37980  itg2addnclem3  37994  iblabsnc  38005  iblmulc2nc  38006  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anclem8  38021  areacirclem1  38029  bfplem2  38144  bfp  38145  rrntotbnd  38157  lcmineqlem1  42468  lcmineqlem12  42479  lcmineqlem18  42485  aks4d1p1p7  42513  aks4d1p8  42526  primrootscoprmpow  42538  posbezout  42539  aks6d1c2lem4  42566  3rdpwhole  42724  fltnlta  43096  3cubeslem2  43117  3cubeslem3r  43119  irrapxlem5  43254  pellexlem2  43258  pellexlem6  43262  pellfundex  43314  jm2.19lem3  43419  jm2.25  43427  jm2.27c  43435  jm3.1lem2  43446  flcidc  43598  reabssgn  44063  sqrtcval  44068  int-mul12d  44610  cvgdvgrat  44740  bccn1  44771  binomcxplemnotnn0  44783  fperiodmullem  45736  xralrple2  45784  fmul01lt1lem2  46015  mccllem  46027  reclimc  46081  cosknegpi  46297  dvsinax  46341  dvnxpaek  46370  dvnmul  46371  itgsinexp  46383  stoweidlem14  46442  stoweidlem26  46454  wallispilem4  46496  wallispilem5  46497  wallispi2lem1  46499  wallispi2  46501  stirlinglem1  46502  stirlinglem3  46504  stirlinglem4  46505  stirlinglem5  46506  stirlinglem6  46507  stirlinglem7  46508  stirlinglem10  46511  dirkertrigeqlem2  46527  dirkertrigeqlem3  46528  dirkercncflem2  46532  fourierdlem26  46561  fourierdlem41  46576  fourierdlem42  46577  fourierdlem56  46590  fourierdlem57  46591  fourierdlem58  46592  fourierdlem62  46596  fourierdlem64  46598  fourierdlem65  46599  fourierdlem95  46629  sqwvfoura  46656  sqwvfourb  46657  fouriersw  46659  etransclem23  46685  etransclem35  46697  etransclem46  46708  sin5tlem1  47319  sin5tlem2  47320  fmtnorec2lem  47999  fmtnorec3  48005  m1expoddALTV  48118  perfectALTVlem2  48192  ztprmneprm  48817  altgsumbc  48822  divge1b  48982  divgt1b  48983  ackval1  49151  affineid  49174  1subrec1sub  49175  rrx2vlinest  49211  line2x  49224