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 9064 | . 2 | |
2 | 1 | sseli 3088 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1480 cn 8713 cz 9047 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 603 ax-in2 604 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 ax-sep 4041 ax-pow 4093 ax-pr 4126 ax-un 4350 ax-setind 4447 ax-cnex 7704 ax-resscn 7705 ax-1cn 7706 ax-1re 7707 ax-icn 7708 ax-addcl 7709 ax-addrcl 7710 ax-mulcl 7711 ax-addcom 7713 ax-addass 7715 ax-distr 7717 ax-i2m1 7718 ax-0lt1 7719 ax-0id 7721 ax-rnegex 7722 ax-cnre 7724 ax-pre-ltirr 7725 ax-pre-ltwlin 7726 ax-pre-lttrn 7727 ax-pre-ltadd 7729 |
This theorem depends on definitions: df-bi 116 df-3or 963 df-3an 964 df-tru 1334 df-fal 1337 df-nf 1437 df-sb 1736 df-eu 2000 df-mo 2001 df-clab 2124 df-cleq 2130 df-clel 2133 df-nfc 2268 df-ne 2307 df-nel 2402 df-ral 2419 df-rex 2420 df-reu 2421 df-rab 2423 df-v 2683 df-sbc 2905 df-dif 3068 df-un 3070 df-in 3072 df-ss 3079 df-pw 3507 df-sn 3528 df-pr 3529 df-op 3531 df-uni 3732 df-int 3767 df-br 3925 df-opab 3985 df-id 4210 df-xp 4540 df-rel 4541 df-cnv 4542 df-co 4543 df-dm 4544 df-iota 5083 df-fun 5120 df-fv 5126 df-riota 5723 df-ov 5770 df-oprab 5771 df-mpo 5772 df-pnf 7795 df-mnf 7796 df-xr 7797 df-ltxr 7798 df-le 7799 df-sub 7928 df-neg 7929 df-inn 8714 df-z 9048 |
This theorem is referenced by: elnnz1 9070 znegcl 9078 nnleltp1 9106 nnltp1le 9107 elz2 9115 nnlem1lt 9128 nnltlem1 9129 nnm1ge0 9130 prime 9143 nneo 9147 zeo 9149 btwnz 9163 indstr 9381 eluz2b2 9390 elnn1uz2 9394 qaddcl 9420 qreccl 9427 elfz1end 9828 fznatpl1 9849 fznn 9862 elfz1b 9863 elfzo0 9952 fzo1fzo0n0 9953 elfzo0z 9954 elfzo1 9960 ubmelm1fzo 9996 intfracq 10086 zmodcl 10110 zmodfz 10112 zmodfzo 10113 zmodid2 10118 zmodidfzo 10119 modfzo0difsn 10161 mulexpzap 10326 nnesq 10404 expnlbnd 10409 expnlbnd2 10410 facdiv 10477 faclbnd 10480 bc0k 10495 bcval5 10502 seq3coll 10578 caucvgrelemcau 10745 resqrexlemlo 10778 resqrexlemcalc3 10781 resqrexlemgt0 10785 absexpzap 10845 climuni 11055 fsum3 11149 arisum 11260 trireciplem 11262 expcnvap0 11264 geo2sum 11276 geo2lim 11278 0.999... 11283 geoihalfsum 11284 cvgratz 11294 dvdsval3 11486 nndivdvds 11488 modmulconst 11514 dvdsle 11531 dvdsssfz1 11539 fzm1ndvds 11543 dvdsfac 11547 oexpneg 11563 nnoddm1d2 11596 divalg2 11612 divalgmod 11613 modremain 11615 ndvdsadd 11617 nndvdslegcd 11643 divgcdz 11649 divgcdnn 11652 divgcdnnr 11653 modgcd 11668 gcddiv 11696 gcdmultiple 11697 gcdmultiplez 11698 gcdzeq 11699 gcdeq 11700 rpmulgcd 11703 rplpwr 11704 rppwr 11705 sqgcd 11706 dvdssqlem 11707 dvdssq 11708 eucalginv 11726 lcmgcdlem 11747 lcmgcdnn 11752 lcmass 11755 coprmgcdb 11758 qredeq 11766 qredeu 11767 cncongr1 11773 cncongr2 11774 1idssfct 11785 isprm2lem 11786 isprm3 11788 isprm4 11789 prmind2 11790 divgcdodd 11810 isprm6 11814 sqrt2irr 11829 pw2dvds 11833 sqrt2irraplemnn 11846 divnumden 11863 divdenle 11864 nn0gcdsq 11867 phivalfi 11877 phicl2 11879 phiprmpw 11887 hashgcdlem 11892 hashgcdeq 11893 oddennn 11894 evenennn 11895 unennn 11899 trilpolemcl 13219 |
Copyright terms: Public domain | W3C validator |