![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > negcl | GIF version |
Description: Closure law for negative. (Contributed by NM, 6-Aug-2003.) |
Ref | Expression |
---|---|
negcl | ⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-neg 7753 | . 2 ⊢ -𝐴 = (0 − 𝐴) | |
2 | 0cn 7577 | . . 3 ⊢ 0 ∈ ℂ | |
3 | subcl 7778 | . . 3 ⊢ ((0 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (0 − 𝐴) ∈ ℂ) | |
4 | 2, 3 | mpan 416 | . 2 ⊢ (𝐴 ∈ ℂ → (0 − 𝐴) ∈ ℂ) |
5 | 1, 4 | syl5eqel 2181 | 1 ⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1445 (class class class)co 5690 ℂcc 7445 0cc0 7447 − cmin 7750 -cneg 7751 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 582 ax-in2 583 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-14 1457 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-sep 3978 ax-pow 4030 ax-pr 4060 ax-setind 4381 ax-resscn 7534 ax-1cn 7535 ax-icn 7537 ax-addcl 7538 ax-addrcl 7539 ax-mulcl 7540 ax-addcom 7542 ax-addass 7544 ax-distr 7546 ax-i2m1 7547 ax-0id 7550 ax-rnegex 7551 ax-cnre 7553 |
This theorem depends on definitions: df-bi 116 df-3an 929 df-tru 1299 df-fal 1302 df-nf 1402 df-sb 1700 df-eu 1958 df-mo 1959 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-ne 2263 df-ral 2375 df-rex 2376 df-reu 2377 df-rab 2379 df-v 2635 df-sbc 2855 df-dif 3015 df-un 3017 df-in 3019 df-ss 3026 df-pw 3451 df-sn 3472 df-pr 3473 df-op 3475 df-uni 3676 df-br 3868 df-opab 3922 df-id 4144 df-xp 4473 df-rel 4474 df-cnv 4475 df-co 4476 df-dm 4477 df-iota 5014 df-fun 5051 df-fv 5057 df-riota 5646 df-ov 5693 df-oprab 5694 df-mpt2 5695 df-sub 7752 df-neg 7753 |
This theorem is referenced by: negicn 7780 negcon1 7831 negdi 7836 negdi2 7837 negsubdi2 7838 neg2sub 7839 negcli 7847 negcld 7877 mulneg2 7971 mul2neg 7973 mulsub 7976 apsub1 8214 subap0 8215 divnegap 8270 divsubdirap 8272 divsubdivap 8292 eqneg 8296 div2negap 8299 divneg2ap 8300 zeo 8950 sqneg 10129 binom2sub 10182 shftval4 10377 shftcan1 10383 shftcan2 10384 crim 10407 resub 10419 imsub 10427 cjneg 10439 cjsub 10441 absneg 10598 abs2dif2 10655 subcn2 10854 efcan 11115 efap0 11116 efne0 11117 efneg 11118 efsub 11120 sinneg 11166 cosneg 11167 tannegap 11168 efmival 11173 sinsub 11180 cossub 11181 sincossq 11188 |
Copyright terms: Public domain | W3C validator |