Theorem subidd 11605

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 11525	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 − 𝐴) = 0)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 − 𝐴) = 0)

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150  0cc0 11152   − cmin 11489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-po 5596  df-so 5597  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-ltxr 11297  df-sub 11491

This theorem is referenced by:  mulsubaddmulsub  11724  leaddle0  11775  cru  12255  iccf1o  13532  elfzo0suble  13742  fzocatel  13764  zmod10  13923  hashfzo  14464  hashfzp1  14466  ccatval21sw  14619  ccats1val2  14661  swrd00  14678  ccatpfx  14735  swrdccat3blem  14773  revccat  14800  repswswrd  14818  climconst  15575  rlimconst  15576  telfsumo  15834  fsumparts  15838  incexc  15869  pwdif  15900  cvgrat  15915  binomfallfaclem2  16072  fallfacfac  16077  bpolysum  16085  divalglem5  16430  nn0seqcvgd  16603  pcmpt2  16926  4sqlem15  16992  efgtlen  19758  srgbinomlem3  20245  fermltlchr  21561  freshmansdream  21610  cayhamlem1  22887  vitalilem1  25656  dvcnp2  25969  dvcnp2OLD  25970  dvferm1lem  26036  c1lip1  26050  dv11cn  26054  ftc1lem5  26095  ftc2  26099  plyeq0lem  26263  dgrcolem2  26328  plydivlem4  26352  qaa  26379  aalioulem3  26390  aaliou3lem2  26399  tayl0  26417  dvntaylp  26427  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  abelthlem9  26498  isosctrlem1  26875  birthdaylem2  27009  rlimcnp  27022  lgam1  27121  basellem2  27139  basellem5  27142  chpub  27278  dchrsum2  27326  sumdchr2  27328  2sqmod  27494  rplogsumlem2  27543  dchrisumlem1  27547  pntlemf  27663  colinearalglem4  28938  crctcsh  29853  eucrct2eupth  30273  ipidsq  30738  dip0r  30745  riesz3i  32090  riesz4i  32091  hmopidmpji  32180  pjclem4  32227  pj3si  32235  cycpmco2lem2  33129  cycpmco2lem4  33131  cycpmco2lem6  33133  znfermltl  33373  ccfldextdgrr  33696  constrrtcc  33740  signsply0  34544  itgexpif  34599  dnizeq0  36457  unbdqndv2lem2  36492  poimir  37639  itg2addnclem3  37659  ftc1cnnc  37678  ftc2nc  37688  areacirc  37699  posbezout  42081  aks6d1c5lem1  42117  aks6d1c5lem2  42119  sticksstones10  42136  sticksstones12a  42138  bcle2d  42160  metakunt24  42209  lsubswap23d  42292  fltnltalem  42648  3cubeslem2  42672  congid  42959  congabseq  42962  jm2.18  42976  dgrsub2  43123  areaquad  43204  ofsubid  44319  isosctrlem1ALT  44931  supxrgelem  45286  constlimc  45579  ioodvbdlimc1lem1  45886  dvnxpaek  45897  dvnmul  45898  voliooico  45947  voliccico  45954  stoweidlem13  45968  stoweidlem23  45978  stoweidlem26  45981  stirlinglem5  46033  dirkertrigeqlem2  46054  fourierdlem4  46066  fourierdlem42  46104  fourierdlem60  46121  fourierdlem61  46122  fourierdlem74  46135  fourierdlem75  46136  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem103  46164  fourierdlem104  46165  fourierdlem107  46168  sqwvfoura  46183  etransclem24  46213  etransclem25  46214  hoidmv1lelem1  46546  hoidmv1lelem2  46547  hoidmvlelem1  46550  hoidmvlelem2  46551  volico2  46596  2elfz2melfz  47267  m1mod0mod1  47293  m1modmmod  48370  eenglngeehlnmlem2  48587  rrx2linest  48591  line2x  48603  itscnhlc0yqe  48608  itsclc0yqsollem1  48611