Theorem negnegd 11533

Description: A number is equal to the negative of its negative. Theorem I.4 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

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

Assertion

Ref	Expression
negnegd	⊢ (𝜑 → --𝐴 = 𝐴)

Proof of Theorem negnegd

Step	Hyp	Ref	Expression
1		negidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		negneg 11481	. 2 ⊢ (𝐴 ∈ ℂ → --𝐴 = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → --𝐴 = 𝐴)

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142  ℂcc 11071  -cneg 11415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-po 5555  df-so 5556  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11218  df-mnf 11219  df-ltxr 11221  df-sub 11416  df-neg 11417

This theorem is referenced by:  negn0  11616  ltnegcon1  11688  ltnegcon2  11689  lenegcon1  11691  lenegcon2  11692  negfi  12141  infm3lem  12150  infrenegsup  12175  zeo  12659  zindd  12674  znnn0nn  12684  supminf  12936  zsupss  12938  max0sub  13199  xnegneg  13217  ceilid  13861  expneg  14082  expaddzlem  14118  expaddz  14119  cjcj  15167  cnpart  15267  risefallfac  16054  sincossq  16208  difmod0  16321  bitsf1  16480  pcid  16909  4sqlem10  16983  mulgnegnn  19126  mulgsubcl  19130  mulgneg  19134  mulgz  19144  mulgass  19153  ghmmulg  19268  cyggeninv  19923  tgpmulg  24153  xrhmeo  25008  cphsqrtcl3  25249  iblneg  25865  itgneg  25866  ditgswap  25921  lhop2  26077  vieta1lem2  26375  ptolemy  26561  tanabsge  26571  tanord  26603  tanregt0  26604  lognegb  26655  logtayl  26725  logtayl2  26727  cxpmul2z  26756  isosctrlem2  26884  dcubic  26911  dquart  26918  atans2  26996  amgmlem  27054  lgamucov  27102  basellem5  27149  basellem9  27153  lgsdir2lem4  27392  dchrisum0flblem1  27572  ostth3  27702  ipasslem3  31036  zconstr  34061  constrsqrtcl  34076  zrhcntr  34276  ftc1anclem6  38197  lcmineqlem12  42657  posbezout  42717  dffltz  43216  rexzrexnn0  43381  acongsym  43553  acongneg2  43554  acongtr  43555  binomcxplemnotnn0  44932  infnsuprnmpt  45825  ltmulneg  45967  rexabslelem  45992  supminfrnmpt  46019  leneg2d  46022  leneg3d  46031  supminfxr  46038  climliminflimsupd  46375  itgsin0pilem1  46524  itgsinexplem1  46528  itgsincmulx  46548  stoweidlem13  46587  fourierdlem39  46720  fourierdlem43  46724  fourierdlem44  46725  etransclem46  46854  smfinflem  47391  sigariz  47437  sigaradd  47440  sqrtnegnre  47901  ceildivmod  47939  requad01  48243  itsclc0yqsol  49386  amgmwlem  50423