Theorem neg0 10971

Description: Minus 0 equals 0. (Contributed by NM, 17-Jan-1997.)

Assertion

Ref	Expression
neg0	⊢ -0 = 0

Proof of Theorem neg0

Step	Hyp	Ref	Expression
1		df-neg 10912	. 2 ⊢ -0 = (0 − 0)
2		0cn 10672	. . 3 ⊢ 0 ∈ ℂ
3		subid 10944	. . 3 ⊢ (0 ∈ ℂ → (0 − 0) = 0)
4	2, 3	ax-mp 5	. 2 ⊢ (0 − 0) = 0
5	1, 4	eqtri 2782	1 ⊢ -0 = 0

Syntax hints:   = wceq 1539   ∈ wcel 2112  (class class class)co 7151  ℂcc 10574  0cc0 10576   − cmin 10909  -cneg 10910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-resscn 10633  ax-1cn 10634  ax-icn 10635  ax-addcl 10636  ax-addrcl 10637  ax-mulcl 10638  ax-mulrcl 10639  ax-mulcom 10640  ax-addass 10641  ax-mulass 10642  ax-distr 10643  ax-i2m1 10644  ax-1ne0 10645  ax-1rid 10646  ax-rnegex 10647  ax-rrecex 10648  ax-cnre 10649  ax-pre-lttri 10650  ax-pre-lttrn 10651  ax-pre-ltadd 10652

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5431  df-po 5444  df-so 5445  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-er 8300  df-en 8529  df-dom 8530  df-sdom 8531  df-pnf 10716  df-mnf 10717  df-ltxr 10719  df-sub 10911  df-neg 10912

This theorem is referenced by:  negeq0  10979  lt0neg1  11185  lt0neg2  11186  le0neg1  11187  le0neg2  11188  neg1lt0  11792  elznn0  12036  znegcl  12057  xneg0  12647  expneg  13488  sqeqd  14574  sqrmo  14660  0risefac  15441  sin0  15551  m1bits  15840  lcmneg  16000  pcneg  16266  mulgneg  18314  mulgneg2  18329  iblrelem  24491  itgrevallem1  24495  ditg0  24553  ditgneg  24557  logtayl  25351  dcubic2  25530  atan0  25594  atancj  25596  ppiub  25888  lgsneg1  26006  rpvmasum2  26196  ostth3  26322  divnumden2  30657  archirngz  30970  ccfldextdgrr  31264  xrge0iif1  31410  fsum2dsub  32107  bj-pinftyccb  34917  bj-minftyccb  34921  itgaddnclem2  35397  ftc1anclem5  35415  areacirc  35431  monotoddzzfi  40257  acongeq  40298  sqwvfourb  43238  etransclem46  43289  sigariz  43844  sigarcol  43845  sigaradd  43847