Theorem negnegd 11558

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  ℂcc 11104  -cneg 11441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-ltxr 11249  df-sub 11442  df-neg 11443

This theorem is referenced by:  negn0  11639  ltnegcon1  11711  ltnegcon2  11712  lenegcon1  11714  lenegcon2  11715  negfi  12159  infm3lem  12168  infrenegsup  12193  zeo  12644  zindd  12659  znnn0nn  12669  supminf  12915  zsupss  12917  max0sub  13171  xnegneg  13189  ceilid  13812  expneg  14031  expaddzlem  14067  expaddz  14068  cjcj  15083  cnpart  15183  risefallfac  15964  sincossq  16115  bitsf1  16383  pcid  16802  4sqlem10  16876  mulgnegnn  18958  mulgsubcl  18962  mulgneg  18966  mulgz  18976  mulgass  18985  ghmmulg  19098  cyggeninv  19745  tgpmulg  23588  xrhmeo  24453  cphsqrtcl3  24695  iblneg  25311  itgneg  25312  ditgswap  25367  lhop2  25523  vieta1lem2  25815  ptolemy  25997  tanabsge  26007  tanord  26038  tanregt0  26039  lognegb  26089  logtayl  26159  logtayl2  26161  cxpmul2z  26190  isosctrlem2  26313  dcubic  26340  dquart  26347  atans2  26425  amgmlem  26483  lgamucov  26531  basellem5  26578  basellem9  26582  lgsdir2lem4  26820  dchrisum0flblem1  27000  ostth3  27130  ipasslem3  30073  ftc1anclem6  36554  lcmineqlem12  40893  dffltz  41372  rexzrexnn0  41527  acongsym  41700  acongneg2  41701  acongtr  41702  binomcxplemnotnn0  43100  infnsuprnmpt  43940  ltmulneg  44088  rexabslelem  44114  supminfrnmpt  44141  leneg2d  44144  leneg3d  44153  supminfxr  44160  climliminflimsupd  44503  itgsin0pilem1  44652  itgsinexplem1  44656  itgsincmulx  44676  stoweidlem13  44715  fourierdlem39  44848  fourierdlem43  44852  fourierdlem44  44853  etransclem46  44982  hoicvr  45250  smfinflem  45519  sigariz  45565  sigaradd  45568  sqrtnegnre  46001  requad01  46275  itsclc0yqsol  47403  amgmwlem  47802