![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > negidd | Structured version Visualization version GIF version |
Description: Addition of a number and its negative. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
negidd.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
Ref | Expression |
---|---|
negidd | ⊢ (𝜑 → (𝐴 + -𝐴) = 0) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | negidd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | negid 10516 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + -𝐴) = 0) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐴 + -𝐴) = 0) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1628 ∈ wcel 2135 (class class class)co 6809 ℂcc 10122 0cc0 10124 + caddc 10127 -cneg 10455 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1867 ax-4 1882 ax-5 1984 ax-6 2050 ax-7 2086 ax-8 2137 ax-9 2144 ax-10 2164 ax-11 2179 ax-12 2192 ax-13 2387 ax-ext 2736 ax-sep 4929 ax-nul 4937 ax-pow 4988 ax-pr 5051 ax-un 7110 ax-resscn 10181 ax-1cn 10182 ax-icn 10183 ax-addcl 10184 ax-addrcl 10185 ax-mulcl 10186 ax-mulrcl 10187 ax-mulcom 10188 ax-addass 10189 ax-mulass 10190 ax-distr 10191 ax-i2m1 10192 ax-1ne0 10193 ax-1rid 10194 ax-rnegex 10195 ax-rrecex 10196 ax-cnre 10197 ax-pre-lttri 10198 ax-pre-lttrn 10199 ax-pre-ltadd 10200 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1631 df-ex 1850 df-nf 1855 df-sb 2043 df-eu 2607 df-mo 2608 df-clab 2743 df-cleq 2749 df-clel 2752 df-nfc 2887 df-ne 2929 df-nel 3032 df-ral 3051 df-rex 3052 df-reu 3053 df-rab 3055 df-v 3338 df-sbc 3573 df-csb 3671 df-dif 3714 df-un 3716 df-in 3718 df-ss 3725 df-nul 4055 df-if 4227 df-pw 4300 df-sn 4318 df-pr 4320 df-op 4324 df-uni 4585 df-br 4801 df-opab 4861 df-mpt 4878 df-id 5170 df-po 5183 df-so 5184 df-xp 5268 df-rel 5269 df-cnv 5270 df-co 5271 df-dm 5272 df-rn 5273 df-res 5274 df-ima 5275 df-iota 6008 df-fun 6047 df-fn 6048 df-f 6049 df-f1 6050 df-fo 6051 df-f1o 6052 df-fv 6053 df-riota 6770 df-ov 6812 df-oprab 6813 df-mpt2 6814 df-er 7907 df-en 8118 df-dom 8119 df-sdom 8120 df-pnf 10264 df-mnf 10265 df-ltxr 10267 df-sub 10456 df-neg 10457 |
This theorem is referenced by: xnegid 12258 xpncan 12270 moddvds 15189 pwp1fsum 15312 bitsres 15393 pcadd2 15792 zaddablx 18471 zringinvg 20033 ditgsplit 23820 dvferm2lem 23944 vieta1 24262 geolim3 24289 ulmshft 24339 cxpneg 24622 dcubic1lem 24765 lgamgulmlem1 24950 archiabllem2c 30054 signsply0 30933 knoppndvlem14 32818 poimir 33751 itgaddnclem2 33778 pellexlem6 37896 pellfund14 37960 binomcxplemnotnn0 39053 reclimc 40384 stoweidlem13 40729 stirlinglem5 40794 etransclem46 40996 2zrngagrp 42449 altgsumbcALT 42637 |
Copyright terms: Public domain | W3C validator |