Theorem mulridd 11160

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034  1c1 11037   · cmul 11041

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-mulcl 11098  ax-mulcom 11100  ax-mulass 11102  ax-distr 11103  ax-1rid 11106  ax-cnre 11109

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366

This theorem is referenced by:  muladd11  11314  muls1d  11608  divrec  11823  diveq1  11837  conjmul  11870  divelunit  13445  modid  13853  addmodlteq  13906  expadd  14064  leexp2r  14134  nnlesq  14165  sqoddm1div8  14203  faclbnd  14250  faclbnd2  14251  faclbnd4lem3  14255  faclbnd6  14259  facavg  14261  bcn0  14270  bcn1  14273  hashf1lem2  14416  hashfac  14418  reccn2  15557  iseraltlem2  15643  iseraltlem3  15644  fsumconst1  15751  hash2iun1dif1  15785  indsumhash  15790  binom11  15795  harmonic  15822  trireciplem  15825  geoserg  15829  pwdif  15831  pwm1geoser  15832  cvgrat  15846  fprodsplit  15929  fprodle  15959  fsumcube  16023  efzval  16067  tanhlt1  16125  tanaddlem  16131  tanadd  16132  cos01gt0  16156  absef  16162  1dvds  16237  bitsfzo  16402  bitsmod  16403  sqgcd  16529  expgcd  16530  lcm1  16577  coprmdvds  16620  qredeu  16625  phiprmpw  16744  coprimeprodsq  16777  pc2dvds  16848  sumhash  16865  fldivp1  16866  pcfaclem  16867  prmpwdvds  16873  prmreclem1  16885  vdwlem3  16952  vdwlem9  16958  prmop1  17007  sylow2a  19592  odadd  19823  zsssubrg  21407  zringcyg  21451  prmirredlem  21454  mulgrhm2  21460  pzriprnglem6  21468  pzriprnglem12  21474  znrrg  21547  mhppwdeg  22145  icopnfcnv  24934  icopnfhmeo  24935  lebnumii  24958  reparphti  24989  itg2const  25732  itg2monolem3  25744  bddibl  25832  dveflem  25971  mvth  25984  dvlipcn  25986  dvivthlem1  26000  dvfsumle  26013  dvfsumabs  26015  dvfsumlem2  26019  plyconst  26196  plyeq0lem  26200  plyco  26231  0dgrb  26236  coefv0  26238  vieta1  26303  aaliou3lem2  26334  tayl0  26352  taylply2  26358  dvtaylp  26360  taylthlem2  26364  radcnvlem1  26403  abelthlem1  26421  abelthlem2  26422  abelthlem3  26423  abelthlem7  26428  abelthlem8  26429  abelthlem9  26430  efper  26468  tangtx  26494  eflogeq  26591  logdivlti  26609  logcnlem4  26634  advlogexp  26644  cxpmul2  26678  dvcxp2  26730  cxpaddle  26741  cxpeq  26746  loglesqrt  26750  relogbexp  26769  ang180lem5  26802  isosctrlem2  26808  isosctrlem3  26809  heron  26827  2efiatan  26907  dvatan  26924  leibpi  26931  birthdaylem3  26942  jensenlem2  26976  logdiflbnd  26983  harmonicbnd4  26999  lgamgulmlem2  27018  lgamcvg2  27043  ftalem5  27065  basellem2  27070  basellem5  27073  basellem8  27076  0sgm  27132  muinv  27181  chpub  27208  logfaclbnd  27210  logexprlim  27213  dchrsum2  27256  sumdchr2  27258  bposlem1  27272  bposlem2  27273  bposlem5  27276  lgsquad2lem1  27372  lgsquad3  27375  2sqlem6  27411  2sqlem8  27414  chtppilim  27463  vmadivsum  27470  dchrisumlem1  27477  dchrisum0flblem1  27496  rpvmasum2  27500  dchrisum0re  27501  dchrisum0lem2a  27505  dchrisum0lem3  27507  rpvmasum  27514  mudivsum  27518  mulogsumlem  27519  vmalogdivsum2  27526  pntrsumo1  27553  pntrlog2bndlem2  27566  pntrlog2bndlem4  27568  pntrlog2bndlem5  27569  pntibndlem2  27579  pntlemc  27583  pntlemf  27593  ostth2lem2  27622  ostth2lem3  27623  ostth2lem4  27624  ostth2  27625  ostth3  27626  ttgcontlem1  28978  axpaschlem  29034  axcontlem2  29059  axcontlem4  29061  axcontlem8  29065  nmoub3i  30869  ubthlem2  30967  htthlem  31013  nmcexi  32122  nmopcoadji  32197  branmfn  32201  gsumind  33435  rearchi  33436  vietadeg1  33769  ccfldextdgrr  33863  nn0constr  33952  constrrecl  33960  constrimcl  33961  constrreinvcl  33963  constrinvcl  33964  constrresqrtcl  33968  constrabscl  33969  cos9thpiminplylem1  33973  madjusmdetlem4  34021  ccatmulgnn0dir  34733  ofcccat  34734  itgexpif  34797  hashreprin  34811  circlemeth  34831  lpadlem2  34871  subfacval2  35422  cvmliftlem2  35521  snmlff  35564  sinccvglem  35907  bcprod  35973  faclimlem1  35978  faclimlem2  35979  faclim2  35983  knoppndvlem14  36838  knoppndvlem15  36839  knoppndvlem16  36840  knoppndvlem18  36842  poimirlem29  38023  poimirlem30  38024  poimirlem31  38025  poimirlem32  38026  itg2addnclem  38045  areacirclem1  38082  areacirclem4  38085  cntotbnd  38170  lcmineqlem11  42531  lcmineqlem12  42532  aks4d1p1p7  42566  aks4d1p8d2  42577  hashscontpow1  42613  2ap1caineq  42637  sticksstones10  42647  sticksstones12a  42649  aks6d1c6lem1  42662  aks6d1c7lem1  42672  aks6d1c7  42676  oddnumth  42795  oexpreposd  42806  readvrec  42846  frlmvscadiccat  43003  fltnltalem  43119  3cubeslem2  43141  3cubeslem3r  43143  irrapxlem1  43274  irrapxlem4  43277  pell1qrgaplem  43325  reglogexpbas  43349  rmspecfund  43361  rmxy1  43374  rmxp1  43384  rmyp1  43385  rmxm1  43386  jm2.17a  43412  jm2.18  43440  jm2.23  43448  jm2.25  43451  jm2.16nn0  43456  relexpmulnn  44160  int-mul11d  44633  nzprmdif  44770  expgrowthi  44784  expgrowth  44786  binomcxplemdvbinom  44804  binomcxplemnotnn0  44807  sqrlearg  46005  fmul01  46032  fmul01lt1lem1  46036  0ellimcdiv  46099  dvxpaek  46390  dvnxpaek  46392  itgiccshift  46430  itgperiod  46431  itgsbtaddcnst  46432  stoweidlem11  46461  stoweidlem26  46476  stoweidlem38  46488  wallispilem4  46518  stirlinglem1  46524  stirlinglem3  46526  stirlinglem6  46529  stirlinglem7  46530  stirlinglem8  46531  stirlinglem10  46533  stirlinglem12  46535  dirkertrigeqlem3  46550  dirkertrigeq  46551  dirkercncflem1  46553  dirkercncflem2  46554  fourierdlem28  46585  fourierdlem30  46587  fourierdlem39  46596  fourierdlem47  46603  fourierdlem60  46616  fourierdlem61  46617  fourierdlem73  46629  fourierdlem83  46639  fourierdlem87  46643  etransclem14  46698  etransclem24  46708  etransclem25  46709  etransclem35  46719  smfmullem1  47241  sin3t  47341  cos3t  47342  sin5tlem1  47343  deccarry  47781  fpprwppr  48237  fpprwpprb  48238  logblt1b  49062  nn0sumshdiglem2  49120  itcovalpclem2  49169  itcovalt2lem1  49173  eenglngeehlnmlem1  49235  eenglngeehlnmlem2  49236  line2ylem  49249