Theorem nnzi 12641

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

Syntax hints:   ∈ wcel 2108  ℕcn 12266  ℤcz 12613

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-i2m1 11223  ax-1ne0 11224  ax-rrecex 11227  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-neg 11495  df-nn 12267  df-z 12614

This theorem is referenced by:  1z  12647  2z  12649  3z  12650  4z  12651  5eluz3  12927  faclbnd4lem1  14332  3dvds  16368  3dvdsdec  16369  divalglem6  16435  divalglem7  16436  divalglem8  16437  divalglem9  16438  ndvdsi  16449  6gcd4e2  16575  3lcm2e6  16769  prm23ge5  16853  pockthi  16945  modxai  17106  mod2xnegi  17109  gcdmodi  17112  strleun  17194  strle1  17195  lt6abl  19913  2logb9irr  26838  ppiublem1  27246  ppiublem2  27247  ppiub  27248  bpos1lem  27326  bposlem6  27333  bposlem8  27335  bposlem9  27336  lgsdir2lem5  27373  2lgsoddprmlem2  27453  ex-mod  30468  ex-dvds  30475  ex-gcd  30476  ex-lcm  30477  ballotlem1  34489  ballotlem2  34491  ballotlemfmpn  34497  ballotlemsdom  34514  ballotlemsel1i  34515  ballotlemsima  34518  ballotlemfrceq  34531  ballotlemfrcn0  34532  chtvalz  34644  hgt750lem  34666  gcdcomnni  41989  gcdnegnni  41990  neggcdnni  41991  gcdaddmzz2nni  41995  12gcd5e1  42004  60gcd7e1  42006  420gcd8e4  42007  lcmeprodgcdi  42008  lcmineqlem23  42052  lcmineqlem  42053  3lexlogpow5ineq1  42055  inductionexd  44168  hoidmvlelem3  46612  fmtnoprmfac2lem1  47553  31prm  47584  mod42tp1mod8  47589  6even  47698  8even  47700  341fppr2  47721  8exp8mod9  47723  9fppr8  47724  nfermltl8rev  47729  nfermltlrev  47731  gbowge7  47750  gbege6  47752  stgoldbwt  47763  sbgoldbwt  47764  sbgoldbm  47771  mogoldbb  47772  sbgoldbo  47774  nnsum3primesle9  47781  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  wtgoldbnnsum4prm  47789  bgoldbnnsum3prm  47791  bgoldbtbndlem1  47792  tgblthelfgott  47802  tgoldbach  47804  gpg5nbgrvtx13starlem2  48028  gpg5nbgr3star  48037  zlmodzxzequa  48413  zlmodzxznm  48414  zlmodzxzequap  48416  zlmodzxzldeplem3  48419  zlmodzxzldep  48421  ldepsnlinclem2  48423  ldepsnlinc  48425