Theorem mullidd 11254

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7416  ℂcc 11125  1c1 11128   · cmul 11132

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-mulcl 11189  ax-mulcom 11191  ax-mulass 11193  ax-distr 11194  ax-1rid 11197  ax-cnre 11200

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7419

This theorem is used by:  adddirp1d  11262  addrid  11417  mulsubfacd  11702  mulcand  11874  receu  11886  divdivdiv  11943  divcan5  11944  subrecd  12071  ltrec  12124  recp1lt1  12140  nndivtr  12310  subhalfhalf  12505  xp1d2m1eqxm1d2  12525  gtndiv  12701  ge2halflem1  13161  lincmb01cmp  13550  iccf1o  13551  ltdifltdiv  13897  modfrac  13947  negmod  13982  addmodid  13985  m1expcl2  14151  expgt1  14166  ltexp2a  14232  leexp2a  14238  binom3  14290  faclbnd  14356  faclbnd4lem4  14362  facavg  14367  bcval5  14384  cshweqrep  14894  01sqrexlem2  15332  absimle  15398  reccn2  15686  iseraltlem2  15772  iseraltlem3  15773  o1fsum  15902  abscvgcvg  15908  indsum  15917  ackbijnn  15919  binom1p  15922  binom1dif  15924  incexclem  15927  incexc  15928  climcndslem1  15940  pwdif  15959  geomulcvg  15967  fprodsplit  16057  fallrisefac  16116  bpolysum  16143  bpolydiflem  16144  bpoly4  16149  efcllem  16167  ef01bndlem  16276  efieq1re  16291  eirrlem  16296  iddvds  16363  pwp1fsum  16485  oddpwp1fsum  16486  bitsfzolem  16528  bitsfzo  16529  rpmulgcd  16651  prmind2  16779  isprm5  16802  phiprm  16872  eulerthlem2  16877  fermltl  16879  hashgcdlem  16883  odzdvds  16891  powm2modprm  16899  modprm0  16901  pythagtriplem4  16915  4sqlem18  17058  vdwapun  17070  mulgnnass  19233  odinv  19689  odadd2  19977  pgpfaclem2  20212  abvneg  20993  pzriprnglem6  21700  pzriprnglem12  21706  nrginvrcnlem  24918  nmoid  24969  blcvx  25025  icopnfcnv  25171  reparphti  25226  pcorevlem  25255  ncvsm1  25383  ncvspi  25385  cphipval2  25470  cphipval  25472  itg11  25920  itg2mulc  25976  itg2monolem1  25979  itgcnlem  26019  iblabs  26058  dvexp  26182  dvmptdiv  26203  dvef  26209  lhop1lem  26242  dvcvx  26249  dvfsumlem1  26255  dvfsumlem2  26256  dvfsumlem4  26258  dvfsum2  26263  plypow  26432  dgrcolem1  26500  plyn0mulidp  26512  vieta1lem2  26542  radcnvlem1  26646  radcnvlem2  26647  dvradcnv  26654  abelthlem6  26669  abelthlem7  26671  abelth2  26675  sinhalfpip  26727  sinhalfpim  26728  coshalfpip  26729  coshalfpim  26730  tangtx  26740  efif1olem4  26780  abslogle  26853  logdivlti  26855  advlog  26889  advlogexp  26890  logtayl  26895  cxpaddlelem  26986  cxpaddle  26987  affineequiv  27058  affineequiv2  27059  chordthmlem5  27071  dcubic2  27079  dcubic  27081  mcubic  27082  binom4  27085  dquartlem1  27086  quart1lem  27090  quart1  27091  quartlem1  27092  quart  27096  efiasin  27123  atantayl  27172  cvxcl  27219  scvxcvx  27220  lgamgulmlem5  27267  lgamcvg2  27289  lgam1  27298  wilthlem1  27302  wilthlem2  27303  basellem9  27323  fsumfldivdiaglem  27423  muinv  27427  chpub  27454  logexprlim  27459  mersenne  27461  perfectlem2  27464  dchrmullid  27486  dchrptlem1  27498  dchrsum2  27502  sumdchr2  27504  bposlem2  27519  bposlem9  27526  lgsval2lem  27541  lgsval4a  27553  lgsneg1  27556  lgsdir2lem4  27562  lgsdir  27566  lgsmulsqcoprm  27577  lgsdirnn0  27578  lgsdinn0  27579  gausslemma2dlem1a  27599  gausslemma2dlem4  27603  gausslemma2dlem7  27607  gausslemma2d  27608  lgseisenlem1  27609  lgseisenlem2  27610  lgseisenlem4  27612  lgsquad2lem1  27618  2sqlem8  27660  chebbnd1lem3  27705  chpchtlim  27713  rplogsumlem1  27718  rplogsumlem2  27719  rpvmasumlem  27721  dchrmusum2  27728  dchrvmasum2lem  27730  dchrvmasumlem2  27732  dchrvmasumlem3  27733  dchrisum0flblem1  27742  mulog2sumlem2  27769  vmalogdivsum2  27772  2vmadivsumlem  27774  log2sumbnd  27778  selberglem2  27780  selberg3lem1  27791  selberg4lem1  27794  pntrlog2bndlem2  27812  pntrlog2bndlem5  27815  pntpbnd1  27820  pntpbnd2  27821  pntibndlem2  27825  pntlemb  27831  pntlemr  27836  pntlemk  27840  pntlemo  27841  brbtwn2  29348  colinearalglem4  29352  ax5seglem3  29374  axbtwnid  29382  axpaschlem  29383  axeuclidlem  29405  axcontlem7  29413  axcontlem8  29414  elntg2  29428  nvm1  31132  nvpi  31134  nvmtri  31138  ipval2  31174  ipasslem1  31298  ipasslem4  31301  bcs2  31649  lnfnaddi  32510  nnmulge  33197  quad3d  33207  2exple2exp  33291  indsumin  33294  ccfldsrarelvec  34168  constrfin  34243  constrremulcl  34264  constrrecl  34266  constrimcl  34267  constrmulcl  34268  constrreinvcl  34269  2sqr3minply  34277  cos9thpiminplylem2  34280  sqsscirc1  34405  eulerpartlemgs2  34878  logdivsqrle  35145  subfacp1lem6  35751  subfaclim  35754  cvxpconn  35808  cvxsconn  35809  resconn  35812  sinccvglem  36238  fwddifn0  36731  nn0prpwlem  36928  knoppndvlem9  37204  knoppndvlem14  37209  bj-bary1lem1  38050  mblfinlem3  38395  itg2addnclem3  38409  iblabsnc  38420  iblmulc2nc  38421  ftc1anclem6  38434  ftc1anclem7  38435  ftc1anclem8  38436  areacirclem1  38444  bfplem2  38560  bfp  38561  rrntotbnd  38573  lcmineqlem1  42882  lcmineqlem12  42893  lcmineqlem18  42899  aks4d1p1p7  42927  aks4d1p8  42940  primrootscoprmpow  42952  posbezout  42953  aks6d1c2lem4  42980  3rdpwhole  43154  fltnlta  43496  3cubeslem2  43517  3cubeslem3r  43519  irrapxlem5  43654  pellexlem2  43658  pellexlem6  43662  pellfundex  43714  jm2.19lem3  43819  jm2.25  43827  jm2.27c  43835  jm3.1lem2  43846  flcidc  43998  reabssgn  44463  sqrtcval  44468  int-mul12d  45010  cvgdvgrat  45124  bccn1  45155  binomcxplemnotnn0  45167  fperiodmullem  46123  xralrple2  46171  fmul01lt1lem2  46402  mccllem  46414  reclimc  46468  cosknegpi  46684  dvsinax  46728  dvnxpaek  46757  dvnmul  46758  itgsinexp  46770  stoweidlem14  46829  stoweidlem26  46841  wallispilem4  46883  wallispilem5  46884  wallispi2lem1  46886  wallispi2  46888  stirlinglem1  46889  stirlinglem3  46891  stirlinglem4  46892  stirlinglem5  46893  stirlinglem6  46894  stirlinglem7  46895  stirlinglem10  46898  dirkertrigeqlem2  46914  dirkertrigeqlem3  46915  dirkercncflem2  46919  fourierdlem26  46948  fourierdlem41  46963  fourierdlem42  46964  fourierdlem56  46977  fourierdlem57  46978  fourierdlem58  46979  fourierdlem62  46983  fourierdlem64  46985  fourierdlem65  46986  fourierdlem95  47016  sqwvfoura  47043  sqwvfourb  47044  fouriersw  47046  etransclem23  47072  etransclem35  47084  etransclem46  47095  sin5tlem1  47724  sin5tlem2  47725  fmtnorec2lem  48432  fmtnorec3  48438  m1expoddALTV  48551  perfectALTVlem2  48625  ztprmneprm  49264  altgsumbc  49269  divge1b  49429  divgt1b  49430  ackval1  49598  affineid  49621  1subrec1sub  49622  rrx2vlinest  49658  line2x  49671  dvsec  50676  dvcsc  50677