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  10422  elfzo0z  10423  elfzo1  10430  ubmelm1fzo  10471  intfracq  10582  zmodcl  10606  zmodfz  10608  zmodfzo  10609  zmodid2  10614  zmodidfzo  10615  modfzo0difsn  10657  mulexpzap  10841  nnesq  10921  expnlbnd  10926  expnlbnd2  10927  nn0ltexp2  10971  facdiv  11000  faclbnd  11003  bc0k  11018  bcval5  11025  seq3coll  11106  ccatval21sw  11182  caucvgrelemcau  11541  resqrexlemlo  11574  resqrexlemcalc3  11577  resqrexlemgt0  11581  absexpzap  11641  climuni  11854  fsum3  11949  arisum  12060  trireciplem  12062  expcnvap0  12064  geo2sum  12076  geo2lim  12078  0.999...  12083  geoihalfsum  12084  cvgratz  12094  zproddc  12141  fprodseq  12145  prod1dc  12148  dvdsval3  12353  nndivdvds  12358  modmulconst  12385  dvdsle  12406  dvdsssfz1  12414  fzm1ndvds  12418  dvdsfac  12422  oexpneg  12439  nnoddm1d2  12472  divalg2  12488  divalgmod  12489  modremain  12491  ndvdsadd  12493  nndvdslegcd  12537  divgcdz  12543  divgcdnn  12547  divgcdnnr  12548  modgcd  12563  gcddiv  12591  gcdmultiple  12592  gcdmultiplez  12593  gcdzeq  12594  gcdeq  12595  rpmulgcd  12598  rplpwr  12599  rppwr  12600  sqgcd  12601  dvdssqlem  12602  dvdssq  12603  eucalginv  12629  lcmgcdlem  12650  lcmgcdnn  12655  lcmass  12658  coprmgcdb  12661  qredeq  12669  qredeu  12670  cncongr1  12676  cncongr2  12677  1idssfct  12688  isprm2lem  12689  isprm3  12691  isprm4  12692  prmind2  12693  prmdc  12703  divgcdodd  12716  isprm6  12720  sqrt2irr  12735  pw2dvds  12739  sqrt2irraplemnn  12752  divnumden  12769  divdenle  12770  nn0gcdsq  12773  phivalfi  12785  phicl2  12787  phiprmpw  12795  hashgcdlem  12811  dvdsfi  12812  hashgcdeq  12813  phisum  12814  nnoddn2prm  12834  pythagtriplem2  12840  pythagtriplem3  12841  pythagtriplem4  12842  pythagtriplem6  12844  pythagtriplem7  12845  pythagtriplem8  12846  pythagtriplem9  12847  pythagtriplem11  12848  pythagtriplem13  12850  pythagtriplem15  12852  pythagtriplem19  12856  pythagtrip  12857  pceu  12869  pccl  12873  pcdiv  12876  pcqcl  12880  pcdvds  12889  pcndvds  12891  pcndvds2  12893  pcelnn  12895  pcz  12906  pcmpt  12917  fldivp1  12922  pcfac  12924  infpnlem1  12933  infpnlem2  12934  prmunb  12936  1arith  12941  oddennn  13014  evenennn  13015  unennn  13019  mulgnn  13714  mulgnngsum  13715  mulgaddcom  13734  mulginvcom  13735  mulgmodid  13749  ghmmulg  13844  mulgass2  14073  znfi  14671  znhash  14672  znidomb  14674  znrrg  14676  rpcxproot  15640  logbgcd1irr  15693  sgmnncl  15714  lgsval  15735  lgsval4a  15753  lgssq2  15772  gausslemma2dlem0c  15782  gausslemma2dlem0e  15784  gausslemma2dlem1a  15789  gausslemma2dlem3  15794  gausslemma2dlem5  15797  lgsquadlem1  15808  lgsquadlem2  15809  lgsquad3  15815  2lgslem1a1  15817  2lgslem3  15832  2lgsoddprm  15844  trilpolemcl  16644