Theorem nnzi 12543

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

Syntax hints:   ∈ wcel 2119  ℕcn 12166  ℤcz 12516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5219  ax-nul 5229  ax-pr 5363  ax-un 7679  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-i2m1 11098  ax-1ne0 11099  ax-rrecex 11102  ax-cnre 11103

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4263  df-if 4456  df-pw 4532  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4840  df-iun 4924  df-br 5074  df-opab 5136  df-mpt 5155  df-tr 5181  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7360  df-om 7808  df-2nd 7933  df-frecs 8222  df-wrecs 8253  df-recs 8302  df-rdg 8340  df-neg 11372  df-nn 12167  df-z 12517

This theorem is referenced by:  1z  12549  2z  12551  3z  12552  4z  12553  5eluz3  12825  faclbnd4lem1  14247  3dvds  16292  3dvdsdec  16293  divalglem6  16359  divalglem7  16360  divalglem8  16361  divalglem9  16362  ndvdsi  16373  6gcd4e2  16499  3lcm2e6  16694  prm23ge5  16778  pockthi  16870  modxai  17031  mod2xnegi  17034  gcdmodi  17037  strleun  17119  strle1  17120  lt6abl  19862  2logb9irr  26778  ppiublem1  27184  ppiublem2  27185  ppiub  27186  bpos1lem  27264  bposlem6  27271  bposlem8  27273  bposlem9  27274  lgsdir2lem5  27311  2lgsoddprmlem2  27391  ex-mod  30538  ex-dvds  30545  ex-gcd  30546  ex-lcm  30547  ballotlem1  34680  ballotlem2  34682  ballotlemfmpn  34688  ballotlemsdom  34705  ballotlemsel1i  34706  ballotlemsima  34709  ballotlemfrceq  34722  ballotlemfrcn0  34723  chtvalz  34822  hgt750lem  34844  gcdcomnni  42482  gcdnegnni  42483  neggcdnni  42484  gcdaddmzz2nni  42488  12gcd5e1  42497  60gcd7e1  42499  420gcd8e4  42500  lcmeprodgcdi  42501  lcmineqlem23  42545  lcmineqlem  42546  3lexlogpow5ineq1  42548  inductionexd  44608  hoidmvlelem3  47048  goldratmolem2  47357  fmtnoprmfac2lem1  48052  31prm  48083  mod42tp1mod8  48088  nprmdvdsfacm1lem4  48109  nprmdvdsfacm1  48110  ppivalnnnprmge6  48112  6even  48210  8even  48212  341fppr2  48233  8exp8mod9  48235  9fppr8  48236  nfermltl8rev  48241  nfermltlrev  48243  gbowge7  48262  gbege6  48264  stgoldbwt  48275  sbgoldbwt  48276  sbgoldbm  48283  mogoldbb  48284  sbgoldbo  48286  nnsum3primesle9  48293  nnsum4primeseven  48299  nnsum4primesevenALTV  48300  wtgoldbnnsum4prm  48301  bgoldbnnsum3prm  48303  bgoldbtbndlem1  48304  tgblthelfgott  48314  tgoldbach  48316  gpg5nbgrvtx13starlem2  48571  gpg5nbgr3star  48580  pgnioedg1  48607  pgnioedg2  48608  pgnioedg3  48609  pgnioedg4  48610  pgnbgreunbgrlem1  48612  pgnbgreunbgrlem4  48618  grlimedgnedg  48630  zlmodzxzequa  48995  zlmodzxznm  48996  zlmodzxzequap  48998  zlmodzxzldeplem3  49001  zlmodzxzldep  49003  ldepsnlinclem2  49005  ldepsnlinc  49007