![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nnz | Unicode version |
Description: A positive integer is an integer. (Contributed by NM, 9-May-2004.) |
Ref | Expression |
---|---|
nnz |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnssz 8663 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | sseli 3006 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-13 1445 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 ax-sep 3922 ax-pow 3974 ax-pr 4000 ax-un 4224 ax-setind 4316 ax-cnex 7339 ax-resscn 7340 ax-1cn 7341 ax-1re 7342 ax-icn 7343 ax-addcl 7344 ax-addrcl 7345 ax-mulcl 7346 ax-addcom 7348 ax-addass 7350 ax-distr 7352 ax-i2m1 7353 ax-0lt1 7354 ax-0id 7356 ax-rnegex 7357 ax-cnre 7359 ax-pre-ltirr 7360 ax-pre-ltwlin 7361 ax-pre-lttrn 7362 ax-pre-ltadd 7364 |
This theorem depends on definitions: df-bi 115 df-3or 921 df-3an 922 df-tru 1288 df-fal 1291 df-nf 1391 df-sb 1688 df-eu 1946 df-mo 1947 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-ne 2250 df-nel 2345 df-ral 2358 df-rex 2359 df-reu 2360 df-rab 2362 df-v 2614 df-sbc 2827 df-dif 2986 df-un 2988 df-in 2990 df-ss 2997 df-pw 3408 df-sn 3428 df-pr 3429 df-op 3431 df-uni 3628 df-int 3663 df-br 3812 df-opab 3866 df-id 4084 df-xp 4407 df-rel 4408 df-cnv 4409 df-co 4410 df-dm 4411 df-iota 4934 df-fun 4971 df-fv 4977 df-riota 5547 df-ov 5594 df-oprab 5595 df-mpt2 5596 df-pnf 7427 df-mnf 7428 df-xr 7429 df-ltxr 7430 df-le 7431 df-sub 7558 df-neg 7559 df-inn 8317 df-z 8647 |
This theorem is referenced by: elnnz1 8669 znegcl 8677 nnleltp1 8705 nnltp1le 8706 elz2 8714 nnlem1lt 8726 nnltlem1 8727 nnm1ge0 8728 prime 8741 nneo 8745 zeo 8747 btwnz 8761 indstr 8976 eluz2b2 8985 elnn1uz2 8989 qaddcl 9015 qreccl 9022 elfz1end 9364 fznatpl1 9383 fznn 9396 elfz1b 9397 elfzo0 9482 fzo1fzo0n0 9483 elfzo0z 9484 elfzo1 9490 ubmelm1fzo 9526 intfracq 9616 zmodcl 9640 zmodfz 9642 zmodfzo 9643 zmodid2 9648 zmodidfzo 9649 modfzo0difsn 9691 expinnval 9795 mulexpzap 9832 nnesq 9908 expnlbnd 9913 expnlbnd2 9914 facdiv 9981 faclbnd 9984 bc0k 9999 ibcval5 10006 caucvgrelemcau 10240 resqrexlemlo 10273 resqrexlemcalc3 10276 resqrexlemgt0 10280 absexpzap 10340 climuni 10506 dvdsval3 10580 nndivdvds 10582 modmulconst 10608 dvdsle 10625 dvdsssfz1 10633 fzm1ndvds 10637 dvdsfac 10641 oexpneg 10657 nnoddm1d2 10690 divalg2 10706 divalgmod 10707 modremain 10709 ndvdsadd 10711 nndvdslegcd 10737 divgcdz 10743 divgcdnn 10746 divgcdnnr 10747 modgcd 10762 gcddiv 10788 gcdmultiple 10789 gcdmultiplez 10790 gcdzeq 10791 gcdeq 10792 rpmulgcd 10795 rplpwr 10796 rppwr 10797 sqgcd 10798 dvdssqlem 10799 dvdssq 10800 eucalginv 10818 lcmgcdlem 10839 lcmgcdnn 10844 lcmass 10847 coprmgcdb 10850 qredeq 10858 qredeu 10859 cncongr1 10865 cncongr2 10866 1idssfct 10877 isprm2lem 10878 isprm3 10880 isprm4 10881 prmind2 10882 divgcdodd 10902 isprm6 10906 sqrt2irr 10921 pw2dvds 10924 sqrt2irraplemnn 10937 divnumden 10954 divdenle 10955 nn0gcdsq 10958 phivalfi 10968 phicl2 10970 phiprmpw 10978 hashgcdlem 10983 hashgcdeq 10984 oddennn 10985 evenennn 10986 unennn 10990 |
Copyright terms: Public domain | W3C validator |