Theorem nnz 12272

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℕcn 11903  ℤcz 12249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-i2m1 10870  ax-1ne0 10871  ax-rrecex 10874  ax-cnre 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-neg 11138  df-nn 11904  df-z 12250

This theorem is referenced by:  elnnz1  12276  znegcl  12285  nnleltp1  12305  nnltp1le  12306  nnlem1lt  12316  nnltlem1  12317  nnm1ge0  12318  prime  12331  nneo  12334  zeo  12336  btwnz  12352  eluz2b2  12590  qaddcl  12634  qreccl  12638  elpqb  12645  elfz1end  13215  fznatpl1  13239  fznn  13253  elfz1b  13254  elfzo0  13356  elfzo0z  13357  elfzo1  13365  fzo1fzo0n0  13366  elfzom1p1elfzo  13395  ubmelm1fzo  13411  quoremz  13503  intfracq  13507  fznnfl  13510  zmodcl  13539  zmodfz  13541  zmodfzo  13542  zmodid2  13547  zmodidfzo  13548  modfzo0difsn  13591  expnnval  13713  mulexpz  13751  nnesq  13870  expnlbnd  13876  expnlbnd2  13877  digit2  13879  faclbnd  13932  bc0k  13953  bcval5  13960  fz1isolem  14103  seqcoll  14106  ccatval21sw  14218  lswccatn0lsw  14224  cshwidxmod  14444  cshwidxn  14450  absexpz  14945  climuni  15189  isercoll  15307  climcnds  15491  arisum  15500  trireciplem  15502  expcnv  15504  pwdif  15508  geo2sum  15513  geo2lim  15515  0.999...  15521  geoihalfsum  15522  rpnnen2lem6  15856  rpnnen2lem9  15859  rpnnen2lem10  15860  dvdsval3  15895  nndivdvds  15900  modmulconst  15925  dvdsle  15947  dvdsssfz1  15955  fzm1ndvds  15959  dvdsfac  15963  mulmoddvds  15967  oexpneg  15982  nnoddm1d2  16023  pwp1fsum  16028  divalg2  16042  divalgmod  16043  modremain  16045  ndvdsadd  16047  nndvdslegcd  16140  divgcdz  16146  divgcdnn  16150  divgcdnnr  16151  modgcd  16168  gcdmultiple  16172  gcddiv  16187  gcdmultipleOLD  16188  gcdmultiplezOLD  16189  gcdzeq  16190  gcdeq  16191  rpmulgcd  16194  rplpwr  16195  rprpwr  16196  sqgcd  16198  dvdssqlem  16199  dvdssq  16200  eucalginv  16217  lcmgcdlem  16239  lcmgcdnn  16244  lcmass  16247  lcmftp  16269  lcmfunsnlem2lem1  16271  coprmgcdb  16282  qredeq  16290  qredeu  16291  coprmprod  16294  coprmproddvdslem  16295  coprmproddvds  16296  cncongr1  16300  cncongr2  16301  1idssfct  16313  isprm2lem  16314  isprm3  16316  prmind2  16318  ge2nprmge4  16334  divgcdodd  16343  isprm6  16347  ncoprmlnprm  16360  divnumden  16380  divdenle  16381  nn0gcdsq  16384  phicl2  16397  phiprmpw  16405  eulerthlem2  16411  hashgcdlem  16417  hashgcdeq  16418  phisum  16419  nnoddn2prm  16440  pythagtriplem3  16447  pythagtriplem4  16448  pythagtriplem6  16450  pythagtriplem7  16451  pythagtriplem8  16452  pythagtriplem9  16453  pythagtriplem11  16454  pythagtriplem13  16456  pythagtriplem15  16458  pythagtriplem19  16462  pythagtrip  16463  iserodd  16464  pclem  16467  pccl  16478  pcdiv  16481  pcqcl  16485  pcdvds  16493  pcndvds  16495  pcndvds2  16497  pcelnn  16499  pcz  16510  pcmpt  16521  fldivp1  16526  pcfac  16528  infpnlem1  16539  prmunb  16543  prmreclem1  16545  1arith  16556  ram0  16651  prmdvdsprmo  16671  prmgaplem4  16683  prmgaplem6  16685  prmgaplem7  16686  cshwshashlem2  16726  setsstruct2  16803  mulgnn  18623  mulgaddcom  18642  mulginvcom  18643  mulgmodid  18657  ghmmulg  18761  dfod2  19086  gexdvds  19104  gexnnod  19108  gexex  19369  mulgass2  19755  qsssubdrg  20569  prmirredlem  20606  znidomb  20681  znrrg  20685  chfacfisf  21911  chfacfisfcpmat  21912  chfacfscmul0  21915  chfacfpmmul0  21919  cayhamlem1  21923  cpmadugsumlemF  21933  lmmo  22439  1stckgenlem  22612  imasdsf1olem  23434  clmmulg  24170  cmetcaulem  24357  ovolunlem1a  24565  ovolicc2lem4  24589  mbfi1fseqlem6  24790  dvexp3  25047  dgreq0  25331  elqaalem2  25385  aaliou3lem1  25407  aaliou3lem2  25408  aaliou3lem3  25409  aaliou3lem9  25415  pserdvlem2  25492  logtayl2  25722  root1eq1  25813  root1cj  25814  logbgcd1irr  25849  atantayl2  25993  birthdaylem2  26007  birthdaylem3  26008  emcllem5  26054  basellem2  26136  basellem3  26137  basellem5  26139  issqf  26190  sgmnncl  26201  prmorcht  26232  mumullem1  26233  mumullem2  26234  sqff1o  26236  dvdsflsumcom  26242  muinv  26247  vmalelog  26258  chtublem  26264  vmasum  26269  logfac2  26270  logfaclbnd  26275  bclbnd  26333  bposlem5  26341  lgsval4a  26372  lgssq2  26391  lgsdchr  26408  gausslemma2dlem0c  26411  gausslemma2dlem0e  26413  gausslemma2dlem1a  26418  gausslemma2dlem5  26424  lgsquadlem1  26433  lgsquadlem2  26434  lgsquad3  26440  2lgslem1a1  26442  2lgslem3  26457  2lgsoddprm  26469  2sqnn  26492  2sqreunnltlem  26503  rplogsumlem1  26537  rplogsumlem2  26538  dchrisumlem2  26543  dchrmusumlema  26546  dchrmusum2  26547  dchrvmasumiflem1  26554  dchrvmaeq0  26557  dchrisum0flblem2  26562  dchrisum0re  26566  dchrisum0lema  26567  dchrisum0lem1b  26568  dchrisum0lem2a  26570  logdivbnd  26609  pntrsumbnd2  26620  ostth2lem1  26671  ostth2lem3  26688  ostth3  26691  axlowdimlem13  27225  crctcshwlkn0lem4  28079  crctcshwlkn0lem5  28080  crctcshwlkn0lem7  28082  wlkiswwlksupgr2  28143  clwwisshclwwslem  28279  clwwlkinwwlk  28305  clwwlkel  28311  clwwlkf  28312  wwlksubclwwlk  28323  clwwlkvbij  28378  eucrctshift  28508  eucrct2eupth  28510  numclwlk2lem2f  28642  bcm1n  31018  pnfinf  31339  isarchiofld  31418  rearchi  31448  submat1n  31657  lmatfvlem  31667  esumcvg  31954  oddpwdc  32221  fibp1  32268  chtvalz  32509  nnltp1ne  32969  erdszelem7  33059  climuzcnv  33529  elfzm12  33533  bcprod  33610  nn0prpwlem  34438  knoppndvlem1  34619  knoppndvlem2  34620  knoppndvlem7  34625  knoppndvlem18  34636  poimirlem13  35717  poimirlem14  35718  mblfinlem2  35742  fzmul  35826  incsequz  35833  geomcau  35844  heibor1lem  35894  bfplem2  35908  lcmfunnnd  39948  metakunt16  40068  metakunt26  40078  nn0rppwr  40254  nn0expgcd  40256  dvdsexpnn  40261  dvdsexpnn0  40262  zrtdvds  40267  fzsplit1nn0  40492  irrapxlem1  40560  pellexlem5  40571  rmynn  40694  jm2.24nn  40697  jm2.17c  40700  congrep  40711  congabseq  40712  acongrep  40718  acongeq  40721  jm2.18  40726  jm2.23  40734  jm2.20nn  40735  jm2.26lem3  40739  jm2.26  40740  jm2.15nn0  40741  jm2.16nn0  40742  jm2.27dlem2  40748  rmydioph  40752  jm3.1  40758  expdiophlem1  40759  expdioph  40761  idomodle  40937  proot1ex  40942  nznngen  41823  sumnnodd  43061  stoweidlem7  43438  stoweidlem17  43448  wallispilem4  43499  stirlinglem2  43506  stirlinglem3  43507  stirlinglem4  43508  stirlinglem12  43516  stirlinglem13  43517  stirlinglem14  43518  stirlinglem15  43519  stirlingr  43521  dirkertrigeqlem1  43529  fouriersw  43662  ovnsubaddlem1  43998  subsubelfzo0  44706  2ffzoeq  44708  iccpartres  44758  iccpartipre  44761  iccpartltu  44765  iccelpart  44773  odz2prm2pw  44903  fmtnoprmfac2lem1  44906  2pwp1prm  44929  lighneallem2  44946  lighneallem4  44950  lighneal  44951  proththd  44954  nneoALTV  45012  divgcdoddALTV  45022  fpprmod  45067  fppr2odd  45071  dfwppr  45078  fpprwppr  45079  fpprwpprb  45080  gbowge7  45103  gbege6  45105  altgsumbc  45576  altgsumbcALT  45577  pw2m1lepw2m1  45749  nnpw2even  45763  nnlog2ge0lt1  45800  logbpw2m1  45801  blenpw2m1  45813  nnpw2blenfzo  45815  nnpw2pmod  45817  nnpw2p  45820  blengt1fldiv2p1  45827  dignn0fr  45835  dignn0flhalflem1  45849  dignn0flhalflem2  45850  nn0sumshdiglemA  45853  nn0sumshdiglemB  45854