Theorem nnz 9362

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℕcn 9007  ℤcz 9343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-sep 4152  ax-pow 4208  ax-pr 4243  ax-un 4469  ax-setind 4574  ax-cnex 7987  ax-resscn 7988  ax-1cn 7989  ax-1re 7990  ax-icn 7991  ax-addcl 7992  ax-addrcl 7993  ax-mulcl 7994  ax-addcom 7996  ax-addass 7998  ax-distr 8000  ax-i2m1 8001  ax-0lt1 8002  ax-0id 8004  ax-rnegex 8005  ax-cnre 8007  ax-pre-ltirr 8008  ax-pre-ltwlin 8009  ax-pre-lttrn 8010  ax-pre-ltadd 8012

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-nel 2463  df-ral 2480  df-rex 2481  df-reu 2482  df-rab 2484  df-v 2765  df-sbc 2990  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-pw 3608  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-int 3876  df-br 4035  df-opab 4096  df-id 4329  df-xp 4670  df-rel 4671  df-cnv 4672  df-co 4673  df-dm 4674  df-iota 5220  df-fun 5261  df-fv 5267  df-riota 5880  df-ov 5928  df-oprab 5929  df-mpo 5930  df-pnf 8080  df-mnf 8081  df-xr 8082  df-ltxr 8083  df-le 8084  df-sub 8216  df-neg 8217  df-inn 9008  df-z 9344

This theorem is referenced by:  elnnz1  9366  znegcl  9374  nnleltp1  9402  nnltp1le  9403  elz2  9414  nnlem1lt  9427  nnltlem1  9428  nnm1ge0  9429  prime  9442  nneo  9446  zeo  9448  btwnz  9462  indstr  9684  eluz2b2  9694  elnn1uz2  9698  qaddcl  9726  qreccl  9733  elpqb  9741  elfz1end  10147  fznatpl1  10168  fznn  10181  elfz1b  10182  elfzo0  10275  fzo1fzo0n0  10276  elfzo0z  10277  elfzo1  10283  ubmelm1fzo  10319  intfracq  10429  zmodcl  10453  zmodfz  10455  zmodfzo  10456  zmodid2  10461  zmodidfzo  10462  modfzo0difsn  10504  mulexpzap  10688  nnesq  10768  expnlbnd  10773  expnlbnd2  10774  nn0ltexp2  10818  facdiv  10847  faclbnd  10850  bc0k  10865  bcval5  10872  seq3coll  10951  caucvgrelemcau  11162  resqrexlemlo  11195  resqrexlemcalc3  11198  resqrexlemgt0  11202  absexpzap  11262  climuni  11475  fsum3  11569  arisum  11680  trireciplem  11682  expcnvap0  11684  geo2sum  11696  geo2lim  11698  0.999...  11703  geoihalfsum  11704  cvgratz  11714  zproddc  11761  fprodseq  11765  prod1dc  11768  dvdsval3  11973  nndivdvds  11978  modmulconst  12005  dvdsle  12026  dvdsssfz1  12034  fzm1ndvds  12038  dvdsfac  12042  oexpneg  12059  nnoddm1d2  12092  divalg2  12108  divalgmod  12109  modremain  12111  ndvdsadd  12113  nndvdslegcd  12157  divgcdz  12163  divgcdnn  12167  divgcdnnr  12168  modgcd  12183  gcddiv  12211  gcdmultiple  12212  gcdmultiplez  12213  gcdzeq  12214  gcdeq  12215  rpmulgcd  12218  rplpwr  12219  rppwr  12220  sqgcd  12221  dvdssqlem  12222  dvdssq  12223  eucalginv  12249  lcmgcdlem  12270  lcmgcdnn  12275  lcmass  12278  coprmgcdb  12281  qredeq  12289  qredeu  12290  cncongr1  12296  cncongr2  12297  1idssfct  12308  isprm2lem  12309  isprm3  12311  isprm4  12312  prmind2  12313  prmdc  12323  divgcdodd  12336  isprm6  12340  sqrt2irr  12355  pw2dvds  12359  sqrt2irraplemnn  12372  divnumden  12389  divdenle  12390  nn0gcdsq  12393  phivalfi  12405  phicl2  12407  phiprmpw  12415  hashgcdlem  12431  dvdsfi  12432  hashgcdeq  12433  phisum  12434  nnoddn2prm  12454  pythagtriplem2  12460  pythagtriplem3  12461  pythagtriplem4  12462  pythagtriplem6  12464  pythagtriplem7  12465  pythagtriplem8  12466  pythagtriplem9  12467  pythagtriplem11  12468  pythagtriplem13  12470  pythagtriplem15  12472  pythagtriplem19  12476  pythagtrip  12477  pceu  12489  pccl  12493  pcdiv  12496  pcqcl  12500  pcdvds  12509  pcndvds  12511  pcndvds2  12513  pcelnn  12515  pcz  12526  pcmpt  12537  fldivp1  12542  pcfac  12544  infpnlem1  12553  infpnlem2  12554  prmunb  12556  1arith  12561  oddennn  12634  evenennn  12635  unennn  12639  mulgnn  13332  mulgnngsum  13333  mulgaddcom  13352  mulginvcom  13353  mulgmodid  13367  ghmmulg  13462  mulgass2  13690  znfi  14287  znhash  14288  znidomb  14290  znrrg  14292  rpcxproot  15234  logbgcd1irr  15287  sgmnncl  15308  lgsval  15329  lgsval4a  15347  lgssq2  15366  gausslemma2dlem0c  15376  gausslemma2dlem0e  15378  gausslemma2dlem1a  15383  gausslemma2dlem3  15388  gausslemma2dlem5  15391  lgsquadlem1  15402  lgsquadlem2  15403  lgsquad3  15409  2lgslem1a1  15411  2lgslem3  15426  2lgsoddprm  15438  trilpolemcl  15768