Theorem negnegd 11531

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ℂcc 11073  -cneg 11413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-po 5549  df-so 5550  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-ltxr 11220  df-sub 11414  df-neg 11415

This theorem is referenced by:  negn0  11614  ltnegcon1  11686  ltnegcon2  11687  lenegcon1  11689  lenegcon2  11690  negfi  12139  infm3lem  12148  infrenegsup  12173  zeo  12627  zindd  12642  znnn0nn  12652  supminf  12901  zsupss  12903  max0sub  13163  xnegneg  13181  ceilid  13820  expneg  14041  expaddzlem  14077  expaddz  14078  cjcj  15113  cnpart  15213  risefallfac  15997  sincossq  16151  difmod0  16264  bitsf1  16423  pcid  16851  4sqlem10  16925  mulgnegnn  19023  mulgsubcl  19027  mulgneg  19031  mulgz  19041  mulgass  19050  ghmmulg  19167  cyggeninv  19820  tgpmulg  23987  xrhmeo  24851  cphsqrtcl3  25094  iblneg  25711  itgneg  25712  ditgswap  25767  lhop2  25927  vieta1lem2  26226  ptolemy  26412  tanabsge  26422  tanord  26454  tanregt0  26455  lognegb  26506  logtayl  26576  logtayl2  26578  cxpmul2z  26607  isosctrlem2  26736  dcubic  26763  dquart  26770  atans2  26848  amgmlem  26907  lgamucov  26955  basellem5  27002  basellem9  27006  lgsdir2lem4  27246  dchrisum0flblem1  27426  ostth3  27556  ipasslem3  30769  zconstr  33761  constrsqrtcl  33776  zrhcntr  33976  ftc1anclem6  37699  lcmineqlem12  42035  posbezout  42095  dffltz  42629  rexzrexnn0  42799  acongsym  42972  acongneg2  42973  acongtr  42974  binomcxplemnotnn0  44352  infnsuprnmpt  45251  ltmulneg  45395  rexabslelem  45421  supminfrnmpt  45448  leneg2d  45451  leneg3d  45460  supminfxr  45467  climliminflimsupd  45806  itgsin0pilem1  45955  itgsinexplem1  45959  itgsincmulx  45979  stoweidlem13  46018  fourierdlem39  46151  fourierdlem43  46155  fourierdlem44  46156  etransclem46  46285  hoicvr  46553  smfinflem  46822  sigariz  46868  sigaradd  46871  sqrtnegnre  47312  ceildivmod  47344  requad01  47626  itsclc0yqsol  48757  amgmwlem  49795