Theorem mullidd 11262

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099  (class class class)co 7420  ℂcc 11136  1c1 11139   · cmul 11143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-mulcl 11200  ax-mulcom 11202  ax-mulass 11204  ax-distr 11205  ax-1rid 11208  ax-cnre 11211

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rex 3068  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-iota 6500  df-fv 6556  df-ov 7423

This theorem is referenced by:  adddirp1d  11270  addrid  11424  mulsubfacd  11705  mulcand  11877  receu  11889  divdivdiv  11945  divcan5  11946  subrec  12073  ltrec  12126  recp1lt1  12142  nndivtr  12289  subhalfhalf  12476  xp1d2m1eqxm1d2  12496  gtndiv  12669  lincmb01cmp  13504  iccf1o  13505  ltdifltdiv  13831  modfrac  13881  negmod  13913  addmodid  13916  m1expcl2  14082  expgt1  14097  ltexp2a  14162  leexp2a  14168  binom3  14218  faclbnd  14281  faclbnd4lem4  14287  facavg  14292  bcval5  14309  cshweqrep  14803  01sqrexlem2  15222  absimle  15288  reccn2  15573  iseraltlem2  15661  iseraltlem3  15662  o1fsum  15791  abscvgcvg  15797  ackbijnn  15806  binom1p  15809  binom1dif  15811  incexclem  15814  incexc  15815  climcndslem1  15827  pwdif  15846  geomulcvg  15854  fprodsplit  15942  fallrisefac  16001  bpolysum  16029  bpolydiflem  16030  bpoly4  16035  efcllem  16053  ef01bndlem  16160  efieq1re  16175  eirrlem  16180  iddvds  16246  pwp1fsum  16367  oddpwp1fsum  16368  bitsfzolem  16408  bitsfzo  16409  rpmulgcd  16531  prmind2  16655  isprm5  16677  phiprm  16745  eulerthlem2  16750  fermltl  16752  hashgcdlem  16756  odzdvds  16763  powm2modprm  16771  modprm0  16773  pythagtriplem4  16787  4sqlem18  16930  vdwapun  16942  mulgnnass  19063  odinv  19515  odadd2  19803  pgpfaclem2  20038  abvneg  20713  pzriprnglem6  21411  pzriprnglem12  21417  nrginvrcnlem  24607  nmoid  24658  blcvx  24713  icopnfcnv  24866  reparphti  24922  reparphtiOLD  24923  pcorevlem  24952  ncvsm1  25081  ncvspi  25083  cphipval2  25168  cphipval  25170  itg11  25619  itg2mulc  25676  itg2monolem1  25679  itgcnlem  25718  iblabs  25757  dvexp  25884  dvmptdiv  25905  dvef  25911  lhop1lem  25945  dvcvx  25952  dvfsumlem1  25959  dvfsumlem2  25960  dvfsumlem2OLD  25961  dvfsumlem4  25963  dvfsum2  25968  plypow  26138  dgrcolem1  26207  vieta1lem2  26245  radcnvlem1  26348  radcnvlem2  26349  dvradcnv  26356  abelthlem6  26372  abelthlem7  26374  abelth2  26378  sinhalfpip  26426  sinhalfpim  26427  coshalfpip  26428  coshalfpim  26429  tangtx  26439  efif1olem4  26478  abslogle  26551  logdivlti  26553  advlog  26587  advlogexp  26588  logtayl  26593  cxpaddlelem  26685  cxpaddle  26686  affineequiv  26754  affineequiv2  26755  chordthmlem5  26767  dcubic2  26775  dcubic  26777  mcubic  26778  binom4  26781  dquartlem1  26782  quart1lem  26786  quart1  26787  quartlem1  26788  quart  26792  efiasin  26819  atantayl  26868  cvxcl  26916  scvxcvx  26917  lgamgulmlem5  26964  lgamcvg2  26986  lgam1  26995  wilthlem1  26999  wilthlem2  27000  basellem9  27020  fsumfldivdiaglem  27120  muinv  27124  chpub  27152  logexprlim  27157  mersenne  27159  perfectlem2  27162  dchrmullid  27184  dchrptlem1  27196  dchrsum2  27200  sumdchr2  27202  bposlem2  27217  bposlem9  27224  lgsval2lem  27239  lgsval4a  27251  lgsneg1  27254  lgsdir2lem4  27260  lgsdir  27264  lgsmulsqcoprm  27275  lgsdirnn0  27276  lgsdinn0  27277  gausslemma2dlem1a  27297  gausslemma2dlem4  27301  gausslemma2dlem7  27305  gausslemma2d  27306  lgseisenlem1  27307  lgseisenlem2  27308  lgseisenlem4  27310  lgsquad2lem1  27316  2sqlem8  27358  chebbnd1lem3  27403  chpchtlim  27411  rplogsumlem1  27416  rplogsumlem2  27417  rpvmasumlem  27419  dchrmusum2  27426  dchrvmasum2lem  27428  dchrvmasumlem2  27430  dchrvmasumlem3  27431  dchrisum0flblem1  27440  mulog2sumlem2  27467  vmalogdivsum2  27470  2vmadivsumlem  27472  log2sumbnd  27476  selberglem2  27478  selberg3lem1  27489  selberg4lem1  27492  pntrlog2bndlem2  27510  pntrlog2bndlem5  27513  pntpbnd1  27518  pntpbnd2  27519  pntibndlem2  27523  pntlemb  27529  pntlemr  27534  pntlemk  27538  pntlemo  27539  brbtwn2  28715  colinearalglem4  28719  ax5seglem3  28741  axbtwnid  28749  axpaschlem  28750  axeuclidlem  28772  axcontlem7  28780  axcontlem8  28781  elntg2  28795  nvm1  30474  nvpi  30476  nvmtri  30480  ipval2  30516  ipasslem1  30640  ipasslem4  30643  bcs2  30991  lnfnaddi  31852  nnmulge  32520  ccfldsrarelvec  33355  sqsscirc1  33509  indsum  33640  indsumin  33641  eulerpartlemgs2  34000  plymulx0  34179  logdivsqrle  34282  subfacp1lem6  34795  subfaclim  34798  cvxpconn  34852  cvxsconn  34853  resconn  34856  sinccvglem  35276  fwddifn0  35760  nn0prpwlem  35806  knoppndvlem9  35995  knoppndvlem14  36000  bj-bary1lem1  36790  mblfinlem3  37132  itg2addnclem3  37146  iblabsnc  37157  iblmulc2nc  37158  ftc1anclem6  37171  ftc1anclem7  37172  ftc1anclem8  37173  areacirclem1  37181  bfplem2  37296  bfp  37297  rrntotbnd  37309  lcmineqlem1  41500  lcmineqlem12  41511  lcmineqlem18  41517  aks4d1p1p7  41545  aks4d1p8  41558  primrootscoprmpow  41570  posbezout  41571  aks6d1c2lem4  41598  fltnlta  42087  3cubeslem2  42105  3cubeslem3r  42107  irrapxlem5  42246  pellexlem2  42250  pellexlem6  42254  pellfundex  42306  jm2.19lem3  42412  jm2.25  42420  jm2.27c  42428  jm3.1lem2  42439  flcidc  42598  reabssgn  43066  sqrtcval  43071  int-mul12d  43613  cvgdvgrat  43750  bccn1  43781  binomcxplemnotnn0  43793  fperiodmullem  44685  xralrple2  44736  fmul01lt1lem2  44973  mccllem  44985  reclimc  45041  cosknegpi  45257  dvsinax  45301  dvnxpaek  45330  dvnmul  45331  itgsinexp  45343  stoweidlem14  45402  stoweidlem26  45414  wallispilem4  45456  wallispilem5  45457  wallispi2lem1  45459  wallispi2  45461  stirlinglem1  45462  stirlinglem3  45464  stirlinglem4  45465  stirlinglem5  45466  stirlinglem6  45467  stirlinglem7  45468  stirlinglem10  45471  dirkertrigeqlem2  45487  dirkertrigeqlem3  45488  dirkercncflem2  45492  fourierdlem26  45521  fourierdlem41  45536  fourierdlem42  45537  fourierdlem56  45550  fourierdlem57  45551  fourierdlem58  45552  fourierdlem62  45556  fourierdlem64  45558  fourierdlem65  45559  fourierdlem95  45589  sqwvfoura  45616  sqwvfourb  45617  fouriersw  45619  etransclem23  45645  etransclem35  45657  etransclem46  45668  fmtnorec2lem  46882  fmtnorec3  46888  m1expoddALTV  46988  perfectALTVlem2  47062  ztprmneprm  47411  altgsumbc  47416  divge1b  47580  divgt1b  47581  ackval1  47754  affineid  47777  1subrec1sub  47778  rrx2vlinest  47814  line2x  47827