Theorem nnzi 12592

Description: A positive integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.)

Hypothesis

Ref	Expression
nnzi.1	⊢ 𝑁 ∈ ℕ

Assertion

Ref	Expression
nnzi	⊢ 𝑁 ∈ ℤ

Proof of Theorem nnzi

Step	Hyp	Ref	Expression
1		nnssz 12586	. 2 ⊢ ℕ ⊆ ℤ
2		nnzi.1	. 2 ⊢ 𝑁 ∈ ℕ
3	1, 2	sselii 3980	1 ⊢ 𝑁 ∈ ℤ

Syntax hints:   ∈ wcel 2104  ℕcn 12218  ℤcz 12564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7729  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-addrcl 11175  ax-mulcl 11176  ax-mulrcl 11177  ax-i2m1 11182  ax-1ne0 11183  ax-rrecex 11186  ax-cnre 11187

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7416  df-om 7860  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-neg 11453  df-nn 12219  df-z 12565

This theorem is referenced by:  1z  12598  2z  12600  3z  12601  4z  12602  faclbnd4lem1  14259  3dvds  16280  3dvdsdec  16281  divalglem6  16347  divalglem7  16348  divalglem8  16349  divalglem9  16350  ndvdsi  16361  6gcd4e2  16486  3lcm2e6  16674  prm23ge5  16754  pockthi  16846  modxai  17007  mod2xnegi  17010  gcdmodi  17013  strleun  17096  strle1  17097  lt6abl  19806  2logb9irr  26534  ppiublem1  26939  ppiublem2  26940  ppiub  26941  bpos1lem  27019  bposlem6  27026  bposlem8  27028  bposlem9  27029  lgsdir2lem5  27066  2lgsoddprmlem2  27146  ex-mod  29967  ex-dvds  29974  ex-gcd  29975  ex-lcm  29976  ballotlem1  33781  ballotlem2  33783  ballotlemfmpn  33789  ballotlemsdom  33806  ballotlemsel1i  33807  ballotlemsima  33810  ballotlemfrceq  33823  ballotlemfrcn0  33824  chtvalz  33937  hgt750lem  33959  gcdcomnni  41162  gcdnegnni  41163  neggcdnni  41164  gcdaddmzz2nni  41168  12gcd5e1  41176  60gcd7e1  41178  420gcd8e4  41179  lcmeprodgcdi  41180  lcmineqlem23  41224  lcmineqlem  41225  3lexlogpow5ineq1  41227  inductionexd  43210  hoidmvlelem3  45613  fmtnoprmfac2lem1  46534  31prm  46565  mod42tp1mod8  46570  6even  46679  8even  46681  341fppr2  46702  8exp8mod9  46704  9fppr8  46705  nfermltl8rev  46710  nfermltlrev  46712  gbowge7  46731  gbege6  46733  stgoldbwt  46744  sbgoldbwt  46745  sbgoldbm  46752  mogoldbb  46753  sbgoldbo  46755  nnsum3primesle9  46762  nnsum4primeseven  46768  nnsum4primesevenALTV  46769  wtgoldbnnsum4prm  46770  bgoldbnnsum3prm  46772  bgoldbtbndlem1  46773  tgblthelfgott  46783  tgoldbach  46785  zlmodzxzequa  47266  zlmodzxznm  47267  zlmodzxzequap  47269  zlmodzxzldeplem3  47272  zlmodzxzldep  47274  ldepsnlinclem2  47276  ldepsnlinc  47278