Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nnzi | Structured version Visualization version GIF version |
Description: A positive integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.) |
Ref | Expression |
---|---|
nnzi.1 | ⊢ 𝑁 ∈ ℕ |
Ref | Expression |
---|---|
nnzi | ⊢ 𝑁 ∈ ℤ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnssz 11991 | . 2 ⊢ ℕ ⊆ ℤ | |
2 | nnzi.1 | . 2 ⊢ 𝑁 ∈ ℕ | |
3 | 1, 2 | sselii 3963 | 1 ⊢ 𝑁 ∈ ℤ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 ℕcn 11627 ℤcz 11970 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7450 ax-1cn 10584 ax-icn 10585 ax-addcl 10586 ax-addrcl 10587 ax-mulcl 10588 ax-mulrcl 10589 ax-i2m1 10594 ax-1ne0 10595 ax-rrecex 10598 ax-cnre 10599 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3or 1080 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3497 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4466 df-pw 4539 df-sn 4560 df-pr 4562 df-tp 4564 df-op 4566 df-uni 4833 df-iun 4914 df-br 5059 df-opab 5121 df-mpt 5139 df-tr 5165 df-id 5454 df-eprel 5459 df-po 5468 df-so 5469 df-fr 5508 df-we 5510 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-pred 6142 df-ord 6188 df-on 6189 df-lim 6190 df-suc 6191 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 df-ov 7148 df-om 7569 df-wrecs 7938 df-recs 7999 df-rdg 8037 df-neg 10862 df-nn 11628 df-z 11971 |
This theorem is referenced by: 1z 12001 2z 12003 3z 12004 4z 12005 faclbnd4lem1 13643 3dvds 15670 3dvdsdec 15671 divalglem6 15739 divalglem7 15740 divalglem8 15741 divalglem9 15742 ndvdsi 15753 6gcd4e2 15876 3lcm2e6 16062 prm23ge5 16142 pockthi 16233 modxai 16394 mod2xnegi 16397 gcdmodi 16400 strleun 16581 strle1 16582 lt6abl 18946 2logb9irr 25300 ppiublem1 25706 ppiublem2 25707 ppiub 25708 bpos1lem 25786 bposlem6 25793 bposlem8 25795 bposlem9 25796 lgsdir2lem5 25833 2lgsoddprmlem2 25913 ex-mod 28156 ex-dvds 28163 ex-gcd 28164 ex-lcm 28165 ballotlem1 31644 ballotlem2 31646 ballotlemfmpn 31652 ballotlemsdom 31669 ballotlemsel1i 31670 ballotlemsima 31673 ballotlemfrceq 31686 ballotlemfrcn0 31687 chtvalz 31800 hgt750lem 31822 inductionexd 40385 hoidmvlelem3 42760 fmtnoprmfac2lem1 43575 31prm 43607 mod42tp1mod8 43614 6even 43723 8even 43725 341fppr2 43746 8exp8mod9 43748 9fppr8 43749 nfermltl8rev 43754 nfermltlrev 43756 gbowge7 43775 gbege6 43777 stgoldbwt 43788 sbgoldbwt 43789 sbgoldbm 43796 mogoldbb 43797 sbgoldbo 43799 nnsum3primesle9 43806 nnsum4primeseven 43812 nnsum4primesevenALTV 43813 wtgoldbnnsum4prm 43814 bgoldbnnsum3prm 43816 bgoldbtbndlem1 43817 tgblthelfgott 43827 tgoldbach 43829 zlmodzxzequa 44449 zlmodzxznm 44450 zlmodzxzequap 44452 zlmodzxzldeplem3 44455 zlmodzxzldep 44457 ldepsnlinclem2 44459 ldepsnlinc 44461 |
Copyright terms: Public domain | W3C validator |