Theorem nnz 9339

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

Syntax hints:   → wi 4   ∈ wcel 2164  ℕcn 8984  ℤcz 9320

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4148  ax-pow 4204  ax-pr 4239  ax-un 4465  ax-setind 4570  ax-cnex 7965  ax-resscn 7966  ax-1cn 7967  ax-1re 7968  ax-icn 7969  ax-addcl 7970  ax-addrcl 7971  ax-mulcl 7972  ax-addcom 7974  ax-addass 7976  ax-distr 7978  ax-i2m1 7979  ax-0lt1 7980  ax-0id 7982  ax-rnegex 7983  ax-cnre 7985  ax-pre-ltirr 7986  ax-pre-ltwlin 7987  ax-pre-lttrn 7988  ax-pre-ltadd 7990

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rab 2481  df-v 2762  df-sbc 2987  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-pw 3604  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-int 3872  df-br 4031  df-opab 4092  df-id 4325  df-xp 4666  df-rel 4667  df-cnv 4668  df-co 4669  df-dm 4670  df-iota 5216  df-fun 5257  df-fv 5263  df-riota 5874  df-ov 5922  df-oprab 5923  df-mpo 5924  df-pnf 8058  df-mnf 8059  df-xr 8060  df-ltxr 8061  df-le 8062  df-sub 8194  df-neg 8195  df-inn 8985  df-z 9321

This theorem is referenced by:  elnnz1  9343  znegcl  9351  nnleltp1  9379  nnltp1le  9380  elz2  9391  nnlem1lt  9404  nnltlem1  9405  nnm1ge0  9406  prime  9419  nneo  9423  zeo  9425  btwnz  9439  indstr  9661  eluz2b2  9671  elnn1uz2  9675  qaddcl  9703  qreccl  9710  elpqb  9718  elfz1end  10124  fznatpl1  10145  fznn  10158  elfz1b  10159  elfzo0  10252  fzo1fzo0n0  10253  elfzo0z  10254  elfzo1  10260  ubmelm1fzo  10296  intfracq  10394  zmodcl  10418  zmodfz  10420  zmodfzo  10421  zmodid2  10426  zmodidfzo  10427  modfzo0difsn  10469  mulexpzap  10653  nnesq  10733  expnlbnd  10738  expnlbnd2  10739  nn0ltexp2  10783  facdiv  10812  faclbnd  10815  bc0k  10830  bcval5  10837  seq3coll  10916  caucvgrelemcau  11127  resqrexlemlo  11160  resqrexlemcalc3  11163  resqrexlemgt0  11167  absexpzap  11227  climuni  11439  fsum3  11533  arisum  11644  trireciplem  11646  expcnvap0  11648  geo2sum  11660  geo2lim  11662  0.999...  11667  geoihalfsum  11668  cvgratz  11678  zproddc  11725  fprodseq  11729  prod1dc  11732  dvdsval3  11937  nndivdvds  11942  modmulconst  11969  dvdsle  11989  dvdsssfz1  11997  fzm1ndvds  12001  dvdsfac  12005  oexpneg  12021  nnoddm1d2  12054  divalg2  12070  divalgmod  12071  modremain  12073  ndvdsadd  12075  nndvdslegcd  12105  divgcdz  12111  divgcdnn  12115  divgcdnnr  12116  modgcd  12131  gcddiv  12159  gcdmultiple  12160  gcdmultiplez  12161  gcdzeq  12162  gcdeq  12163  rpmulgcd  12166  rplpwr  12167  rppwr  12168  sqgcd  12169  dvdssqlem  12170  dvdssq  12171  eucalginv  12197  lcmgcdlem  12218  lcmgcdnn  12223  lcmass  12226  coprmgcdb  12229  qredeq  12237  qredeu  12238  cncongr1  12244  cncongr2  12245  1idssfct  12256  isprm2lem  12257  isprm3  12259  isprm4  12260  prmind2  12261  prmdc  12271  divgcdodd  12284  isprm6  12288  sqrt2irr  12303  pw2dvds  12307  sqrt2irraplemnn  12320  divnumden  12337  divdenle  12338  nn0gcdsq  12341  phivalfi  12353  phicl2  12355  phiprmpw  12363  hashgcdlem  12379  hashgcdeq  12380  phisum  12381  nnoddn2prm  12401  pythagtriplem2  12407  pythagtriplem3  12408  pythagtriplem4  12409  pythagtriplem6  12411  pythagtriplem7  12412  pythagtriplem8  12413  pythagtriplem9  12414  pythagtriplem11  12415  pythagtriplem13  12417  pythagtriplem15  12419  pythagtriplem19  12423  pythagtrip  12424  pceu  12436  pccl  12440  pcdiv  12443  pcqcl  12447  pcdvds  12456  pcndvds  12458  pcndvds2  12460  pcelnn  12462  pcz  12473  pcmpt  12484  fldivp1  12489  pcfac  12491  infpnlem1  12500  infpnlem2  12501  prmunb  12503  1arith  12508  oddennn  12552  evenennn  12553  unennn  12557  mulgnn  13199  mulgnngsum  13200  mulgaddcom  13219  mulginvcom  13220  mulgmodid  13234  ghmmulg  13329  mulgass2  13557  znfi  14154  znhash  14155  znidomb  14157  znrrg  14159  rpcxproot  15089  logbgcd1irr  15140  lgsval  15161  lgsval4a  15179  lgssq2  15198  gausslemma2dlem0c  15208  gausslemma2dlem0e  15210  gausslemma2dlem1a  15215  gausslemma2dlem3  15220  gausslemma2dlem5  15223  lgsquadlem1  15234  lgsquadlem2  15235  lgsquad3  15241  2lgslem1a1  15243  2lgslem3  15258  2lgsoddprm  15270  trilpolemcl  15597