![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > znegcld | Structured version Unicode 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 10784 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 16 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-sep 4514 ax-nul 4522 ax-pow 4571 ax-pr 4632 ax-un 6475 ax-resscn 9443 ax-1cn 9444 ax-icn 9445 ax-addcl 9446 ax-addrcl 9447 ax-mulcl 9448 ax-mulrcl 9449 ax-mulcom 9450 ax-addass 9451 ax-mulass 9452 ax-distr 9453 ax-i2m1 9454 ax-1ne0 9455 ax-1rid 9456 ax-rnegex 9457 ax-rrecex 9458 ax-cnre 9459 ax-pre-lttri 9460 ax-pre-lttrn 9461 ax-pre-ltadd 9462 ax-pre-mulgt0 9463 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-nel 2647 df-ral 2800 df-rex 2801 df-reu 2802 df-rab 2804 df-v 3073 df-sbc 3288 df-csb 3390 df-dif 3432 df-un 3434 df-in 3436 df-ss 3443 df-pss 3445 df-nul 3739 df-if 3893 df-pw 3963 df-sn 3979 df-pr 3981 df-tp 3983 df-op 3985 df-uni 4193 df-iun 4274 df-br 4394 df-opab 4452 df-mpt 4453 df-tr 4487 df-eprel 4733 df-id 4737 df-po 4742 df-so 4743 df-fr 4780 df-we 4782 df-ord 4823 df-on 4824 df-lim 4825 df-suc 4826 df-xp 4947 df-rel 4948 df-cnv 4949 df-co 4950 df-dm 4951 df-rn 4952 df-res 4953 df-ima 4954 df-iota 5482 df-fun 5521 df-fn 5522 df-f 5523 df-f1 5524 df-fo 5525 df-f1o 5526 df-fv 5527 df-riota 6154 df-ov 6196 df-oprab 6197 df-mpt2 6198 df-om 6580 df-recs 6935 df-rdg 6969 df-er 7204 df-en 7414 df-dom 7415 df-sdom 7416 df-pnf 9524 df-mnf 9525 df-xr 9526 df-ltxr 9527 df-le 9528 df-sub 9701 df-neg 9702 df-nn 10427 df-z 10751 |
This theorem is referenced by: zriotaneg 10858 zsupss 11048 ceicl 11792 modnegd 11864 expaddzlem 12017 climshft2 13171 fsumshftm 13359 eftlub 13504 dvdsadd2b 13686 bitscmp 13745 bitsf1 13753 bitsres 13780 modgcd 13831 pcneg 14051 gznegcl 14107 gzcjcl 14108 4sqlem10 14119 mulgdirlem 15762 mulgdir 15763 subgmulg 15806 zringlpirlem3 18023 zlpirlem3 18028 aannenlem1 21920 geolim3 21931 aaliou3lem1 21934 aaliou3lem2 21935 aaliou3lem3 21936 aaliou3lem5 21939 aaliou3lem6 21940 aaliou3lem7 21941 ulmshft 21981 sineq0 22109 wilthlem1 22532 lgseisenlem2 22815 2sqlem4 22832 padicabvcxp 23007 gxmul 23910 gxmodid 23911 numdenneg 26224 archirngz 26344 archiabllem1b 26347 archiabllem2c 26350 qqhval2lem 26548 ltflcei 28560 cntotbnd 28836 pellexlem5 29315 pell1234qrreccl 29336 pellfund14 29380 congsub 29454 acongeq 29467 dvdsacongtr 29468 jm2.19 29483 jm2.25 29489 jm2.26lem3 29491 sineq0ALT 31976 |
Copyright terms: Public domain | W3C validator |