Theorem nnz 9218

Description: A positive integer is an integer. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nnz	⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

Proof of Theorem nnz

Step	Hyp	Ref	Expression
1		nnssz 9216	. 2 ⊢ ℕ ⊆ ℤ
2	1	sseli 3143	1 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2141  ℕcn 8865  ℤcz 9199

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-sep 4105  ax-pow 4158  ax-pr 4192  ax-un 4416  ax-setind 4519  ax-cnex 7852  ax-resscn 7853  ax-1cn 7854  ax-1re 7855  ax-icn 7856  ax-addcl 7857  ax-addrcl 7858  ax-mulcl 7859  ax-addcom 7861  ax-addass 7863  ax-distr 7865  ax-i2m1 7866  ax-0lt1 7867  ax-0id 7869  ax-rnegex 7870  ax-cnre 7872  ax-pre-ltirr 7873  ax-pre-ltwlin 7874  ax-pre-lttrn 7875  ax-pre-ltadd 7877

This theorem depends on definitions:  df-bi 116  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-int 3830  df-br 3988  df-opab 4049  df-id 4276  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-iota 5158  df-fun 5198  df-fv 5204  df-riota 5806  df-ov 5853  df-oprab 5854  df-mpo 5855  df-pnf 7943  df-mnf 7944  df-xr 7945  df-ltxr 7946  df-le 7947  df-sub 8079  df-neg 8080  df-inn 8866  df-z 9200

This theorem is referenced by:  elnnz1  9222  znegcl  9230  nnleltp1  9258  nnltp1le  9259  elz2  9270  nnlem1lt  9283  nnltlem1  9284  nnm1ge0  9285  prime  9298  nneo  9302  zeo  9304  btwnz  9318  indstr  9539  eluz2b2  9549  elnn1uz2  9553  qaddcl  9581  qreccl  9588  elpqb  9595  elfz1end  9998  fznatpl1  10019  fznn  10032  elfz1b  10033  elfzo0  10125  fzo1fzo0n0  10126  elfzo0z  10127  elfzo1  10133  ubmelm1fzo  10169  intfracq  10263  zmodcl  10287  zmodfz  10289  zmodfzo  10290  zmodid2  10295  zmodidfzo  10296  modfzo0difsn  10338  mulexpzap  10503  nnesq  10582  expnlbnd  10587  expnlbnd2  10588  nn0ltexp2  10631  facdiv  10659  faclbnd  10662  bc0k  10677  bcval5  10684  seq3coll  10764  caucvgrelemcau  10931  resqrexlemlo  10964  resqrexlemcalc3  10967  resqrexlemgt0  10971  absexpzap  11031  climuni  11243  fsum3  11337  arisum  11448  trireciplem  11450  expcnvap0  11452  geo2sum  11464  geo2lim  11466  0.999...  11471  geoihalfsum  11472  cvgratz  11482  zproddc  11529  fprodseq  11533  prod1dc  11536  dvdsval3  11740  nndivdvds  11745  modmulconst  11772  dvdsle  11791  dvdsssfz1  11799  fzm1ndvds  11803  dvdsfac  11807  oexpneg  11823  nnoddm1d2  11856  divalg2  11872  divalgmod  11873  modremain  11875  ndvdsadd  11877  nndvdslegcd  11907  divgcdz  11913  divgcdnn  11917  divgcdnnr  11918  modgcd  11933  gcddiv  11961  gcdmultiple  11962  gcdmultiplez  11963  gcdzeq  11964  gcdeq  11965  rpmulgcd  11968  rplpwr  11969  rppwr  11970  sqgcd  11971  dvdssqlem  11972  dvdssq  11973  eucalginv  11997  lcmgcdlem  12018  lcmgcdnn  12023  lcmass  12026  coprmgcdb  12029  qredeq  12037  qredeu  12038  cncongr1  12044  cncongr2  12045  1idssfct  12056  isprm2lem  12057  isprm3  12059  isprm4  12060  prmind2  12061  prmdc  12071  divgcdodd  12084  isprm6  12088  sqrt2irr  12103  pw2dvds  12107  sqrt2irraplemnn  12120  divnumden  12137  divdenle  12138  nn0gcdsq  12141  phivalfi  12153  phicl2  12155  phiprmpw  12163  hashgcdlem  12179  hashgcdeq  12180  phisum  12181  nnoddn2prm  12201  pythagtriplem2  12207  pythagtriplem3  12208  pythagtriplem4  12209  pythagtriplem6  12211  pythagtriplem7  12212  pythagtriplem8  12213  pythagtriplem9  12214  pythagtriplem11  12215  pythagtriplem13  12217  pythagtriplem15  12219  pythagtriplem19  12223  pythagtrip  12224  pceu  12236  pccl  12240  pcdiv  12243  pcqcl  12247  pcdvds  12255  pcndvds  12257  pcndvds2  12259  pcelnn  12261  pcz  12272  pcmpt  12282  fldivp1  12287  pcfac  12289  infpnlem1  12298  infpnlem2  12299  prmunb  12301  1arith  12306  oddennn  12334  evenennn  12335  unennn  12339  rpcxproot  13549  logbgcd1irr  13600  lgsval  13620  lgsval4a  13638  lgssq2  13657  trilpolemcl  13991