Theorem mullidd 11192

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066  1c1 11069   · cmul 11073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-mulcl 11130  ax-mulcom 11132  ax-mulass 11134  ax-distr 11135  ax-1rid 11138  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  adddirp1d  11200  addrid  11354  mulsubfacd  11639  mulcand  11811  receu  11823  divdivdiv  11883  divcan5  11884  subrecd  12011  ltrec  12065  recp1lt1  12081  nndivtr  12233  subhalfhalf  12416  xp1d2m1eqxm1d2  12436  gtndiv  12611  ge2halflem1  13068  lincmb01cmp  13456  iccf1o  13457  ltdifltdiv  13796  modfrac  13846  negmod  13881  addmodid  13884  m1expcl2  14050  expgt1  14065  ltexp2a  14131  leexp2a  14137  binom3  14189  faclbnd  14255  faclbnd4lem4  14261  facavg  14266  bcval5  14283  cshweqrep  14786  01sqrexlem2  15209  absimle  15275  reccn2  15563  iseraltlem2  15649  iseraltlem3  15650  o1fsum  15779  abscvgcvg  15785  ackbijnn  15794  binom1p  15797  binom1dif  15799  incexclem  15802  incexc  15803  climcndslem1  15815  pwdif  15834  geomulcvg  15842  fprodsplit  15932  fallrisefac  15991  bpolysum  16019  bpolydiflem  16020  bpoly4  16025  efcllem  16043  ef01bndlem  16152  efieq1re  16167  eirrlem  16172  iddvds  16239  pwp1fsum  16361  oddpwp1fsum  16362  bitsfzolem  16404  bitsfzo  16405  rpmulgcd  16527  prmind2  16655  isprm5  16677  phiprm  16747  eulerthlem2  16752  fermltl  16754  hashgcdlem  16758  odzdvds  16766  powm2modprm  16774  modprm0  16776  pythagtriplem4  16790  4sqlem18  16933  vdwapun  16945  mulgnnass  19041  odinv  19491  odadd2  19779  pgpfaclem2  20014  abvneg  20735  pzriprnglem6  21396  pzriprnglem12  21402  nrginvrcnlem  24579  nmoid  24630  blcvx  24686  icopnfcnv  24840  reparphti  24896  reparphtiOLD  24897  pcorevlem  24926  ncvsm1  25054  ncvspi  25056  cphipval2  25141  cphipval  25143  itg11  25592  itg2mulc  25648  itg2monolem1  25651  itgcnlem  25691  iblabs  25730  dvexp  25857  dvmptdiv  25878  dvef  25884  lhop1lem  25918  dvcvx  25925  dvfsumlem1  25932  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumlem4  25936  dvfsum2  25941  plypow  26110  dgrcolem1  26179  vieta1lem2  26219  radcnvlem1  26322  radcnvlem2  26323  dvradcnv  26330  abelthlem6  26346  abelthlem7  26348  abelth2  26352  sinhalfpip  26401  sinhalfpim  26402  coshalfpip  26403  coshalfpim  26404  tangtx  26414  efif1olem4  26454  abslogle  26527  logdivlti  26529  advlog  26563  advlogexp  26564  logtayl  26569  cxpaddlelem  26661  cxpaddle  26662  affineequiv  26733  affineequiv2  26734  chordthmlem5  26746  dcubic2  26754  dcubic  26756  mcubic  26757  binom4  26760  dquartlem1  26761  quart1lem  26765  quart1  26766  quartlem1  26767  quart  26771  efiasin  26798  atantayl  26847  cvxcl  26895  scvxcvx  26896  lgamgulmlem5  26943  lgamcvg2  26965  lgam1  26974  wilthlem1  26978  wilthlem2  26979  basellem9  26999  fsumfldivdiaglem  27099  muinv  27103  chpub  27131  logexprlim  27136  mersenne  27138  perfectlem2  27141  dchrmullid  27163  dchrptlem1  27175  dchrsum2  27179  sumdchr2  27181  bposlem2  27196  bposlem9  27203  lgsval2lem  27218  lgsval4a  27230  lgsneg1  27233  lgsdir2lem4  27239  lgsdir  27243  lgsmulsqcoprm  27254  lgsdirnn0  27255  lgsdinn0  27256  gausslemma2dlem1a  27276  gausslemma2dlem4  27280  gausslemma2dlem7  27284  gausslemma2d  27285  lgseisenlem1  27286  lgseisenlem2  27287  lgseisenlem4  27289  lgsquad2lem1  27295  2sqlem8  27337  chebbnd1lem3  27382  chpchtlim  27390  rplogsumlem1  27395  rplogsumlem2  27396  rpvmasumlem  27398  dchrmusum2  27405  dchrvmasum2lem  27407  dchrvmasumlem2  27409  dchrvmasumlem3  27410  dchrisum0flblem1  27419  mulog2sumlem2  27446  vmalogdivsum2  27449  2vmadivsumlem  27451  log2sumbnd  27455  selberglem2  27457  selberg3lem1  27468  selberg4lem1  27471  pntrlog2bndlem2  27489  pntrlog2bndlem5  27492  pntpbnd1  27497  pntpbnd2  27498  pntibndlem2  27502  pntlemb  27508  pntlemr  27513  pntlemk  27517  pntlemo  27518  brbtwn2  28832  colinearalglem4  28836  ax5seglem3  28858  axbtwnid  28866  axpaschlem  28867  axeuclidlem  28889  axcontlem7  28897  axcontlem8  28898  elntg2  28912  nvm1  30594  nvpi  30596  nvmtri  30600  ipval2  30636  ipasslem1  30760  ipasslem4  30763  bcs2  31111  lnfnaddi  31972  nnmulge  32662  quad3d  32673  2exple2exp  32770  indsum  32784  indsumin  32785  ccfldsrarelvec  33666  constrfin  33736  constrremulcl  33757  constrrecl  33759  constrimcl  33760  constrmulcl  33761  constrreinvcl  33762  2sqr3minply  33770  cos9thpiminplylem2  33773  sqsscirc1  33898  eulerpartlemgs2  34371  plymulx0  34538  logdivsqrle  34641  subfacp1lem6  35172  subfaclim  35175  cvxpconn  35229  cvxsconn  35230  resconn  35233  sinccvglem  35659  fwddifn0  36152  nn0prpwlem  36310  knoppndvlem9  36508  knoppndvlem14  36513  bj-bary1lem1  37299  mblfinlem3  37653  itg2addnclem3  37667  iblabsnc  37678  iblmulc2nc  37679  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anclem8  37694  areacirclem1  37702  bfplem2  37817  bfp  37818  rrntotbnd  37830  lcmineqlem1  42017  lcmineqlem12  42028  lcmineqlem18  42034  aks4d1p1p7  42062  aks4d1p8  42075  primrootscoprmpow  42087  posbezout  42088  aks6d1c2lem4  42115  3rdpwhole  42280  fltnlta  42651  3cubeslem2  42673  3cubeslem3r  42675  irrapxlem5  42814  pellexlem2  42818  pellexlem6  42822  pellfundex  42874  jm2.19lem3  42980  jm2.25  42988  jm2.27c  42996  jm3.1lem2  43007  flcidc  43159  reabssgn  43625  sqrtcval  43630  int-mul12d  44172  cvgdvgrat  44302  bccn1  44333  binomcxplemnotnn0  44345  fperiodmullem  45301  xralrple2  45350  fmul01lt1lem2  45583  mccllem  45595  reclimc  45651  cosknegpi  45867  dvsinax  45911  dvnxpaek  45940  dvnmul  45941  itgsinexp  45953  stoweidlem14  46012  stoweidlem26  46024  wallispilem4  46066  wallispilem5  46067  wallispi2lem1  46069  wallispi2  46071  stirlinglem1  46072  stirlinglem3  46074  stirlinglem4  46075  stirlinglem5  46076  stirlinglem6  46077  stirlinglem7  46078  stirlinglem10  46081  dirkertrigeqlem2  46097  dirkertrigeqlem3  46098  dirkercncflem2  46102  fourierdlem26  46131  fourierdlem41  46146  fourierdlem42  46147  fourierdlem56  46160  fourierdlem57  46161  fourierdlem58  46162  fourierdlem62  46166  fourierdlem64  46168  fourierdlem65  46169  fourierdlem95  46199  sqwvfoura  46226  sqwvfourb  46227  fouriersw  46229  etransclem23  46255  etransclem35  46267  etransclem46  46278  fmtnorec2lem  47543  fmtnorec3  47549  m1expoddALTV  47649  perfectALTVlem2  47723  ztprmneprm  48335  altgsumbc  48340  divge1b  48501  divgt1b  48502  ackval1  48670  affineid  48693  1subrec1sub  48694  rrx2vlinest  48730  line2x  48743