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

Theorem subidd 10000
Description: Subtraction of a number from itself. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
negidd.1  |-  ( ph  ->  A  e.  CC )
Assertion
Ref Expression
subidd  |-  ( ph  ->  ( A  -  A
)  =  0 )

Proof of Theorem subidd
StepHypRef Expression
1 negidd.1 . 2  |-  ( ph  ->  A  e.  CC )
2 subid 9919 . 2  |-  ( A  e.  CC  ->  ( A  -  A )  =  0 )
31, 2syl 17 1  |-  ( ph  ->  ( A  -  A
)  =  0 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1455    e. wcel 1898  (class class class)co 6315   CCcc 9563   0cc0 9565    - cmin 9886
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-po 4774  df-so 4775  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-pnf 9703  df-mnf 9704  df-ltxr 9706  df-sub 9888
This theorem is referenced by:  leaddle0  10157  cru  10629  iccf1o  11805  fzocatel  12009  zmod10  12145  hashfzo  12634  ccats1val2  12797  swrd00  12811  swrdccat3blem  12888  revccat  12908  repswswrd  12924  climconst  13656  rlimconst  13657  telfsumo  13911  fsumparts  13915  incexc  13944  cvgrat  13988  binomfallfaclem2  14142  fallfacfac  14147  bpolysum  14155  divalglem5OLD  14425  divalglem5  14426  nn0seqcvgd  14578  pcmpt2  14887  4sqlem15OLD  14952  4sqlem15  14958  efgtlen  17425  srgbinomlem3  17824  cayhamlem1  19939  vitalilem1  22615  dvcnp2  22923  dvferm1lem  22985  c1lip1  22998  dv11cn  23002  ftc1lem5  23041  ftc2  23045  plyeq0lem  23213  dgrcolem2  23277  plydivlem4  23298  qaa  23328  aalioulem3  23339  aaliou3lem2  23348  tayl0  23366  dvntaylp  23375  taylthlem1  23377  taylthlem2  23378  abelthlem9  23444  isosctrlem1  23796  birthdaylem2  23927  rlimcnp  23940  lgam1  24038  basellem2  24057  basellem5  24060  chpub  24197  dchrsum2  24245  sumdchr2  24247  rplogsumlem2  24372  dchrisumlem1  24376  pntlemf  24492  colinearalglem4  24988  wlkdvspthlem  25386  ipidsq  26398  dip0r  26405  riesz3i  27764  riesz4i  27765  hmopidmpji  27854  pjclem4  27901  pj3si  27909  2sqmod  28458  signsply0  29489  poimir  32018  itg2addnclem3  32040  ftc1cnnc  32061  ftc2nc  32071  areacirc  32082  congid  35866  congabseq  35869  jm2.18  35888  dgrsub2  36039  areaquad  36146  ofsubid  36717  isosctrlem1ALT  37371  supxrgelem  37598  constlimc  37742  ioodvbdlimc1lem1  37841  ioodvbdlimc1lem1OLD  37843  dvnxpaek  37855  dvnmul  37856  stoweidlem13  37911  stoweidlem23  37921  stoweidlem26  37924  stirlinglem5  37978  dirkertrigeqlem2  37999  fourierdlem4  38011  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem60  38068  fourierdlem61  38069  fourierdlem74  38082  fourierdlem75  38083  fourierdlem89  38097  fourierdlem90  38098  fourierdlem91  38099  fourierdlem103  38111  fourierdlem104  38112  fourierdlem107  38115  sqwvfoura  38130  etransclem24  38161  etransclem25  38162  hoidmv1lelem1  38451  hoidmv1lelem2  38452  hoidmvlelem1  38455  hoidmvlelem2  38456  m1mod0mod1  38761  ccatpfx  38990  2elfz2melfz  39100  m1modmmod  40597
  Copyright terms: Public domain W3C validator