Theorem mulridd 11153

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027  1c1 11030   · cmul 11034

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-mulcl 11091  ax-mulcom 11093  ax-mulass 11095  ax-distr 11096  ax-1rid 11099  ax-cnre 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363

This theorem is referenced by:  muladd11  11307  muls1d  11601  divrec  11816  diveq1  11830  conjmul  11863  divelunit  13438  modid  13846  addmodlteq  13899  expadd  14057  leexp2r  14127  nnlesq  14158  sqoddm1div8  14196  faclbnd  14243  faclbnd2  14244  faclbnd4lem3  14248  faclbnd6  14252  facavg  14254  bcn0  14263  bcn1  14266  hashf1lem2  14409  hashfac  14411  reccn2  15550  iseraltlem2  15636  iseraltlem3  15637  fsumconst1  15744  hash2iun1dif1  15778  indsumhash  15783  binom11  15788  harmonic  15815  trireciplem  15818  geoserg  15822  pwdif  15824  pwm1geoser  15825  cvgrat  15839  fprodsplit  15922  fprodle  15952  fsumcube  16016  efzval  16060  tanhlt1  16118  tanaddlem  16124  tanadd  16125  cos01gt0  16149  absef  16155  1dvds  16230  bitsfzo  16395  bitsmod  16396  sqgcd  16522  expgcd  16523  lcm1  16570  coprmdvds  16613  qredeu  16618  phiprmpw  16737  coprimeprodsq  16770  pc2dvds  16841  sumhash  16858  fldivp1  16859  pcfaclem  16860  prmpwdvds  16866  prmreclem1  16878  vdwlem3  16945  vdwlem9  16951  prmop1  17000  sylow2a  19585  odadd  19816  zsssubrg  21415  zringcyg  21459  prmirredlem  21462  mulgrhm2  21468  pzriprnglem6  21476  pzriprnglem12  21482  znrrg  21555  mhppwdeg  22126  icopnfcnv  24919  icopnfhmeo  24920  lebnumii  24943  reparphti  24974  itg2const  25717  itg2monolem3  25729  bddibl  25817  dveflem  25956  mvth  25969  dvlipcn  25971  dvivthlem1  25985  dvfsumle  25998  dvfsumabs  26000  dvfsumlem2  26004  plyconst  26181  plyeq0lem  26185  plyco  26216  0dgrb  26221  coefv0  26223  vieta1  26289  aaliou3lem2  26320  tayl0  26338  taylply2  26344  taylply2OLD  26345  dvtaylp  26347  taylthlem2  26351  taylthlem2OLD  26352  radcnvlem1  26391  abelthlem1  26409  abelthlem2  26410  abelthlem3  26411  abelthlem7  26416  abelthlem8  26417  abelthlem9  26418  efper  26456  tangtx  26482  eflogeq  26579  logdivlti  26597  logcnlem4  26622  advlogexp  26632  cxpmul2  26666  dvcxp2  26718  cxpaddle  26729  cxpeq  26734  loglesqrt  26738  relogbexp  26757  ang180lem5  26790  isosctrlem2  26796  isosctrlem3  26797  heron  26815  2efiatan  26895  dvatan  26912  leibpi  26919  birthdaylem3  26930  jensenlem2  26965  logdiflbnd  26972  harmonicbnd4  26988  lgamgulmlem2  27007  lgamcvg2  27032  ftalem5  27054  basellem2  27059  basellem5  27062  basellem8  27065  0sgm  27121  muinv  27170  chpub  27197  logfaclbnd  27199  logexprlim  27202  dchrsum2  27245  sumdchr2  27247  bposlem1  27261  bposlem2  27262  bposlem5  27265  lgsquad2lem1  27361  lgsquad3  27364  2sqlem6  27400  2sqlem8  27403  chtppilim  27452  vmadivsum  27459  dchrisumlem1  27466  dchrisum0flblem1  27485  rpvmasum2  27489  dchrisum0re  27490  dchrisum0lem2a  27494  dchrisum0lem3  27496  rpvmasum  27503  mudivsum  27507  mulogsumlem  27508  vmalogdivsum2  27515  pntrsumo1  27542  pntrlog2bndlem2  27555  pntrlog2bndlem4  27557  pntrlog2bndlem5  27558  pntibndlem2  27568  pntlemc  27572  pntlemf  27582  ostth2lem2  27611  ostth2lem3  27612  ostth2lem4  27613  ostth2  27614  ostth3  27615  ttgcontlem1  28967  axpaschlem  29023  axcontlem2  29048  axcontlem4  29050  axcontlem8  29054  nmoub3i  30859  ubthlem2  30957  htthlem  31003  nmcexi  32112  nmopcoadji  32187  branmfn  32191  gsumind  33420  rearchi  33421  vietadeg1  33737  ccfldextdgrr  33832  nn0constr  33921  constrrecl  33929  constrimcl  33930  constrreinvcl  33932  constrinvcl  33933  constrresqrtcl  33937  constrabscl  33938  cos9thpiminplylem1  33942  madjusmdetlem4  33990  ccatmulgnn0dir  34702  ofcccat  34703  itgexpif  34766  hashreprin  34780  circlemeth  34800  lpadlem2  34840  subfacval2  35385  cvmliftlem2  35484  snmlff  35527  sinccvglem  35870  bcprod  35936  faclimlem1  35941  faclimlem2  35942  faclim2  35946  knoppndvlem14  36801  knoppndvlem15  36802  knoppndvlem16  36803  knoppndvlem18  36805  poimirlem29  37984  poimirlem30  37985  poimirlem31  37986  poimirlem32  37987  itg2addnclem  38006  areacirclem1  38043  areacirclem4  38046  cntotbnd  38131  lcmineqlem11  42492  lcmineqlem12  42493  aks4d1p1p7  42527  aks4d1p8d2  42538  hashscontpow1  42574  2ap1caineq  42598  sticksstones10  42608  sticksstones12a  42610  aks6d1c6lem1  42623  aks6d1c7lem1  42633  aks6d1c7  42637  oddnumth  42757  oexpreposd  42768  readvrec  42808  frlmvscadiccat  42965  fltnltalem  43109  3cubeslem2  43131  3cubeslem3r  43133  irrapxlem1  43268  irrapxlem4  43271  pell1qrgaplem  43319  reglogexpbas  43343  rmspecfund  43355  rmxy1  43368  rmxp1  43378  rmyp1  43379  rmxm1  43380  jm2.17a  43406  jm2.18  43434  jm2.23  43442  jm2.25  43445  jm2.16nn0  43450  relexpmulnn  44154  int-mul11d  44627  nzprmdif  44764  expgrowthi  44778  expgrowth  44780  binomcxplemdvbinom  44798  binomcxplemnotnn0  44801  sqrlearg  46001  fmul01  46028  fmul01lt1lem1  46032  0ellimcdiv  46095  dvxpaek  46386  dvnxpaek  46388  itgiccshift  46426  itgperiod  46427  itgsbtaddcnst  46428  stoweidlem11  46457  stoweidlem26  46472  stoweidlem38  46484  wallispilem4  46514  stirlinglem1  46520  stirlinglem3  46522  stirlinglem6  46525  stirlinglem7  46526  stirlinglem8  46527  stirlinglem10  46529  stirlinglem12  46531  dirkertrigeqlem3  46546  dirkertrigeq  46547  dirkercncflem1  46549  dirkercncflem2  46550  fourierdlem28  46581  fourierdlem30  46583  fourierdlem39  46592  fourierdlem47  46599  fourierdlem60  46612  fourierdlem61  46613  fourierdlem73  46625  fourierdlem83  46635  fourierdlem87  46639  etransclem14  46694  etransclem24  46704  etransclem25  46705  etransclem35  46715  smfmullem1  47237  sin3t  47335  cos3t  47336  sin5tlem1  47337  deccarry  47771  fpprwppr  48227  fpprwpprb  48228  logblt1b  49052  nn0sumshdiglem2  49110  itcovalpclem2  49159  itcovalt2lem1  49163  eenglngeehlnmlem1  49225  eenglngeehlnmlem2  49226  line2ylem  49239