Theorem nnzi 12344

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

Syntax hints:   ∈ wcel 2110  ℕcn 11973  ℤcz 12319

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 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356  ax-un 7582  ax-1cn 10930  ax-icn 10931  ax-addcl 10932  ax-addrcl 10933  ax-mulcl 10934  ax-mulrcl 10935  ax-i2m1 10940  ax-1ne0 10941  ax-rrecex 10944  ax-cnre 10945

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-ral 3071  df-rex 3072  df-reu 3073  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-tr 5197  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6201  df-ord 6268  df-on 6269  df-lim 6270  df-suc 6271  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-ov 7274  df-om 7707  df-2nd 7825  df-frecs 8088  df-wrecs 8119  df-recs 8193  df-rdg 8232  df-neg 11208  df-nn 11974  df-z 12320

This theorem is referenced by:  1z  12350  2z  12352  3z  12353  4z  12354  faclbnd4lem1  14005  3dvds  16038  3dvdsdec  16039  divalglem6  16105  divalglem7  16106  divalglem8  16107  divalglem9  16108  ndvdsi  16119  6gcd4e2  16244  3lcm2e6  16434  prm23ge5  16514  pockthi  16606  modxai  16767  mod2xnegi  16770  gcdmodi  16773  strleun  16856  strle1  16857  lt6abl  19494  2logb9irr  25943  ppiublem1  26348  ppiublem2  26349  ppiub  26350  bpos1lem  26428  bposlem6  26435  bposlem8  26437  bposlem9  26438  lgsdir2lem5  26475  2lgsoddprmlem2  26555  ex-mod  28809  ex-dvds  28816  ex-gcd  28817  ex-lcm  28818  ballotlem1  32449  ballotlem2  32451  ballotlemfmpn  32457  ballotlemsdom  32474  ballotlemsel1i  32475  ballotlemsima  32478  ballotlemfrceq  32491  ballotlemfrcn0  32492  chtvalz  32605  hgt750lem  32627  gcdcomnni  39994  gcdnegnni  39995  neggcdnni  39996  gcdaddmzz2nni  40000  12gcd5e1  40008  60gcd7e1  40010  420gcd8e4  40011  lcmeprodgcdi  40012  lcmineqlem23  40056  lcmineqlem  40057  3lexlogpow5ineq1  40059  inductionexd  41735  hoidmvlelem3  44106  fmtnoprmfac2lem1  44987  31prm  45018  mod42tp1mod8  45023  6even  45132  8even  45134  341fppr2  45155  8exp8mod9  45157  9fppr8  45158  nfermltl8rev  45163  nfermltlrev  45165  gbowge7  45184  gbege6  45186  stgoldbwt  45197  sbgoldbwt  45198  sbgoldbm  45205  mogoldbb  45206  sbgoldbo  45208  nnsum3primesle9  45215  nnsum4primeseven  45221  nnsum4primesevenALTV  45222  wtgoldbnnsum4prm  45223  bgoldbnnsum3prm  45225  bgoldbtbndlem1  45226  tgblthelfgott  45236  tgoldbach  45238  zlmodzxzequa  45806  zlmodzxznm  45807  zlmodzxzequap  45809  zlmodzxzldeplem3  45812  zlmodzxzldep  45814  ldepsnlinclem2  45816  ldepsnlinc  45818