Theorem subidd 11658

Description: Subtraction of a number from itself. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
negidd.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
subidd	⊢ (𝜑 → (𝐴 − 𝐴) = 0)

Proof of Theorem subidd

Step	Hyp	Ref	Expression
1		negidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		subid 11578	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 − 𝐴) = 0)
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐴 − 𝐴) = 0)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11199  0cc0 11201   − cmin 11542

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-resscn 11258  ax-1cn 11259  ax-icn 11260  ax-addcl 11261  ax-addrcl 11262  ax-mulcl 11263  ax-mulrcl 11264  ax-mulcom 11265  ax-addass 11266  ax-mulass 11267  ax-distr 11268  ax-i2m1 11269  ax-1ne0 11270  ax-1rid 11271  ax-rnegex 11272  ax-rrecex 11273  ax-cnre 11274  ax-pre-lttri 11275  ax-pre-lttrn 11276  ax-pre-ltadd 11277

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-er 8718  df-en 8975  df-dom 8976  df-sdom 8977  df-pnf 11346  df-mnf 11347  df-ltxr 11349  df-sub 11544

This theorem is used by:  mulsubaddmulsub  11781  leaddle0  11832  cru  12313  iccf1o  13628  elfzo0suble  13842  fzocatel  13865  zmod10  14028  hashfzo  14575  hashfzp1  14577  ccatval21sw  14732  ccats1val2  14776  swrd00  14793  ccatpfx  14851  swrdccat3blem  14889  revccat  14916  repswswrd  14936  climconst  15711  rlimconst  15712  telfsumo  15970  fsumparts  15974  incexc  16007  pwdif  16038  cvgrat  16053  binomfallfaclem2  16207  fallfacfac  16212  bpolysum  16220  divalglem5  16568  nn0seqcvgd  16746  pcmpt2  17072  4sqlem15  17138  efgtlen  19941  srgbinomlem3  20455  fermltlchr  21836  freshmansdream  21881  cayhamlem1  23185  vitalilem1  25930  dvcnp2  26241  dvferm1lem  26305  c1lip1  26318  dv11cn  26322  ftc1lem5  26361  ftc2  26365  plyeq0lem  26530  dgrcolem2  26594  plydivlem4  26618  qaa  26648  aalioulem3  26662  aaliou3lem2  26671  tayl0  26690  dvntaylp  26699  taylthlem1  26701  taylthlem2  26702  abelthlem9  26768  isosctrlem1  27147  birthdaylem2  27281  rlimcnp  27294  lgam1  27392  basellem2  27410  basellem5  27413  chpub  27548  dchrsum2  27596  sumdchr2  27598  2sqmod  27764  rplogsumlem2  27813  dchrisumlem1  27817  pntlemf  27933  colinearalglem4  29488  crctcsh  30414  eucrct2eupth  30847  ipidsq  31313  dip0r  31320  riesz3i  32665  riesz4i  32666  hmopidmpji  32755  pjclem4  32802  pj3si  32810  cycpmco2lem2  33731  cycpmco2lem4  33733  cycpmco2lem6  33735  znfermltl  33965  vietalem  34254  ccfldextdgrr  34347  constrrtcc  34410  signsply0  35223  itgexpif  35278  dnizeq0  37416  unbdqndv2lem2  37451  qdiff  38324  poimir  38647  itg2addnclem3  38667  ftc1cnnc  38686  ftc2nc  38696  areacirc  38707  posbezout  43226  aks6d1c5lem1  43262  aks6d1c5lem2  43264  sticksstones10  43281  sticksstones12a  43283  bcle2d  43305  fltnltalem  43749  3cubeslem2  43771  congid  44054  congabseq  44057  jm2.18  44071  dgrsub2  44213  areaquad  44294  ofsubid  45384  isosctrlem1ALT  45992  supxrgelem  46425  constlimc  46712  ioodvbdlimc1lem1  47017  dvnxpaek  47028  dvnmul  47029  voliooico  47078  voliccico  47085  stoweidlem13  47099  stoweidlem23  47109  stoweidlem26  47112  stirlinglem5  47164  dirkertrigeqlem2  47185  fourierdlem4  47197  fourierdlem42  47235  fourierdlem60  47252  fourierdlem61  47253  fourierdlem74  47266  fourierdlem75  47267  fourierdlem89  47281  fourierdlem90  47282  fourierdlem91  47283  fourierdlem103  47295  fourierdlem104  47296  fourierdlem107  47299  sqwvfoura  47314  etransclem24  47344  etransclem25  47345  hoidmv1lelem1  47677  hoidmv1lelem2  47678  hoidmvlelem1  47681  hoidmvlelem2  47682  volico2  47727  sqrtnnaa  47989  2elfz2melfz  48464  m1mod0mod1  48506  m1modmmod  48510  pgnbgreunbgrlem2lem1  49288  pgnbgreunbgrlem2lem2  49289  eenglngeehlnmlem2  49926  rrx2linest  49930  line2x  49942  itscnhlc0yqe  49947  itsclc0yqsollem1  49950