Theorem nnz 12351

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℕcn 11982  ℤcz 12328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353  ax-un 7597  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-i2m1 10948  ax-1ne0 10949  ax-rrecex 10952  ax-cnre 10953

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-ov 7287  df-om 7722  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-neg 11217  df-nn 11983  df-z 12329

This theorem is referenced by:  elnnz1  12355  znegcl  12364  nnleltp1  12384  nnltp1le  12385  nnlem1lt  12395  nnltlem1  12396  nnm1ge0  12397  prime  12410  nneo  12413  zeo  12415  btwnz  12432  eluz2b2  12670  qaddcl  12714  qreccl  12718  elpqb  12725  elfz1end  13295  fznatpl1  13319  fznn  13333  elfz1b  13334  elfzo0  13437  elfzo0z  13438  elfzo1  13446  fzo1fzo0n0  13447  elfzom1p1elfzo  13476  ubmelm1fzo  13492  quoremz  13584  intfracq  13588  fznnfl  13591  zmodcl  13620  zmodfz  13622  zmodfzo  13623  zmodid2  13628  zmodidfzo  13629  modfzo0difsn  13672  expnnval  13794  mulexpz  13832  nnesq  13951  expnlbnd  13957  expnlbnd2  13958  digit2  13960  faclbnd  14013  bc0k  14034  bcval5  14041  fz1isolem  14184  seqcoll  14187  ccatval21sw  14299  lswccatn0lsw  14305  cshwidxmod  14525  cshwidxn  14531  absexpz  15026  climuni  15270  isercoll  15388  climcnds  15572  arisum  15581  trireciplem  15583  expcnv  15585  pwdif  15589  geo2sum  15594  geo2lim  15596  0.999...  15602  geoihalfsum  15603  rpnnen2lem6  15937  rpnnen2lem9  15940  rpnnen2lem10  15941  dvdsval3  15976  nndivdvds  15981  modmulconst  16006  dvdsle  16028  dvdsssfz1  16036  fzm1ndvds  16040  dvdsfac  16044  mulmoddvds  16048  oexpneg  16063  nnoddm1d2  16104  pwp1fsum  16109  divalg2  16123  divalgmod  16124  modremain  16126  ndvdsadd  16128  nndvdslegcd  16221  divgcdz  16227  divgcdnn  16231  divgcdnnr  16232  modgcd  16249  gcdmultiple  16253  gcddiv  16268  gcdmultipleOLD  16269  gcdmultiplezOLD  16270  gcdzeq  16271  gcdeq  16272  rpmulgcd  16275  rplpwr  16276  rprpwr  16277  sqgcd  16279  dvdssqlem  16280  dvdssq  16281  eucalginv  16298  lcmgcdlem  16320  lcmgcdnn  16325  lcmass  16328  lcmftp  16350  lcmfunsnlem2lem1  16352  coprmgcdb  16363  qredeq  16371  qredeu  16372  coprmprod  16375  coprmproddvdslem  16376  coprmproddvds  16377  cncongr1  16381  cncongr2  16382  1idssfct  16394  isprm2lem  16395  isprm3  16397  prmind2  16399  ge2nprmge4  16415  divgcdodd  16424  isprm6  16428  ncoprmlnprm  16441  divnumden  16461  divdenle  16462  nn0gcdsq  16465  phicl2  16478  phiprmpw  16486  eulerthlem2  16492  hashgcdlem  16498  hashgcdeq  16499  phisum  16500  nnoddn2prm  16521  pythagtriplem3  16528  pythagtriplem4  16529  pythagtriplem6  16531  pythagtriplem7  16532  pythagtriplem8  16533  pythagtriplem9  16534  pythagtriplem11  16535  pythagtriplem13  16537  pythagtriplem15  16539  pythagtriplem19  16543  pythagtrip  16544  iserodd  16545  pclem  16548  pccl  16559  pcdiv  16562  pcqcl  16566  pcdvds  16574  pcndvds  16576  pcndvds2  16578  pcelnn  16580  pcz  16591  pcmpt  16602  fldivp1  16607  pcfac  16609  infpnlem1  16620  prmunb  16624  prmreclem1  16626  1arith  16637  ram0  16732  prmdvdsprmo  16752  prmgaplem4  16764  prmgaplem6  16766  prmgaplem7  16767  cshwshashlem2  16807  setsstruct2  16884  mulgnn  18717  mulgaddcom  18736  mulginvcom  18737  mulgmodid  18751  ghmmulg  18855  dfod2  19180  gexdvds  19198  gexnnod  19202  gexex  19463  mulgass2  19849  qsssubdrg  20666  prmirredlem  20703  znidomb  20778  znrrg  20782  chfacfisf  22012  chfacfisfcpmat  22013  chfacfscmul0  22016  chfacfpmmul0  22020  cayhamlem1  22024  cpmadugsumlemF  22034  lmmo  22540  1stckgenlem  22713  imasdsf1olem  23535  clmmulg  24273  cmetcaulem  24461  ovolunlem1a  24669  ovolicc2lem4  24693  mbfi1fseqlem6  24894  dvexp3  25151  dgreq0  25435  elqaalem2  25489  aaliou3lem1  25511  aaliou3lem2  25512  aaliou3lem3  25513  aaliou3lem9  25519  pserdvlem2  25596  logtayl2  25826  root1eq1  25917  root1cj  25918  logbgcd1irr  25953  atantayl2  26097  birthdaylem2  26111  birthdaylem3  26112  emcllem5  26158  basellem2  26240  basellem3  26241  basellem5  26243  issqf  26294  sgmnncl  26305  prmorcht  26336  mumullem1  26337  mumullem2  26338  sqff1o  26340  dvdsflsumcom  26346  muinv  26351  vmalelog  26362  chtublem  26368  vmasum  26373  logfac2  26374  logfaclbnd  26379  bclbnd  26437  bposlem5  26445  lgsval4a  26476  lgssq2  26495  lgsdchr  26512  gausslemma2dlem0c  26515  gausslemma2dlem0e  26517  gausslemma2dlem1a  26522  gausslemma2dlem5  26528  lgsquadlem1  26537  lgsquadlem2  26538  lgsquad3  26544  2lgslem1a1  26546  2lgslem3  26561  2lgsoddprm  26573  2sqnn  26596  2sqreunnltlem  26607  rplogsumlem1  26641  rplogsumlem2  26642  dchrisumlem2  26647  dchrmusumlema  26650  dchrmusum2  26651  dchrvmasumiflem1  26658  dchrvmaeq0  26661  dchrisum0flblem2  26666  dchrisum0re  26670  dchrisum0lema  26671  dchrisum0lem1b  26672  dchrisum0lem2a  26674  logdivbnd  26713  pntrsumbnd2  26724  ostth2lem1  26775  ostth2lem3  26792  ostth3  26795  axlowdimlem13  27331  crctcshwlkn0lem4  28187  crctcshwlkn0lem5  28188  crctcshwlkn0lem7  28190  wlkiswwlksupgr2  28251  clwwisshclwwslem  28387  clwwlkinwwlk  28413  clwwlkel  28419  clwwlkf  28420  wwlksubclwwlk  28431  clwwlkvbij  28486  eucrctshift  28616  eucrct2eupth  28618  numclwlk2lem2f  28750  bcm1n  31125  pnfinf  31446  isarchiofld  31525  rearchi  31555  submat1n  31764  lmatfvlem  31774  esumcvg  32063  oddpwdc  32330  fibp1  32377  chtvalz  32618  nnltp1ne  33078  erdszelem7  33168  climuzcnv  33638  elfzm12  33642  bcprod  33713  nn0prpwlem  34520  knoppndvlem1  34701  knoppndvlem2  34702  knoppndvlem7  34707  knoppndvlem18  34718  poimirlem13  35799  poimirlem14  35800  mblfinlem2  35824  fzmul  35908  incsequz  35915  geomcau  35926  heibor1lem  35976  bfplem2  35990  lcmfunnnd  40027  metakunt16  40147  metakunt26  40157  nn0rppwr  40340  nn0expgcd  40342  dvdsexpnn  40347  dvdsexpnn0  40348  zrtdvds  40353  fzsplit1nn0  40583  irrapxlem1  40651  pellexlem5  40662  rmynn  40785  jm2.24nn  40788  jm2.17c  40791  congrep  40802  congabseq  40803  acongrep  40809  acongeq  40812  jm2.18  40817  jm2.23  40825  jm2.20nn  40826  jm2.26lem3  40830  jm2.26  40831  jm2.15nn0  40832  jm2.16nn0  40833  jm2.27dlem2  40839  rmydioph  40843  jm3.1  40849  expdiophlem1  40850  expdioph  40852  idomodle  41028  proot1ex  41033  nznngen  41941  sumnnodd  43178  stoweidlem7  43555  stoweidlem17  43565  wallispilem4  43616  stirlinglem2  43623  stirlinglem3  43624  stirlinglem4  43625  stirlinglem12  43633  stirlinglem13  43634  stirlinglem14  43635  stirlinglem15  43636  stirlingr  43638  dirkertrigeqlem1  43646  fouriersw  43779  ovnsubaddlem1  44115  subsubelfzo0  44829  2ffzoeq  44831  iccpartres  44881  iccpartipre  44884  iccpartltu  44888  iccelpart  44896  odz2prm2pw  45026  fmtnoprmfac2lem1  45029  2pwp1prm  45052  lighneallem2  45069  lighneallem4  45073  lighneal  45074  proththd  45077  nneoALTV  45135  divgcdoddALTV  45145  fpprmod  45190  fppr2odd  45194  dfwppr  45201  fpprwppr  45202  fpprwpprb  45203  gbowge7  45226  gbege6  45228  altgsumbc  45699  altgsumbcALT  45700  pw2m1lepw2m1  45872  nnpw2even  45886  nnlog2ge0lt1  45923  logbpw2m1  45924  blenpw2m1  45936  nnpw2blenfzo  45938  nnpw2pmod  45940  nnpw2p  45943  blengt1fldiv2p1  45950  dignn0fr  45958  dignn0flhalflem1  45972  dignn0flhalflem2  45973  nn0sumshdiglemA  45976  nn0sumshdiglemB  45977