![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > negnegd | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
negidd.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
Ref | Expression |
---|---|
negnegd | ⊢ (𝜑 → --𝐴 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | negidd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | negneg 10786 | . 2 ⊢ (𝐴 ∈ ℂ → --𝐴 = 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → --𝐴 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1522 ∈ wcel 2080 ℂcc 10384 -cneg 10720 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 ax-5 1889 ax-6 1948 ax-7 1993 ax-8 2082 ax-9 2090 ax-10 2111 ax-11 2125 ax-12 2140 ax-13 2343 ax-ext 2768 ax-sep 5097 ax-nul 5104 ax-pow 5160 ax-pr 5224 ax-un 7322 ax-resscn 10443 ax-1cn 10444 ax-icn 10445 ax-addcl 10446 ax-addrcl 10447 ax-mulcl 10448 ax-mulrcl 10449 ax-mulcom 10450 ax-addass 10451 ax-mulass 10452 ax-distr 10453 ax-i2m1 10454 ax-1ne0 10455 ax-1rid 10456 ax-rnegex 10457 ax-rrecex 10458 ax-cnre 10459 ax-pre-lttri 10460 ax-pre-lttrn 10461 ax-pre-ltadd 10462 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1763 df-nf 1767 df-sb 2042 df-mo 2575 df-eu 2611 df-clab 2775 df-cleq 2787 df-clel 2862 df-nfc 2934 df-ne 2984 df-nel 3090 df-ral 3109 df-rex 3110 df-reu 3111 df-rab 3113 df-v 3438 df-sbc 3708 df-csb 3814 df-dif 3864 df-un 3866 df-in 3868 df-ss 3876 df-nul 4214 df-if 4384 df-pw 4457 df-sn 4475 df-pr 4477 df-op 4481 df-uni 4748 df-br 4965 df-opab 5027 df-mpt 5044 df-id 5351 df-po 5365 df-so 5366 df-xp 5452 df-rel 5453 df-cnv 5454 df-co 5455 df-dm 5456 df-rn 5457 df-res 5458 df-ima 5459 df-iota 6192 df-fun 6230 df-fn 6231 df-f 6232 df-f1 6233 df-fo 6234 df-f1o 6235 df-fv 6236 df-riota 6980 df-ov 7022 df-oprab 7023 df-mpo 7024 df-er 8142 df-en 8361 df-dom 8362 df-sdom 8363 df-pnf 10526 df-mnf 10527 df-ltxr 10529 df-sub 10721 df-neg 10722 |
This theorem is referenced by: negn0 10919 ltnegcon1 10991 ltnegcon2 10992 lenegcon1 10994 lenegcon2 10995 negfi 11439 fiminreOLD 11440 infm3lem 11449 infrenegsup 11474 zeo 11918 zindd 11933 znnn0nn 11944 supminf 12184 zsupss 12186 max0sub 12439 xnegneg 12457 ceilid 13069 expneg 13287 expaddzlem 13322 expaddz 13323 cjcj 14333 cnpart 14433 risefallfac 15211 sincossq 15362 bitsf1 15628 pcid 16038 4sqlem10 16112 mulgnegnn 17993 mulgsubcl 17997 mulgneg 18001 mulgz 18009 mulgass 18018 ghmmulg 18111 cyggeninv 18725 tgpmulg 22385 xrhmeo 23233 cphsqrtcl3 23474 iblneg 24086 itgneg 24087 ditgswap 24140 lhop2 24295 vieta1lem2 24583 ptolemy 24765 tanabsge 24775 tanord 24803 tanregt0 24804 lognegb 24854 logtayl 24924 logtayl2 24926 cxpmul2z 24955 isosctrlem2 25078 dcubic 25105 dquart 25112 atans2 25190 amgmlem 25249 lgamucov 25297 basellem5 25344 basellem9 25348 lgsdir2lem4 25586 dchrisum0flblem1 25766 ostth3 25896 ipasslem3 28293 ftc1anclem6 34516 dffltz 38781 rexzrexnn0 38899 acongsym 39071 acongneg2 39072 acongtr 39073 binomcxplemnotnn0 40239 infnsuprnmpt 41076 ltmulneg 41218 rexabslelem 41247 supminfrnmpt 41274 leneg2d 41278 leneg3d 41288 supminfxr 41295 climliminflimsupd 41637 itgsin0pilem1 41790 itgsinexplem1 41794 itgsincmulx 41814 stoweidlem13 41854 fourierdlem39 41987 fourierdlem43 41991 fourierdlem44 41992 etransclem46 42121 hoicvr 42386 smfinflem 42647 sigariz 42676 sigaradd 42679 sqrtnegnre 43037 requad01 43282 itsclc0yqsol 44246 amgmwlem 44397 |
Copyright terms: Public domain | W3C validator |