Theorem mullidd 11186

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

Syntax hints:   → wi 4   = wceq 1550   ∈ wcel 2132  (class class class)co 7381  ℂcc 11057  1c1 11060   · cmul 11064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-mulcl 11121  ax-mulcom 11123  ax-mulass 11125  ax-distr 11126  ax-1rid 11129  ax-cnre 11132

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-rex 3077  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-iota 6462  df-fv 6514  df-ov 7384

This theorem is referenced by:  adddirp1d  11194  addrid  11349  mulsubfacd  11634  mulcand  11806  receu  11818  divdivdiv  11878  divcan5  11879  subrecd  12006  ltrec  12060  recp1lt1  12076  nndivtr  12246  subhalfhalf  12441  xp1d2m1eqxm1d2  12461  gtndiv  12636  ge2halflem1  13096  lincmb01cmp  13485  iccf1o  13486  ltdifltdiv  13830  modfrac  13880  negmod  13915  addmodid  13918  m1expcl2  14084  expgt1  14099  ltexp2a  14165  leexp2a  14171  binom3  14223  faclbnd  14289  faclbnd4lem4  14295  facavg  14300  bcval5  14317  cshweqrep  14820  01sqrexlem2  15242  absimle  15308  reccn2  15596  iseraltlem2  15682  iseraltlem3  15683  o1fsum  15813  abscvgcvg  15819  indsum  15828  ackbijnn  15830  binom1p  15833  binom1dif  15835  incexclem  15838  incexc  15839  climcndslem1  15851  pwdif  15870  geomulcvg  15878  fprodsplit  15968  fallrisefac  16027  bpolysum  16055  bpolydiflem  16056  bpoly4  16061  efcllem  16079  ef01bndlem  16188  efieq1re  16203  eirrlem  16208  iddvds  16275  pwp1fsum  16397  oddpwp1fsum  16398  bitsfzolem  16440  bitsfzo  16441  rpmulgcd  16563  prmind2  16691  isprm5  16714  phiprm  16784  eulerthlem2  16789  fermltl  16791  hashgcdlem  16795  odzdvds  16803  powm2modprm  16811  modprm0  16813  pythagtriplem4  16827  4sqlem18  16970  vdwapun  16982  mulgnnass  19123  odinv  19573  odadd2  19861  pgpfaclem2  20096  abvneg  20844  pzriprnglem6  21507  pzriprnglem12  21513  nrginvrcnlem  24720  nmoid  24771  blcvx  24827  icopnfcnv  24973  reparphti  25028  pcorevlem  25057  ncvsm1  25185  ncvspi  25187  cphipval2  25272  cphipval  25274  itg11  25722  itg2mulc  25778  itg2monolem1  25781  itgcnlem  25821  iblabs  25860  dvexp  25984  dvmptdiv  26005  dvef  26011  lhop1lem  26044  dvcvx  26051  dvfsumlem1  26057  dvfsumlem2  26058  dvfsumlem4  26060  dvfsum2  26065  plypow  26234  dgrcolem1  26302  vieta1lem2  26341  radcnvlem1  26442  radcnvlem2  26443  dvradcnv  26450  abelthlem6  26465  abelthlem7  26467  abelth2  26471  sinhalfpip  26523  sinhalfpim  26524  coshalfpip  26525  coshalfpim  26526  tangtx  26536  efif1olem4  26576  abslogle  26649  logdivlti  26651  advlog  26685  advlogexp  26686  logtayl  26691  cxpaddlelem  26782  cxpaddle  26783  affineequiv  26854  affineequiv2  26855  chordthmlem5  26867  dcubic2  26875  dcubic  26877  mcubic  26878  binom4  26881  dquartlem1  26882  quart1lem  26886  quart1  26887  quartlem1  26888  quart  26892  efiasin  26919  atantayl  26968  cvxcl  27015  scvxcvx  27016  lgamgulmlem5  27063  lgamcvg2  27085  lgam1  27094  wilthlem1  27098  wilthlem2  27099  basellem9  27119  fsumfldivdiaglem  27219  muinv  27223  chpub  27250  logexprlim  27255  mersenne  27257  perfectlem2  27260  dchrmullid  27282  dchrptlem1  27294  dchrsum2  27298  sumdchr2  27300  bposlem2  27315  bposlem9  27322  lgsval2lem  27337  lgsval4a  27349  lgsneg1  27352  lgsdir2lem4  27358  lgsdir  27362  lgsmulsqcoprm  27373  lgsdirnn0  27374  lgsdinn0  27375  gausslemma2dlem1a  27395  gausslemma2dlem4  27399  gausslemma2dlem7  27403  gausslemma2d  27404  lgseisenlem1  27405  lgseisenlem2  27406  lgseisenlem4  27408  lgsquad2lem1  27414  2sqlem8  27456  chebbnd1lem3  27501  chpchtlim  27509  rplogsumlem1  27514  rplogsumlem2  27515  rpvmasumlem  27517  dchrmusum2  27524  dchrvmasum2lem  27526  dchrvmasumlem2  27528  dchrvmasumlem3  27529  dchrisum0flblem1  27538  mulog2sumlem2  27565  vmalogdivsum2  27568  2vmadivsumlem  27570  log2sumbnd  27574  selberglem2  27576  selberg3lem1  27587  selberg4lem1  27590  pntrlog2bndlem2  27608  pntrlog2bndlem5  27611  pntpbnd1  27616  pntpbnd2  27617  pntibndlem2  27621  pntlemb  27627  pntlemr  27632  pntlemk  27636  pntlemo  27637  brbtwn2  29041  colinearalglem4  29045  ax5seglem3  29067  axbtwnid  29075  axpaschlem  29076  axeuclidlem  29098  axcontlem7  29106  axcontlem8  29107  elntg2  29121  nvm1  30803  nvpi  30805  nvmtri  30809  ipval2  30845  ipasslem1  30969  ipasslem4  30972  bcs2  31320  lnfnaddi  32181  nnmulge  32880  quad3d  32890  2exple2exp  32986  indsumin  32989  ccfldsrarelvec  33912  constrfin  33987  constrremulcl  34008  constrrecl  34010  constrimcl  34011  constrmulcl  34012  constrreinvcl  34013  2sqr3minply  34021  cos9thpiminplylem2  34024  sqsscirc1  34149  eulerpartlemgs2  34621  plymulx0  34788  logdivsqrle  34891  subfacp1lem6  35473  subfaclim  35476  cvxpconn  35530  cvxsconn  35531  resconn  35534  sinccvglem  35960  fwddifn0  36452  nn0prpwlem  36620  knoppndvlem9  36896  knoppndvlem14  36901  bj-bary1lem1  37741  mblfinlem3  38096  itg2addnclem3  38110  iblabsnc  38121  iblmulc2nc  38122  ftc1anclem6  38135  ftc1anclem7  38136  ftc1anclem8  38137  areacirclem1  38145  bfplem2  38260  bfp  38261  rrntotbnd  38273  lcmineqlem1  42584  lcmineqlem12  42595  lcmineqlem18  42601  aks4d1p1p7  42629  aks4d1p8  42642  primrootscoprmpow  42654  posbezout  42655  aks6d1c2lem4  42682  3rdpwhole  42839  fltnlta  43183  3cubeslem2  43204  3cubeslem3r  43206  irrapxlem5  43341  pellexlem2  43345  pellexlem6  43349  pellfundex  43401  jm2.19lem3  43506  jm2.25  43514  jm2.27c  43522  jm3.1lem2  43533  flcidc  43685  reabssgn  44150  sqrtcval  44155  int-mul12d  44697  cvgdvgrat  44827  bccn1  44858  binomcxplemnotnn0  44870  fperiodmullem  45820  xralrple2  45868  fmul01lt1lem2  46099  mccllem  46111  reclimc  46165  cosknegpi  46381  dvsinax  46425  dvnxpaek  46454  dvnmul  46455  itgsinexp  46467  stoweidlem14  46526  stoweidlem26  46538  wallispilem4  46580  wallispilem5  46581  wallispi2lem1  46583  wallispi2  46585  stirlinglem1  46586  stirlinglem3  46588  stirlinglem4  46589  stirlinglem5  46590  stirlinglem6  46591  stirlinglem7  46592  stirlinglem10  46595  dirkertrigeqlem2  46611  dirkertrigeqlem3  46612  dirkercncflem2  46616  fourierdlem26  46645  fourierdlem41  46660  fourierdlem42  46661  fourierdlem56  46674  fourierdlem57  46675  fourierdlem58  46676  fourierdlem62  46680  fourierdlem64  46682  fourierdlem65  46683  fourierdlem95  46713  sqwvfoura  46740  sqwvfourb  46741  fouriersw  46743  etransclem23  46769  etransclem35  46781  etransclem46  46792  sin5tlem1  47405  sin5tlem2  47406  fmtnorec2lem  48089  fmtnorec3  48095  m1expoddALTV  48208  perfectALTVlem2  48282  ztprmneprm  48907  altgsumbc  48912  divge1b  49072  divgt1b  49073  ackval1  49241  affineid  49264  1subrec1sub  49265  rrx2vlinest  49301  line2x  49314