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

Theorem subid1d 10573
Description: Identity law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
negidd.1 (𝜑𝐴 ∈ ℂ)
Assertion
Ref Expression
subid1d (𝜑 → (𝐴 − 0) = 𝐴)

Proof of Theorem subid1d
StepHypRef Expression
1 negidd.1 . 2 (𝜑𝐴 ∈ ℂ)
2 subid1 10493 . 2 (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴)
31, 2syl 17 1 (𝜑 → (𝐴 − 0) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  wcel 2139  (class class class)co 6813  cc 10126  0cc0 10128  cmin 10458
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-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-po 5187  df-so 5188  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-er 7911  df-en 8122  df-dom 8123  df-sdom 8124  df-pnf 10268  df-mnf 10269  df-ltxr 10271  df-sub 10460
This theorem is referenced by:  suble0  10734  lesub0  10737  ltm1  11055  nn0sub  11535  max0sub  12220  modid  12889  modeqmodmin  12934  muldivbinom2  13241  bcn0  13291  bcnn  13293  hashfzo0  13409  hashfz0  13411  ccatlid  13558  swrd0val  13620  swrd0f  13627  swrdid  13628  swrdswrd0  13662  spllen  13705  splfv1  13706  splfv2a  13707  cshwsublen  13742  cshwlen  13745  repswcshw  13758  remul2  14069  clim0c  14437  rlimrecl  14510  o1rlimmul  14548  rlimno1  14583  incexclem  14767  supcvg  14787  geolim  14800  fallfacval3  14942  binomfallfaclem2  14970  bpolydiflem  14984  bpoly3  14988  addmodlteqALT  15249  dvdsmod  15252  ndvdssub  15335  nn0seqcvgd  15485  phiprmpw  15683  pczpre  15754  pcaddlem  15794  pcmpt2  15799  prmreclem4  15825  4sqlem9  15852  4sqlem11  15861  ramcl  15935  oddvdsnn0  18163  odf1o2  18188  srgbinomlem4  18743  psrlidm  19605  coe1sclmul  19854  coe1sclmul2  19856  cply1mul  19866  zndvds0  20101  recld2  22818  i1fadd  23661  mbfi1fseqlem6  23686  itgposval  23761  dveflem  23941  dv11cn  23963  lhop1lem  23975  coemulc  24210  plydivlem3  24249  plyrem  24259  vieta1lem2  24265  aareccl  24280  aalioulem3  24288  aaliou2b  24295  dvntaylp  24324  taylthlem1  24326  psercn  24379  pserdvlem2  24381  abelthlem2  24385  abelthlem3  24386  abelthlem5  24388  abelthlem7  24391  sinmpi  24438  cosppi  24441  sinhalfpim  24444  sincosq2sgn  24450  logcnlem3  24589  logcnlem4  24590  advlog  24599  efopn  24603  logtayl  24605  pythag  24746  chordthmlem5  24762  atanlogsublem  24841  rlimcnp  24891  efrlim  24895  rlimcxp  24899  cxploglim2  24904  emcllem5  24925  zetacvg  24940  lgamgulmlem2  24955  lgamcvg2  24980  0sgmppw  25122  ppiub  25128  chtublem  25135  logfacrlim  25148  logexprlim  25149  chtppilimlem2  25362  rplogsumlem2  25373  dchrisumlem3  25379  dchrvmasumiflem1  25389  dchrisum0lem2  25406  selberg2lem  25438  logdivbnd  25444  pntrsumo1  25453  pntrlog2bndlem4  25468  pntpbnd1  25474  axlowdimlem17  26037  crctcshlem4  26923  clwlkclwwlklem2a1  27115  clwlkclwwlklem2a  27121  clwlkclwwlklem3  27124  clwlkclwwlk  27125  ipidsq  27874  nmcfnexi  29219  sgnsub  30915  knoppndvlem10  32818  poimirlem19  33741  poimirlem20  33742  ftc1anc  33806  cntotbnd  33908  irrapxlem3  37890  irrapxlem4  37891  pell14qrgt0  37925  pell1qrgaplem  37939  acongeq  38052  jm2.18  38057  hashnzfz  39021  hashnzfz2  39022  hashnzfzclim  39023  bccn1  39045  binomcxplemnotnn0  39057  dstregt0  39992  absimlere  40208  ellimcabssub0  40352  0ellimcdiv  40384  clim0cf  40389  fprodsubrecnncnvlem  40624  ioodvbdlimc2lem  40652  dvnxpaek  40660  dvnmul  40661  itgsbtaddcnst  40701  stoweidlem7  40727  stoweidlem11  40731  stoweidlem26  40746  dirkertrigeqlem2  40819  fourierdlem57  40883  fourierdlem60  40886  fourierdlem61  40887  fourierdlem68  40894  fourierdlem104  40930  fourierdlem107  40933  fourierdlem109  40935  etransclem4  40958  etransclem23  40977  etransclem27  40981  etransclem31  40985  etransclem35  40989  sigarexp  41554  sigaradd  41561  pfxmpt  41897  pfxfv  41909  pfxpfx  41925  pwdif  42011  m1modmmod  42826  dignn0flhalflem1  42919
  Copyright terms: Public domain W3C validator