Theorem nnz 11665

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

Syntax hints:   → wi 4   ∈ wcel 2156  ℕcn 11305  ℤcz 11643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-resscn 10278  ax-1cn 10279  ax-icn 10280  ax-addcl 10281  ax-addrcl 10282  ax-mulcl 10283  ax-mulrcl 10284  ax-mulcom 10285  ax-addass 10286  ax-mulass 10287  ax-distr 10288  ax-i2m1 10289  ax-1ne0 10290  ax-1rid 10291  ax-rnegex 10292  ax-rrecex 10293  ax-cnre 10294  ax-pre-lttri 10295  ax-pre-lttrn 10296  ax-pre-ltadd 10297  ax-pre-mulgt0 10298

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-riota 6835  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-om 7296  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-er 7979  df-en 8193  df-dom 8194  df-sdom 8195  df-pnf 10361  df-mnf 10362  df-xr 10363  df-ltxr 10364  df-le 10365  df-sub 10553  df-neg 10554  df-nn 11306  df-z 11644

This theorem is referenced by:  elnnz1  11669  znegcl  11678  nnleltp1  11698  nnltp1le  11699  nnlem1lt  11709  nnltlem1  11710  nnm1ge0  11711  prime  11724  nneo  11727  zeo  11729  btwnz  11745  eluz2b2  11980  qaddcl  12023  qreccl  12027  elfz1end  12594  fznatpl1  12618  fznn  12631  elfz1b  12632  elfzo0  12733  elfzo0z  12734  elfzo1  12742  fzo1fzo0n0  12743  ubmelm1fzo  12788  quoremz  12878  intfracq  12882  fznnfl  12885  zmodcl  12914  zmodfz  12916  zmodfzo  12917  zmodid2  12922  zmodidfzo  12923  modfzo0difsn  12966  expnnval  13086  mulexpz  13123  nnesq  13211  expnlbnd  13217  expnlbnd2  13218  digit2  13220  faclbnd  13297  bc0k  13318  bcval5  13325  fz1isolem  13462  seqcoll  13465  ccatval21sw  13582  lswccatn0lsw  13588  cshwidxmod  13773  cshwidxn  13779  absexpz  14268  climuni  14506  isercoll  14621  climcnds  14805  arisum  14814  trireciplem  14816  expcnv  14818  geo2sum  14826  geo2lim  14828  0.999...  14834  geoihalfsum  14835  rpnnen2lem6  15168  rpnnen2lem9  15171  rpnnen2lem10  15172  dvdsval3  15207  nndivdvds  15212  modmulconst  15236  dvdsle  15255  dvdsssfz1  15263  fzm1ndvds  15267  dvdsfac  15271  mulmoddvds  15274  oexpneg  15289  nnoddm1d2  15322  pwp1fsum  15334  divalg2  15348  divalgmod  15349  modremain  15351  ndvdsadd  15353  nndvdslegcd  15446  divgcdz  15452  divgcdnn  15455  divgcdnnr  15456  modgcd  15472  gcddiv  15487  gcdmultiple  15488  gcdmultiplez  15489  gcdzeq  15490  gcdeq  15491  rpmulgcd  15494  rplpwr  15495  rppwr  15496  sqgcd  15497  dvdssqlem  15498  dvdssq  15499  eucalginv  15516  lcmgcdlem  15538  lcmgcdnn  15543  lcmass  15546  lcmftp  15568  lcmfunsnlem2lem1  15570  coprmgcdb  15581  qredeq  15589  qredeu  15590  coprmprod  15593  coprmproddvdslem  15594  coprmproddvds  15595  cncongr1  15599  cncongr2  15600  1idssfct  15611  isprm2lem  15612  isprm3  15614  prmind2  15616  divgcdodd  15639  isprm6  15643  ncoprmlnprm  15653  divnumden  15673  divdenle  15674  nn0gcdsq  15677  phicl2  15690  phiprmpw  15698  eulerthlem2  15704  hashgcdlem  15710  hashgcdeq  15711  phisum  15712  nnoddn2prm  15733  pythagtriplem3  15740  pythagtriplem4  15741  pythagtriplem6  15743  pythagtriplem7  15744  pythagtriplem8  15745  pythagtriplem9  15746  pythagtriplem11  15747  pythagtriplem13  15749  pythagtriplem15  15751  pythagtriplem19  15755  pythagtrip  15756  iserodd  15757  pclem  15760  pccl  15771  pcdiv  15774  pcqcl  15778  pcdvds  15785  pcndvds  15787  pcndvds2  15789  pcelnn  15791  pcz  15802  pcmpt  15813  fldivp1  15818  pcfac  15820  infpnlem1  15831  prmunb  15835  prmreclem1  15837  1arith  15848  ram0  15943  prmdvdsprmo  15963  prmgaplem4  15975  prmgaplem6  15977  prmgaplem7  15978  cshwshashlem2  16015  setsstruct2  16107  setsstructOLD  16110  mulgnn  17752  mulgaddcom  17768  mulginvcom  17769  mulgmodid  17783  ghmmulg  17874  dfod2  18182  gexdvds  18200  gexnnod  18204  gexex  18457  mulgass2  18803  qsssubdrg  20013  prmirredlem  20049  znidomb  20117  znrrg  20121  chfacfisf  20872  chfacfisfcpmat  20873  chfacfscmul0  20876  chfacfpmmul0  20880  cayhamlem1  20884  cpmadugsumlemF  20894  lmmo  21398  1stckgenlem  21570  imasdsf1olem  22391  clmmulg  23113  cmetcaulem  23298  ovolunlem1a  23477  ovolicc2lem4  23501  mbfi1fseqlem6  23701  dvexp3  23955  dgreq0  24235  elqaalem2  24289  aaliou3lem1  24311  aaliou3lem2  24312  aaliou3lem3  24313  aaliou3lem9  24319  pserdvlem2  24396  logtayl2  24622  root1eq1  24710  root1cj  24711  atantayl2  24879  birthdaylem2  24893  birthdaylem3  24894  emcllem5  24940  basellem2  25022  basellem3  25023  basellem5  25025  issqf  25076  sgmnncl  25087  prmorcht  25118  mumullem1  25119  mumullem2  25120  sqff1o  25122  dvdsflsumcom  25128  muinv  25133  vmalelog  25144  chtublem  25150  vmasum  25155  logfac2  25156  logfaclbnd  25161  bclbnd  25219  bposlem5  25227  lgsval4a  25258  lgssq2  25277  lgsdchr  25294  gausslemma2dlem0c  25297  gausslemma2dlem0e  25299  gausslemma2dlem1a  25304  gausslemma2dlem5  25310  lgsquadlem1  25319  lgsquadlem2  25320  lgsquad3  25326  2lgslem1a1  25328  2lgslem3  25343  2lgsoddprm  25355  rplogsumlem1  25387  rplogsumlem2  25388  dchrisumlem2  25393  dchrmusumlema  25396  dchrmusum2  25397  dchrvmasumiflem1  25404  dchrvmaeq0  25407  dchrisum0flblem2  25412  dchrisum0re  25416  dchrisum0lema  25417  dchrisum0lem1b  25418  dchrisum0lem2a  25420  logdivbnd  25459  pntrsumbnd2  25470  ostth2lem1  25521  ostth2lem3  25538  ostth3  25541  axlowdimlem13  26048  crctcshwlkn0lem4  26934  crctcshwlkn0lem5  26935  crctcshwlkn0lem7  26937  wlkiswwlksupgr2  27004  clwwisshclwwslem  27157  clwwlkinwwlk  27189  clwwlkel  27195  clwwlkf  27196  wwlksubclwwlk  27209  clwwlkvbij  27282  clwwlkvbijOLDOLD  27283  clwwlkvbijOLD  27284  eucrctshift  27416  eucrct2eupth  27418  numclwlk2lem2f  27557  numclwlk2lem2fOLD  27564  bcm1n  29881  pnfinf  30062  isarchiofld  30142  rearchi  30167  submat1n  30196  lmatfvlem  30206  esumcvg  30473  oddpwdc  30741  fibp1  30788  chtvalz  31032  erdszelem7  31502  climuzcnv  31887  elfzm12  31891  bcprod  31946  nn0prpwlem  32638  knoppndvlem1  32820  knoppndvlem2  32821  knoppndvlem7  32826  knoppndvlem18  32837  poimirlem13  33735  poimirlem14  33736  mblfinlem2  33760  fzmul  33848  incsequz  33855  geomcau  33866  heibor1lem  33919  bfplem2  33933  fzsplit1nn0  37819  irrapxlem1  37888  pellexlem5  37899  rmynn  38024  jm2.24nn  38027  jm2.17c  38030  congrep  38041  congabseq  38042  acongrep  38048  acongeq  38051  jm2.18  38056  jm2.23  38064  jm2.20nn  38065  jm2.26lem3  38069  jm2.26  38070  jm2.15nn0  38071  jm2.16nn0  38072  jm2.27dlem2  38078  rmydioph  38082  jm3.1  38088  expdiophlem1  38089  expdioph  38091  idomodle  38275  proot1ex  38280  nznngen  39015  sumnnodd  40342  stoweidlem7  40703  stoweidlem17  40713  wallispilem4  40764  stirlinglem2  40771  stirlinglem3  40772  stirlinglem4  40773  stirlinglem12  40781  stirlinglem13  40782  stirlinglem14  40783  stirlinglem15  40784  stirlingr  40786  dirkertrigeqlem1  40794  fouriersw  40927  ovnsubaddlem1  41266  subsubelfzo0  41911  2ffzoeq  41913  iccpartres  41929  iccpartipre  41932  iccpartltu  41936  iccelpart  41944  odz2prm2pw  42050  fmtnoprmfac2lem1  42053  pwdif  42076  2pwp1prm  42078  lighneallem2  42098  lighneallem4  42102  lighneal  42103  proththd  42106  nneoALTV  42158  divgcdoddALTV  42168  gbowge7  42226  gbege6  42228  altgsumbc  42698  altgsumbcALT  42699  pw2m1lepw2m1  42878  nnpw2even  42891  nnlog2ge0lt1  42928  logbpw2m1  42929  blenpw2m1  42941  nnpw2blenfzo  42943  nnpw2pmod  42945  nnpw2p  42948  blengt1fldiv2p1  42955  dignn0fr  42963  dignn0flhalflem1  42977  dignn0flhalflem2  42978  nn0sumshdiglemA  42981  nn0sumshdiglemB  42982