Theorem mullidd 11308

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182  1c1 11185   · cmul 11189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-mulcl 11246  ax-mulcom 11248  ax-mulass 11250  ax-distr 11251  ax-1rid 11254  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  adddirp1d  11316  addrid  11470  mulsubfacd  11751  mulcand  11923  receu  11935  divdivdiv  11995  divcan5  11996  subrec  12123  ltrec  12177  recp1lt1  12193  nndivtr  12340  subhalfhalf  12527  xp1d2m1eqxm1d2  12547  gtndiv  12720  lincmb01cmp  13555  iccf1o  13556  ltdifltdiv  13885  modfrac  13935  negmod  13967  addmodid  13970  m1expcl2  14136  expgt1  14151  ltexp2a  14216  leexp2a  14222  binom3  14273  faclbnd  14339  faclbnd4lem4  14345  facavg  14350  bcval5  14367  cshweqrep  14869  01sqrexlem2  15292  absimle  15358  reccn2  15643  iseraltlem2  15731  iseraltlem3  15732  o1fsum  15861  abscvgcvg  15867  ackbijnn  15876  binom1p  15879  binom1dif  15881  incexclem  15884  incexc  15885  climcndslem1  15897  pwdif  15916  geomulcvg  15924  fprodsplit  16014  fallrisefac  16073  bpolysum  16101  bpolydiflem  16102  bpoly4  16107  efcllem  16125  ef01bndlem  16232  efieq1re  16247  eirrlem  16252  iddvds  16318  pwp1fsum  16439  oddpwp1fsum  16440  bitsfzolem  16480  bitsfzo  16481  rpmulgcd  16604  prmind2  16732  isprm5  16754  phiprm  16824  eulerthlem2  16829  fermltl  16831  hashgcdlem  16835  odzdvds  16842  powm2modprm  16850  modprm0  16852  pythagtriplem4  16866  4sqlem18  17009  vdwapun  17021  mulgnnass  19149  odinv  19603  odadd2  19891  pgpfaclem2  20126  abvneg  20849  pzriprnglem6  21520  pzriprnglem12  21526  nrginvrcnlem  24733  nmoid  24784  blcvx  24839  icopnfcnv  24992  reparphti  25048  reparphtiOLD  25049  pcorevlem  25078  ncvsm1  25207  ncvspi  25209  cphipval2  25294  cphipval  25296  itg11  25745  itg2mulc  25802  itg2monolem1  25805  itgcnlem  25845  iblabs  25884  dvexp  26011  dvmptdiv  26032  dvef  26038  lhop1lem  26072  dvcvx  26079  dvfsumlem1  26086  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsumlem4  26090  dvfsum2  26095  plypow  26264  dgrcolem1  26333  vieta1lem2  26371  radcnvlem1  26474  radcnvlem2  26475  dvradcnv  26482  abelthlem6  26498  abelthlem7  26500  abelth2  26504  sinhalfpip  26552  sinhalfpim  26553  coshalfpip  26554  coshalfpim  26555  tangtx  26565  efif1olem4  26605  abslogle  26678  logdivlti  26680  advlog  26714  advlogexp  26715  logtayl  26720  cxpaddlelem  26812  cxpaddle  26813  affineequiv  26884  affineequiv2  26885  chordthmlem5  26897  dcubic2  26905  dcubic  26907  mcubic  26908  binom4  26911  dquartlem1  26912  quart1lem  26916  quart1  26917  quartlem1  26918  quart  26922  efiasin  26949  atantayl  26998  cvxcl  27046  scvxcvx  27047  lgamgulmlem5  27094  lgamcvg2  27116  lgam1  27125  wilthlem1  27129  wilthlem2  27130  basellem9  27150  fsumfldivdiaglem  27250  muinv  27254  chpub  27282  logexprlim  27287  mersenne  27289  perfectlem2  27292  dchrmullid  27314  dchrptlem1  27326  dchrsum2  27330  sumdchr2  27332  bposlem2  27347  bposlem9  27354  lgsval2lem  27369  lgsval4a  27381  lgsneg1  27384  lgsdir2lem4  27390  lgsdir  27394  lgsmulsqcoprm  27405  lgsdirnn0  27406  lgsdinn0  27407  gausslemma2dlem1a  27427  gausslemma2dlem4  27431  gausslemma2dlem7  27435  gausslemma2d  27436  lgseisenlem1  27437  lgseisenlem2  27438  lgseisenlem4  27440  lgsquad2lem1  27446  2sqlem8  27488  chebbnd1lem3  27533  chpchtlim  27541  rplogsumlem1  27546  rplogsumlem2  27547  rpvmasumlem  27549  dchrmusum2  27556  dchrvmasum2lem  27558  dchrvmasumlem2  27560  dchrvmasumlem3  27561  dchrisum0flblem1  27570  mulog2sumlem2  27597  vmalogdivsum2  27600  2vmadivsumlem  27602  log2sumbnd  27606  selberglem2  27608  selberg3lem1  27619  selberg4lem1  27622  pntrlog2bndlem2  27640  pntrlog2bndlem5  27643  pntpbnd1  27648  pntpbnd2  27649  pntibndlem2  27653  pntlemb  27659  pntlemr  27664  pntlemk  27668  pntlemo  27669  brbtwn2  28938  colinearalglem4  28942  ax5seglem3  28964  axbtwnid  28972  axpaschlem  28973  axeuclidlem  28995  axcontlem7  29003  axcontlem8  29004  elntg2  29018  nvm1  30697  nvpi  30699  nvmtri  30703  ipval2  30739  ipasslem1  30863  ipasslem4  30866  bcs2  31214  lnfnaddi  32075  nnmulge  32752  quad3d  32757  ccfldsrarelvec  33681  constrfin  33736  2sqr3minply  33738  sqsscirc1  33854  indsum  33985  indsumin  33986  eulerpartlemgs2  34345  plymulx0  34524  logdivsqrle  34627  subfacp1lem6  35153  subfaclim  35156  cvxpconn  35210  cvxsconn  35211  resconn  35214  sinccvglem  35640  fwddifn0  36128  nn0prpwlem  36288  knoppndvlem9  36486  knoppndvlem14  36491  bj-bary1lem1  37277  mblfinlem3  37619  itg2addnclem3  37633  iblabsnc  37644  iblmulc2nc  37645  ftc1anclem6  37658  ftc1anclem7  37659  ftc1anclem8  37660  areacirclem1  37668  bfplem2  37783  bfp  37784  rrntotbnd  37796  lcmineqlem1  41986  lcmineqlem12  41997  lcmineqlem18  42003  aks4d1p1p7  42031  aks4d1p8  42044  primrootscoprmpow  42056  posbezout  42057  aks6d1c2lem4  42084  fltnlta  42618  3cubeslem2  42641  3cubeslem3r  42643  irrapxlem5  42782  pellexlem2  42786  pellexlem6  42790  pellfundex  42842  jm2.19lem3  42948  jm2.25  42956  jm2.27c  42964  jm3.1lem2  42975  flcidc  43131  reabssgn  43598  sqrtcval  43603  int-mul12d  44145  cvgdvgrat  44282  bccn1  44313  binomcxplemnotnn0  44325  fperiodmullem  45218  xralrple2  45269  fmul01lt1lem2  45506  mccllem  45518  reclimc  45574  cosknegpi  45790  dvsinax  45834  dvnxpaek  45863  dvnmul  45864  itgsinexp  45876  stoweidlem14  45935  stoweidlem26  45947  wallispilem4  45989  wallispilem5  45990  wallispi2lem1  45992  wallispi2  45994  stirlinglem1  45995  stirlinglem3  45997  stirlinglem4  45998  stirlinglem5  45999  stirlinglem6  46000  stirlinglem7  46001  stirlinglem10  46004  dirkertrigeqlem2  46020  dirkertrigeqlem3  46021  dirkercncflem2  46025  fourierdlem26  46054  fourierdlem41  46069  fourierdlem42  46070  fourierdlem56  46083  fourierdlem57  46084  fourierdlem58  46085  fourierdlem62  46089  fourierdlem64  46091  fourierdlem65  46092  fourierdlem95  46122  sqwvfoura  46149  sqwvfourb  46150  fouriersw  46152  etransclem23  46178  etransclem35  46190  etransclem46  46201  fmtnorec2lem  47416  fmtnorec3  47422  m1expoddALTV  47522  perfectALTVlem2  47596  ztprmneprm  48072  altgsumbc  48077  divge1b  48241  divgt1b  48242  ackval1  48415  affineid  48438  1subrec1sub  48439  rrx2vlinest  48475  line2x  48488