Theorem nnz 9498

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℕcn 9143  ℤcz 9479

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 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635  ax-cnex 8123  ax-resscn 8124  ax-1cn 8125  ax-1re 8126  ax-icn 8127  ax-addcl 8128  ax-addrcl 8129  ax-mulcl 8130  ax-addcom 8132  ax-addass 8134  ax-distr 8136  ax-i2m1 8137  ax-0lt1 8138  ax-0id 8140  ax-rnegex 8141  ax-cnre 8143  ax-pre-ltirr 8144  ax-pre-ltwlin 8145  ax-pre-lttrn 8146  ax-pre-ltadd 8148

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-nel 2498  df-ral 2515  df-rex 2516  df-reu 2517  df-rab 2519  df-v 2804  df-sbc 3032  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-br 4089  df-opab 4151  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-iota 5286  df-fun 5328  df-fv 5334  df-riota 5971  df-ov 6021  df-oprab 6022  df-mpo 6023  df-pnf 8216  df-mnf 8217  df-xr 8218  df-ltxr 8219  df-le 8220  df-sub 8352  df-neg 8353  df-inn 9144  df-z 9480

This theorem is referenced by:  elnnz1  9502  znegcl  9510  nnnle0  9528  nnleltp1  9539  nnltp1le  9540  elz2  9551  nnlem1lt  9564  nnltlem1  9565  nnm1ge0  9566  prime  9579  nneo  9583  zeo  9585  btwnz  9599  indstr  9827  eluz2b2  9837  elnn1uz2  9841  qaddcl  9869  qreccl  9876  elpqb  9884  elfz1end  10290  fznatpl1  10311  fznn  10324  elfz1b  10325  elfzo0  10421  fzo1fzo0n0  10423  elfzo0z  10424  elfzo1  10431  ubmelm1fzo  10472  intfracq  10583  zmodcl  10607  zmodfz  10609  zmodfzo  10610  zmodid2  10615  zmodidfzo  10616  modfzo0difsn  10658  mulexpzap  10842  nnesq  10922  expnlbnd  10927  expnlbnd2  10928  nn0ltexp2  10972  facdiv  11001  faclbnd  11004  bc0k  11019  bcval5  11026  seq3coll  11107  ccatval21sw  11186  caucvgrelemcau  11545  resqrexlemlo  11578  resqrexlemcalc3  11581  resqrexlemgt0  11585  absexpzap  11645  climuni  11858  fsum3  11953  arisum  12064  trireciplem  12066  expcnvap0  12068  geo2sum  12080  geo2lim  12082  0.999...  12087  geoihalfsum  12088  cvgratz  12098  zproddc  12145  fprodseq  12149  prod1dc  12152  dvdsval3  12357  nndivdvds  12362  modmulconst  12389  dvdsle  12410  dvdsssfz1  12418  fzm1ndvds  12422  dvdsfac  12426  oexpneg  12443  nnoddm1d2  12476  divalg2  12492  divalgmod  12493  modremain  12495  ndvdsadd  12497  nndvdslegcd  12541  divgcdz  12547  divgcdnn  12551  divgcdnnr  12552  modgcd  12567  gcddiv  12595  gcdmultiple  12596  gcdmultiplez  12597  gcdzeq  12598  gcdeq  12599  rpmulgcd  12602  rplpwr  12603  rppwr  12604  sqgcd  12605  dvdssqlem  12606  dvdssq  12607  eucalginv  12633  lcmgcdlem  12654  lcmgcdnn  12659  lcmass  12662  coprmgcdb  12665  qredeq  12673  qredeu  12674  cncongr1  12680  cncongr2  12681  1idssfct  12692  isprm2lem  12693  isprm3  12695  isprm4  12696  prmind2  12697  prmdc  12707  divgcdodd  12720  isprm6  12724  sqrt2irr  12739  pw2dvds  12743  sqrt2irraplemnn  12756  divnumden  12773  divdenle  12774  nn0gcdsq  12777  phivalfi  12789  phicl2  12791  phiprmpw  12799  hashgcdlem  12815  dvdsfi  12816  hashgcdeq  12817  phisum  12818  nnoddn2prm  12838  pythagtriplem2  12844  pythagtriplem3  12845  pythagtriplem4  12846  pythagtriplem6  12848  pythagtriplem7  12849  pythagtriplem8  12850  pythagtriplem9  12851  pythagtriplem11  12852  pythagtriplem13  12854  pythagtriplem15  12856  pythagtriplem19  12860  pythagtrip  12861  pceu  12873  pccl  12877  pcdiv  12880  pcqcl  12884  pcdvds  12893  pcndvds  12895  pcndvds2  12897  pcelnn  12899  pcz  12910  pcmpt  12921  fldivp1  12926  pcfac  12928  infpnlem1  12937  infpnlem2  12938  prmunb  12940  1arith  12945  oddennn  13018  evenennn  13019  unennn  13023  mulgnn  13718  mulgnngsum  13719  mulgaddcom  13738  mulginvcom  13739  mulgmodid  13753  ghmmulg  13848  mulgass2  14077  znfi  14675  znhash  14676  znidomb  14678  znrrg  14680  rpcxproot  15644  logbgcd1irr  15697  sgmnncl  15718  lgsval  15739  lgsval4a  15757  lgssq2  15776  gausslemma2dlem0c  15786  gausslemma2dlem0e  15788  gausslemma2dlem1a  15793  gausslemma2dlem3  15798  gausslemma2dlem5  15801  lgsquadlem1  15812  lgsquadlem2  15813  lgsquad3  15819  2lgslem1a1  15821  2lgslem3  15836  2lgsoddprm  15848  trilpolemcl  16667