Theorem nnz 9201

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 9199	. 2 ⊢ ℕ ⊆ ℤ
2	1	sseli 3133	1 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2135  ℕcn 8848  ℤcz 9182

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 604  ax-in2 605  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-13 2137  ax-14 2138  ax-ext 2146  ax-sep 4094  ax-pow 4147  ax-pr 4181  ax-un 4405  ax-setind 4508  ax-cnex 7835  ax-resscn 7836  ax-1cn 7837  ax-1re 7838  ax-icn 7839  ax-addcl 7840  ax-addrcl 7841  ax-mulcl 7842  ax-addcom 7844  ax-addass 7846  ax-distr 7848  ax-i2m1 7849  ax-0lt1 7850  ax-0id 7852  ax-rnegex 7853  ax-cnre 7855  ax-pre-ltirr 7856  ax-pre-ltwlin 7857  ax-pre-lttrn 7858  ax-pre-ltadd 7860

This theorem depends on definitions:  df-bi 116  df-3or 968  df-3an 969  df-tru 1345  df-fal 1348  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ne 2335  df-nel 2430  df-ral 2447  df-rex 2448  df-reu 2449  df-rab 2451  df-v 2723  df-sbc 2947  df-dif 3113  df-un 3115  df-in 3117  df-ss 3124  df-pw 3555  df-sn 3576  df-pr 3577  df-op 3579  df-uni 3784  df-int 3819  df-br 3977  df-opab 4038  df-id 4265  df-xp 4604  df-rel 4605  df-cnv 4606  df-co 4607  df-dm 4608  df-iota 5147  df-fun 5184  df-fv 5190  df-riota 5792  df-ov 5839  df-oprab 5840  df-mpo 5841  df-pnf 7926  df-mnf 7927  df-xr 7928  df-ltxr 7929  df-le 7930  df-sub 8062  df-neg 8063  df-inn 8849  df-z 9183

This theorem is referenced by:  elnnz1  9205  znegcl  9213  nnleltp1  9241  nnltp1le  9242  elz2  9253  nnlem1lt  9266  nnltlem1  9267  nnm1ge0  9268  prime  9281  nneo  9285  zeo  9287  btwnz  9301  indstr  9522  eluz2b2  9532  elnn1uz2  9536  qaddcl  9564  qreccl  9571  elpqb  9578  elfz1end  9980  fznatpl1  10001  fznn  10014  elfz1b  10015  elfzo0  10107  fzo1fzo0n0  10108  elfzo0z  10109  elfzo1  10115  ubmelm1fzo  10151  intfracq  10245  zmodcl  10269  zmodfz  10271  zmodfzo  10272  zmodid2  10277  zmodidfzo  10278  modfzo0difsn  10320  mulexpzap  10485  nnesq  10563  expnlbnd  10568  expnlbnd2  10569  nn0ltexp2  10612  facdiv  10640  faclbnd  10643  bc0k  10658  bcval5  10665  seq3coll  10741  caucvgrelemcau  10908  resqrexlemlo  10941  resqrexlemcalc3  10944  resqrexlemgt0  10948  absexpzap  11008  climuni  11220  fsum3  11314  arisum  11425  trireciplem  11427  expcnvap0  11429  geo2sum  11441  geo2lim  11443  0.999...  11448  geoihalfsum  11449  cvgratz  11459  zproddc  11506  fprodseq  11510  prod1dc  11513  dvdsval3  11717  nndivdvds  11722  modmulconst  11749  dvdsle  11767  dvdsssfz1  11775  fzm1ndvds  11779  dvdsfac  11783  oexpneg  11799  nnoddm1d2  11832  divalg2  11848  divalgmod  11849  modremain  11851  ndvdsadd  11853  nndvdslegcd  11883  divgcdz  11889  divgcdnn  11893  divgcdnnr  11894  modgcd  11909  gcddiv  11937  gcdmultiple  11938  gcdmultiplez  11939  gcdzeq  11940  gcdeq  11941  rpmulgcd  11944  rplpwr  11945  rppwr  11946  sqgcd  11947  dvdssqlem  11948  dvdssq  11949  eucalginv  11967  lcmgcdlem  11988  lcmgcdnn  11993  lcmass  11996  coprmgcdb  11999  qredeq  12007  qredeu  12008  cncongr1  12014  cncongr2  12015  1idssfct  12026  isprm2lem  12027  isprm3  12029  isprm4  12030  prmind2  12031  prmdc  12041  divgcdodd  12052  isprm6  12056  sqrt2irr  12071  pw2dvds  12075  sqrt2irraplemnn  12088  divnumden  12105  divdenle  12106  nn0gcdsq  12109  phivalfi  12121  phicl2  12123  phiprmpw  12131  hashgcdlem  12147  hashgcdeq  12148  phisum  12149  nnoddn2prm  12169  pythagtriplem2  12175  pythagtriplem3  12176  pythagtriplem4  12177  pythagtriplem6  12179  pythagtriplem7  12180  pythagtriplem8  12181  pythagtriplem9  12182  pythagtriplem11  12183  pythagtriplem13  12185  pythagtriplem15  12187  pythagtriplem19  12191  pythagtrip  12192  pceu  12204  pccl  12208  pcdiv  12211  pcqcl  12215  pcdvds  12223  pcndvds  12225  pcndvds2  12227  pcelnn  12229  pcz  12240  pcmpt  12250  fldivp1  12255  pcfac  12257  oddennn  12262  evenennn  12263  unennn  12267  rpcxproot  13375  logbgcd1irr  13426  trilpolemcl  13750