![]() |
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 11817 | . 2 ⊢ ℕ ⊆ ℤ | |
2 | nnzi.1 | . 2 ⊢ 𝑁 ∈ ℕ | |
3 | 1, 2 | sselii 3857 | 1 ⊢ 𝑁 ∈ ℤ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2050 ℕcn 11441 ℤcz 11796 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-sep 5061 ax-nul 5068 ax-pow 5120 ax-pr 5187 ax-un 7281 ax-1cn 10395 ax-icn 10396 ax-addcl 10397 ax-addrcl 10398 ax-mulcl 10399 ax-mulrcl 10400 ax-i2m1 10405 ax-1ne0 10406 ax-rrecex 10409 ax-cnre 10410 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2583 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-ral 3093 df-rex 3094 df-reu 3095 df-rab 3097 df-v 3417 df-sbc 3684 df-csb 3789 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-pss 3847 df-nul 4181 df-if 4352 df-pw 4425 df-sn 4443 df-pr 4445 df-tp 4447 df-op 4449 df-uni 4714 df-iun 4795 df-br 4931 df-opab 4993 df-mpt 5010 df-tr 5032 df-id 5313 df-eprel 5318 df-po 5327 df-so 5328 df-fr 5367 df-we 5369 df-xp 5414 df-rel 5415 df-cnv 5416 df-co 5417 df-dm 5418 df-rn 5419 df-res 5420 df-ima 5421 df-pred 5988 df-ord 6034 df-on 6035 df-lim 6036 df-suc 6037 df-iota 6154 df-fun 6192 df-fn 6193 df-f 6194 df-f1 6195 df-fo 6196 df-f1o 6197 df-fv 6198 df-ov 6981 df-om 7399 df-wrecs 7752 df-recs 7814 df-rdg 7852 df-neg 10675 df-nn 11442 df-z 11797 |
This theorem is referenced by: 1z 11828 2z 11830 3z 11831 4z 11832 faclbnd4lem1 13471 3dvds 15543 3dvdsdec 15544 divalglem6 15612 divalglem7 15613 divalglem8 15614 divalglem9 15615 ndvdsi 15626 6gcd4e2 15745 3lcm2e6 15931 prm23ge5 16011 pockthi 16102 modxai 16263 mod2xnegi 16266 gcdmodi 16269 strleun 16450 strle1 16451 lt6abl 18772 2logb9irr 25077 ppiublem1 25483 ppiublem2 25484 ppiub 25485 bpos1lem 25563 bposlem6 25570 bposlem8 25572 bposlem9 25573 lgsdir2lem5 25610 2lgsoddprmlem2 25690 ex-mod 28009 ex-dvds 28016 ex-gcd 28017 ex-lcm 28018 ballotlem1 31390 ballotlem2 31392 ballotlemfmpn 31398 ballotlemsdom 31415 ballotlemsel1i 31416 ballotlemsima 31419 ballotlemfrceq 31432 ballotlemfrcn0 31433 chtvalz 31548 hgt750lem 31570 inductionexd 39868 hoidmvlelem3 42311 fmtnoprmfac2lem1 43097 31prm 43129 mod42tp1mod8 43136 6even 43245 8even 43247 341fppr2 43268 8exp8mod9 43270 9fppr8 43271 nfermltl8rev 43276 nfermltlrev 43278 gbowge7 43297 gbege6 43299 stgoldbwt 43310 sbgoldbwt 43311 sbgoldbm 43318 mogoldbb 43319 sbgoldbo 43321 nnsum3primesle9 43328 nnsum4primeseven 43334 nnsum4primesevenALTV 43335 wtgoldbnnsum4prm 43336 bgoldbnnsum3prm 43338 bgoldbtbndlem1 43339 tgblthelfgott 43349 tgoldbach 43351 zlmodzxzequa 43919 zlmodzxznm 43920 zlmodzxzequap 43922 zlmodzxzldeplem3 43925 zlmodzxzldep 43927 ldepsnlinclem2 43929 ldepsnlinc 43931 |
Copyright terms: Public domain | W3C validator |