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  37846  poimirlem30  37847  poimirlem31  37848  poimirlem32  37849  itg2addnclem  37868  areacirclem1  37905  areacirclem4  37908  cntotbnd  37993  lcmineqlem11  42289  lcmineqlem12  42290  aks4d1p1p7  42324  aks4d1p8d2  42335  hashscontpow1  42371  2ap1caineq  42395  sticksstones10  42405  sticksstones12a  42407  aks6d1c6lem1  42420  aks6d1c7lem1  42430  aks6d1c7  42434  oddnumth  42562  oexpreposd  42573  readvrec  42613  frlmvscadiccat  42757  fltnltalem  42901  3cubeslem2  42923  3cubeslem3r  42925  irrapxlem1  43060  irrapxlem4  43063  pell1qrgaplem  43111  reglogexpbas  43135  rmspecfund  43147  rmxy1  43160  rmxp1  43170  rmyp1  43171  rmxm1  43172  jm2.17a  43198  jm2.18  43226  jm2.23  43234  jm2.25  43237  jm2.16nn0  43242  relexpmulnn  43946  int-mul11d  44419  nzprmdif  44556  expgrowthi  44570  expgrowth  44572  binomcxplemdvbinom  44590  binomcxplemnotnn0  44593  sqrlearg  45795  fmul01  45822  fmul01lt1lem1  45826  0ellimcdiv  45889  dvxpaek  46180  dvnxpaek  46182  itgiccshift  46220  itgperiod  46221  itgsbtaddcnst  46222  stoweidlem11  46251  stoweidlem26  46266  stoweidlem38  46278  wallispilem4  46308  stirlinglem1  46314  stirlinglem3  46316  stirlinglem6  46319  stirlinglem7  46320  stirlinglem8  46321  stirlinglem10  46323  stirlinglem12  46325  dirkertrigeqlem3  46340  dirkertrigeq  46341  dirkercncflem1  46343  dirkercncflem2  46344  fourierdlem28  46375  fourierdlem30  46377  fourierdlem39  46386  fourierdlem47  46393  fourierdlem60  46406  fourierdlem61  46407  fourierdlem73  46419  fourierdlem83  46429  fourierdlem87  46433  etransclem14  46488  etransclem24  46498  etransclem25  46499  etransclem35  46509  smfmullem1  47031  deccarry  47553  fpprwppr  47981  fpprwpprb  47982  logblt1b  48806  nn0sumshdiglem2  48864  itcovalpclem2  48913  itcovalt2lem1  48917  eenglngeehlnmlem1  48979  eenglngeehlnmlem2  48980  line2ylem  48993