Theorem mulridd 11126

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  (class class class)co 7346  ℂcc 11001  1c1 11004   · cmul 11008

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-resscn 11060  ax-1cn 11061  ax-icn 11062  ax-addcl 11063  ax-mulcl 11065  ax-mulcom 11067  ax-mulass 11069  ax-distr 11070  ax-1rid 11073  ax-cnre 11076

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349

This theorem is referenced by:  muladd11  11280  muls1d  11574  divrec  11789  diveq1  11803  conjmul  11835  divelunit  13391  modid  13797  addmodlteq  13850  expadd  14008  leexp2r  14078  nnlesq  14109  sqoddm1div8  14147  faclbnd  14194  faclbnd2  14195  faclbnd4lem3  14199  faclbnd6  14203  facavg  14205  bcn0  14214  bcn1  14217  hashf1lem2  14360  hashfac  14362  reccn2  15501  iseraltlem2  15587  iseraltlem3  15588  hash2iun1dif1  15728  binom11  15736  harmonic  15763  trireciplem  15766  geoserg  15770  pwdif  15772  pwm1geoser  15773  cvgrat  15787  fprodsplit  15870  fprodle  15900  fsumcube  15964  efzval  16008  tanhlt1  16066  tanaddlem  16072  tanadd  16073  cos01gt0  16097  absef  16103  1dvds  16178  bitsfzo  16343  bitsmod  16344  sqgcd  16470  expgcd  16471  lcm1  16518  coprmdvds  16561  qredeu  16566  phiprmpw  16684  coprimeprodsq  16717  pc2dvds  16788  sumhash  16805  fldivp1  16806  pcfaclem  16807  prmpwdvds  16813  prmreclem1  16825  vdwlem3  16892  vdwlem9  16898  prmop1  16947  sylow2a  19529  odadd  19760  zsssubrg  21360  zringcyg  21404  prmirredlem  21407  mulgrhm2  21413  pzriprnglem6  21421  pzriprnglem12  21427  znrrg  21500  mhppwdeg  22063  icopnfcnv  24865  icopnfhmeo  24866  lebnumii  24890  reparphti  24921  reparphtiOLD  24922  itg2const  25666  itg2monolem3  25678  bddibl  25766  dveflem  25908  mvth  25922  dvlipcn  25924  dvivthlem1  25938  dvfsumle  25951  dvfsumleOLD  25952  dvfsumabs  25954  dvfsumlem2  25958  dvfsumlem2OLD  25959  plyconst  26136  plyeq0lem  26140  plyco  26171  0dgrb  26176  coefv0  26178  vieta1  26245  aaliou3lem2  26276  tayl0  26294  taylply2  26300  taylply2OLD  26301  dvtaylp  26303  taylthlem2  26307  taylthlem2OLD  26308  radcnvlem1  26347  abelthlem1  26366  abelthlem2  26367  abelthlem3  26368  abelthlem7  26373  abelthlem8  26374  abelthlem9  26375  efper  26413  tangtx  26439  eflogeq  26536  logdivlti  26554  logcnlem4  26579  advlogexp  26589  cxpmul2  26623  dvcxp2  26675  cxpaddle  26687  cxpeq  26692  loglesqrt  26696  relogbexp  26715  ang180lem5  26748  isosctrlem2  26754  isosctrlem3  26755  heron  26773  2efiatan  26853  dvatan  26870  leibpi  26877  birthdaylem3  26888  jensenlem2  26923  logdiflbnd  26930  harmonicbnd4  26946  lgamgulmlem2  26965  lgamcvg2  26990  ftalem5  27012  basellem2  27017  basellem5  27020  basellem8  27023  0sgm  27079  muinv  27128  chpub  27156  logfaclbnd  27158  logexprlim  27161  dchrsum2  27204  sumdchr2  27206  bposlem1  27220  bposlem2  27221  bposlem5  27224  lgsquad2lem1  27320  lgsquad3  27323  2sqlem6  27359  2sqlem8  27362  chtppilim  27411  vmadivsum  27418  dchrisumlem1  27425  dchrisum0flblem1  27444  rpvmasum2  27448  dchrisum0re  27449  dchrisum0lem2a  27453  dchrisum0lem3  27455  rpvmasum  27462  mudivsum  27466  mulogsumlem  27467  vmalogdivsum2  27474  pntrsumo1  27501  pntrlog2bndlem2  27514  pntrlog2bndlem4  27516  pntrlog2bndlem5  27517  pntibndlem2  27527  pntlemc  27531  pntlemf  27541  ostth2lem2  27570  ostth2lem3  27571  ostth2lem4  27572  ostth2  27573  ostth3  27574  ttgcontlem1  28861  axpaschlem  28916  axcontlem2  28941  axcontlem4  28943  axcontlem8  28947  nmoub3i  30748  ubthlem2  30846  htthlem  30892  nmcexi  32001  nmopcoadji  32076  branmfn  32080  gsumind  33305  rearchi  33306  ccfldextdgrr  33680  nn0constr  33769  constrrecl  33777  constrimcl  33778  constrreinvcl  33780  constrinvcl  33781  constrresqrtcl  33785  constrabscl  33786  cos9thpiminplylem1  33790  madjusmdetlem4  33838  ccatmulgnn0dir  34550  ofcccat  34551  itgexpif  34614  hashreprin  34628  circlemeth  34648  lpadlem2  34688  subfacval2  35219  cvmliftlem2  35318  snmlff  35361  sinccvglem  35704  bcprod  35770  faclimlem1  35775  faclimlem2  35776  faclim2  35780  knoppndvlem14  36558  knoppndvlem15  36559  knoppndvlem16  36560  knoppndvlem18  36562  poimirlem29  37688  poimirlem30  37689  poimirlem31  37690  poimirlem32  37691  itg2addnclem  37710  areacirclem1  37747  areacirclem4  37750  cntotbnd  37835  lcmineqlem11  42071  lcmineqlem12  42072  aks4d1p1p7  42106  aks4d1p8d2  42117  hashscontpow1  42153  2ap1caineq  42177  sticksstones10  42187  sticksstones12a  42189  aks6d1c6lem1  42202  aks6d1c7lem1  42212  aks6d1c7  42216  oddnumth  42343  oexpreposd  42354  readvrec  42394  frlmvscadiccat  42538  fltnltalem  42694  3cubeslem2  42717  3cubeslem3r  42719  irrapxlem1  42854  irrapxlem4  42857  pell1qrgaplem  42905  reglogexpbas  42929  rmspecfund  42941  rmxy1  42954  rmxp1  42964  rmyp1  42965  rmxm1  42966  jm2.17a  42992  jm2.18  43020  jm2.23  43028  jm2.25  43031  jm2.16nn0  43036  relexpmulnn  43741  int-mul11d  44214  nzprmdif  44351  expgrowthi  44365  expgrowth  44367  binomcxplemdvbinom  44385  binomcxplemnotnn0  44388  sqrlearg  45592  fmul01  45619  fmul01lt1lem1  45623  0ellimcdiv  45686  dvxpaek  45977  dvnxpaek  45979  itgiccshift  46017  itgperiod  46018  itgsbtaddcnst  46019  stoweidlem11  46048  stoweidlem26  46063  stoweidlem38  46075  wallispilem4  46105  stirlinglem1  46111  stirlinglem3  46113  stirlinglem6  46116  stirlinglem7  46117  stirlinglem8  46118  stirlinglem10  46120  stirlinglem12  46122  dirkertrigeqlem3  46137  dirkertrigeq  46138  dirkercncflem1  46140  dirkercncflem2  46141  fourierdlem28  46172  fourierdlem30  46174  fourierdlem39  46183  fourierdlem47  46190  fourierdlem60  46203  fourierdlem61  46204  fourierdlem73  46216  fourierdlem83  46226  fourierdlem87  46230  etransclem14  46285  etransclem24  46295  etransclem25  46296  etransclem35  46306  smfmullem1  46828  deccarry  47341  fpprwppr  47769  fpprwpprb  47770  logblt1b  48595  nn0sumshdiglem2  48653  itcovalpclem2  48702  itcovalt2lem1  48706  eenglngeehlnmlem1  48768  eenglngeehlnmlem2  48769  line2ylem  48782