Theorem mullidd 11276

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150  1c1 11153   · cmul 11157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-mulcl 11214  ax-mulcom 11216  ax-mulass 11218  ax-distr 11219  ax-1rid 11222  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433

This theorem is referenced by:  adddirp1d  11284  addrid  11438  mulsubfacd  11721  mulcand  11893  receu  11905  divdivdiv  11965  divcan5  11966  subrec  12093  ltrec  12147  recp1lt1  12163  nndivtr  12310  subhalfhalf  12497  xp1d2m1eqxm1d2  12517  gtndiv  12692  ge2halflem1  13147  lincmb01cmp  13531  iccf1o  13532  ltdifltdiv  13870  modfrac  13920  negmod  13953  addmodid  13956  m1expcl2  14122  expgt1  14137  ltexp2a  14202  leexp2a  14208  binom3  14259  faclbnd  14325  faclbnd4lem4  14331  facavg  14336  bcval5  14353  cshweqrep  14855  01sqrexlem2  15278  absimle  15344  reccn2  15629  iseraltlem2  15715  iseraltlem3  15716  o1fsum  15845  abscvgcvg  15851  ackbijnn  15860  binom1p  15863  binom1dif  15865  incexclem  15868  incexc  15869  climcndslem1  15881  pwdif  15900  geomulcvg  15908  fprodsplit  15998  fallrisefac  16057  bpolysum  16085  bpolydiflem  16086  bpoly4  16091  efcllem  16109  ef01bndlem  16216  efieq1re  16231  eirrlem  16236  iddvds  16303  pwp1fsum  16424  oddpwp1fsum  16425  bitsfzolem  16467  bitsfzo  16468  rpmulgcd  16590  prmind2  16718  isprm5  16740  phiprm  16810  eulerthlem2  16815  fermltl  16817  hashgcdlem  16821  odzdvds  16828  powm2modprm  16836  modprm0  16838  pythagtriplem4  16852  4sqlem18  16995  vdwapun  17007  mulgnnass  19139  odinv  19593  odadd2  19881  pgpfaclem2  20116  abvneg  20843  pzriprnglem6  21514  pzriprnglem12  21520  nrginvrcnlem  24727  nmoid  24778  blcvx  24833  icopnfcnv  24986  reparphti  25042  reparphtiOLD  25043  pcorevlem  25072  ncvsm1  25201  ncvspi  25203  cphipval2  25288  cphipval  25290  itg11  25739  itg2mulc  25796  itg2monolem1  25799  itgcnlem  25839  iblabs  25878  dvexp  26005  dvmptdiv  26026  dvef  26032  lhop1lem  26066  dvcvx  26073  dvfsumlem1  26080  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumlem4  26084  dvfsum2  26089  plypow  26258  dgrcolem1  26327  vieta1lem2  26367  radcnvlem1  26470  radcnvlem2  26471  dvradcnv  26478  abelthlem6  26494  abelthlem7  26496  abelth2  26500  sinhalfpip  26548  sinhalfpim  26549  coshalfpip  26550  coshalfpim  26551  tangtx  26561  efif1olem4  26601  abslogle  26674  logdivlti  26676  advlog  26710  advlogexp  26711  logtayl  26716  cxpaddlelem  26808  cxpaddle  26809  affineequiv  26880  affineequiv2  26881  chordthmlem5  26893  dcubic2  26901  dcubic  26903  mcubic  26904  binom4  26907  dquartlem1  26908  quart1lem  26912  quart1  26913  quartlem1  26914  quart  26918  efiasin  26945  atantayl  26994  cvxcl  27042  scvxcvx  27043  lgamgulmlem5  27090  lgamcvg2  27112  lgam1  27121  wilthlem1  27125  wilthlem2  27126  basellem9  27146  fsumfldivdiaglem  27246  muinv  27250  chpub  27278  logexprlim  27283  mersenne  27285  perfectlem2  27288  dchrmullid  27310  dchrptlem1  27322  dchrsum2  27326  sumdchr2  27328  bposlem2  27343  bposlem9  27350  lgsval2lem  27365  lgsval4a  27377  lgsneg1  27380  lgsdir2lem4  27386  lgsdir  27390  lgsmulsqcoprm  27401  lgsdirnn0  27402  lgsdinn0  27403  gausslemma2dlem1a  27423  gausslemma2dlem4  27427  gausslemma2dlem7  27431  gausslemma2d  27432  lgseisenlem1  27433  lgseisenlem2  27434  lgseisenlem4  27436  lgsquad2lem1  27442  2sqlem8  27484  chebbnd1lem3  27529  chpchtlim  27537  rplogsumlem1  27542  rplogsumlem2  27543  rpvmasumlem  27545  dchrmusum2  27552  dchrvmasum2lem  27554  dchrvmasumlem2  27556  dchrvmasumlem3  27557  dchrisum0flblem1  27566  mulog2sumlem2  27593  vmalogdivsum2  27596  2vmadivsumlem  27598  log2sumbnd  27602  selberglem2  27604  selberg3lem1  27615  selberg4lem1  27618  pntrlog2bndlem2  27636  pntrlog2bndlem5  27639  pntpbnd1  27644  pntpbnd2  27645  pntibndlem2  27649  pntlemb  27655  pntlemr  27660  pntlemk  27664  pntlemo  27665  brbtwn2  28934  colinearalglem4  28938  ax5seglem3  28960  axbtwnid  28968  axpaschlem  28969  axeuclidlem  28991  axcontlem7  28999  axcontlem8  29000  elntg2  29014  nvm1  30693  nvpi  30695  nvmtri  30699  ipval2  30735  ipasslem1  30859  ipasslem4  30862  bcs2  31210  lnfnaddi  32071  nnmulge  32755  quad3d  32760  ccfldsrarelvec  33695  constrfin  33750  2sqr3minply  33752  sqsscirc1  33868  indsum  34001  indsumin  34002  eulerpartlemgs2  34361  plymulx0  34540  logdivsqrle  34643  subfacp1lem6  35169  subfaclim  35172  cvxpconn  35226  cvxsconn  35227  resconn  35230  sinccvglem  35656  fwddifn0  36145  nn0prpwlem  36304  knoppndvlem9  36502  knoppndvlem14  36507  bj-bary1lem1  37293  mblfinlem3  37645  itg2addnclem3  37659  iblabsnc  37670  iblmulc2nc  37671  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anclem8  37686  areacirclem1  37694  bfplem2  37809  bfp  37810  rrntotbnd  37822  lcmineqlem1  42010  lcmineqlem12  42021  lcmineqlem18  42027  aks4d1p1p7  42055  aks4d1p8  42068  primrootscoprmpow  42080  posbezout  42081  aks6d1c2lem4  42108  fltnlta  42649  3cubeslem2  42672  3cubeslem3r  42674  irrapxlem5  42813  pellexlem2  42817  pellexlem6  42821  pellfundex  42873  jm2.19lem3  42979  jm2.25  42987  jm2.27c  42995  jm3.1lem2  43006  flcidc  43158  reabssgn  43625  sqrtcval  43630  int-mul12d  44172  cvgdvgrat  44308  bccn1  44339  binomcxplemnotnn0  44351  fperiodmullem  45253  xralrple2  45303  fmul01lt1lem2  45540  mccllem  45552  reclimc  45608  cosknegpi  45824  dvsinax  45868  dvnxpaek  45897  dvnmul  45898  itgsinexp  45910  stoweidlem14  45969  stoweidlem26  45981  wallispilem4  46023  wallispilem5  46024  wallispi2lem1  46026  wallispi2  46028  stirlinglem1  46029  stirlinglem3  46031  stirlinglem4  46032  stirlinglem5  46033  stirlinglem6  46034  stirlinglem7  46035  stirlinglem10  46038  dirkertrigeqlem2  46054  dirkertrigeqlem3  46055  dirkercncflem2  46059  fourierdlem26  46088  fourierdlem41  46103  fourierdlem42  46104  fourierdlem56  46117  fourierdlem57  46118  fourierdlem58  46119  fourierdlem62  46123  fourierdlem64  46125  fourierdlem65  46126  fourierdlem95  46156  sqwvfoura  46183  sqwvfourb  46184  fouriersw  46186  etransclem23  46212  etransclem35  46224  etransclem46  46235  fmtnorec2lem  47466  fmtnorec3  47472  m1expoddALTV  47572  perfectALTVlem2  47646  ztprmneprm  48191  altgsumbc  48196  divge1b  48357  divgt1b  48358  ackval1  48530  affineid  48553  1subrec1sub  48554  rrx2vlinest  48590  line2x  48603