Theorem mulid2d 10648

Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
mulid2d	⊢ (𝜑 → (1 · 𝐴) = 𝐴)

Proof of Theorem mulid2d

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		mulid2 10629	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → (1 · 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524  1c1 10527   · cmul 10531

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-mulcom 10590  ax-mulass 10592  ax-distr 10593  ax-1rid 10596  ax-cnre 10599

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138

This theorem is referenced by:  adddirp1d  10656  addid1  10809  mulsubfacd  11090  mulcand  11262  receu  11274  divdivdiv  11330  divcan5  11331  subrec  11458  ltrec  11511  recp1lt1  11527  nndivtr  11672  subhalfhalf  11859  xp1d2m1eqxm1d2  11879  gtndiv  12047  lincmb01cmp  12873  iccf1o  12874  ltdifltdiv  13199  modfrac  13247  negmod  13279  addmodid  13282  m1expcl2  13447  expgt1  13463  ltexp2a  13526  leexp2a  13532  binom3  13581  faclbnd  13646  faclbnd4lem4  13652  facavg  13657  bcval5  13674  cshweqrep  14174  sqrlem2  14595  absimle  14661  reccn2  14945  iseraltlem2  15031  iseraltlem3  15032  o1fsum  15160  abscvgcvg  15166  ackbijnn  15175  binom1p  15178  binom1dif  15180  incexclem  15183  incexc  15184  climcndslem1  15196  pwdif  15215  geomulcvg  15224  fprodsplit  15312  fallrisefac  15371  bpolysum  15399  bpolydiflem  15400  bpoly4  15405  efcllem  15423  ef01bndlem  15529  efieq1re  15544  eirrlem  15549  iddvds  15615  pwp1fsum  15732  oddpwp1fsum  15733  bitsfzolem  15773  bitsfzo  15774  rpmulgcd  15896  prmind2  16019  isprm5  16041  phiprm  16104  eulerthlem2  16109  fermltl  16111  hashgcdlem  16115  odzdvds  16122  powm2modprm  16130  modprm0  16132  pythagtriplem4  16146  4sqlem18  16288  vdwapun  16300  mulgnnass  18254  odinv  18680  odadd2  18962  pgpfaclem2  19197  abvneg  19598  nrginvrcnlem  23297  nmoid  23348  blcvx  23403  icopnfcnv  23547  reparphti  23602  pcorevlem  23631  ncvsm1  23759  ncvspi  23761  cphipval2  23845  cphipval  23847  itg11  24295  itg2mulc  24351  itg2monolem1  24354  itgcnlem  24393  iblabs  24432  dvexp  24556  dvmptdiv  24577  dvef  24583  lhop1lem  24616  dvcvx  24623  dvfsumlem1  24629  dvfsumlem2  24630  dvfsumlem4  24632  dvfsum2  24637  plypow  24802  dgrcolem1  24870  vieta1lem2  24907  radcnvlem1  25008  radcnvlem2  25009  dvradcnv  25016  abelthlem6  25031  abelthlem7  25033  abelth2  25037  sinhalfpip  25085  sinhalfpim  25086  coshalfpip  25087  coshalfpim  25088  tangtx  25098  efif1olem4  25137  abslogle  25209  logdivlti  25211  advlog  25245  advlogexp  25246  logtayl  25251  cxpaddlelem  25340  cxpaddle  25341  affineequiv  25409  affineequiv2  25410  chordthmlem5  25422  dcubic2  25430  dcubic  25432  mcubic  25433  binom4  25436  dquartlem1  25437  quart1lem  25441  quart1  25442  quartlem1  25443  quart  25447  efiasin  25474  atantayl  25523  cvxcl  25570  scvxcvx  25571  lgamgulmlem5  25618  lgamcvg2  25640  lgam1  25649  wilthlem1  25653  wilthlem2  25654  basellem9  25674  fsumfldivdiaglem  25774  muinv  25778  chpub  25804  logexprlim  25809  mersenne  25811  perfectlem2  25814  dchrmulid2  25836  dchrptlem1  25848  dchrsum2  25852  sumdchr2  25854  bposlem2  25869  bposlem9  25876  lgsval2lem  25891  lgsval4a  25903  lgsneg1  25906  lgsdir2lem4  25912  lgsdir  25916  lgsmulsqcoprm  25927  lgsdirnn0  25928  lgsdinn0  25929  gausslemma2dlem1a  25949  gausslemma2dlem4  25953  gausslemma2dlem7  25957  gausslemma2d  25958  lgseisenlem1  25959  lgseisenlem2  25960  lgseisenlem4  25962  lgsquad2lem1  25968  2sqlem8  26010  chebbnd1lem3  26055  chpchtlim  26063  rplogsumlem1  26068  rplogsumlem2  26069  rpvmasumlem  26071  dchrmusum2  26078  dchrvmasum2lem  26080  dchrvmasumlem2  26082  dchrvmasumlem3  26083  dchrisum0flblem1  26092  mulog2sumlem2  26119  vmalogdivsum2  26122  2vmadivsumlem  26124  log2sumbnd  26128  selberglem2  26130  selberg3lem1  26141  selberg4lem1  26144  pntrlog2bndlem2  26162  pntrlog2bndlem5  26165  pntpbnd1  26170  pntpbnd2  26171  pntibndlem2  26175  pntlemb  26181  pntlemr  26186  pntlemk  26190  pntlemo  26191  brbtwn2  26699  colinearalglem4  26703  ax5seglem3  26725  axbtwnid  26733  axpaschlem  26734  axeuclidlem  26756  axcontlem7  26764  axcontlem8  26765  elntg2  26779  nvm1  28448  nvpi  28450  nvmtri  28454  ipval2  28490  ipasslem1  28614  ipasslem4  28617  bcs2  28965  lnfnaddi  29826  nnmulge  30500  ccfldsrarelvec  31144  sqsscirc1  31261  indsum  31390  indsumin  31391  eulerpartlemgs2  31748  plymulx0  31927  logdivsqrle  32031  subfacp1lem6  32545  subfaclim  32548  cvxpconn  32602  cvxsconn  32603  resconn  32606  sinccvglem  33028  fwddifn0  33738  nn0prpwlem  33783  knoppndvlem9  33972  knoppndvlem14  33977  bj-bary1lem1  34725  mblfinlem3  35096  itg2addnclem3  35110  iblabsnc  35121  iblmulc2nc  35122  ftc1anclem6  35135  ftc1anclem7  35136  ftc1anclem8  35137  areacirclem1  35145  bfplem2  35261  bfp  35262  rrntotbnd  35274  lcmineqlem1  39317  lcmineqlem12  39328  lcmineqlem18  39334  3lexlogpow5ineq2  39342  fltnlta  39619  3cubeslem2  39626  3cubeslem3r  39628  irrapxlem5  39767  pellexlem2  39771  pellexlem6  39775  pellfundex  39827  jm2.19lem3  39932  jm2.25  39940  jm2.27c  39948  jm3.1lem2  39959  flcidc  40118  reabssgn  40336  sqrtcval  40341  int-mul12d  40889  cvgdvgrat  41017  bccn1  41048  binomcxplemnotnn0  41060  fperiodmullem  41935  xralrple2  41986  fmul01lt1lem2  42227  mccllem  42239  reclimc  42295  cosknegpi  42511  dvsinax  42555  dvnxpaek  42584  dvnmul  42585  itgsinexp  42597  stoweidlem14  42656  stoweidlem26  42668  wallispilem4  42710  wallispilem5  42711  wallispi2lem1  42713  wallispi2  42715  stirlinglem1  42716  stirlinglem3  42718  stirlinglem4  42719  stirlinglem5  42720  stirlinglem6  42721  stirlinglem7  42722  stirlinglem10  42725  dirkertrigeqlem2  42741  dirkertrigeqlem3  42742  dirkercncflem2  42746  fourierdlem26  42775  fourierdlem41  42790  fourierdlem42  42791  fourierdlem56  42804  fourierdlem57  42805  fourierdlem58  42806  fourierdlem62  42810  fourierdlem64  42812  fourierdlem65  42813  fourierdlem95  42843  sqwvfoura  42870  sqwvfourb  42871  fouriersw  42873  etransclem23  42899  etransclem35  42911  etransclem46  42922  fmtnorec2lem  44059  fmtnorec3  44065  m1expoddALTV  44166  perfectALTVlem2  44240  ztprmneprm  44749  altgsumbc  44754  divge1b  44921  divgt1b  44922  ackval1  45095  affineid  45118  1subrec1sub  45119  rrx2vlinest  45155  line2x  45168