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

Theorem mulid2d 10648
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 10629 . 2 (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
31, 2syl 17 1 (𝜑 → (1 · 𝐴) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  (class class class)co 7145  cc 10524  1c1 10527   · cmul 10531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-mulcom 10590  ax-mulass 10592  ax-distr 10593  ax-1rid 10596  ax-cnre 10599
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-iota 6308  df-fv 6357  df-ov 7148
This theorem is referenced by:  adddirp1d  10656  addid1  10809  mulsubfacd  11090  mulcand  11262  receu  11274  divdivdiv  11330  divcan5  11331  subrec  11458  ltrec  11511  recp1lt1  11527  nndivtr  11673  subhalfhalf  11860  xp1d2m1eqxm1d2  11880  gtndiv  12048  lincmb01cmp  12871  iccf1o  12872  ltdifltdiv  13194  modfrac  13242  negmod  13274  addmodid  13277  m1expcl2  13441  expgt1  13457  ltexp2a  13520  leexp2a  13526  binom3  13575  faclbnd  13640  faclbnd4lem4  13646  facavg  13651  bcval5  13668  cshweqrep  14173  sqrlem2  14593  absimle  14659  reccn2  14943  iseraltlem2  15029  iseraltlem3  15030  o1fsum  15158  abscvgcvg  15164  ackbijnn  15173  binom1p  15176  binom1dif  15178  incexclem  15181  incexc  15182  climcndslem1  15194  pwdif  15213  geomulcvg  15222  fprodsplit  15310  fallrisefac  15369  bpolysum  15397  bpolydiflem  15398  bpoly4  15403  efcllem  15421  ef01bndlem  15527  efieq1re  15542  eirrlem  15547  iddvds  15613  pwp1fsum  15732  oddpwp1fsum  15733  bitsfzolem  15773  bitsfzo  15774  rpmulgcd  15896  prmind2  16019  isprm5  16041  phiprm  16104  eulerthlem2  16109  fermltl  16111  hashgcdlem  16115  odzdvds  16122  powm2modprm  16130  modprm0  16132  pythagtriplem4  16146  4sqlem18  16288  vdwapun  16300  mulgnnass  18202  odinv  18619  odadd2  18900  pgpfaclem2  19135  abvneg  19536  nrginvrcnlem  23229  nmoid  23280  blcvx  23335  icopnfcnv  23475  reparphti  23530  pcorevlem  23559  ncvsm1  23687  ncvspi  23689  cphipval2  23773  cphipval  23775  itg11  24221  itg2mulc  24277  itg2monolem1  24280  itgcnlem  24319  iblabs  24358  dvexp  24479  dvmptdiv  24500  dvef  24506  lhop1lem  24539  dvcvx  24546  dvfsumlem1  24552  dvfsumlem2  24553  dvfsumlem4  24555  dvfsum2  24560  plypow  24724  dgrcolem1  24792  vieta1lem2  24829  radcnvlem1  24930  radcnvlem2  24931  dvradcnv  24938  abelthlem6  24953  abelthlem7  24955  abelth2  24959  sinhalfpip  25007  sinhalfpim  25008  coshalfpip  25009  coshalfpim  25010  tangtx  25020  efif1olem4  25056  abslogle  25128  logdivlti  25130  advlog  25164  advlogexp  25165  logtayl  25170  cxpaddlelem  25259  cxpaddle  25260  affineequiv  25328  affineequiv2  25329  chordthmlem5  25341  dcubic2  25349  dcubic  25351  mcubic  25352  binom4  25355  dquartlem1  25356  quart1lem  25360  quart1  25361  quartlem1  25362  quart  25366  efiasin  25393  atantayl  25442  cvxcl  25490  scvxcvx  25491  lgamgulmlem5  25538  lgamcvg2  25560  lgam1  25569  wilthlem1  25573  wilthlem2  25574  basellem9  25594  fsumfldivdiaglem  25694  muinv  25698  chpub  25724  logexprlim  25729  mersenne  25731  perfectlem2  25734  dchrmulid2  25756  dchrptlem1  25768  dchrsum2  25772  sumdchr2  25774  bposlem2  25789  bposlem9  25796  lgsval2lem  25811  lgsval4a  25823  lgsneg1  25826  lgsdir2lem4  25832  lgsdir  25836  lgsmulsqcoprm  25847  lgsdirnn0  25848  lgsdinn0  25849  gausslemma2dlem1a  25869  gausslemma2dlem4  25873  gausslemma2dlem7  25877  gausslemma2d  25878  lgseisenlem1  25879  lgseisenlem2  25880  lgseisenlem4  25882  lgsquad2lem1  25888  2sqlem8  25930  chebbnd1lem3  25975  chpchtlim  25983  rplogsumlem1  25988  rplogsumlem2  25989  rpvmasumlem  25991  dchrmusum2  25998  dchrvmasum2lem  26000  dchrvmasumlem2  26002  dchrvmasumlem3  26003  dchrisum0flblem1  26012  mulog2sumlem2  26039  vmalogdivsum2  26042  2vmadivsumlem  26044  log2sumbnd  26048  selberglem2  26050  selberg3lem1  26061  selberg4lem1  26064  pntrlog2bndlem2  26082  pntrlog2bndlem5  26085  pntpbnd1  26090  pntpbnd2  26091  pntibndlem2  26095  pntlemb  26101  pntlemr  26106  pntlemk  26110  pntlemo  26111  brbtwn2  26619  colinearalglem4  26623  ax5seglem3  26645  axbtwnid  26653  axpaschlem  26654  axeuclidlem  26676  axcontlem7  26684  axcontlem8  26685  elntg2  26699  nvm1  28370  nvpi  28372  nvmtri  28376  ipval2  28412  ipasslem1  28536  ipasslem4  28539  bcs2  28887  lnfnaddi  29748  nnmulge  30401  ccfldsrarelvec  30956  sqsscirc1  31051  indsum  31180  indsumin  31181  eulerpartlemgs2  31538  plymulx0  31717  logdivsqrle  31821  subfacp1lem6  32330  subfaclim  32333  cvxpconn  32387  cvxsconn  32388  resconn  32391  sinccvglem  32813  fwddifn0  33523  nn0prpwlem  33568  knoppndvlem9  33757  knoppndvlem14  33762  bj-bary1lem1  34481  mblfinlem3  34813  itg2addnclem3  34827  iblabsnc  34838  iblmulc2nc  34839  ftc1anclem6  34854  ftc1anclem7  34855  ftc1anclem8  34856  areacirclem1  34864  bfplem2  34984  bfp  34985  rrntotbnd  34997  fltnlta  39155  3cubeslem2  39162  3cubeslem3r  39164  irrapxlem5  39303  pellexlem2  39307  pellexlem6  39311  pellfundex  39363  jm2.19lem3  39468  jm2.25  39476  jm2.27c  39484  jm3.1lem2  39495  flcidc  39654  int-mul12d  40417  cvgdvgrat  40525  bccn1  40556  binomcxplemnotnn0  40568  fperiodmullem  41450  xralrple2  41502  fmul01lt1lem2  41746  mccllem  41758  reclimc  41814  cosknegpi  42030  dvsinax  42077  dvnxpaek  42107  dvnmul  42108  itgsinexp  42120  stoweidlem14  42180  stoweidlem26  42192  wallispilem4  42234  wallispilem5  42235  wallispi2lem1  42237  wallispi2  42239  stirlinglem1  42240  stirlinglem3  42242  stirlinglem4  42243  stirlinglem5  42244  stirlinglem6  42245  stirlinglem7  42246  stirlinglem10  42249  dirkertrigeqlem2  42265  dirkertrigeqlem3  42266  dirkercncflem2  42270  fourierdlem26  42299  fourierdlem41  42314  fourierdlem42  42315  fourierdlem56  42328  fourierdlem57  42329  fourierdlem58  42330  fourierdlem62  42334  fourierdlem64  42336  fourierdlem65  42337  fourierdlem95  42367  sqwvfoura  42394  sqwvfourb  42395  fouriersw  42397  etransclem23  42423  etransclem35  42435  etransclem46  42446  fmtnorec2lem  43551  fmtnorec3  43557  m1expoddALTV  43660  perfectALTVlem2  43734  ztprmneprm  44293  altgsumbc  44298  divge1b  44465  divgt1b  44466  affineid  44589  1subrec1sub  44590  rrx2vlinest  44626  line2x  44639
  Copyright terms: Public domain W3C validator