Theorem nnzi 12645

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

This proof depends on syntax axioms:   ∈ wcel 2145  ℕcn 12260  ℤcz 12618

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7737  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-i2m1 11195  ax-1ne0 11196  ax-rrecex 11199  ax-cnre 11200

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7417  df-om 7864  df-2nd 7988  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-neg 11471  df-nn 12261  df-z 12619

This theorem is used by:  1z  12651  2z  12653  3z  12654  4z  12655  5eluz3  12935  faclbnd4lem1  14360  3dvds  16424  3dvdsdec  16425  divalglem6  16491  divalglem7  16492  divalglem8  16493  divalglem9  16494  ndvdsi  16505  6gcd4e2  16631  3lcm2e6  16826  prm23ge5  16910  pockthi  17002  modxai  17163  mod2xnegi  17166  gcdmodi  17169  strleun  17252  strle1  17253  lt6abl  20025  2logb9irr  27035  ppiublem1  27441  ppiublem2  27442  ppiub  27443  bpos1lem  27521  bposlem6  27528  bposlem8  27530  bposlem9  27531  lgsdir2lem5  27568  2lgsoddprmlem2  27648  ex-mod  30932  ex-dvds  30939  ex-gcd  30940  ex-lcm  30941  ballotlem1  35001  ballotlem2  35003  ballotlemfmpn  35009  ballotlemsdom  35026  ballotlemsel1i  35027  ballotlemsima  35030  ballotlemfrceq  35043  ballotlemfrcn0  35044  chtvalz  35140  hgt750lem  35162  gcdcomnni  42857  gcdnegnni  42858  neggcdnni  42859  gcdaddmzz2nni  42863  12gcd5e1  42872  60gcd7e1  42874  420gcd8e4  42875  lcmeprodgcdi  42876  lcmineqlem23  42920  lcmineqlem  42921  3lexlogpow5ineq1  42923  inductionexd  44998  hoidmvlelem3  47428  goldratmolem2  47754  fmtnoprmfac2lem1  48472  31prm  48503  mod42tp1mod8  48508  nprmdvdsfacm1lem4  48529  nprmdvdsfacm1  48530  ppivalnnnprmge6  48532  6even  48630  8even  48632  341fppr2  48653  8exp8mod9  48655  9fppr8  48656  nfermltl8rev  48661  nfermltlrev  48663  gbowge7  48682  gbege6  48684  stgoldbwt  48695  sbgoldbwt  48696  sbgoldbm  48703  mogoldbb  48704  sbgoldbo  48706  nnsum3primesle9  48713  nnsum4primeseven  48719  nnsum4primesevenALTV  48720  wtgoldbnnsum4prm  48721  bgoldbnnsum3prm  48723  bgoldbtbndlem1  48724  tgblthelfgott  48734  tgoldbach  48736  gpg5nbgrvtx13starlem2  48991  gpg5nbgr3star  49000  pgnioedg1  49027  pgnioedg2  49028  pgnioedg3  49029  pgnioedg4  49030  pgnbgreunbgrlem1  49032  pgnbgreunbgrlem4  49038  grlimedgnedg  49050  zlmodzxzequa  49429  zlmodzxznm  49430  zlmodzxzequap  49432  zlmodzxzldeplem3  49435  zlmodzxzldep  49437  ldepsnlinclem2  49439  ldepsnlinc  49441  veronesev1lem  50809  veronesev2lem  50810  veronesev3lem  50811  veronesev4lem  50812  veronesev5lem  50813  veronesev6lem  50814