Theorem nnz 9347

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℕcn 8992  ℤcz 9328

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 7972  ax-resscn 7973  ax-1cn 7974  ax-1re 7975  ax-icn 7976  ax-addcl 7977  ax-addrcl 7978  ax-mulcl 7979  ax-addcom 7981  ax-addass 7983  ax-distr 7985  ax-i2m1 7986  ax-0lt1 7987  ax-0id 7989  ax-rnegex 7990  ax-cnre 7992  ax-pre-ltirr 7993  ax-pre-ltwlin 7994  ax-pre-lttrn 7995  ax-pre-ltadd 7997

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 5878  df-ov 5926  df-oprab 5927  df-mpo 5928  df-pnf 8065  df-mnf 8066  df-xr 8067  df-ltxr 8068  df-le 8069  df-sub 8201  df-neg 8202  df-inn 8993  df-z 9329

This theorem is referenced by:  elnnz1  9351  znegcl  9359  nnleltp1  9387  nnltp1le  9388  elz2  9399  nnlem1lt  9412  nnltlem1  9413  nnm1ge0  9414  prime  9427  nneo  9431  zeo  9433  btwnz  9447  indstr  9669  eluz2b2  9679  elnn1uz2  9683  qaddcl  9711  qreccl  9718  elpqb  9726  elfz1end  10132  fznatpl1  10153  fznn  10166  elfz1b  10167  elfzo0  10260  fzo1fzo0n0  10261  elfzo0z  10262  elfzo1  10268  ubmelm1fzo  10304  intfracq  10414  zmodcl  10438  zmodfz  10440  zmodfzo  10441  zmodid2  10446  zmodidfzo  10447  modfzo0difsn  10489  mulexpzap  10673  nnesq  10753  expnlbnd  10758  expnlbnd2  10759  nn0ltexp2  10803  facdiv  10832  faclbnd  10835  bc0k  10850  bcval5  10857  seq3coll  10936  caucvgrelemcau  11147  resqrexlemlo  11180  resqrexlemcalc3  11183  resqrexlemgt0  11187  absexpzap  11247  climuni  11460  fsum3  11554  arisum  11665  trireciplem  11667  expcnvap0  11669  geo2sum  11681  geo2lim  11683  0.999...  11688  geoihalfsum  11689  cvgratz  11699  zproddc  11746  fprodseq  11750  prod1dc  11753  dvdsval3  11958  nndivdvds  11963  modmulconst  11990  dvdsle  12011  dvdsssfz1  12019  fzm1ndvds  12023  dvdsfac  12027  oexpneg  12044  nnoddm1d2  12077  divalg2  12093  divalgmod  12094  modremain  12096  ndvdsadd  12098  nndvdslegcd  12142  divgcdz  12148  divgcdnn  12152  divgcdnnr  12153  modgcd  12168  gcddiv  12196  gcdmultiple  12197  gcdmultiplez  12198  gcdzeq  12199  gcdeq  12200  rpmulgcd  12203  rplpwr  12204  rppwr  12205  sqgcd  12206  dvdssqlem  12207  dvdssq  12208  eucalginv  12234  lcmgcdlem  12255  lcmgcdnn  12260  lcmass  12263  coprmgcdb  12266  qredeq  12274  qredeu  12275  cncongr1  12281  cncongr2  12282  1idssfct  12293  isprm2lem  12294  isprm3  12296  isprm4  12297  prmind2  12298  prmdc  12308  divgcdodd  12321  isprm6  12325  sqrt2irr  12340  pw2dvds  12344  sqrt2irraplemnn  12357  divnumden  12374  divdenle  12375  nn0gcdsq  12378  phivalfi  12390  phicl2  12392  phiprmpw  12400  hashgcdlem  12416  dvdsfi  12417  hashgcdeq  12418  phisum  12419  nnoddn2prm  12439  pythagtriplem2  12445  pythagtriplem3  12446  pythagtriplem4  12447  pythagtriplem6  12449  pythagtriplem7  12450  pythagtriplem8  12451  pythagtriplem9  12452  pythagtriplem11  12453  pythagtriplem13  12455  pythagtriplem15  12457  pythagtriplem19  12461  pythagtrip  12462  pceu  12474  pccl  12478  pcdiv  12481  pcqcl  12485  pcdvds  12494  pcndvds  12496  pcndvds2  12498  pcelnn  12500  pcz  12511  pcmpt  12522  fldivp1  12527  pcfac  12529  infpnlem1  12538  infpnlem2  12539  prmunb  12541  1arith  12546  oddennn  12619  evenennn  12620  unennn  12624  mulgnn  13266  mulgnngsum  13267  mulgaddcom  13286  mulginvcom  13287  mulgmodid  13301  ghmmulg  13396  mulgass2  13624  znfi  14221  znhash  14222  znidomb  14224  znrrg  14226  rpcxproot  15160  logbgcd1irr  15213  sgmnncl  15234  lgsval  15255  lgsval4a  15273  lgssq2  15292  gausslemma2dlem0c  15302  gausslemma2dlem0e  15304  gausslemma2dlem1a  15309  gausslemma2dlem3  15314  gausslemma2dlem5  15317  lgsquadlem1  15328  lgsquadlem2  15329  lgsquad3  15335  2lgslem1a1  15337  2lgslem3  15352  2lgsoddprm  15364  trilpolemcl  15691