Theorem nnz 11751

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℕcn 11374  ℤcz 11728

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-i2m1 10340  ax-1ne0 10341  ax-rrecex 10344  ax-cnre 10345

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-ov 6925  df-om 7344  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-neg 10609  df-nn 11375  df-z 11729

This theorem is referenced by:  elnnz1  11755  znegcl  11764  nnleltp1  11784  nnltp1le  11785  nnlem1lt  11795  nnltlem1  11796  nnm1ge0  11797  prime  11810  nneo  11813  zeo  11815  btwnz  11831  eluz2b2  12068  qaddcl  12112  qreccl  12116  elpqb  12123  elfz1end  12688  fznatpl1  12712  fznn  12726  elfz1b  12727  elfzo0  12828  elfzo0z  12829  elfzo1  12837  fzo1fzo0n0  12838  ubmelm1fzo  12883  quoremz  12973  intfracq  12977  fznnfl  12980  zmodcl  13009  zmodfz  13011  zmodfzo  13012  zmodid2  13017  zmodidfzo  13018  modfzo0difsn  13061  expnnval  13181  mulexpz  13218  nnesq  13307  expnlbnd  13313  expnlbnd2  13314  digit2  13316  faclbnd  13395  bc0k  13416  bcval5  13423  fz1isolem  13559  seqcoll  13562  ccatval21sw  13675  lswccatn0lsw  13681  cshwidxmod  13954  cshwidxn  13960  absexpz  14452  climuni  14691  isercoll  14806  climcnds  14987  arisum  14996  trireciplem  14998  expcnv  15000  geo2sum  15008  geo2lim  15010  0.999...  15016  geoihalfsum  15017  rpnnen2lem6  15352  rpnnen2lem9  15355  rpnnen2lem10  15356  dvdsval3  15391  nndivdvds  15396  modmulconst  15420  dvdsle  15439  dvdsssfz1  15447  fzm1ndvds  15451  dvdsfac  15455  mulmoddvds  15458  oexpneg  15473  nnoddm1d2  15516  pwp1fsum  15521  divalg2  15535  divalgmod  15536  modremain  15538  ndvdsadd  15540  nndvdslegcd  15633  divgcdz  15639  divgcdnn  15642  divgcdnnr  15643  modgcd  15659  gcddiv  15674  gcdmultiple  15675  gcdmultiplez  15676  gcdzeq  15677  gcdeq  15678  rpmulgcd  15681  rplpwr  15682  rppwr  15683  sqgcd  15684  dvdssqlem  15685  dvdssq  15686  eucalginv  15703  lcmgcdlem  15725  lcmgcdnn  15730  lcmass  15733  lcmftp  15755  lcmfunsnlem2lem1  15757  coprmgcdb  15768  qredeq  15776  qredeu  15777  coprmprod  15780  coprmproddvdslem  15781  coprmproddvds  15782  cncongr1  15786  cncongr2  15787  1idssfct  15798  isprm2lem  15799  isprm3  15801  prmind2  15803  divgcdodd  15826  isprm6  15830  ncoprmlnprm  15840  divnumden  15860  divdenle  15861  nn0gcdsq  15864  phicl2  15877  phiprmpw  15885  eulerthlem2  15891  hashgcdlem  15897  hashgcdeq  15898  phisum  15899  nnoddn2prm  15920  pythagtriplem3  15927  pythagtriplem4  15928  pythagtriplem6  15930  pythagtriplem7  15931  pythagtriplem8  15932  pythagtriplem9  15933  pythagtriplem11  15934  pythagtriplem13  15936  pythagtriplem15  15938  pythagtriplem19  15942  pythagtrip  15943  iserodd  15944  pclem  15947  pccl  15958  pcdiv  15961  pcqcl  15965  pcdvds  15972  pcndvds  15974  pcndvds2  15976  pcelnn  15978  pcz  15989  pcmpt  16000  fldivp1  16005  pcfac  16007  infpnlem1  16018  prmunb  16022  prmreclem1  16024  1arith  16035  ram0  16130  prmdvdsprmo  16150  prmgaplem4  16162  prmgaplem6  16164  prmgaplem7  16165  cshwshashlem2  16202  setsstruct2  16293  mulgnn  17934  mulgaddcom  17950  mulginvcom  17951  mulgmodid  17965  ghmmulg  18056  dfod2  18365  gexdvds  18383  gexnnod  18387  gexex  18642  mulgass2  18988  qsssubdrg  20201  prmirredlem  20237  znidomb  20305  znrrg  20309  chfacfisf  21066  chfacfisfcpmat  21067  chfacfscmul0  21070  chfacfpmmul0  21074  cayhamlem1  21078  cpmadugsumlemF  21088  lmmo  21592  1stckgenlem  21765  imasdsf1olem  22586  clmmulg  23308  cmetcaulem  23494  ovolunlem1a  23700  ovolicc2lem4  23724  mbfi1fseqlem6  23924  dvexp3  24178  dgreq0  24458  elqaalem2  24512  aaliou3lem1  24534  aaliou3lem2  24535  aaliou3lem3  24536  aaliou3lem9  24542  pserdvlem2  24619  logtayl2  24845  root1eq1  24936  root1cj  24937  logbgcd1irr  24972  atantayl2  25116  birthdaylem2  25131  birthdaylem3  25132  emcllem5  25178  basellem2  25260  basellem3  25261  basellem5  25263  issqf  25314  sgmnncl  25325  prmorcht  25356  mumullem1  25357  mumullem2  25358  sqff1o  25360  dvdsflsumcom  25366  muinv  25371  vmalelog  25382  chtublem  25388  vmasum  25393  logfac2  25394  logfaclbnd  25399  bclbnd  25457  bposlem5  25465  lgsval4a  25496  lgssq2  25515  lgsdchr  25532  gausslemma2dlem0c  25535  gausslemma2dlem0e  25537  gausslemma2dlem1a  25542  gausslemma2dlem5  25548  lgsquadlem1  25557  lgsquadlem2  25558  lgsquad3  25564  2lgslem1a1  25566  2lgslem3  25581  2lgsoddprm  25593  rplogsumlem1  25625  rplogsumlem2  25626  dchrisumlem2  25631  dchrmusumlema  25634  dchrmusum2  25635  dchrvmasumiflem1  25642  dchrvmaeq0  25645  dchrisum0flblem2  25650  dchrisum0re  25654  dchrisum0lema  25655  dchrisum0lem1b  25656  dchrisum0lem2a  25658  logdivbnd  25697  pntrsumbnd2  25708  ostth2lem1  25759  ostth2lem3  25776  ostth3  25779  axlowdimlem13  26303  crctcshwlkn0lem4  27162  crctcshwlkn0lem5  27163  crctcshwlkn0lem7  27165  wlkiswwlksupgr2  27226  clwwisshclwwslem  27403  clwwlkinwwlk  27429  clwwlkinwwlkOLD  27430  clwwlkel  27437  clwwlkfOLD  27438  clwwlkf  27443  wwlksubclwwlk  27455  wwlksubclwwlkOLD  27456  clwwlkvbij  27515  clwwlkvbijOLD  27516  eucrctshift  27647  eucrct2eupthOLD  27650  eucrct2eupth  27651  numclwlk2lem2f  27805  numclwlk2lem2fOLD  27808  bcm1n  30118  pnfinf  30299  isarchiofld  30379  rearchi  30404  submat1n  30469  lmatfvlem  30479  esumcvg  30746  oddpwdc  31014  fibp1  31062  chtvalz  31309  erdszelem7  31778  climuzcnv  32162  elfzm12  32166  bcprod  32218  nn0prpwlem  32905  knoppndvlem1  33085  knoppndvlem2  33086  knoppndvlem7  33091  knoppndvlem18  33102  poimirlem13  34050  poimirlem14  34051  mblfinlem2  34075  fzmul  34163  incsequz  34170  geomcau  34181  heibor1lem  34234  bfplem2  34248  nn0rppwr  38164  nn0expgcd  38166  zrtdvds  38173  fzsplit1nn0  38281  irrapxlem1  38350  pellexlem5  38361  rmynn  38486  jm2.24nn  38489  jm2.17c  38492  congrep  38503  congabseq  38504  acongrep  38510  acongeq  38513  jm2.18  38518  jm2.23  38526  jm2.20nn  38527  jm2.26lem3  38531  jm2.26  38532  jm2.15nn0  38533  jm2.16nn0  38534  jm2.27dlem2  38540  rmydioph  38544  jm3.1  38550  expdiophlem1  38551  expdioph  38553  idomodle  38737  proot1ex  38742  nznngen  39475  sumnnodd  40774  stoweidlem7  41155  stoweidlem17  41165  wallispilem4  41216  stirlinglem2  41223  stirlinglem3  41224  stirlinglem4  41225  stirlinglem12  41233  stirlinglem13  41234  stirlinglem14  41235  stirlinglem15  41236  stirlingr  41238  dirkertrigeqlem1  41246  fouriersw  41379  ovnsubaddlem1  41715  subsubelfzo0  42372  2ffzoeq  42374  iccpartres  42390  iccpartipre  42393  iccpartltu  42397  iccelpart  42405  odz2prm2pw  42500  fmtnoprmfac2lem1  42503  pwdif  42526  2pwp1prm  42528  lighneallem2  42548  lighneallem4  42552  lighneal  42553  proththd  42556  nneoALTV  42612  divgcdoddALTV  42622  gbowge7  42680  gbege6  42682  altgsumbc  43149  altgsumbcALT  43150  pw2m1lepw2m1  43329  nnpw2even  43342  nnlog2ge0lt1  43379  logbpw2m1  43380  blenpw2m1  43392  nnpw2blenfzo  43394  nnpw2pmod  43396  nnpw2p  43399  blengt1fldiv2p1  43406  dignn0fr  43414  dignn0flhalflem1  43428  dignn0flhalflem2  43429  nn0sumshdiglemA  43432  nn0sumshdiglemB  43433