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

Theorem mulid1d 10095
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 10075 . 2 (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
31, 2syl 17 1 (𝜑 → (𝐴 · 1) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030  (class class class)co 6690  cc 9972  1c1 9975   · cmul 9979
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-mulcl 10036  ax-mulcom 10038  ax-mulass 10040  ax-distr 10041  ax-1rid 10044  ax-cnre 10047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693
This theorem is referenced by:  muladd11  10244  muls1d  10529  divrec  10739  diveq1  10756  conjmul  10780  divelunit  12352  modid  12735  addmodlteq  12785  expadd  12942  leexp2r  12958  nnlesq  13008  sqoddm1div8  13068  faclbnd  13117  faclbnd2  13118  faclbnd4lem3  13122  faclbnd6  13126  facavg  13128  bcn0  13137  bcn1  13140  hashf1lem2  13278  hashfac  13280  reccn2  14371  iseraltlem2  14457  iseraltlem3  14458  hash2iun1dif1  14600  binom11  14608  harmonic  14635  trireciplem  14638  geoserg  14642  cvgrat  14659  fprodsplit  14740  fprodle  14771  fsumcube  14835  efzval  14876  tanhlt1  14934  tanaddlem  14940  tanadd  14941  cos01gt0  14965  absef  14971  1dvds  15043  3dvdsOLD  15100  bitsfzo  15204  bitsmod  15205  gcdmultiple  15316  sqgcd  15325  lcm1  15370  coprmdvds  15413  coprmdvdsOLD  15414  qredeu  15419  phiprmpw  15528  coprimeprodsq  15560  pc2dvds  15630  sumhash  15647  fldivp1  15648  pcfaclem  15649  prmpwdvds  15655  prmreclem1  15667  vdwlem3  15734  vdwlem9  15740  prmop1  15789  sylow2a  18080  odadd  18299  zsssubrg  19852  zringcyg  19887  prmirredlem  19889  mulgrhm2  19895  znrrg  19962  icopnfcnv  22788  icopnfhmeo  22789  lebnumii  22812  reparphti  22843  itg2const  23552  itg2monolem3  23564  bddibl  23651  dveflem  23787  mvth  23800  dvlipcn  23802  dvivthlem1  23816  dvfsumle  23829  dvfsumabs  23831  dvfsumlem2  23835  plyconst  24007  plyeq0lem  24011  plyco  24042  0dgrb  24047  coefv0  24049  vieta1  24112  aaliou3lem2  24143  tayl0  24161  taylply2  24167  dvtaylp  24169  taylthlem2  24173  radcnvlem1  24212  abelthlem1  24230  abelthlem2  24231  abelthlem3  24232  abelthlem7  24237  abelthlem8  24238  abelthlem9  24239  efper  24276  tangtx  24302  eflogeq  24393  logdivlti  24411  logcnlem4  24436  advlogexp  24446  cxpmul2  24480  dvcxp2  24527  cxpaddle  24538  cxpeq  24543  loglesqrt  24544  relogbexp  24563  ang180lem5  24588  isosctrlem2  24594  isosctrlem3  24595  heron  24610  2efiatan  24690  dvatan  24707  leibpi  24714  birthdaylem3  24725  jensenlem2  24759  logdiflbnd  24766  harmonicbnd4  24782  lgamgulmlem2  24801  lgamcvg2  24826  wilthlem2  24840  ftalem5  24848  basellem2  24853  basellem5  24856  basellem8  24859  0sgm  24915  muinv  24964  chpub  24990  logfaclbnd  24992  logexprlim  24995  dchrsum2  25038  sumdchr2  25040  bposlem1  25054  bposlem2  25055  bposlem5  25058  lgsquad2lem1  25154  lgsquad3  25157  2sqlem6  25193  2sqlem8  25196  chtppilim  25209  vmadivsum  25216  dchrisumlem1  25223  dchrisum0flblem1  25242  rpvmasum2  25246  dchrisum0re  25247  dchrisum0lem2a  25251  dchrisum0lem3  25253  rpvmasum  25260  mudivsum  25264  mulogsumlem  25265  vmalogdivsum2  25272  pntrsumo1  25299  pntrlog2bndlem2  25312  pntrlog2bndlem4  25314  pntrlog2bndlem5  25315  pntibndlem2  25325  pntlemc  25329  pntlemf  25339  ostth2lem2  25368  ostth2lem3  25369  ostth2lem4  25370  ostth2  25371  ostth3  25372  ttgcontlem1  25810  axpaschlem  25865  axcontlem2  25890  axcontlem4  25892  axcontlem8  25896  nmoub3i  27756  ubthlem2  27855  htthlem  27902  nmcexi  29013  nmopcoadji  29088  branmfn  29092  rearchi  29970  madjusmdetlem4  30024  ccatmulgnn0dir  30747  ofcccat  30748  itgexpif  30812  hashreprin  30826  circlemeth  30846  subfacval2  31295  cvmliftlem2  31394  snmlff  31437  sinccvglem  31692  bcprod  31750  faclimlem1  31755  faclimlem2  31756  faclim2  31760  knoppndvlem14  32641  knoppndvlem15  32642  knoppndvlem16  32643  knoppndvlem18  32645  poimirlem29  33568  poimirlem30  33569  poimirlem31  33570  poimirlem32  33571  itg2addnclem  33591  areacirclem1  33630  areacirclem4  33633  cntotbnd  33725  irrapxlem1  37703  irrapxlem4  37706  pell1qrgaplem  37754  reglogexpbas  37778  rmspecsqrtnqOLD  37788  rmspecfund  37791  rmxy1  37804  rmxp1  37814  rmyp1  37815  rmxm1  37816  jm2.17a  37844  jm2.18  37872  jm2.23  37880  jm2.25  37883  jm2.16nn0  37888  relexpmulnn  38318  int-mul11d  38802  nzprmdif  38835  expgrowthi  38849  expgrowth  38851  binomcxplemdvbinom  38869  binomcxplemnotnn0  38872  sqrlearg  40098  fmul01  40130  fmul01lt1lem1  40134  0ellimcdiv  40199  dvxpaek  40473  dvnxpaek  40475  itgiccshift  40514  itgperiod  40515  itgsbtaddcnst  40516  stoweidlem11  40546  stoweidlem26  40561  stoweidlem38  40573  wallispilem4  40603  stirlinglem1  40609  stirlinglem3  40611  stirlinglem6  40614  stirlinglem7  40615  stirlinglem8  40616  stirlinglem10  40618  stirlinglem12  40620  dirkertrigeqlem3  40635  dirkertrigeq  40636  dirkercncflem1  40638  dirkercncflem2  40639  fourierdlem28  40670  fourierdlem30  40672  fourierdlem39  40681  fourierdlem47  40688  fourierdlem60  40701  fourierdlem61  40702  fourierdlem73  40714  fourierdlem83  40724  fourierdlem87  40728  etransclem14  40783  etransclem24  40793  etransclem25  40794  etransclem35  40804  smfmullem1  41319  deccarry  41646  pwdif  41826  pwm1geoserALT  41827  logblt1b  42683  nn0sumshdiglem2  42741
  Copyright terms: Public domain W3C validator