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

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

Proof of Theorem mulid2d
StepHypRef Expression
1 addcld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 mulid2 10230 . 2 (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
31, 2syl 17 1 (𝜑 → (1 · 𝐴) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  wcel 2139  (class class class)co 6813  cc 10126  1c1 10129   · cmul 10133
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-mulcl 10190  ax-mulcom 10192  ax-mulass 10194  ax-distr 10195  ax-1rid 10198  ax-cnre 10201
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6816
This theorem is referenced by:  adddirp1d  10258  addid1  10408  mulsubfacd  10684  mulcand  10852  receu  10864  divdivdiv  10918  divcan5  10919  subrec  11046  ltrec  11097  recp1lt1  11113  nndivtr  11254  subhalfhalf  11458  xp1d2m1eqxm1d2  11478  gtndiv  11646  lincmb01cmp  12508  iccf1o  12509  ltdifltdiv  12829  modfrac  12877  negmod  12909  addmodid  12912  m1expcl2  13076  expgt1  13092  ltexp2a  13106  leexp2a  13110  binom3  13179  faclbnd  13271  faclbnd4lem4  13277  facavg  13282  bcval5  13299  cshweqrep  13767  sqrlem2  14183  absimle  14248  reccn2  14526  iseraltlem2  14612  iseraltlem3  14613  o1fsum  14744  abscvgcvg  14750  ackbijnn  14759  binom1p  14762  binom1dif  14764  incexclem  14767  incexc  14768  climcndslem1  14780  geomulcvg  14806  fprodsplit  14895  fallrisefac  14955  bpolysum  14983  bpolydiflem  14984  bpoly4  14989  efcllem  15007  ef01bndlem  15113  efieq1re  15128  eirrlem  15131  iddvds  15197  pwp1fsum  15316  oddpwp1fsum  15317  bitsfzolem  15358  bitsfzo  15359  rpmulgcd  15477  prmind2  15600  isprm5  15621  phiprm  15684  eulerthlem2  15689  fermltl  15691  hashgcdlem  15695  odzdvds  15702  powm2modprm  15710  modprm0  15712  pythagtriplem4  15726  pcexp  15766  4sqlem18  15868  vdwapun  15880  mulgnnass  17777  mulgnnassOLD  17778  odinv  18178  odadd2  18452  pgpfaclem2  18681  abvneg  19036  nrginvrcnlem  22696  nmoid  22747  blcvx  22802  icopnfcnv  22942  reparphti  22997  pcorevlem  23026  ncvsm1  23154  ncvspi  23156  cphipval2  23240  cphipval  23242  itg11  23657  itg2mulc  23713  itg2monolem1  23716  itgcnlem  23755  iblabs  23794  dvexp  23915  dvmptdiv  23936  dvef  23942  lhop1lem  23975  dvcvx  23982  dvfsumlem1  23988  dvfsumlem2  23989  dvfsumlem4  23991  dvfsum2  23996  plypow  24160  dgrcolem1  24228  vieta1lem2  24265  radcnvlem1  24366  radcnvlem2  24367  dvradcnv  24374  abelthlem2  24385  abelthlem6  24389  abelthlem7  24391  abelth2  24395  sinhalfpip  24443  sinhalfpim  24444  coshalfpip  24445  coshalfpim  24446  tangtx  24456  efif1olem4  24490  abslogle  24563  logdivlti  24565  advlog  24599  advlogexp  24600  logtayl  24605  cxpaddlelem  24691  cxpaddle  24692  affineequiv  24752  affineequiv2  24753  chordthmlem5  24762  dcubic2  24770  dcubic  24772  mcubic  24773  binom4  24776  dquartlem1  24777  quart1lem  24781  quart1  24782  quartlem1  24783  quart  24787  efiasin  24814  atantayl  24863  cvxcl  24910  scvxcvx  24911  lgamgulmlem5  24958  lgamcvg2  24980  lgam1  24989  wilthlem1  24993  wilthlem2  24994  basellem9  25014  fsumfldivdiaglem  25114  muinv  25118  chpub  25144  logexprlim  25149  mersenne  25151  perfectlem2  25154  dchrmulid2  25176  dchrptlem1  25188  dchrsum2  25192  sumdchr2  25194  bposlem2  25209  bposlem9  25216  lgsval2lem  25231  lgsval4a  25243  lgsneg1  25246  lgsdir2lem4  25252  lgsdir  25256  lgsmulsqcoprm  25267  lgsdirnn0  25268  lgsdinn0  25269  gausslemma2dlem1a  25289  gausslemma2dlem4  25293  gausslemma2dlem7  25297  gausslemma2d  25298  lgseisenlem1  25299  lgseisenlem2  25300  lgseisenlem4  25302  lgsquad2lem1  25308  2sqlem8  25350  chebbnd1lem3  25359  chpchtlim  25367  rplogsumlem1  25372  rplogsumlem2  25373  rpvmasumlem  25375  dchrmusum2  25382  dchrvmasum2lem  25384  dchrvmasumlem2  25386  dchrvmasumlem3  25387  dchrisum0flblem1  25396  mulog2sumlem2  25423  vmalogdivsum2  25426  2vmadivsumlem  25428  log2sumbnd  25432  selberglem2  25434  chpdifbndlem1  25441  selberg3lem1  25445  selberg4lem1  25448  pntrlog2bndlem2  25466  pntrlog2bndlem5  25469  pntpbnd1  25474  pntpbnd2  25475  pntibndlem2  25479  pntlemb  25485  pntlemr  25490  pntlemk  25494  pntlemo  25495  brbtwn2  25984  colinearalglem4  25988  ax5seglem3  26010  axbtwnid  26018  axpaschlem  26019  axeuclidlem  26041  axcontlem7  26049  axcontlem8  26050  nvm1  27829  nvpi  27831  nvmtri  27835  ipval2  27871  ipasslem1  27995  ipasslem4  27998  bcs2  28348  lnfnaddi  29211  nnmulge  29824  sqsscirc1  30263  indsum  30392  indsumin  30393  eulerpartlemgs2  30751  plymulx0  30933  logdivsqrle  31037  subfacp1lem6  31474  subfaclim  31477  cvxpconn  31531  cvxsconn  31532  resconn  31535  sinccvglem  31873  fwddifn0  32577  nn0prpwlem  32623  knoppndvlem9  32817  knoppndvlem14  32822  bj-bary1lem1  33472  mblfinlem3  33761  itg2addnclem3  33776  iblabsnc  33787  iblmulc2nc  33788  ftc1anclem6  33803  ftc1anclem7  33804  ftc1anclem8  33805  areacirclem1  33813  bfplem2  33935  bfp  33936  rrntotbnd  33948  irrapxlem5  37892  pellexlem2  37896  pellexlem6  37900  pellfundex  37952  jm2.19lem3  38060  jm2.25  38068  jm2.27c  38076  jm3.1lem2  38087  flcidc  38246  int-mul12d  38988  cvgdvgrat  39014  bccn1  39045  binomcxplemnotnn0  39057  fperiodmullem  40016  xralrple2  40068  fmul01lt1lem2  40320  mccllem  40332  reclimc  40388  cosknegpi  40583  dvsinax  40630  dvnxpaek  40660  dvnmul  40661  itgsinexp  40673  stoweidlem14  40734  stoweidlem26  40746  wallispilem4  40788  wallispilem5  40789  wallispi2lem1  40791  wallispi2  40793  stirlinglem1  40794  stirlinglem3  40796  stirlinglem4  40797  stirlinglem5  40798  stirlinglem6  40799  stirlinglem7  40800  stirlinglem10  40803  dirkertrigeqlem2  40819  dirkertrigeqlem3  40820  dirkercncflem2  40824  fourierdlem26  40853  fourierdlem41  40868  fourierdlem42  40869  fourierdlem56  40882  fourierdlem57  40883  fourierdlem58  40884  fourierdlem62  40888  fourierdlem64  40890  fourierdlem65  40891  fourierdlem95  40921  sqwvfoura  40948  sqwvfourb  40949  fouriersw  40951  etransclem23  40977  etransclem35  40989  etransclem46  41000  fmtnorec2lem  41964  fmtnorec3  41970  pwdif  42011  m1expoddALTV  42071  perfectALTVlem2  42141  ztprmneprm  42635  altgsumbc  42640  divge1b  42812  divgt1b  42813
  Copyright terms: Public domain W3C validator