Theorem mulridd 11149

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024  1c1 11027   · cmul 11031

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 2115  ax-9 2123  ax-ext 2708  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-mulcl 11088  ax-mulcom 11090  ax-mulass 11092  ax-distr 11093  ax-1rid 11096  ax-cnre 11099

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 2715  df-cleq 2728  df-clel 2811  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361

This theorem is referenced by:  muladd11  11303  muls1d  11597  divrec  11812  diveq1  11826  conjmul  11858  divelunit  13410  modid  13816  addmodlteq  13869  expadd  14027  leexp2r  14097  nnlesq  14128  sqoddm1div8  14166  faclbnd  14213  faclbnd2  14214  faclbnd4lem3  14218  faclbnd6  14222  facavg  14224  bcn0  14233  bcn1  14236  hashf1lem2  14379  hashfac  14381  reccn2  15520  iseraltlem2  15606  iseraltlem3  15607  hash2iun1dif1  15747  binom11  15755  harmonic  15782  trireciplem  15785  geoserg  15789  pwdif  15791  pwm1geoser  15792  cvgrat  15806  fprodsplit  15889  fprodle  15919  fsumcube  15983  efzval  16027  tanhlt1  16085  tanaddlem  16091  tanadd  16092  cos01gt0  16116  absef  16122  1dvds  16197  bitsfzo  16362  bitsmod  16363  sqgcd  16489  expgcd  16490  lcm1  16537  coprmdvds  16580  qredeu  16585  phiprmpw  16703  coprimeprodsq  16736  pc2dvds  16807  sumhash  16824  fldivp1  16825  pcfaclem  16826  prmpwdvds  16832  prmreclem1  16844  vdwlem3  16911  vdwlem9  16917  prmop1  16966  sylow2a  19548  odadd  19779  zsssubrg  21380  zringcyg  21424  prmirredlem  21427  mulgrhm2  21433  pzriprnglem6  21441  pzriprnglem12  21447  znrrg  21520  mhppwdeg  22093  icopnfcnv  24896  icopnfhmeo  24897  lebnumii  24921  reparphti  24952  reparphtiOLD  24953  itg2const  25697  itg2monolem3  25709  bddibl  25797  dveflem  25939  mvth  25953  dvlipcn  25955  dvivthlem1  25969  dvfsumle  25982  dvfsumleOLD  25983  dvfsumabs  25985  dvfsumlem2  25989  dvfsumlem2OLD  25990  plyconst  26167  plyeq0lem  26171  plyco  26202  0dgrb  26207  coefv0  26209  vieta1  26276  aaliou3lem2  26307  tayl0  26325  taylply2  26331  taylply2OLD  26332  dvtaylp  26334  taylthlem2  26338  taylthlem2OLD  26339  radcnvlem1  26378  abelthlem1  26397  abelthlem2  26398  abelthlem3  26399  abelthlem7  26404  abelthlem8  26405  abelthlem9  26406  efper  26444  tangtx  26470  eflogeq  26567  logdivlti  26585  logcnlem4  26610  advlogexp  26620  cxpmul2  26654  dvcxp2  26706  cxpaddle  26718  cxpeq  26723  loglesqrt  26727  relogbexp  26746  ang180lem5  26779  isosctrlem2  26785  isosctrlem3  26786  heron  26804  2efiatan  26884  dvatan  26901  leibpi  26908  birthdaylem3  26919  jensenlem2  26954  logdiflbnd  26961  harmonicbnd4  26977  lgamgulmlem2  26996  lgamcvg2  27021  ftalem5  27043  basellem2  27048  basellem5  27051  basellem8  27054  0sgm  27110  muinv  27159  chpub  27187  logfaclbnd  27189  logexprlim  27192  dchrsum2  27235  sumdchr2  27237  bposlem1  27251  bposlem2  27252  bposlem5  27255  lgsquad2lem1  27351  lgsquad3  27354  2sqlem6  27390  2sqlem8  27393  chtppilim  27442  vmadivsum  27449  dchrisumlem1  27456  dchrisum0flblem1  27475  rpvmasum2  27479  dchrisum0re  27480  dchrisum0lem2a  27484  dchrisum0lem3  27486  rpvmasum  27493  mudivsum  27497  mulogsumlem  27498  vmalogdivsum2  27505  pntrsumo1  27532  pntrlog2bndlem2  27545  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  pntibndlem2  27558  pntlemc  27562  pntlemf  27572  ostth2lem2  27601  ostth2lem3  27602  ostth2lem4  27603  ostth2  27604  ostth3  27605  ttgcontlem1  28957  axpaschlem  29013  axcontlem2  29038  axcontlem4  29040  axcontlem8  29044  nmoub3i  30848  ubthlem2  30946  htthlem  30992  nmcexi  32101  nmopcoadji  32176  branmfn  32180  gsumind  33426  rearchi  33427  vietadeg1  33734  ccfldextdgrr  33829  nn0constr  33918  constrrecl  33926  constrimcl  33927  constrreinvcl  33929  constrinvcl  33930  constrresqrtcl  33934  constrabscl  33935  cos9thpiminplylem1  33939  madjusmdetlem4  33987  ccatmulgnn0dir  34699  ofcccat  34700  itgexpif  34763  hashreprin  34777  circlemeth  34797  lpadlem2  34837  subfacval2  35381  cvmliftlem2  35480  snmlff  35523  sinccvglem  35866  bcprod  35932  faclimlem1  35937  faclimlem2  35938  faclim2  35942  knoppndvlem14  36725  knoppndvlem15  36726  knoppndvlem16  36727  knoppndvlem18  36729  poimirlem29  37850  poimirlem30  37851  poimirlem31  37852  poimirlem32  37853  itg2addnclem  37872  areacirclem1  37909  areacirclem4  37912  cntotbnd  37997  lcmineqlem11  42293  lcmineqlem12  42294  aks4d1p1p7  42328  aks4d1p8d2  42339  hashscontpow1  42375  2ap1caineq  42399  sticksstones10  42409  sticksstones12a  42411  aks6d1c6lem1  42424  aks6d1c7lem1  42434  aks6d1c7  42438  oddnumth  42566  oexpreposd  42577  readvrec  42617  frlmvscadiccat  42761  fltnltalem  42905  3cubeslem2  42927  3cubeslem3r  42929  irrapxlem1  43064  irrapxlem4  43067  pell1qrgaplem  43115  reglogexpbas  43139  rmspecfund  43151  rmxy1  43164  rmxp1  43174  rmyp1  43175  rmxm1  43176  jm2.17a  43202  jm2.18  43230  jm2.23  43238  jm2.25  43241  jm2.16nn0  43246  relexpmulnn  43950  int-mul11d  44423  nzprmdif  44560  expgrowthi  44574  expgrowth  44576  binomcxplemdvbinom  44594  binomcxplemnotnn0  44597  sqrlearg  45799  fmul01  45826  fmul01lt1lem1  45830  0ellimcdiv  45893  dvxpaek  46184  dvnxpaek  46186  itgiccshift  46224  itgperiod  46225  itgsbtaddcnst  46226  stoweidlem11  46255  stoweidlem26  46270  stoweidlem38  46282  wallispilem4  46312  stirlinglem1  46318  stirlinglem3  46320  stirlinglem6  46323  stirlinglem7  46324  stirlinglem8  46325  stirlinglem10  46327  stirlinglem12  46329  dirkertrigeqlem3  46344  dirkertrigeq  46345  dirkercncflem1  46347  dirkercncflem2  46348  fourierdlem28  46379  fourierdlem30  46381  fourierdlem39  46390  fourierdlem47  46397  fourierdlem60  46410  fourierdlem61  46411  fourierdlem73  46423  fourierdlem83  46433  fourierdlem87  46437  etransclem14  46492  etransclem24  46502  etransclem25  46503  etransclem35  46513  smfmullem1  47035  deccarry  47557  fpprwppr  47985  fpprwpprb  47986  logblt1b  48810  nn0sumshdiglem2  48868  itcovalpclem2  48917  itcovalt2lem1  48921  eenglngeehlnmlem1  48983  eenglngeehlnmlem2  48984  line2ylem  48997