Theorem negnegd 11487

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ℂcc 11027  -cneg 11369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-po 5526  df-so 5527  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-ltxr 11175  df-sub 11370  df-neg 11371

This theorem is referenced by:  negn0  11570  ltnegcon1  11642  ltnegcon2  11643  lenegcon1  11645  lenegcon2  11646  negfi  12096  infm3lem  12105  infrenegsup  12130  zeo  12606  zindd  12621  znnn0nn  12631  supminf  12876  zsupss  12878  max0sub  13139  xnegneg  13157  ceilid  13801  expneg  14022  expaddzlem  14058  expaddz  14059  cjcj  15093  cnpart  15193  risefallfac  15980  sincossq  16134  difmod0  16247  bitsf1  16406  pcid  16835  4sqlem10  16909  mulgnegnn  19051  mulgsubcl  19055  mulgneg  19059  mulgz  19069  mulgass  19078  ghmmulg  19194  cyggeninv  19849  tgpmulg  24076  xrhmeo  24931  cphsqrtcl3  25172  iblneg  25788  itgneg  25789  ditgswap  25844  lhop2  26000  vieta1lem2  26295  ptolemy  26478  tanabsge  26488  tanord  26520  tanregt0  26521  lognegb  26572  logtayl  26642  logtayl2  26644  cxpmul2z  26673  isosctrlem2  26801  dcubic  26828  dquart  26835  atans2  26913  amgmlem  26971  lgamucov  27019  basellem5  27066  basellem9  27070  lgsdir2lem4  27309  dchrisum0flblem1  27489  ostth3  27619  ipasslem3  30922  zconstr  33948  constrsqrtcl  33963  zrhcntr  34163  ftc1anclem6  38065  lcmineqlem12  42525  posbezout  42585  dffltz  43084  rexzrexnn0  43249  acongsym  43421  acongneg2  43422  acongtr  43423  binomcxplemnotnn0  44800  infnsuprnmpt  45694  ltmulneg  45836  rexabslelem  45861  supminfrnmpt  45888  leneg2d  45891  leneg3d  45900  supminfxr  45907  climliminflimsupd  46244  itgsin0pilem1  46393  itgsinexplem1  46397  itgsincmulx  46417  stoweidlem13  46456  fourierdlem39  46589  fourierdlem43  46593  fourierdlem44  46594  etransclem46  46723  smfinflem  47260  sigariz  47306  sigaradd  47309  sqrtnegnre  47770  ceildivmod  47808  requad01  48112  itsclc0yqsol  49255  amgmwlem  50292