![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > znegcld | GIF version |
Description: Closure law for negative integers. (Contributed by Mario Carneiro, 28-May-2016.) |
Ref | Expression |
---|---|
zred.1 | ⊢ (𝜑 → 𝐴 ∈ ℤ) |
Ref | Expression |
---|---|
znegcld | ⊢ (𝜑 → -𝐴 ∈ ℤ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zred.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℤ) | |
2 | znegcl 9309 | . 2 ⊢ (𝐴 ∈ ℤ → -𝐴 ∈ ℤ) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → -𝐴 ∈ ℤ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2160 -cneg 8154 ℤcz 9278 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2162 ax-14 2163 ax-ext 2171 ax-sep 4136 ax-pow 4189 ax-pr 4224 ax-un 4448 ax-setind 4551 ax-cnex 7927 ax-resscn 7928 ax-1cn 7929 ax-1re 7930 ax-icn 7931 ax-addcl 7932 ax-addrcl 7933 ax-mulcl 7934 ax-addcom 7936 ax-addass 7938 ax-distr 7940 ax-i2m1 7941 ax-0lt1 7942 ax-0id 7944 ax-rnegex 7945 ax-cnre 7947 ax-pre-ltirr 7948 ax-pre-ltwlin 7949 ax-pre-lttrn 7950 ax-pre-ltadd 7952 |
This theorem depends on definitions: df-bi 117 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ne 2361 df-nel 2456 df-ral 2473 df-rex 2474 df-reu 2475 df-rab 2477 df-v 2754 df-sbc 2978 df-dif 3146 df-un 3148 df-in 3150 df-ss 3157 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-int 3860 df-br 4019 df-opab 4080 df-id 4308 df-xp 4647 df-rel 4648 df-cnv 4649 df-co 4650 df-dm 4651 df-iota 5193 df-fun 5234 df-fv 5240 df-riota 5848 df-ov 5895 df-oprab 5896 df-mpo 5897 df-pnf 8019 df-mnf 8020 df-xr 8021 df-ltxr 8022 df-le 8023 df-sub 8155 df-neg 8156 df-inn 8945 df-z 9279 |
This theorem is referenced by: ceilqval 10332 ceiqcl 10333 exp3val 10548 expnegap0 10554 expaddzaplem 10589 seq3shft 10874 nn0abscl 11121 climshft2 11341 fsumshftm 11480 eftlub 11725 zdvdsdc 11846 dvdsadd2b 11874 divalglemex 11954 divalglemeuneg 11955 infssuzex 11977 zsupssdc 11982 gcdaddm 12012 modgcd 12019 pcneg 12352 gznegcl 12402 gzcjcl 12403 4sqlem10 12414 4sqexercise1 12425 4sqexercise2 12426 4sqlemsdc 12427 mulgfng 13059 mulgdirlem 13086 mulgdir 13087 mulgmodid 13094 subgmulg 13120 lgsval 14842 lgseisenlem2 14888 2sqlem4 14902 |
Copyright terms: Public domain | W3C validator |