Theorem nnz 9595

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

Syntax hints:   → wi 4   ∈ wcel 2203  ℕcn 9236  ℤcz 9576

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4227  ax-pow 4286  ax-pr 4321  ax-un 4553  ax-setind 4658  ax-cnex 8217  ax-resscn 8218  ax-1cn 8219  ax-1re 8220  ax-icn 8221  ax-addcl 8222  ax-addrcl 8223  ax-mulcl 8224  ax-addcom 8226  ax-addass 8228  ax-distr 8230  ax-i2m1 8231  ax-0lt1 8232  ax-0id 8234  ax-rnegex 8235  ax-cnre 8237  ax-pre-ltirr 8238  ax-pre-ltwlin 8239  ax-pre-lttrn 8240  ax-pre-ltadd 8242

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-nel 2508  df-ral 2525  df-rex 2526  df-reu 2527  df-rab 2529  df-v 2814  df-sbc 3042  df-dif 3212  df-un 3214  df-in 3216  df-ss 3223  df-pw 3670  df-sn 3694  df-pr 3695  df-op 3697  df-uni 3914  df-int 3949  df-br 4109  df-opab 4171  df-id 4413  df-xp 4754  df-rel 4755  df-cnv 4756  df-co 4757  df-dm 4758  df-iota 5311  df-fun 5353  df-fv 5359  df-riota 6002  df-ov 6052  df-oprab 6053  df-mpo 6054  df-pnf 8309  df-mnf 8310  df-xr 8311  df-ltxr 8312  df-le 8313  df-sub 8445  df-neg 8446  df-inn 9237  df-z 9577

This theorem is referenced by:  elnnz1  9599  znegcl  9607  nnnle0  9625  nnleltp1  9636  nnltp1le  9637  elz2  9648  nnlem1lt  9661  nnltlem1  9662  nnm1ge0  9663  prime  9676  nneo  9680  zeo  9682  btwnz  9696  indstr  9924  eluz2b2  9934  elnn1uz2  9938  qaddcl  9966  qreccl  9973  elpqb  9981  elfz1end  10388  fznatpl1  10409  fznn  10422  elfz1b  10423  elfzo0  10519  fzo1fzo0n0  10521  elfzo0z  10522  elfzo1  10529  ubmelm1fzo  10570  intfracq  10681  zmodcl  10705  zmodfz  10707  zmodfzo  10708  zmodid2  10713  zmodidfzo  10714  modfzo0difsn  10756  mulexpzap  10940  nnesq  11020  expnlbnd  11025  expnlbnd2  11026  nn0ltexp2  11070  facdiv  11099  faclbnd  11102  bc0k  11117  bcval5  11124  seq3coll  11210  ccatval21sw  11289  caucvgrelemcau  11661  resqrexlemlo  11694  resqrexlemcalc3  11697  resqrexlemgt0  11701  absexpzap  11761  climuni  11974  fsum3  12069  arisum  12180  trireciplem  12182  expcnvap0  12184  geo2sum  12196  geo2lim  12198  0.999...  12203  geoihalfsum  12204  cvgratz  12214  zproddc  12261  fprodseq  12265  prod1dc  12268  dvdsval3  12473  nndivdvds  12478  modmulconst  12505  dvdsle  12526  dvdsssfz1  12534  fzm1ndvds  12538  dvdsfac  12542  oexpneg  12559  nnoddm1d2  12592  divalg2  12608  divalgmod  12609  modremain  12611  ndvdsadd  12613  nndvdslegcd  12657  divgcdz  12663  divgcdnn  12667  divgcdnnr  12668  modgcd  12683  gcddiv  12711  gcdmultiple  12712  gcdmultiplez  12713  gcdzeq  12714  gcdeq  12715  rpmulgcd  12718  rplpwr  12719  rppwr  12720  sqgcd  12721  dvdssqlem  12722  dvdssq  12723  eucalginv  12749  lcmgcdlem  12770  lcmgcdnn  12775  lcmass  12778  coprmgcdb  12781  qredeq  12789  qredeu  12790  cncongr1  12796  cncongr2  12797  1idssfct  12808  isprm2lem  12809  isprm3  12811  isprm4  12812  prmind2  12813  prmdc  12823  divgcdodd  12836  isprm6  12840  sqrt2irr  12855  pw2dvds  12859  sqrt2irraplemnn  12872  divnumden  12889  divdenle  12890  nn0gcdsq  12893  phivalfi  12905  phicl2  12907  phiprmpw  12915  hashgcdlem  12931  dvdsfi  12932  hashgcdeq  12933  phisum  12934  nnoddn2prm  12954  pythagtriplem2  12960  pythagtriplem3  12961  pythagtriplem4  12962  pythagtriplem6  12964  pythagtriplem7  12965  pythagtriplem8  12966  pythagtriplem9  12967  pythagtriplem11  12968  pythagtriplem13  12970  pythagtriplem15  12972  pythagtriplem19  12976  pythagtrip  12977  pceu  12989  pccl  12993  pcdiv  12996  pcqcl  13000  pcdvds  13009  pcndvds  13011  pcndvds2  13013  pcelnn  13015  pcz  13026  pcmpt  13037  fldivp1  13042  pcfac  13044  infpnlem1  13053  infpnlem2  13054  prmunb  13056  1arith  13061  oddennn  13135  evenennn  13136  unennn  13140  mulgnn  13835  mulgnngsum  13836  mulgaddcom  13855  mulginvcom  13856  mulgmodid  13870  ghmmulg  13965  mulgass2  14194  znfi  14795  znhash  14796  znidomb  14798  znrrg  14800  rpcxproot  15771  logbgcd1irr  15824  sgmnncl  15848  lgsval  15869  lgsval4a  15887  lgssq2  15906  gausslemma2dlem0c  15916  gausslemma2dlem0e  15918  gausslemma2dlem1a  15923  gausslemma2dlem3  15928  gausslemma2dlem5  15931  lgsquadlem1  15942  lgsquadlem2  15943  lgsquad3  15949  2lgslem1a1  15951  2lgslem3  15966  2lgsoddprm  15978  trilpolemcl  16813