Theorem mullidd 11231

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  (class class class)co 7408  ℂcc 11107  1c1 11110   · cmul 11114

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-mulcl 11171  ax-mulcom 11173  ax-mulass 11175  ax-distr 11176  ax-1rid 11179  ax-cnre 11182

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7411

This theorem is referenced by:  adddirp1d  11239  addrid  11393  mulsubfacd  11674  mulcand  11846  receu  11858  divdivdiv  11914  divcan5  11915  subrec  12042  ltrec  12095  recp1lt1  12111  nndivtr  12258  subhalfhalf  12445  xp1d2m1eqxm1d2  12465  gtndiv  12638  lincmb01cmp  13471  iccf1o  13472  ltdifltdiv  13798  modfrac  13848  negmod  13880  addmodid  13883  m1expcl2  14050  expgt1  14065  ltexp2a  14130  leexp2a  14136  binom3  14186  faclbnd  14249  faclbnd4lem4  14255  facavg  14260  bcval5  14277  cshweqrep  14770  01sqrexlem2  15189  absimle  15255  reccn2  15540  iseraltlem2  15628  iseraltlem3  15629  o1fsum  15758  abscvgcvg  15764  ackbijnn  15773  binom1p  15776  binom1dif  15778  incexclem  15781  incexc  15782  climcndslem1  15794  pwdif  15813  geomulcvg  15821  fprodsplit  15909  fallrisefac  15968  bpolysum  15996  bpolydiflem  15997  bpoly4  16002  efcllem  16020  ef01bndlem  16126  efieq1re  16141  eirrlem  16146  iddvds  16212  pwp1fsum  16333  oddpwp1fsum  16334  bitsfzolem  16374  bitsfzo  16375  rpmulgcd  16497  prmind2  16621  isprm5  16643  phiprm  16709  eulerthlem2  16714  fermltl  16716  hashgcdlem  16720  odzdvds  16727  powm2modprm  16735  modprm0  16737  pythagtriplem4  16751  4sqlem18  16894  vdwapun  16906  mulgnnass  18988  odinv  19428  odadd2  19716  pgpfaclem2  19951  abvneg  20441  nrginvrcnlem  24207  nmoid  24258  blcvx  24313  icopnfcnv  24457  reparphti  24512  pcorevlem  24541  ncvsm1  24670  ncvspi  24672  cphipval2  24757  cphipval  24759  itg11  25207  itg2mulc  25264  itg2monolem1  25267  itgcnlem  25306  iblabs  25345  dvexp  25469  dvmptdiv  25490  dvef  25496  lhop1lem  25529  dvcvx  25536  dvfsumlem1  25542  dvfsumlem2  25543  dvfsumlem4  25545  dvfsum2  25550  plypow  25718  dgrcolem1  25786  vieta1lem2  25823  radcnvlem1  25924  radcnvlem2  25925  dvradcnv  25932  abelthlem6  25947  abelthlem7  25949  abelth2  25953  sinhalfpip  26001  sinhalfpim  26002  coshalfpip  26003  coshalfpim  26004  tangtx  26014  efif1olem4  26053  abslogle  26125  logdivlti  26127  advlog  26161  advlogexp  26162  logtayl  26167  cxpaddlelem  26256  cxpaddle  26257  affineequiv  26325  affineequiv2  26326  chordthmlem5  26338  dcubic2  26346  dcubic  26348  mcubic  26349  binom4  26352  dquartlem1  26353  quart1lem  26357  quart1  26358  quartlem1  26359  quart  26363  efiasin  26390  atantayl  26439  cvxcl  26486  scvxcvx  26487  lgamgulmlem5  26534  lgamcvg2  26556  lgam1  26565  wilthlem1  26569  wilthlem2  26570  basellem9  26590  fsumfldivdiaglem  26690  muinv  26694  chpub  26720  logexprlim  26725  mersenne  26727  perfectlem2  26730  dchrmullid  26752  dchrptlem1  26764  dchrsum2  26768  sumdchr2  26770  bposlem2  26785  bposlem9  26792  lgsval2lem  26807  lgsval4a  26819  lgsneg1  26822  lgsdir2lem4  26828  lgsdir  26832  lgsmulsqcoprm  26843  lgsdirnn0  26844  lgsdinn0  26845  gausslemma2dlem1a  26865  gausslemma2dlem4  26869  gausslemma2dlem7  26873  gausslemma2d  26874  lgseisenlem1  26875  lgseisenlem2  26876  lgseisenlem4  26878  lgsquad2lem1  26884  2sqlem8  26926  chebbnd1lem3  26971  chpchtlim  26979  rplogsumlem1  26984  rplogsumlem2  26985  rpvmasumlem  26987  dchrmusum2  26994  dchrvmasum2lem  26996  dchrvmasumlem2  26998  dchrvmasumlem3  26999  dchrisum0flblem1  27008  mulog2sumlem2  27035  vmalogdivsum2  27038  2vmadivsumlem  27040  log2sumbnd  27044  selberglem2  27046  selberg3lem1  27057  selberg4lem1  27060  pntrlog2bndlem2  27078  pntrlog2bndlem5  27081  pntpbnd1  27086  pntpbnd2  27087  pntibndlem2  27091  pntlemb  27097  pntlemr  27102  pntlemk  27106  pntlemo  27107  brbtwn2  28160  colinearalglem4  28164  ax5seglem3  28186  axbtwnid  28194  axpaschlem  28195  axeuclidlem  28217  axcontlem7  28225  axcontlem8  28226  elntg2  28240  nvm1  29913  nvpi  29915  nvmtri  29919  ipval2  29955  ipasslem1  30079  ipasslem4  30082  bcs2  30430  lnfnaddi  31291  nnmulge  31958  ccfldsrarelvec  32740  sqsscirc1  32883  indsum  33014  indsumin  33015  eulerpartlemgs2  33374  plymulx0  33553  logdivsqrle  33657  subfacp1lem6  34171  subfaclim  34174  cvxpconn  34228  cvxsconn  34229  resconn  34232  sinccvglem  34652  fwddifn0  35131  gg-reparphti  35167  gg-dvfsumlem2  35178  nn0prpwlem  35202  knoppndvlem9  35391  knoppndvlem14  35396  bj-bary1lem1  36187  mblfinlem3  36522  itg2addnclem3  36536  iblabsnc  36547  iblmulc2nc  36548  ftc1anclem6  36561  ftc1anclem7  36562  ftc1anclem8  36563  areacirclem1  36571  bfplem2  36686  bfp  36687  rrntotbnd  36699  lcmineqlem1  40889  lcmineqlem12  40900  lcmineqlem18  40906  aks4d1p1p7  40934  aks4d1p8  40947  fltnlta  41406  3cubeslem2  41413  3cubeslem3r  41415  irrapxlem5  41554  pellexlem2  41558  pellexlem6  41562  pellfundex  41614  jm2.19lem3  41720  jm2.25  41728  jm2.27c  41736  jm3.1lem2  41747  flcidc  41906  reabssgn  42377  sqrtcval  42382  int-mul12d  42925  cvgdvgrat  43062  bccn1  43093  binomcxplemnotnn0  43105  fperiodmullem  44003  xralrple2  44054  fmul01lt1lem2  44291  mccllem  44303  reclimc  44359  cosknegpi  44575  dvsinax  44619  dvnxpaek  44648  dvnmul  44649  itgsinexp  44661  stoweidlem14  44720  stoweidlem26  44732  wallispilem4  44774  wallispilem5  44775  wallispi2lem1  44777  wallispi2  44779  stirlinglem1  44780  stirlinglem3  44782  stirlinglem4  44783  stirlinglem5  44784  stirlinglem6  44785  stirlinglem7  44786  stirlinglem10  44789  dirkertrigeqlem2  44805  dirkertrigeqlem3  44806  dirkercncflem2  44810  fourierdlem26  44839  fourierdlem41  44854  fourierdlem42  44855  fourierdlem56  44868  fourierdlem57  44869  fourierdlem58  44870  fourierdlem62  44874  fourierdlem64  44876  fourierdlem65  44877  fourierdlem95  44907  sqwvfoura  44934  sqwvfourb  44935  fouriersw  44937  etransclem23  44963  etransclem35  44975  etransclem46  44986  fmtnorec2lem  46200  fmtnorec3  46206  m1expoddALTV  46306  perfectALTVlem2  46380  pzriprnglem6  46800  pzriprnglem12  46806  ztprmneprm  47013  altgsumbc  47018  divge1b  47183  divgt1b  47184  ackval1  47357  affineid  47380  1subrec1sub  47381  rrx2vlinest  47417  line2x  47430