Theorem negnegd 11490

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ℂcc 11030  -cneg 11372

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11175  df-mnf 11176  df-ltxr 11178  df-sub 11373  df-neg 11374

This theorem is referenced by:  negn0  11573  ltnegcon1  11645  ltnegcon2  11646  lenegcon1  11648  lenegcon2  11649  negfi  12099  infm3lem  12108  infrenegsup  12133  zeo  12609  zindd  12624  znnn0nn  12634  supminf  12879  zsupss  12881  max0sub  13142  xnegneg  13160  ceilid  13804  expneg  14025  expaddzlem  14061  expaddz  14062  cjcj  15096  cnpart  15196  risefallfac  15983  sincossq  16137  difmod0  16250  bitsf1  16409  pcid  16838  4sqlem10  16912  mulgnegnn  19054  mulgsubcl  19058  mulgneg  19062  mulgz  19072  mulgass  19081  ghmmulg  19197  cyggeninv  19852  tgpmulg  24071  xrhmeo  24926  cphsqrtcl3  25167  iblneg  25783  itgneg  25784  ditgswap  25839  lhop2  25995  vieta1lem2  26291  ptolemy  26476  tanabsge  26486  tanord  26518  tanregt0  26519  lognegb  26570  logtayl  26640  logtayl2  26642  cxpmul2z  26671  isosctrlem2  26799  dcubic  26826  dquart  26833  atans2  26911  amgmlem  26970  lgamucov  27018  basellem5  27065  basellem9  27069  lgsdir2lem4  27308  dchrisum0flblem1  27488  ostth3  27618  ipasslem3  30922  zconstr  33927  constrsqrtcl  33942  zrhcntr  34142  ftc1anclem6  38036  lcmineqlem12  42496  posbezout  42556  dffltz  43084  rexzrexnn0  43253  acongsym  43425  acongneg2  43426  acongtr  43427  binomcxplemnotnn0  44804  infnsuprnmpt  45700  ltmulneg  45842  rexabslelem  45867  supminfrnmpt  45894  leneg2d  45897  leneg3d  45906  supminfxr  45913  climliminflimsupd  46250  itgsin0pilem1  46399  itgsinexplem1  46403  itgsincmulx  46423  stoweidlem13  46462  fourierdlem39  46595  fourierdlem43  46599  fourierdlem44  46600  etransclem46  46729  smfinflem  47266  sigariz  47312  sigaradd  47315  sqrtnegnre  47770  ceildivmod  47808  requad01  48112  itsclc0yqsol  49255  amgmwlem  50292