Theorem mullidd 11152

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026  1c1 11029   · cmul 11033

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 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-mulcl 11090  ax-mulcom 11092  ax-mulass 11094  ax-distr 11095  ax-1rid 11098  ax-cnre 11101

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356

This theorem is referenced by:  adddirp1d  11160  addrid  11314  mulsubfacd  11599  mulcand  11771  receu  11783  divdivdiv  11843  divcan5  11844  subrecd  11971  ltrec  12025  recp1lt1  12041  nndivtr  12193  subhalfhalf  12376  xp1d2m1eqxm1d2  12396  gtndiv  12571  ge2halflem1  13028  lincmb01cmp  13416  iccf1o  13417  ltdifltdiv  13756  modfrac  13806  negmod  13841  addmodid  13844  m1expcl2  14010  expgt1  14025  ltexp2a  14091  leexp2a  14097  binom3  14149  faclbnd  14215  faclbnd4lem4  14221  facavg  14226  bcval5  14243  cshweqrep  14745  01sqrexlem2  15168  absimle  15234  reccn2  15522  iseraltlem2  15608  iseraltlem3  15609  o1fsum  15738  abscvgcvg  15744  ackbijnn  15753  binom1p  15756  binom1dif  15758  incexclem  15761  incexc  15762  climcndslem1  15774  pwdif  15793  geomulcvg  15801  fprodsplit  15891  fallrisefac  15950  bpolysum  15978  bpolydiflem  15979  bpoly4  15984  efcllem  16002  ef01bndlem  16111  efieq1re  16126  eirrlem  16131  iddvds  16198  pwp1fsum  16320  oddpwp1fsum  16321  bitsfzolem  16363  bitsfzo  16364  rpmulgcd  16486  prmind2  16614  isprm5  16636  phiprm  16706  eulerthlem2  16711  fermltl  16713  hashgcdlem  16717  odzdvds  16725  powm2modprm  16733  modprm0  16735  pythagtriplem4  16749  4sqlem18  16892  vdwapun  16904  mulgnnass  19006  odinv  19458  odadd2  19746  pgpfaclem2  19981  abvneg  20729  pzriprnglem6  21411  pzriprnglem12  21417  nrginvrcnlem  24595  nmoid  24646  blcvx  24702  icopnfcnv  24856  reparphti  24912  reparphtiOLD  24913  pcorevlem  24942  ncvsm1  25070  ncvspi  25072  cphipval2  25157  cphipval  25159  itg11  25608  itg2mulc  25664  itg2monolem1  25667  itgcnlem  25707  iblabs  25746  dvexp  25873  dvmptdiv  25894  dvef  25900  lhop1lem  25934  dvcvx  25941  dvfsumlem1  25948  dvfsumlem2  25949  dvfsumlem2OLD  25950  dvfsumlem4  25952  dvfsum2  25957  plypow  26126  dgrcolem1  26195  vieta1lem2  26235  radcnvlem1  26338  radcnvlem2  26339  dvradcnv  26346  abelthlem6  26362  abelthlem7  26364  abelth2  26368  sinhalfpip  26417  sinhalfpim  26418  coshalfpip  26419  coshalfpim  26420  tangtx  26430  efif1olem4  26470  abslogle  26543  logdivlti  26545  advlog  26579  advlogexp  26580  logtayl  26585  cxpaddlelem  26677  cxpaddle  26678  affineequiv  26749  affineequiv2  26750  chordthmlem5  26762  dcubic2  26770  dcubic  26772  mcubic  26773  binom4  26776  dquartlem1  26777  quart1lem  26781  quart1  26782  quartlem1  26783  quart  26787  efiasin  26814  atantayl  26863  cvxcl  26911  scvxcvx  26912  lgamgulmlem5  26959  lgamcvg2  26981  lgam1  26990  wilthlem1  26994  wilthlem2  26995  basellem9  27015  fsumfldivdiaglem  27115  muinv  27119  chpub  27147  logexprlim  27152  mersenne  27154  perfectlem2  27157  dchrmullid  27179  dchrptlem1  27191  dchrsum2  27195  sumdchr2  27197  bposlem2  27212  bposlem9  27219  lgsval2lem  27234  lgsval4a  27246  lgsneg1  27249  lgsdir2lem4  27255  lgsdir  27259  lgsmulsqcoprm  27270  lgsdirnn0  27271  lgsdinn0  27272  gausslemma2dlem1a  27292  gausslemma2dlem4  27296  gausslemma2dlem7  27300  gausslemma2d  27301  lgseisenlem1  27302  lgseisenlem2  27303  lgseisenlem4  27305  lgsquad2lem1  27311  2sqlem8  27353  chebbnd1lem3  27398  chpchtlim  27406  rplogsumlem1  27411  rplogsumlem2  27412  rpvmasumlem  27414  dchrmusum2  27421  dchrvmasum2lem  27423  dchrvmasumlem2  27425  dchrvmasumlem3  27426  dchrisum0flblem1  27435  mulog2sumlem2  27462  vmalogdivsum2  27465  2vmadivsumlem  27467  log2sumbnd  27471  selberglem2  27473  selberg3lem1  27484  selberg4lem1  27487  pntrlog2bndlem2  27505  pntrlog2bndlem5  27508  pntpbnd1  27513  pntpbnd2  27514  pntibndlem2  27518  pntlemb  27524  pntlemr  27529  pntlemk  27533  pntlemo  27534  brbtwn2  28868  colinearalglem4  28872  ax5seglem3  28894  axbtwnid  28902  axpaschlem  28903  axeuclidlem  28925  axcontlem7  28933  axcontlem8  28934  elntg2  28948  nvm1  30627  nvpi  30629  nvmtri  30633  ipval2  30669  ipasslem1  30793  ipasslem4  30796  bcs2  31144  lnfnaddi  32005  nnmulge  32695  quad3d  32706  2exple2exp  32803  indsum  32817  indsumin  32818  ccfldsrarelvec  33642  constrfin  33712  constrremulcl  33733  constrrecl  33735  constrimcl  33736  constrmulcl  33737  constrreinvcl  33738  2sqr3minply  33746  cos9thpiminplylem2  33749  sqsscirc1  33874  eulerpartlemgs2  34347  plymulx0  34514  logdivsqrle  34617  subfacp1lem6  35157  subfaclim  35160  cvxpconn  35214  cvxsconn  35215  resconn  35218  sinccvglem  35644  fwddifn0  36137  nn0prpwlem  36295  knoppndvlem9  36493  knoppndvlem14  36498  bj-bary1lem1  37284  mblfinlem3  37638  itg2addnclem3  37652  iblabsnc  37663  iblmulc2nc  37664  ftc1anclem6  37677  ftc1anclem7  37678  ftc1anclem8  37679  areacirclem1  37687  bfplem2  37802  bfp  37803  rrntotbnd  37815  lcmineqlem1  42002  lcmineqlem12  42013  lcmineqlem18  42019  aks4d1p1p7  42047  aks4d1p8  42060  primrootscoprmpow  42072  posbezout  42073  aks6d1c2lem4  42100  3rdpwhole  42265  fltnlta  42636  3cubeslem2  42658  3cubeslem3r  42660  irrapxlem5  42799  pellexlem2  42803  pellexlem6  42807  pellfundex  42859  jm2.19lem3  42964  jm2.25  42972  jm2.27c  42980  jm3.1lem2  42991  flcidc  43143  reabssgn  43609  sqrtcval  43614  int-mul12d  44156  cvgdvgrat  44286  bccn1  44317  binomcxplemnotnn0  44329  fperiodmullem  45285  xralrple2  45334  fmul01lt1lem2  45567  mccllem  45579  reclimc  45635  cosknegpi  45851  dvsinax  45895  dvnxpaek  45924  dvnmul  45925  itgsinexp  45937  stoweidlem14  45996  stoweidlem26  46008  wallispilem4  46050  wallispilem5  46051  wallispi2lem1  46053  wallispi2  46055  stirlinglem1  46056  stirlinglem3  46058  stirlinglem4  46059  stirlinglem5  46060  stirlinglem6  46061  stirlinglem7  46062  stirlinglem10  46065  dirkertrigeqlem2  46081  dirkertrigeqlem3  46082  dirkercncflem2  46086  fourierdlem26  46115  fourierdlem41  46130  fourierdlem42  46131  fourierdlem56  46144  fourierdlem57  46145  fourierdlem58  46146  fourierdlem62  46150  fourierdlem64  46152  fourierdlem65  46153  fourierdlem95  46183  sqwvfoura  46210  sqwvfourb  46211  fouriersw  46213  etransclem23  46239  etransclem35  46251  etransclem46  46262  fmtnorec2lem  47527  fmtnorec3  47533  m1expoddALTV  47633  perfectALTVlem2  47707  ztprmneprm  48319  altgsumbc  48324  divge1b  48485  divgt1b  48486  ackval1  48654  affineid  48677  1subrec1sub  48678  rrx2vlinest  48714  line2x  48727