Theorem mullidd 11211

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

Syntax hints:   → wi 4   = wceq 1561   ∈ wcel 2143  (class class class)co 7396  ℂcc 11082  1c1 11085   · cmul 11089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735  ax-resscn 11141  ax-1cn 11142  ax-icn 11143  ax-addcl 11144  ax-mulcl 11146  ax-mulcom 11148  ax-mulass 11150  ax-distr 11151  ax-1rid 11154  ax-cnre 11157

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3088  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-iota 6477  df-fv 6529  df-ov 7399

This theorem is referenced by:  adddirp1d  11219  addrid  11374  mulsubfacd  11659  mulcand  11831  receu  11843  divdivdiv  11903  divcan5  11904  subrecd  12031  ltrec  12084  recp1lt1  12100  nndivtr  12270  subhalfhalf  12465  xp1d2m1eqxm1d2  12485  gtndiv  12660  ge2halflem1  13120  lincmb01cmp  13509  iccf1o  13510  ltdifltdiv  13854  modfrac  13904  negmod  13939  addmodid  13942  m1expcl2  14108  expgt1  14123  ltexp2a  14189  leexp2a  14195  binom3  14247  faclbnd  14313  faclbnd4lem4  14319  facavg  14324  bcval5  14341  cshweqrep  14844  01sqrexlem2  15280  absimle  15346  reccn2  15634  iseraltlem2  15720  iseraltlem3  15721  o1fsum  15851  abscvgcvg  15857  indsum  15866  ackbijnn  15868  binom1p  15871  binom1dif  15873  incexclem  15876  incexc  15877  climcndslem1  15889  pwdif  15908  geomulcvg  15916  fprodsplit  16006  fallrisefac  16065  bpolysum  16093  bpolydiflem  16094  bpoly4  16099  efcllem  16117  ef01bndlem  16226  efieq1re  16241  eirrlem  16246  iddvds  16313  pwp1fsum  16435  oddpwp1fsum  16436  bitsfzolem  16478  bitsfzo  16479  rpmulgcd  16601  prmind2  16729  isprm5  16752  phiprm  16822  eulerthlem2  16827  fermltl  16829  hashgcdlem  16833  odzdvds  16841  powm2modprm  16849  modprm0  16851  pythagtriplem4  16865  4sqlem18  17008  vdwapun  17020  mulgnnass  19161  odinv  19611  odadd2  19899  pgpfaclem2  20134  abvneg  20882  pzriprnglem6  21545  pzriprnglem12  21551  nrginvrcnlem  24758  nmoid  24809  blcvx  24865  icopnfcnv  25011  reparphti  25066  pcorevlem  25095  ncvsm1  25223  ncvspi  25225  cphipval2  25310  cphipval  25312  itg11  25760  itg2mulc  25816  itg2monolem1  25819  itgcnlem  25859  iblabs  25898  dvexp  26022  dvmptdiv  26043  dvef  26049  lhop1lem  26082  dvcvx  26089  dvfsumlem1  26095  dvfsumlem2  26096  dvfsumlem4  26098  dvfsum2  26103  plypow  26272  dgrcolem1  26340  plyn0mulidp  26352  vieta1lem2  26382  radcnvlem1  26483  radcnvlem2  26484  dvradcnv  26491  abelthlem6  26506  abelthlem7  26508  abelth2  26512  sinhalfpip  26564  sinhalfpim  26565  coshalfpip  26566  coshalfpim  26567  tangtx  26577  efif1olem4  26617  abslogle  26690  logdivlti  26692  advlog  26726  advlogexp  26727  logtayl  26732  cxpaddlelem  26823  cxpaddle  26824  affineequiv  26895  affineequiv2  26896  chordthmlem5  26908  dcubic2  26916  dcubic  26918  mcubic  26919  binom4  26922  dquartlem1  26923  quart1lem  26927  quart1  26928  quartlem1  26929  quart  26933  efiasin  26960  atantayl  27009  cvxcl  27056  scvxcvx  27057  lgamgulmlem5  27104  lgamcvg2  27126  lgam1  27135  wilthlem1  27139  wilthlem2  27140  basellem9  27160  fsumfldivdiaglem  27260  muinv  27264  chpub  27291  logexprlim  27296  mersenne  27298  perfectlem2  27301  dchrmullid  27323  dchrptlem1  27335  dchrsum2  27339  sumdchr2  27341  bposlem2  27356  bposlem9  27363  lgsval2lem  27378  lgsval4a  27390  lgsneg1  27393  lgsdir2lem4  27399  lgsdir  27403  lgsmulsqcoprm  27414  lgsdirnn0  27415  lgsdinn0  27416  gausslemma2dlem1a  27436  gausslemma2dlem4  27440  gausslemma2dlem7  27444  gausslemma2d  27445  lgseisenlem1  27446  lgseisenlem2  27447  lgseisenlem4  27449  lgsquad2lem1  27455  2sqlem8  27497  chebbnd1lem3  27542  chpchtlim  27550  rplogsumlem1  27555  rplogsumlem2  27556  rpvmasumlem  27558  dchrmusum2  27565  dchrvmasum2lem  27567  dchrvmasumlem2  27569  dchrvmasumlem3  27570  dchrisum0flblem1  27579  mulog2sumlem2  27606  vmalogdivsum2  27609  2vmadivsumlem  27611  log2sumbnd  27615  selberglem2  27617  selberg3lem1  27628  selberg4lem1  27631  pntrlog2bndlem2  27649  pntrlog2bndlem5  27652  pntpbnd1  27657  pntpbnd2  27658  pntibndlem2  27662  pntlemb  27668  pntlemr  27673  pntlemk  27677  pntlemo  27678  brbtwn2  29113  colinearalglem4  29117  ax5seglem3  29139  axbtwnid  29147  axpaschlem  29148  axeuclidlem  29170  axcontlem7  29178  axcontlem8  29179  elntg2  29193  nvm1  30875  nvpi  30877  nvmtri  30881  ipval2  30917  ipasslem1  31041  ipasslem4  31044  bcs2  31392  lnfnaddi  32253  nnmulge  32947  quad3d  32957  2exple2exp  33042  indsumin  33045  ccfldsrarelvec  33970  constrfin  34045  constrremulcl  34066  constrrecl  34068  constrimcl  34069  constrmulcl  34070  constrreinvcl  34071  2sqr3minply  34079  cos9thpiminplylem2  34082  sqsscirc1  34207  eulerpartlemgs2  34679  logdivsqrle  34946  subfacp1lem6  35540  subfaclim  35543  cvxpconn  35597  cvxsconn  35598  resconn  35601  sinccvglem  36027  fwddifn0  36519  nn0prpwlem  36687  knoppndvlem9  36963  knoppndvlem14  36968  bj-bary1lem1  37808  mblfinlem3  38163  itg2addnclem3  38177  iblabsnc  38188  iblmulc2nc  38189  ftc1anclem6  38202  ftc1anclem7  38203  ftc1anclem8  38204  areacirclem1  38212  bfplem2  38327  bfp  38328  rrntotbnd  38340  lcmineqlem1  42651  lcmineqlem12  42662  lcmineqlem18  42668  aks4d1p1p7  42696  aks4d1p8  42709  primrootscoprmpow  42721  posbezout  42722  aks6d1c2lem4  42749  3rdpwhole  42906  fltnlta  43250  3cubeslem2  43271  3cubeslem3r  43273  irrapxlem5  43408  pellexlem2  43412  pellexlem6  43416  pellfundex  43468  jm2.19lem3  43573  jm2.25  43581  jm2.27c  43589  jm3.1lem2  43600  flcidc  43752  reabssgn  44217  sqrtcval  44222  int-mul12d  44764  cvgdvgrat  44880  bccn1  44911  binomcxplemnotnn0  44923  fperiodmullem  45873  xralrple2  45921  fmul01lt1lem2  46152  mccllem  46164  reclimc  46218  cosknegpi  46434  dvsinax  46478  dvnxpaek  46507  dvnmul  46508  itgsinexp  46520  stoweidlem14  46579  stoweidlem26  46591  wallispilem4  46633  wallispilem5  46634  wallispi2lem1  46636  wallispi2  46638  stirlinglem1  46639  stirlinglem3  46641  stirlinglem4  46642  stirlinglem5  46643  stirlinglem6  46644  stirlinglem7  46645  stirlinglem10  46648  dirkertrigeqlem2  46664  dirkertrigeqlem3  46665  dirkercncflem2  46669  fourierdlem26  46698  fourierdlem41  46713  fourierdlem42  46714  fourierdlem56  46727  fourierdlem57  46728  fourierdlem58  46729  fourierdlem62  46733  fourierdlem64  46735  fourierdlem65  46736  fourierdlem95  46766  sqwvfoura  46793  sqwvfourb  46794  fouriersw  46796  etransclem23  46822  etransclem35  46834  etransclem46  46845  sin5tlem1  47458  sin5tlem2  47459  fmtnorec2lem  48142  fmtnorec3  48148  m1expoddALTV  48261  perfectALTVlem2  48335  ztprmneprm  48960  altgsumbc  48965  divge1b  49125  divgt1b  49126  ackval1  49294  affineid  49317  1subrec1sub  49318  rrx2vlinest  49354  line2x  49367