![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > negcl | Structured version Visualization version GIF version |
Description: Closure law for negative. (Contributed by NM, 6-Aug-2003.) |
Ref | Expression |
---|---|
negcl | ⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-neg 10671 | . 2 ⊢ -𝐴 = (0 − 𝐴) | |
2 | 0cn 10429 | . . 3 ⊢ 0 ∈ ℂ | |
3 | subcl 10683 | . . 3 ⊢ ((0 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (0 − 𝐴) ∈ ℂ) | |
4 | 2, 3 | mpan 678 | . 2 ⊢ (𝐴 ∈ ℂ → (0 − 𝐴) ∈ ℂ) |
5 | 1, 4 | syl5eqel 2863 | 1 ⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2051 (class class class)co 6974 ℂcc 10331 0cc0 10333 − cmin 10668 -cneg 10669 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2743 ax-sep 5056 ax-nul 5063 ax-pow 5115 ax-pr 5182 ax-un 7277 ax-resscn 10390 ax-1cn 10391 ax-icn 10392 ax-addcl 10393 ax-addrcl 10394 ax-mulcl 10395 ax-mulrcl 10396 ax-mulcom 10397 ax-addass 10398 ax-mulass 10399 ax-distr 10400 ax-i2m1 10401 ax-1ne0 10402 ax-1rid 10403 ax-rnegex 10404 ax-rrecex 10405 ax-cnre 10406 ax-pre-lttri 10407 ax-pre-lttrn 10408 ax-pre-ltadd 10409 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3or 1070 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2752 df-cleq 2764 df-clel 2839 df-nfc 2911 df-ne 2961 df-nel 3067 df-ral 3086 df-rex 3087 df-reu 3088 df-rab 3090 df-v 3410 df-sbc 3675 df-csb 3780 df-dif 3825 df-un 3827 df-in 3829 df-ss 3836 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4709 df-br 4926 df-opab 4988 df-mpt 5005 df-id 5308 df-po 5322 df-so 5323 df-xp 5409 df-rel 5410 df-cnv 5411 df-co 5412 df-dm 5413 df-rn 5414 df-res 5415 df-ima 5416 df-iota 6149 df-fun 6187 df-fn 6188 df-f 6189 df-f1 6190 df-fo 6191 df-f1o 6192 df-fv 6193 df-riota 6935 df-ov 6977 df-oprab 6978 df-mpo 6979 df-er 8087 df-en 8305 df-dom 8306 df-sdom 8307 df-pnf 10474 df-mnf 10475 df-ltxr 10477 df-sub 10670 df-neg 10671 |
This theorem is referenced by: negicn 10685 negcon1 10737 negdi 10742 negdi2 10743 negsubdi2 10744 neg2sub 10745 negcli 10753 negcld 10783 mulneg2 10876 mul2neg 10878 mulsub 10882 divneg 11131 divsubdir 11133 divsubdiv 11155 eqneg 11159 div2neg 11162 divneg2 11163 zeo 11879 sqneg 13295 binom2sub 13394 shftval4 14295 shftcan1 14301 shftcan2 14302 crim 14333 resub 14345 imsub 14353 cjneg 14365 cjsub 14367 absneg 14496 abs2dif2 14552 sqreulem 14578 sqreu 14579 subcn2 14810 risefallfac 15236 fallrisefac 15237 fallfac0 15240 binomrisefac 15254 efcan 15307 efne0 15308 efneg 15309 efsub 15311 sinneg 15357 cosneg 15358 tanneg 15359 efmival 15364 sinhval 15365 coshval 15366 sinsub 15379 cossub 15380 sincossq 15387 cnaddablx 18756 cnaddabl 18757 cnaddinv 18759 cncrng 20283 cnfldneg 20288 cnlmod 23462 cnstrcvs 23463 cncvs 23467 plyremlem 24611 reeff1o 24753 sin2pim 24789 cos2pim 24790 cxpsub 24981 cxpsqrt 25002 logrec 25057 asinlem3 25165 asinneg 25180 acosneg 25181 sinasin 25183 asinsin 25186 cosasin 25198 atantan 25217 cnaddabloOLD 28150 hvsubdistr2 28621 spanunsni 29152 ltflcei 34358 dvasin 34456 sub2times 41001 cosknegpi 41612 etransclem18 42000 etransclem46 42028 addsubeq0 42934 altgsumbcALT 43797 1subrec1sub 44092 sinhpcosh 44238 |
Copyright terms: Public domain | W3C validator |