Theorem mulridd 11307

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

Hypothesis

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

Assertion

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

Proof of Theorem mulridd

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182  1c1 11185   · cmul 11189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-mulcl 11246  ax-mulcom 11248  ax-mulass 11250  ax-distr 11251  ax-1rid 11254  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  muladd11  11460  muls1d  11750  divrec  11965  diveq1  11979  conjmul  12011  divelunit  13554  modid  13947  addmodlteq  13997  expadd  14155  leexp2r  14224  nnlesq  14254  sqoddm1div8  14292  faclbnd  14339  faclbnd2  14340  faclbnd4lem3  14344  faclbnd6  14348  facavg  14350  bcn0  14359  bcn1  14362  hashf1lem2  14505  hashfac  14507  reccn2  15643  iseraltlem2  15731  iseraltlem3  15732  hash2iun1dif1  15872  binom11  15880  harmonic  15907  trireciplem  15910  geoserg  15914  pwdif  15916  pwm1geoser  15917  cvgrat  15931  fprodsplit  16014  fprodle  16044  fsumcube  16108  efzval  16150  tanhlt1  16208  tanaddlem  16214  tanadd  16215  cos01gt0  16239  absef  16245  1dvds  16319  bitsfzo  16481  bitsmod  16482  sqgcd  16609  expgcd  16610  lcm1  16657  coprmdvds  16700  qredeu  16705  phiprmpw  16823  coprimeprodsq  16855  pc2dvds  16926  sumhash  16943  fldivp1  16944  pcfaclem  16945  prmpwdvds  16951  prmreclem1  16963  vdwlem3  17030  vdwlem9  17036  prmop1  17085  sylow2a  19661  odadd  19892  zsssubrg  21466  zringcyg  21503  prmirredlem  21506  mulgrhm2  21512  pzriprnglem6  21520  pzriprnglem12  21526  znrrg  21607  mhppwdeg  22177  icopnfcnv  24992  icopnfhmeo  24993  lebnumii  25017  reparphti  25048  reparphtiOLD  25049  itg2const  25795  itg2monolem3  25807  bddibl  25895  dveflem  26037  mvth  26051  dvlipcn  26053  dvivthlem1  26067  dvfsumle  26080  dvfsumleOLD  26081  dvfsumabs  26083  dvfsumlem2  26087  dvfsumlem2OLD  26088  plyconst  26265  plyeq0lem  26269  plyco  26300  0dgrb  26305  coefv0  26307  vieta1  26372  aaliou3lem2  26403  tayl0  26421  taylply2  26427  taylply2OLD  26428  dvtaylp  26430  taylthlem2  26434  taylthlem2OLD  26435  radcnvlem1  26474  abelthlem1  26493  abelthlem2  26494  abelthlem3  26495  abelthlem7  26500  abelthlem8  26501  abelthlem9  26502  efper  26539  tangtx  26565  eflogeq  26662  logdivlti  26680  logcnlem4  26705  advlogexp  26715  cxpmul2  26749  dvcxp2  26801  cxpaddle  26813  cxpeq  26818  loglesqrt  26822  relogbexp  26841  ang180lem5  26874  isosctrlem2  26880  isosctrlem3  26881  heron  26899  2efiatan  26979  dvatan  26996  leibpi  27003  birthdaylem3  27014  jensenlem2  27049  logdiflbnd  27056  harmonicbnd4  27072  lgamgulmlem2  27091  lgamcvg2  27116  ftalem5  27138  basellem2  27143  basellem5  27146  basellem8  27149  0sgm  27205  muinv  27254  chpub  27282  logfaclbnd  27284  logexprlim  27287  dchrsum2  27330  sumdchr2  27332  bposlem1  27346  bposlem2  27347  bposlem5  27350  lgsquad2lem1  27446  lgsquad3  27449  2sqlem6  27485  2sqlem8  27488  chtppilim  27537  vmadivsum  27544  dchrisumlem1  27551  dchrisum0flblem1  27570  rpvmasum2  27574  dchrisum0re  27575  dchrisum0lem2a  27579  dchrisum0lem3  27581  rpvmasum  27588  mudivsum  27592  mulogsumlem  27593  vmalogdivsum2  27600  pntrsumo1  27627  pntrlog2bndlem2  27640  pntrlog2bndlem4  27642  pntrlog2bndlem5  27643  pntibndlem2  27653  pntlemc  27657  pntlemf  27667  ostth2lem2  27696  ostth2lem3  27697  ostth2lem4  27698  ostth2  27699  ostth3  27700  ttgcontlem1  28917  axpaschlem  28973  axcontlem2  28998  axcontlem4  29000  axcontlem8  29004  nmoub3i  30805  ubthlem2  30903  htthlem  30949  nmcexi  32058  nmopcoadji  32133  branmfn  32137  rearchi  33339  ccfldextdgrr  33682  madjusmdetlem4  33776  ccatmulgnn0dir  34519  ofcccat  34520  itgexpif  34583  hashreprin  34597  circlemeth  34617  lpadlem2  34657  subfacval2  35155  cvmliftlem2  35254  snmlff  35297  sinccvglem  35640  bcprod  35700  faclimlem1  35705  faclimlem2  35706  faclim2  35710  knoppndvlem14  36491  knoppndvlem15  36492  knoppndvlem16  36493  knoppndvlem18  36495  poimirlem29  37609  poimirlem30  37610  poimirlem31  37611  poimirlem32  37612  itg2addnclem  37631  areacirclem1  37668  areacirclem4  37671  cntotbnd  37756  lcmineqlem11  41996  lcmineqlem12  41997  aks4d1p1p7  42031  aks4d1p8d2  42042  hashscontpow1  42078  2ap1caineq  42102  sticksstones10  42112  sticksstones12a  42114  aks6d1c6lem1  42127  aks6d1c7lem1  42137  aks6d1c7  42141  oddnumth  42299  oexpreposd  42309  frlmvscadiccat  42461  fltnltalem  42617  3cubeslem2  42641  3cubeslem3r  42643  irrapxlem1  42778  irrapxlem4  42781  pell1qrgaplem  42829  reglogexpbas  42853  rmspecfund  42865  rmxy1  42879  rmxp1  42889  rmyp1  42890  rmxm1  42891  jm2.17a  42917  jm2.18  42945  jm2.23  42953  jm2.25  42956  jm2.16nn0  42961  relexpmulnn  43671  int-mul11d  44144  nzprmdif  44288  expgrowthi  44302  expgrowth  44304  binomcxplemdvbinom  44322  binomcxplemnotnn0  44325  sqrlearg  45471  fmul01  45501  fmul01lt1lem1  45505  0ellimcdiv  45570  dvxpaek  45861  dvnxpaek  45863  itgiccshift  45901  itgperiod  45902  itgsbtaddcnst  45903  stoweidlem11  45932  stoweidlem26  45947  stoweidlem38  45959  wallispilem4  45989  stirlinglem1  45995  stirlinglem3  45997  stirlinglem6  46000  stirlinglem7  46001  stirlinglem8  46002  stirlinglem10  46004  stirlinglem12  46006  dirkertrigeqlem3  46021  dirkertrigeq  46022  dirkercncflem1  46024  dirkercncflem2  46025  fourierdlem28  46056  fourierdlem30  46058  fourierdlem39  46067  fourierdlem47  46074  fourierdlem60  46087  fourierdlem61  46088  fourierdlem73  46100  fourierdlem83  46110  fourierdlem87  46114  etransclem14  46169  etransclem24  46179  etransclem25  46180  etransclem35  46190  smfmullem1  46712  deccarry  47226  fpprwppr  47613  fpprwpprb  47614  logblt1b  48298  nn0sumshdiglem2  48356  itcovalpclem2  48405  itcovalt2lem1  48409  eenglngeehlnmlem1  48471  eenglngeehlnmlem2  48472  line2ylem  48485