Theorem mullidd 11233

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2142  (class class class)co 7412  ℂcc 11104  1c1 11107   · cmul 11111

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-mulcl 11168  ax-mulcom 11170  ax-mulass 11172  ax-distr 11173  ax-1rid 11176  ax-cnre 11179

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rex 3089  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-ov 7415

This theorem is used by:  adddirp1d  11241  addrid  11396  mulsubfacd  11681  mulcand  11853  receu  11865  divdivdiv  11922  divcan5  11923  subrecd  12050  ltrec  12103  recp1lt1  12119  nndivtr  12289  subhalfhalf  12484  xp1d2m1eqxm1d2  12504  gtndiv  12679  ge2halflem1  13139  lincmb01cmp  13528  iccf1o  13529  ltdifltdiv  13874  modfrac  13924  negmod  13959  addmodid  13962  m1expcl2  14128  expgt1  14143  ltexp2a  14209  leexp2a  14215  binom3  14267  faclbnd  14333  faclbnd4lem4  14339  facavg  14344  bcval5  14361  cshweqrep  14865  01sqrexlem2  15301  absimle  15367  reccn2  15655  iseraltlem2  15741  iseraltlem3  15742  o1fsum  15872  abscvgcvg  15878  indsum  15887  ackbijnn  15889  binom1p  15892  binom1dif  15894  incexclem  15897  incexc  15898  climcndslem1  15910  pwdif  15929  geomulcvg  15937  fprodsplit  16027  fallrisefac  16086  bpolysum  16113  bpolydiflem  16114  bpoly4  16119  efcllem  16137  ef01bndlem  16246  efieq1re  16261  eirrlem  16266  iddvds  16333  pwp1fsum  16455  oddpwp1fsum  16456  bitsfzolem  16498  bitsfzo  16499  rpmulgcd  16621  prmind2  16749  isprm5  16772  phiprm  16842  eulerthlem2  16847  fermltl  16849  hashgcdlem  16853  odzdvds  16861  powm2modprm  16869  modprm0  16871  pythagtriplem4  16885  4sqlem18  17028  vdwapun  17040  mulgnnass  19181  odinv  19637  odadd2  19925  pgpfaclem2  20160  abvneg  20940  pzriprnglem6  21647  pzriprnglem12  21653  nrginvrcnlem  24859  nmoid  24910  blcvx  24966  icopnfcnv  25112  reparphti  25167  pcorevlem  25196  ncvsm1  25324  ncvspi  25326  cphipval2  25411  cphipval  25413  itg11  25861  itg2mulc  25917  itg2monolem1  25920  itgcnlem  25960  iblabs  25999  dvexp  26123  dvmptdiv  26144  dvef  26150  lhop1lem  26183  dvcvx  26190  dvfsumlem1  26196  dvfsumlem2  26197  dvfsumlem4  26199  dvfsum2  26204  plypow  26373  dgrcolem1  26441  plyn0mulidp  26453  vieta1lem2  26483  radcnvlem1  26587  radcnvlem2  26588  dvradcnv  26595  abelthlem6  26610  abelthlem7  26612  abelth2  26616  sinhalfpip  26668  sinhalfpim  26669  coshalfpip  26670  coshalfpim  26671  tangtx  26681  efif1olem4  26721  abslogle  26794  logdivlti  26796  advlog  26830  advlogexp  26831  logtayl  26836  cxpaddlelem  26927  cxpaddle  26928  affineequiv  26999  affineequiv2  27000  chordthmlem5  27012  dcubic2  27020  dcubic  27022  mcubic  27023  binom4  27026  dquartlem1  27027  quart1lem  27031  quart1  27032  quartlem1  27033  quart  27037  efiasin  27064  atantayl  27113  cvxcl  27160  scvxcvx  27161  lgamgulmlem5  27208  lgamcvg2  27230  lgam1  27239  wilthlem1  27243  wilthlem2  27244  basellem9  27264  fsumfldivdiaglem  27364  muinv  27368  chpub  27395  logexprlim  27400  mersenne  27402  perfectlem2  27405  dchrmullid  27427  dchrptlem1  27439  dchrsum2  27443  sumdchr2  27445  bposlem2  27460  bposlem9  27467  lgsval2lem  27482  lgsval4a  27494  lgsneg1  27497  lgsdir2lem4  27503  lgsdir  27507  lgsmulsqcoprm  27518  lgsdirnn0  27519  lgsdinn0  27520  gausslemma2dlem1a  27540  gausslemma2dlem4  27544  gausslemma2dlem7  27548  gausslemma2d  27549  lgseisenlem1  27550  lgseisenlem2  27551  lgseisenlem4  27553  lgsquad2lem1  27559  2sqlem8  27601  chebbnd1lem3  27646  chpchtlim  27654  rplogsumlem1  27659  rplogsumlem2  27660  rpvmasumlem  27662  dchrmusum2  27669  dchrvmasum2lem  27671  dchrvmasumlem2  27673  dchrvmasumlem3  27674  dchrisum0flblem1  27683  mulog2sumlem2  27710  vmalogdivsum2  27713  2vmadivsumlem  27715  log2sumbnd  27719  selberglem2  27721  selberg3lem1  27732  selberg4lem1  27735  pntrlog2bndlem2  27753  pntrlog2bndlem5  27756  pntpbnd1  27761  pntpbnd2  27762  pntibndlem2  27766  pntlemb  27772  pntlemr  27777  pntlemk  27781  pntlemo  27782  brbtwn2  29266  colinearalglem4  29270  ax5seglem3  29292  axbtwnid  29300  axpaschlem  29301  axeuclidlem  29323  axcontlem7  29331  axcontlem8  29332  elntg2  29346  nvm1  31028  nvpi  31030  nvmtri  31034  ipval2  31070  ipasslem1  31194  ipasslem4  31197  bcs2  31545  lnfnaddi  32406  nnmulge  33095  quad3d  33105  2exple2exp  33189  indsumin  33192  ccfldsrarelvec  34070  constrfin  34145  constrremulcl  34166  constrrecl  34168  constrimcl  34169  constrmulcl  34170  constrreinvcl  34171  2sqr3minply  34179  cos9thpiminplylem2  34182  sqsscirc1  34307  eulerpartlemgs2  34779  logdivsqrle  35046  subfacp1lem6  35685  subfaclim  35688  cvxpconn  35742  cvxsconn  35743  resconn  35746  sinccvglem  36172  fwddifn0  36664  nn0prpwlem  36861  knoppndvlem9  37137  knoppndvlem14  37142  bj-bary1lem1  37983  mblfinlem3  38338  itg2addnclem3  38352  iblabsnc  38363  iblmulc2nc  38364  ftc1anclem6  38377  ftc1anclem7  38378  ftc1anclem8  38379  areacirclem1  38387  bfplem2  38502  bfp  38503  rrntotbnd  38515  lcmineqlem1  42824  lcmineqlem12  42835  lcmineqlem18  42841  aks4d1p1p7  42869  aks4d1p8  42882  primrootscoprmpow  42894  posbezout  42895  aks6d1c2lem4  42922  3rdpwhole  43081  fltnlta  43423  3cubeslem2  43444  3cubeslem3r  43446  irrapxlem5  43581  pellexlem2  43585  pellexlem6  43589  pellfundex  43641  jm2.19lem3  43746  jm2.25  43754  jm2.27c  43762  jm3.1lem2  43773  flcidc  43925  reabssgn  44390  sqrtcval  44395  int-mul12d  44937  cvgdvgrat  45051  bccn1  45082  binomcxplemnotnn0  45094  fperiodmullem  46050  xralrple2  46098  fmul01lt1lem2  46329  mccllem  46341  reclimc  46395  cosknegpi  46611  dvsinax  46655  dvnxpaek  46684  dvnmul  46685  itgsinexp  46697  stoweidlem14  46756  stoweidlem26  46768  wallispilem4  46810  wallispilem5  46811  wallispi2lem1  46813  wallispi2  46815  stirlinglem1  46816  stirlinglem3  46818  stirlinglem4  46819  stirlinglem5  46820  stirlinglem6  46821  stirlinglem7  46822  stirlinglem10  46825  dirkertrigeqlem2  46841  dirkertrigeqlem3  46842  dirkercncflem2  46846  fourierdlem26  46875  fourierdlem41  46890  fourierdlem42  46891  fourierdlem56  46904  fourierdlem57  46905  fourierdlem58  46906  fourierdlem62  46910  fourierdlem64  46912  fourierdlem65  46913  fourierdlem95  46943  sqwvfoura  46970  sqwvfourb  46971  fouriersw  46973  etransclem23  46999  etransclem35  47011  etransclem46  47022  sin5tlem1  47638  sin5tlem2  47639  fmtnorec2lem  48322  fmtnorec3  48328  m1expoddALTV  48441  perfectALTVlem2  48515  ztprmneprm  49155  altgsumbc  49160  divge1b  49320  divgt1b  49321  ackval1  49489  affineid  49512  1subrec1sub  49513  rrx2vlinest  49549  line2x  49562