Theorem nnz 11992

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℕcn 11625  ℤcz 11969

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-i2m1 10594  ax-1ne0 10595  ax-rrecex 10598  ax-cnre 10599

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-ov 7138  df-om 7561  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-neg 10862  df-nn 11626  df-z 11970

This theorem is referenced by:  elnnz1  11996  znegcl  12005  nnleltp1  12025  nnltp1le  12026  nnlem1lt  12036  nnltlem1  12037  nnm1ge0  12038  prime  12051  nneo  12054  zeo  12056  btwnz  12072  eluz2b2  12309  qaddcl  12352  qreccl  12356  elpqb  12363  elfz1end  12932  fznatpl1  12956  fznn  12970  elfz1b  12971  elfzo0  13073  elfzo0z  13074  elfzo1  13082  fzo1fzo0n0  13083  elfzom1p1elfzo  13112  ubmelm1fzo  13128  quoremz  13218  intfracq  13222  fznnfl  13225  zmodcl  13254  zmodfz  13256  zmodfzo  13257  zmodid2  13262  zmodidfzo  13263  modfzo0difsn  13306  expnnval  13428  mulexpz  13465  nnesq  13584  expnlbnd  13590  expnlbnd2  13591  digit2  13593  faclbnd  13646  bc0k  13667  bcval5  13674  fz1isolem  13815  seqcoll  13818  ccatval21sw  13930  lswccatn0lsw  13936  cshwidxmod  14156  cshwidxn  14162  absexpz  14657  climuni  14901  isercoll  15016  climcnds  15198  arisum  15207  trireciplem  15209  expcnv  15211  pwdif  15215  geo2sum  15221  geo2lim  15223  0.999...  15229  geoihalfsum  15230  rpnnen2lem6  15564  rpnnen2lem9  15567  rpnnen2lem10  15568  dvdsval3  15603  nndivdvds  15608  modmulconst  15633  dvdsle  15652  dvdsssfz1  15660  fzm1ndvds  15664  dvdsfac  15668  mulmoddvds  15671  oexpneg  15686  nnoddm1d2  15727  pwp1fsum  15732  divalg2  15746  divalgmod  15747  modremain  15749  ndvdsadd  15751  nndvdslegcd  15844  divgcdz  15850  divgcdnn  15853  divgcdnnr  15854  modgcd  15870  gcdmultiple  15874  gcddiv  15889  gcdmultipleOLD  15890  gcdmultiplezOLD  15891  gcdzeq  15892  gcdeq  15893  rpmulgcd  15896  rplpwr  15897  rppwr  15898  sqgcd  15899  dvdssqlem  15900  dvdssq  15901  eucalginv  15918  lcmgcdlem  15940  lcmgcdnn  15945  lcmass  15948  lcmftp  15970  lcmfunsnlem2lem1  15972  coprmgcdb  15983  qredeq  15991  qredeu  15992  coprmprod  15995  coprmproddvdslem  15996  coprmproddvds  15997  cncongr1  16001  cncongr2  16002  1idssfct  16014  isprm2lem  16015  isprm3  16017  prmind2  16019  ge2nprmge4  16035  divgcdodd  16044  isprm6  16048  ncoprmlnprm  16058  divnumden  16078  divdenle  16079  nn0gcdsq  16082  phicl2  16095  phiprmpw  16103  eulerthlem2  16109  hashgcdlem  16115  hashgcdeq  16116  phisum  16117  nnoddn2prm  16138  pythagtriplem3  16145  pythagtriplem4  16146  pythagtriplem6  16148  pythagtriplem7  16149  pythagtriplem8  16150  pythagtriplem9  16151  pythagtriplem11  16152  pythagtriplem13  16154  pythagtriplem15  16156  pythagtriplem19  16160  pythagtrip  16161  iserodd  16162  pclem  16165  pccl  16176  pcdiv  16179  pcqcl  16183  pcdvds  16190  pcndvds  16192  pcndvds2  16194  pcelnn  16196  pcz  16207  pcmpt  16218  fldivp1  16223  pcfac  16225  infpnlem1  16236  prmunb  16240  prmreclem1  16242  1arith  16253  ram0  16348  prmdvdsprmo  16368  prmgaplem4  16380  prmgaplem6  16382  prmgaplem7  16383  cshwshashlem2  16422  setsstruct2  16513  mulgnn  18224  mulgaddcom  18243  mulginvcom  18244  mulgmodid  18258  ghmmulg  18362  dfod2  18683  gexdvds  18701  gexnnod  18705  gexex  18966  mulgass2  19347  qsssubdrg  20150  prmirredlem  20186  znidomb  20253  znrrg  20257  chfacfisf  21459  chfacfisfcpmat  21460  chfacfscmul0  21463  chfacfpmmul0  21467  cayhamlem1  21471  cpmadugsumlemF  21481  lmmo  21985  1stckgenlem  22158  imasdsf1olem  22980  clmmulg  23706  cmetcaulem  23892  ovolunlem1a  24100  ovolicc2lem4  24124  mbfi1fseqlem6  24324  dvexp3  24581  dgreq0  24862  elqaalem2  24916  aaliou3lem1  24938  aaliou3lem2  24939  aaliou3lem3  24940  aaliou3lem9  24946  pserdvlem2  25023  logtayl2  25253  root1eq1  25344  root1cj  25345  logbgcd1irr  25380  atantayl2  25524  birthdaylem2  25538  birthdaylem3  25539  emcllem5  25585  basellem2  25667  basellem3  25668  basellem5  25670  issqf  25721  sgmnncl  25732  prmorcht  25763  mumullem1  25764  mumullem2  25765  sqff1o  25767  dvdsflsumcom  25773  muinv  25778  vmalelog  25789  chtublem  25795  vmasum  25800  logfac2  25801  logfaclbnd  25806  bclbnd  25864  bposlem5  25872  lgsval4a  25903  lgssq2  25922  lgsdchr  25939  gausslemma2dlem0c  25942  gausslemma2dlem0e  25944  gausslemma2dlem1a  25949  gausslemma2dlem5  25955  lgsquadlem1  25964  lgsquadlem2  25965  lgsquad3  25971  2lgslem1a1  25973  2lgslem3  25988  2lgsoddprm  26000  2sqnn  26023  2sqreunnltlem  26034  rplogsumlem1  26068  rplogsumlem2  26069  dchrisumlem2  26074  dchrmusumlema  26077  dchrmusum2  26078  dchrvmasumiflem1  26085  dchrvmaeq0  26088  dchrisum0flblem2  26093  dchrisum0re  26097  dchrisum0lema  26098  dchrisum0lem1b  26099  dchrisum0lem2a  26101  logdivbnd  26140  pntrsumbnd2  26151  ostth2lem1  26202  ostth2lem3  26219  ostth3  26222  axlowdimlem13  26748  crctcshwlkn0lem4  27599  crctcshwlkn0lem5  27600  crctcshwlkn0lem7  27602  wlkiswwlksupgr2  27663  clwwisshclwwslem  27799  clwwlkinwwlk  27825  clwwlkel  27831  clwwlkf  27832  wwlksubclwwlk  27843  clwwlkvbij  27898  eucrctshift  28028  eucrct2eupth  28030  numclwlk2lem2f  28162  bcm1n  30544  pnfinf  30862  isarchiofld  30941  rearchi  30966  submat1n  31158  lmatfvlem  31168  esumcvg  31455  oddpwdc  31722  fibp1  31769  chtvalz  32010  nnltp1ne  32459  erdszelem7  32557  climuzcnv  33027  elfzm12  33031  bcprod  33083  nn0prpwlem  33783  knoppndvlem1  33964  knoppndvlem2  33965  knoppndvlem7  33970  knoppndvlem18  33981  poimirlem13  35070  poimirlem14  35071  mblfinlem2  35095  fzmul  35179  incsequz  35186  geomcau  35197  heibor1lem  35247  bfplem2  35261  lcmfunnnd  39300  metakunt16  39365  metakunt26  39375  nn0rppwr  39490  nn0expgcd  39492  zrtdvds  39501  fzsplit1nn0  39695  irrapxlem1  39763  pellexlem5  39774  rmynn  39897  jm2.24nn  39900  jm2.17c  39903  congrep  39914  congabseq  39915  acongrep  39921  acongeq  39924  jm2.18  39929  jm2.23  39937  jm2.20nn  39938  jm2.26lem3  39942  jm2.26  39943  jm2.15nn0  39944  jm2.16nn0  39945  jm2.27dlem2  39951  rmydioph  39955  jm3.1  39961  expdiophlem1  39962  expdioph  39964  idomodle  40140  proot1ex  40145  nznngen  41020  sumnnodd  42272  stoweidlem7  42649  stoweidlem17  42659  wallispilem4  42710  stirlinglem2  42717  stirlinglem3  42718  stirlinglem4  42719  stirlinglem12  42727  stirlinglem13  42728  stirlinglem14  42729  stirlinglem15  42730  stirlingr  42732  dirkertrigeqlem1  42740  fouriersw  42873  ovnsubaddlem1  43209  subsubelfzo0  43883  2ffzoeq  43885  iccpartres  43935  iccpartipre  43938  iccpartltu  43942  iccelpart  43950  odz2prm2pw  44080  fmtnoprmfac2lem1  44083  2pwp1prm  44106  lighneallem2  44124  lighneallem4  44128  lighneal  44129  proththd  44132  nneoALTV  44190  divgcdoddALTV  44200  fpprmod  44245  fppr2odd  44249  dfwppr  44256  fpprwppr  44257  fpprwpprb  44258  gbowge7  44281  gbege6  44283  altgsumbc  44754  altgsumbcALT  44755  pw2m1lepw2m1  44929  nnpw2even  44943  nnlog2ge0lt1  44980  logbpw2m1  44981  blenpw2m1  44993  nnpw2blenfzo  44995  nnpw2pmod  44997  nnpw2p  45000  blengt1fldiv2p1  45007  dignn0fr  45015  dignn0flhalflem1  45029  dignn0flhalflem2  45030  nn0sumshdiglemA  45033  nn0sumshdiglemB  45034