Theorem nnzi 12545

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 12540	. 2 ⊢ ℕ ⊆ ℤ
2		nnzi.1	. 2 ⊢ 𝑁 ∈ ℕ
3	1, 2	sselii 3919	1 ⊢ 𝑁 ∈ ℤ

Syntax hints:   ∈ wcel 2114  ℕcn 12168  ℤcz 12518

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371  ax-un 7683  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-i2m1 11100  ax-1ne0 11101  ax-rrecex 11104  ax-cnre 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7364  df-om 7812  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-neg 11374  df-nn 12169  df-z 12519

This theorem is referenced by:  1z  12551  2z  12553  3z  12554  4z  12555  5eluz3  12827  faclbnd4lem1  14249  3dvds  16294  3dvdsdec  16295  divalglem6  16361  divalglem7  16362  divalglem8  16363  divalglem9  16364  ndvdsi  16375  6gcd4e2  16501  3lcm2e6  16696  prm23ge5  16780  pockthi  16872  modxai  17033  mod2xnegi  17036  gcdmodi  17039  strleun  17121  strle1  17122  lt6abl  19864  2logb9irr  26775  ppiublem1  27182  ppiublem2  27183  ppiub  27184  bpos1lem  27262  bposlem6  27269  bposlem8  27271  bposlem9  27272  lgsdir2lem5  27309  2lgsoddprmlem2  27389  ex-mod  30537  ex-dvds  30544  ex-gcd  30545  ex-lcm  30546  ballotlem1  34650  ballotlem2  34652  ballotlemfmpn  34658  ballotlemsdom  34675  ballotlemsel1i  34676  ballotlemsima  34679  ballotlemfrceq  34692  ballotlemfrcn0  34693  chtvalz  34792  hgt750lem  34814  gcdcomnni  42444  gcdnegnni  42445  neggcdnni  42446  gcdaddmzz2nni  42450  12gcd5e1  42459  60gcd7e1  42461  420gcd8e4  42462  lcmeprodgcdi  42463  lcmineqlem23  42507  lcmineqlem  42508  3lexlogpow5ineq1  42510  inductionexd  44603  hoidmvlelem3  47046  fmtnoprmfac2lem1  48044  31prm  48075  mod42tp1mod8  48080  nprmdvdsfacm1lem4  48101  nprmdvdsfacm1  48102  ppivalnnnprmge6  48104  6even  48202  8even  48204  341fppr2  48225  8exp8mod9  48227  9fppr8  48228  nfermltl8rev  48233  nfermltlrev  48235  gbowge7  48254  gbege6  48256  stgoldbwt  48267  sbgoldbwt  48268  sbgoldbm  48275  mogoldbb  48276  sbgoldbo  48278  nnsum3primesle9  48285  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  wtgoldbnnsum4prm  48293  bgoldbnnsum3prm  48295  bgoldbtbndlem1  48296  tgblthelfgott  48306  tgoldbach  48308  gpg5nbgrvtx13starlem2  48563  gpg5nbgr3star  48572  pgnioedg1  48599  pgnioedg2  48600  pgnioedg3  48601  pgnioedg4  48602  pgnbgreunbgrlem1  48604  pgnbgreunbgrlem4  48610  grlimedgnedg  48622  zlmodzxzequa  48987  zlmodzxznm  48988  zlmodzxzequap  48990  zlmodzxzldeplem3  48993  zlmodzxzldep  48995  ldepsnlinclem2  48997  ldepsnlinc  48999