Theorem mullidd 11354

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225  1c1 11228   · cmul 11232

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-mulcl 11289  ax-mulcom 11291  ax-mulass 11293  ax-distr 11294  ax-1rid 11297  ax-cnre 11300

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-ov 7446

This theorem is used by:  adddirp1d  11362  addrid  11517  mulsubfacd  11804  mulcand  11976  receu  11988  divdivdiv  12045  divcan5  12046  subrecd  12173  ltrec  12226  recp1lt1  12242  nndivtr  12412  subhalfhalf  12607  xp1d2m1eqxm1d2  12627  gtndiv  12803  ge2halflem1  13264  lincmb01cmp  13653  iccf1o  13654  ltdifltdiv  14001  modfrac  14051  negmod  14086  addmodid  14089  m1expcl2  14255  expgt1  14270  ltexp2a  14336  leexp2a  14342  binom3  14395  faclbnd  14461  faclbnd4lem4  14467  facavg  14472  bcval5  14489  cshweqrep  15000  01sqrexlem2  15439  absimle  15505  reccn2  15793  iseraltlem2  15879  iseraltlem3  15880  o1fsum  16009  abscvgcvg  16015  indsum  16024  ackbijnn  16026  binom1p  16029  binom1dif  16031  incexclem  16034  incexc  16035  climcndslem1  16047  pwdif  16066  geomulcvg  16074  fprodsplit  16162  fallrisefac  16221  bpolysum  16248  bpolydiflem  16249  bpoly4  16254  efcllem  16272  ef01bndlem  16381  efieq1re  16396  eirrlem  16401  iddvds  16468  pwp1fsum  16590  oddpwp1fsum  16591  bitsfzolem  16633  bitsfzo  16634  rpmulgcd  16760  prmind2  16889  isprm5  16912  phiprm  16983  eulerthlem2  16988  fermltl  16990  hashgcdlem  16994  odzdvds  17002  powm2modprm  17010  modprm0  17012  pythagtriplem4  17026  4sqlem18  17169  vdwapun  17181  mulgnnass  19348  odinv  19805  odadd2  20093  pgpfaclem2  20328  abvneg  21113  pzriprnglem6  21822  pzriprnglem12  21828  nrginvrcnlem  25040  nmoid  25091  blcvx  25147  icopnfcnv  25293  reparphti  25348  pcorevlem  25377  ncvsm1  25505  ncvspi  25507  cphipval2  25592  cphipval  25594  itg11  26042  itg2mulc  26098  itg2monolem1  26101  itgcnlem  26140  iblabs  26179  dvexp  26303  dvmptdiv  26324  dvef  26330  lhop1lem  26363  dvcvx  26370  dvfsumlem1  26376  dvfsumlem2  26377  dvfsumlem4  26379  dvfsum2  26384  plypow  26553  dgrcolem1  26622  plyn0mulidp  26632  vieta1lem2  26664  radcnvlem1  26770  radcnvlem2  26771  dvradcnv  26778  abelthlem6  26793  abelthlem7  26795  abelth2  26799  sinhalfpip  26851  sinhalfpim  26852  coshalfpip  26853  coshalfpim  26854  tangtx  26864  efif1olem4  26903  abslogle  26976  logdivlti  26978  advlog  27012  advlogexp  27013  logtayl  27018  cxpaddlelem  27109  cxpaddle  27110  affineequiv  27181  affineequiv2  27182  chordthmlem5  27194  dcubic2  27202  dcubic  27204  mcubic  27205  binom4  27208  dquartlem1  27209  quart1lem  27213  quart1  27214  quartlem1  27215  quart  27219  efiasin  27246  atantayl  27295  cvxcl  27342  scvxcvx  27343  lgamgulmlem5  27390  lgamcvg2  27412  lgam1  27421  wilthlem1  27425  wilthlem2  27426  basellem9  27446  fsumfldivdiaglem  27546  muinv  27550  chpub  27577  logexprlim  27582  mersenne  27584  perfectlem2  27587  dchrmullid  27609  dchrptlem1  27621  dchrsum2  27625  sumdchr2  27627  bposlem2  27642  bposlem9  27649  lgsval2lem  27664  lgsval4a  27676  lgsneg1  27679  lgsdir2lem4  27685  lgsdir  27689  lgsmulsqcoprm  27700  lgsdirnn0  27701  lgsdinn0  27702  gausslemma2dlem1a  27722  gausslemma2dlem4  27726  gausslemma2dlem7  27730  gausslemma2d  27731  lgseisenlem1  27732  lgseisenlem2  27733  lgseisenlem4  27735  lgsquad2lem1  27741  2sqlem8  27783  chebbnd1lem3  27828  chpchtlim  27836  rplogsumlem1  27841  rplogsumlem2  27842  rpvmasumlem  27844  dchrmusum2  27851  dchrvmasum2lem  27853  dchrvmasumlem2  27855  dchrvmasumlem3  27856  dchrisum0flblem1  27865  mulog2sumlem2  27892  vmalogdivsum2  27895  2vmadivsumlem  27897  log2sumbnd  27901  selberglem2  27903  selberg3lem1  27914  selberg4lem1  27917  pntrlog2bndlem2  27935  pntrlog2bndlem5  27938  pntpbnd1  27943  pntpbnd2  27944  pntibndlem2  27948  pntlemb  27954  pntlemr  27959  pntlemk  27963  pntlemo  27964  brbtwn2  29513  colinearalglem4  29517  ax5seglem3  29539  axbtwnid  29547  axpaschlem  29548  axeuclidlem  29570  axcontlem7  29578  axcontlem8  29579  elntg2  29593  nvm1  31297  nvpi  31299  nvmtri  31303  ipval2  31339  ipasslem1  31463  ipasslem4  31466  bcs2  31814  lnfnaddi  32675  nnmulge  33401  quad3d  33411  2exple2exp  33495  indsumin  33498  ccfldsrarelvec  34373  constrfin  34448  constrremulcl  34469  constrrecl  34471  constrimcl  34472  constrmulcl  34473  constrreinvcl  34474  2sqr3minply  34482  cos9thpiminplylem2  34485  sqsscirc1  34610  eulerpartlemgs2  35082  logdivsqrle  35349  subfacp1lem6  36117  subfaclim  36120  cvxpconn  36174  cvxsconn  36175  resconn  36178  sinccvglem  36604  fwddifn0  37107  nn0prpwlem  37288  knoppndvlem9  37564  knoppndvlem14  37569  bj-bary1lem1  38424  mblfinlem3  38769  itg2addnclem3  38783  iblabsnc  38794  iblmulc2nc  38795  ftc1anclem6  38808  ftc1anclem7  38809  ftc1anclem8  38810  areacirclem1  38818  bfplem2  38949  bfp  38950  rrntotbnd  38962  lcmineqlem1  43271  lcmineqlem12  43282  lcmineqlem18  43288  aks4d1p1p7  43316  aks4d1p8  43329  primrootscoprmpow  43341  posbezout  43342  aks6d1c2lem4  43369  3rdpwhole  43542  fltnlta  43867  3cubeslem2  43888  3cubeslem3r  43890  irrapxlem5  44026  pellexlem2  44030  pellexlem6  44034  pellfundex  44086  jm2.19lem3  44191  jm2.25  44199  jm2.27c  44207  jm3.1lem2  44218  flcidc  44364  reabssgn  44828  sqrtcval  44833  int-mul12d  45375  cvgdvgrat  45489  bccn1  45520  binomcxplemnotnn0  45532  fperiodmullem  46524  xralrple2  46571  fmul01lt1lem2  46802  mccllem  46814  reclimc  46868  cosknegpi  47084  dvsinax  47128  dvnxpaek  47157  dvnmul  47158  itgsinexp  47170  stoweidlem14  47229  stoweidlem26  47241  wallispilem4  47283  wallispilem5  47284  wallispi2lem1  47286  wallispi2  47288  stirlinglem1  47289  stirlinglem3  47291  stirlinglem4  47292  stirlinglem5  47293  stirlinglem6  47294  stirlinglem7  47295  stirlinglem10  47298  dirkertrigeqlem2  47314  dirkertrigeqlem3  47315  dirkercncflem2  47319  fourierdlem26  47348  fourierdlem41  47363  fourierdlem42  47364  fourierdlem56  47377  fourierdlem57  47378  fourierdlem58  47379  fourierdlem62  47383  fourierdlem64  47385  fourierdlem65  47386  fourierdlem95  47416  sqwvfoura  47443  sqwvfourb  47444  fouriersw  47446  etransclem23  47472  etransclem35  47484  etransclem46  47495  sin5tlem1  48124  sin5tlem2  48125  fmtnorec2lem  48832  fmtnorec3  48838  m1expoddALTV  48951  perfectALTVlem2  49025  ztprmneprm  49664  altgsumbc  49669  divge1b  49829  divgt1b  49830  ackval1  49998  affineid  50021  1subrec1sub  50022  rrx2vlinest  50058  line2x  50071  dvsec  51136  dvcsc  51137