Theorem mullidd 11279

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153  1c1 11156   · cmul 11160

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-mulcl 11217  ax-mulcom 11219  ax-mulass 11221  ax-distr 11222  ax-1rid 11225  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434

This theorem is referenced by:  adddirp1d  11287  addrid  11441  mulsubfacd  11724  mulcand  11896  receu  11908  divdivdiv  11968  divcan5  11969  subrec  12096  ltrec  12150  recp1lt1  12166  nndivtr  12313  subhalfhalf  12500  xp1d2m1eqxm1d2  12520  gtndiv  12695  ge2halflem1  13150  lincmb01cmp  13535  iccf1o  13536  ltdifltdiv  13874  modfrac  13924  negmod  13957  addmodid  13960  m1expcl2  14126  expgt1  14141  ltexp2a  14206  leexp2a  14212  binom3  14263  faclbnd  14329  faclbnd4lem4  14335  facavg  14340  bcval5  14357  cshweqrep  14859  01sqrexlem2  15282  absimle  15348  reccn2  15633  iseraltlem2  15719  iseraltlem3  15720  o1fsum  15849  abscvgcvg  15855  ackbijnn  15864  binom1p  15867  binom1dif  15869  incexclem  15872  incexc  15873  climcndslem1  15885  pwdif  15904  geomulcvg  15912  fprodsplit  16002  fallrisefac  16061  bpolysum  16089  bpolydiflem  16090  bpoly4  16095  efcllem  16113  ef01bndlem  16220  efieq1re  16235  eirrlem  16240  iddvds  16307  pwp1fsum  16428  oddpwp1fsum  16429  bitsfzolem  16471  bitsfzo  16472  rpmulgcd  16594  prmind2  16722  isprm5  16744  phiprm  16814  eulerthlem2  16819  fermltl  16821  hashgcdlem  16825  odzdvds  16833  powm2modprm  16841  modprm0  16843  pythagtriplem4  16857  4sqlem18  17000  vdwapun  17012  mulgnnass  19127  odinv  19579  odadd2  19867  pgpfaclem2  20102  abvneg  20827  pzriprnglem6  21497  pzriprnglem12  21503  nrginvrcnlem  24712  nmoid  24763  blcvx  24819  icopnfcnv  24973  reparphti  25029  reparphtiOLD  25030  pcorevlem  25059  ncvsm1  25188  ncvspi  25190  cphipval2  25275  cphipval  25277  itg11  25726  itg2mulc  25782  itg2monolem1  25785  itgcnlem  25825  iblabs  25864  dvexp  25991  dvmptdiv  26012  dvef  26018  lhop1lem  26052  dvcvx  26059  dvfsumlem1  26066  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumlem4  26070  dvfsum2  26075  plypow  26244  dgrcolem1  26313  vieta1lem2  26353  radcnvlem1  26456  radcnvlem2  26457  dvradcnv  26464  abelthlem6  26480  abelthlem7  26482  abelth2  26486  sinhalfpip  26534  sinhalfpim  26535  coshalfpip  26536  coshalfpim  26537  tangtx  26547  efif1olem4  26587  abslogle  26660  logdivlti  26662  advlog  26696  advlogexp  26697  logtayl  26702  cxpaddlelem  26794  cxpaddle  26795  affineequiv  26866  affineequiv2  26867  chordthmlem5  26879  dcubic2  26887  dcubic  26889  mcubic  26890  binom4  26893  dquartlem1  26894  quart1lem  26898  quart1  26899  quartlem1  26900  quart  26904  efiasin  26931  atantayl  26980  cvxcl  27028  scvxcvx  27029  lgamgulmlem5  27076  lgamcvg2  27098  lgam1  27107  wilthlem1  27111  wilthlem2  27112  basellem9  27132  fsumfldivdiaglem  27232  muinv  27236  chpub  27264  logexprlim  27269  mersenne  27271  perfectlem2  27274  dchrmullid  27296  dchrptlem1  27308  dchrsum2  27312  sumdchr2  27314  bposlem2  27329  bposlem9  27336  lgsval2lem  27351  lgsval4a  27363  lgsneg1  27366  lgsdir2lem4  27372  lgsdir  27376  lgsmulsqcoprm  27387  lgsdirnn0  27388  lgsdinn0  27389  gausslemma2dlem1a  27409  gausslemma2dlem4  27413  gausslemma2dlem7  27417  gausslemma2d  27418  lgseisenlem1  27419  lgseisenlem2  27420  lgseisenlem4  27422  lgsquad2lem1  27428  2sqlem8  27470  chebbnd1lem3  27515  chpchtlim  27523  rplogsumlem1  27528  rplogsumlem2  27529  rpvmasumlem  27531  dchrmusum2  27538  dchrvmasum2lem  27540  dchrvmasumlem2  27542  dchrvmasumlem3  27543  dchrisum0flblem1  27552  mulog2sumlem2  27579  vmalogdivsum2  27582  2vmadivsumlem  27584  log2sumbnd  27588  selberglem2  27590  selberg3lem1  27601  selberg4lem1  27604  pntrlog2bndlem2  27622  pntrlog2bndlem5  27625  pntpbnd1  27630  pntpbnd2  27631  pntibndlem2  27635  pntlemb  27641  pntlemr  27646  pntlemk  27650  pntlemo  27651  brbtwn2  28920  colinearalglem4  28924  ax5seglem3  28946  axbtwnid  28954  axpaschlem  28955  axeuclidlem  28977  axcontlem7  28985  axcontlem8  28986  elntg2  29000  nvm1  30684  nvpi  30686  nvmtri  30690  ipval2  30726  ipasslem1  30850  ipasslem4  30853  bcs2  31201  lnfnaddi  32062  nnmulge  32749  quad3d  32754  2exple2exp  32834  indsum  32846  indsumin  32847  ccfldsrarelvec  33721  constrfin  33787  2sqr3minply  33791  sqsscirc1  33907  eulerpartlemgs2  34382  plymulx0  34562  logdivsqrle  34665  subfacp1lem6  35190  subfaclim  35193  cvxpconn  35247  cvxsconn  35248  resconn  35251  sinccvglem  35677  fwddifn0  36165  nn0prpwlem  36323  knoppndvlem9  36521  knoppndvlem14  36526  bj-bary1lem1  37312  mblfinlem3  37666  itg2addnclem3  37680  iblabsnc  37691  iblmulc2nc  37692  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anclem8  37707  areacirclem1  37715  bfplem2  37830  bfp  37831  rrntotbnd  37843  lcmineqlem1  42030  lcmineqlem12  42041  lcmineqlem18  42047  aks4d1p1p7  42075  aks4d1p8  42088  primrootscoprmpow  42100  posbezout  42101  aks6d1c2lem4  42128  fltnlta  42673  3cubeslem2  42696  3cubeslem3r  42698  irrapxlem5  42837  pellexlem2  42841  pellexlem6  42845  pellfundex  42897  jm2.19lem3  43003  jm2.25  43011  jm2.27c  43019  jm3.1lem2  43030  flcidc  43182  reabssgn  43649  sqrtcval  43654  int-mul12d  44196  cvgdvgrat  44332  bccn1  44363  binomcxplemnotnn0  44375  fperiodmullem  45315  xralrple2  45365  fmul01lt1lem2  45600  mccllem  45612  reclimc  45668  cosknegpi  45884  dvsinax  45928  dvnxpaek  45957  dvnmul  45958  itgsinexp  45970  stoweidlem14  46029  stoweidlem26  46041  wallispilem4  46083  wallispilem5  46084  wallispi2lem1  46086  wallispi2  46088  stirlinglem1  46089  stirlinglem3  46091  stirlinglem4  46092  stirlinglem5  46093  stirlinglem6  46094  stirlinglem7  46095  stirlinglem10  46098  dirkertrigeqlem2  46114  dirkertrigeqlem3  46115  dirkercncflem2  46119  fourierdlem26  46148  fourierdlem41  46163  fourierdlem42  46164  fourierdlem56  46177  fourierdlem57  46178  fourierdlem58  46179  fourierdlem62  46183  fourierdlem64  46185  fourierdlem65  46186  fourierdlem95  46216  sqwvfoura  46243  sqwvfourb  46244  fouriersw  46246  etransclem23  46272  etransclem35  46284  etransclem46  46295  fmtnorec2lem  47529  fmtnorec3  47535  m1expoddALTV  47635  perfectALTVlem2  47709  ztprmneprm  48263  altgsumbc  48268  divge1b  48429  divgt1b  48430  ackval1  48602  affineid  48625  1subrec1sub  48626  rrx2vlinest  48662  line2x  48675