Theorem mullidd 11155

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7361  ℂcc 11029  1c1 11032   · cmul 11036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11088  ax-1cn 11089  ax-icn 11090  ax-addcl 11091  ax-mulcl 11093  ax-mulcom 11095  ax-mulass 11097  ax-distr 11098  ax-1rid 11101  ax-cnre 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6449  df-fv 6501  df-ov 7364

This theorem is referenced by:  adddirp1d  11163  addrid  11318  mulsubfacd  11603  mulcand  11775  receu  11787  divdivdiv  11847  divcan5  11848  subrecd  11975  ltrec  12029  recp1lt1  12045  nndivtr  12197  subhalfhalf  12380  xp1d2m1eqxm1d2  12400  gtndiv  12574  ge2halflem1  13027  lincmb01cmp  13416  iccf1o  13417  ltdifltdiv  13759  modfrac  13809  negmod  13844  addmodid  13847  m1expcl2  14013  expgt1  14028  ltexp2a  14094  leexp2a  14100  binom3  14152  faclbnd  14218  faclbnd4lem4  14224  facavg  14229  bcval5  14246  cshweqrep  14749  01sqrexlem2  15171  absimle  15237  reccn2  15525  iseraltlem2  15611  iseraltlem3  15612  o1fsum  15741  abscvgcvg  15747  ackbijnn  15756  binom1p  15759  binom1dif  15761  incexclem  15764  incexc  15765  climcndslem1  15777  pwdif  15796  geomulcvg  15804  fprodsplit  15894  fallrisefac  15953  bpolysum  15981  bpolydiflem  15982  bpoly4  15987  efcllem  16005  ef01bndlem  16114  efieq1re  16129  eirrlem  16134  iddvds  16201  pwp1fsum  16323  oddpwp1fsum  16324  bitsfzolem  16366  bitsfzo  16367  rpmulgcd  16489  prmind2  16617  isprm5  16639  phiprm  16709  eulerthlem2  16714  fermltl  16716  hashgcdlem  16720  odzdvds  16728  powm2modprm  16736  modprm0  16738  pythagtriplem4  16752  4sqlem18  16895  vdwapun  16907  mulgnnass  19044  odinv  19495  odadd2  19783  pgpfaclem2  20018  abvneg  20764  pzriprnglem6  21446  pzriprnglem12  21452  nrginvrcnlem  24640  nmoid  24691  blcvx  24747  icopnfcnv  24901  reparphti  24957  reparphtiOLD  24958  pcorevlem  24987  ncvsm1  25115  ncvspi  25117  cphipval2  25202  cphipval  25204  itg11  25653  itg2mulc  25709  itg2monolem1  25712  itgcnlem  25752  iblabs  25791  dvexp  25918  dvmptdiv  25939  dvef  25945  lhop1lem  25979  dvcvx  25986  dvfsumlem1  25993  dvfsumlem2  25994  dvfsumlem2OLD  25995  dvfsumlem4  25997  dvfsum2  26002  plypow  26171  dgrcolem1  26240  vieta1lem2  26280  radcnvlem1  26383  radcnvlem2  26384  dvradcnv  26391  abelthlem6  26407  abelthlem7  26409  abelth2  26413  sinhalfpip  26462  sinhalfpim  26463  coshalfpip  26464  coshalfpim  26465  tangtx  26475  efif1olem4  26515  abslogle  26588  logdivlti  26590  advlog  26624  advlogexp  26625  logtayl  26630  cxpaddlelem  26722  cxpaddle  26723  affineequiv  26794  affineequiv2  26795  chordthmlem5  26807  dcubic2  26815  dcubic  26817  mcubic  26818  binom4  26821  dquartlem1  26822  quart1lem  26826  quart1  26827  quartlem1  26828  quart  26832  efiasin  26859  atantayl  26908  cvxcl  26956  scvxcvx  26957  lgamgulmlem5  27004  lgamcvg2  27026  lgam1  27035  wilthlem1  27039  wilthlem2  27040  basellem9  27060  fsumfldivdiaglem  27160  muinv  27164  chpub  27192  logexprlim  27197  mersenne  27199  perfectlem2  27202  dchrmullid  27224  dchrptlem1  27236  dchrsum2  27240  sumdchr2  27242  bposlem2  27257  bposlem9  27264  lgsval2lem  27279  lgsval4a  27291  lgsneg1  27294  lgsdir2lem4  27300  lgsdir  27304  lgsmulsqcoprm  27315  lgsdirnn0  27316  lgsdinn0  27317  gausslemma2dlem1a  27337  gausslemma2dlem4  27341  gausslemma2dlem7  27345  gausslemma2d  27346  lgseisenlem1  27347  lgseisenlem2  27348  lgseisenlem4  27350  lgsquad2lem1  27356  2sqlem8  27398  chebbnd1lem3  27443  chpchtlim  27451  rplogsumlem1  27456  rplogsumlem2  27457  rpvmasumlem  27459  dchrmusum2  27466  dchrvmasum2lem  27468  dchrvmasumlem2  27470  dchrvmasumlem3  27471  dchrisum0flblem1  27480  mulog2sumlem2  27507  vmalogdivsum2  27510  2vmadivsumlem  27512  log2sumbnd  27516  selberglem2  27518  selberg3lem1  27529  selberg4lem1  27532  pntrlog2bndlem2  27550  pntrlog2bndlem5  27553  pntpbnd1  27558  pntpbnd2  27559  pntibndlem2  27563  pntlemb  27569  pntlemr  27574  pntlemk  27578  pntlemo  27579  brbtwn2  28983  colinearalglem4  28987  ax5seglem3  29009  axbtwnid  29017  axpaschlem  29018  axeuclidlem  29040  axcontlem7  29048  axcontlem8  29049  elntg2  29063  nvm1  30745  nvpi  30747  nvmtri  30751  ipval2  30787  ipasslem1  30911  ipasslem4  30914  bcs2  31262  lnfnaddi  32123  nnmulge  32821  quad3d  32832  2exple2exp  32929  indsum  32945  indsumin  32946  ccfldsrarelvec  33841  constrfin  33916  constrremulcl  33937  constrrecl  33939  constrimcl  33940  constrmulcl  33941  constrreinvcl  33942  2sqr3minply  33950  cos9thpiminplylem2  33953  sqsscirc1  34078  eulerpartlemgs2  34550  plymulx0  34717  logdivsqrle  34820  subfacp1lem6  35392  subfaclim  35395  cvxpconn  35449  cvxsconn  35450  resconn  35453  sinccvglem  35879  fwddifn0  36371  nn0prpwlem  36529  knoppndvlem9  36733  knoppndvlem14  36738  bj-bary1lem1  37529  mblfinlem3  37873  itg2addnclem3  37887  iblabsnc  37898  iblmulc2nc  37899  ftc1anclem6  37912  ftc1anclem7  37913  ftc1anclem8  37914  areacirclem1  37922  bfplem2  38037  bfp  38038  rrntotbnd  38050  lcmineqlem1  42362  lcmineqlem12  42373  lcmineqlem18  42379  aks4d1p1p7  42407  aks4d1p8  42420  primrootscoprmpow  42432  posbezout  42433  aks6d1c2lem4  42460  3rdpwhole  42625  fltnlta  42984  3cubeslem2  43005  3cubeslem3r  43007  irrapxlem5  43146  pellexlem2  43150  pellexlem6  43154  pellfundex  43206  jm2.19lem3  43311  jm2.25  43319  jm2.27c  43327  jm3.1lem2  43338  flcidc  43490  reabssgn  43955  sqrtcval  43960  int-mul12d  44502  cvgdvgrat  44632  bccn1  44663  binomcxplemnotnn0  44675  fperiodmullem  45628  xralrple2  45676  fmul01lt1lem2  45908  mccllem  45920  reclimc  45974  cosknegpi  46190  dvsinax  46234  dvnxpaek  46263  dvnmul  46264  itgsinexp  46276  stoweidlem14  46335  stoweidlem26  46347  wallispilem4  46389  wallispilem5  46390  wallispi2lem1  46392  wallispi2  46394  stirlinglem1  46395  stirlinglem3  46397  stirlinglem4  46398  stirlinglem5  46399  stirlinglem6  46400  stirlinglem7  46401  stirlinglem10  46404  dirkertrigeqlem2  46420  dirkertrigeqlem3  46421  dirkercncflem2  46425  fourierdlem26  46454  fourierdlem41  46469  fourierdlem42  46470  fourierdlem56  46483  fourierdlem57  46484  fourierdlem58  46485  fourierdlem62  46489  fourierdlem64  46491  fourierdlem65  46492  fourierdlem95  46522  sqwvfoura  46549  sqwvfourb  46550  fouriersw  46552  etransclem23  46578  etransclem35  46590  etransclem46  46601  fmtnorec2lem  47865  fmtnorec3  47871  m1expoddALTV  47971  perfectALTVlem2  48045  ztprmneprm  48670  altgsumbc  48675  divge1b  48835  divgt1b  48836  ackval1  49004  affineid  49027  1subrec1sub  49028  rrx2vlinest  49064  line2x  49077