MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulid1d Structured version   Visualization version   GIF version

Theorem mulid1d 10170
Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
addcld.1 (𝜑𝐴 ∈ ℂ)
Assertion
Ref Expression
mulid1d (𝜑 → (𝐴 · 1) = 𝐴)

Proof of Theorem mulid1d
StepHypRef Expression
1 addcld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 mulid1 10150 . 2 (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
31, 2syl 17 1 (𝜑 → (𝐴 · 1) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1596  wcel 2103  (class class class)co 6765  cc 10047  1c1 10050   · cmul 10054
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-mulcl 10111  ax-mulcom 10113  ax-mulass 10115  ax-distr 10116  ax-1rid 10119  ax-cnre 10122
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ral 3019  df-rex 3020  df-rab 3023  df-v 3306  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-br 4761  df-iota 5964  df-fv 6009  df-ov 6768
This theorem is referenced by:  muladd11  10319  muls1d  10604  divrec  10814  diveq1  10831  conjmul  10855  divelunit  12428  modid  12810  addmodlteq  12860  expadd  13017  leexp2r  13033  nnlesq  13083  sqoddm1div8  13143  faclbnd  13192  faclbnd2  13193  faclbnd4lem3  13197  faclbnd6  13201  facavg  13203  bcn0  13212  bcn1  13215  hashf1lem2  13353  hashfac  13355  reccn2  14447  iseraltlem2  14533  iseraltlem3  14534  hash2iun1dif1  14676  binom11  14684  harmonic  14711  trireciplem  14714  geoserg  14718  cvgrat  14735  fprodsplit  14816  fprodle  14847  fsumcube  14911  efzval  14952  tanhlt1  15010  tanaddlem  15016  tanadd  15017  cos01gt0  15041  absef  15047  1dvds  15119  3dvdsOLD  15176  bitsfzo  15280  bitsmod  15281  gcdmultiple  15392  sqgcd  15401  lcm1  15446  coprmdvds  15489  coprmdvdsOLD  15490  qredeu  15495  phiprmpw  15604  coprimeprodsq  15636  pc2dvds  15706  sumhash  15723  fldivp1  15724  pcfaclem  15725  prmpwdvds  15731  prmreclem1  15743  vdwlem3  15810  vdwlem9  15816  prmop1  15865  sylow2a  18155  odadd  18374  zsssubrg  19927  zringcyg  19962  prmirredlem  19964  mulgrhm2  19970  znrrg  20037  icopnfcnv  22863  icopnfhmeo  22864  lebnumii  22887  reparphti  22918  itg2const  23627  itg2monolem3  23639  bddibl  23726  dveflem  23862  mvth  23875  dvlipcn  23877  dvivthlem1  23891  dvfsumle  23904  dvfsumabs  23906  dvfsumlem2  23910  plyconst  24082  plyeq0lem  24086  plyco  24117  0dgrb  24122  coefv0  24124  vieta1  24187  aaliou3lem2  24218  tayl0  24236  taylply2  24242  dvtaylp  24244  taylthlem2  24248  radcnvlem1  24287  abelthlem1  24305  abelthlem2  24306  abelthlem3  24307  abelthlem7  24312  abelthlem8  24313  abelthlem9  24314  efper  24351  tangtx  24377  eflogeq  24468  logdivlti  24486  logcnlem4  24511  advlogexp  24521  cxpmul2  24555  dvcxp2  24602  cxpaddle  24613  cxpeq  24618  loglesqrt  24619  relogbexp  24638  ang180lem5  24663  isosctrlem2  24669  isosctrlem3  24670  heron  24685  2efiatan  24765  dvatan  24782  leibpi  24789  birthdaylem3  24800  jensenlem2  24834  logdiflbnd  24841  harmonicbnd4  24857  lgamgulmlem2  24876  lgamcvg2  24901  wilthlem2  24915  ftalem5  24923  basellem2  24928  basellem5  24931  basellem8  24934  0sgm  24990  muinv  25039  chpub  25065  logfaclbnd  25067  logexprlim  25070  dchrsum2  25113  sumdchr2  25115  bposlem1  25129  bposlem2  25130  bposlem5  25133  lgsquad2lem1  25229  lgsquad3  25232  2sqlem6  25268  2sqlem8  25271  chtppilim  25284  vmadivsum  25291  dchrisumlem1  25298  dchrisum0flblem1  25317  rpvmasum2  25321  dchrisum0re  25322  dchrisum0lem2a  25326  dchrisum0lem3  25328  rpvmasum  25335  mudivsum  25339  mulogsumlem  25340  vmalogdivsum2  25347  pntrsumo1  25374  pntrlog2bndlem2  25387  pntrlog2bndlem4  25389  pntrlog2bndlem5  25390  pntibndlem2  25400  pntlemc  25404  pntlemf  25414  ostth2lem2  25443  ostth2lem3  25444  ostth2lem4  25445  ostth2  25446  ostth3  25447  ttgcontlem1  25885  axpaschlem  25940  axcontlem2  25965  axcontlem4  25967  axcontlem8  25971  nmoub3i  27858  ubthlem2  27957  htthlem  28004  nmcexi  29115  nmopcoadji  29190  branmfn  29194  rearchi  30072  madjusmdetlem4  30126  ccatmulgnn0dir  30849  ofcccat  30850  itgexpif  30914  hashreprin  30928  circlemeth  30948  subfacval2  31397  cvmliftlem2  31496  snmlff  31539  sinccvglem  31794  bcprod  31852  faclimlem1  31857  faclimlem2  31858  faclim2  31862  knoppndvlem14  32743  knoppndvlem15  32744  knoppndvlem16  32745  knoppndvlem18  32747  poimirlem29  33670  poimirlem30  33671  poimirlem31  33672  poimirlem32  33673  itg2addnclem  33693  areacirclem1  33732  areacirclem4  33735  cntotbnd  33827  irrapxlem1  37805  irrapxlem4  37808  pell1qrgaplem  37856  reglogexpbas  37880  rmspecsqrtnqOLD  37890  rmspecfund  37893  rmxy1  37906  rmxp1  37916  rmyp1  37917  rmxm1  37918  jm2.17a  37946  jm2.18  37974  jm2.23  37982  jm2.25  37985  jm2.16nn0  37990  relexpmulnn  38420  int-mul11d  38904  nzprmdif  38937  expgrowthi  38951  expgrowth  38953  binomcxplemdvbinom  38971  binomcxplemnotnn0  38974  sqrlearg  40200  fmul01  40232  fmul01lt1lem1  40236  0ellimcdiv  40301  dvxpaek  40575  dvnxpaek  40577  itgiccshift  40616  itgperiod  40617  itgsbtaddcnst  40618  stoweidlem11  40648  stoweidlem26  40663  stoweidlem38  40675  wallispilem4  40705  stirlinglem1  40711  stirlinglem3  40713  stirlinglem6  40716  stirlinglem7  40717  stirlinglem8  40718  stirlinglem10  40720  stirlinglem12  40722  dirkertrigeqlem3  40737  dirkertrigeq  40738  dirkercncflem1  40740  dirkercncflem2  40741  fourierdlem28  40772  fourierdlem30  40774  fourierdlem39  40783  fourierdlem47  40790  fourierdlem60  40803  fourierdlem61  40804  fourierdlem73  40816  fourierdlem83  40826  fourierdlem87  40830  etransclem14  40885  etransclem24  40895  etransclem25  40896  etransclem35  40906  smfmullem1  41421  deccarry  41748  pwdif  41928  pwm1geoserALT  41929  logblt1b  42785  nn0sumshdiglem2  42843
  Copyright terms: Public domain W3C validator