Theorem nnz 11399

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

Syntax hints:   → wi 4   ∈ wcel 1990  ℕcn 11020  ℤcz 11377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-z 11378

This theorem is referenced by:  elnnz1  11403  znegcl  11412  nnleltp1  11432  nnltp1le  11433  nnlem1lt  11443  nnltlem1  11444  nnm1ge0  11445  prime  11458  nneo  11461  zeo  11463  btwnz  11479  eluz2b2  11761  qaddcl  11804  qreccl  11808  elfz1end  12371  fznatpl1  12395  fznn  12408  elfz1b  12409  elfzo0  12508  elfzo0z  12509  elfzo1  12517  fzo1fzo0n0  12518  ubmelm1fzo  12564  quoremz  12654  intfracq  12658  fznnfl  12661  zmodcl  12690  zmodfz  12692  zmodfzo  12693  zmodid2  12698  zmodidfzo  12699  modfzo0difsn  12742  expnnval  12863  mulexpz  12900  nnesq  12988  expnlbnd  12994  expnlbnd2  12995  digit2  12997  faclbnd  13077  bc0k  13098  bcval5  13105  fz1isolem  13245  seqcoll  13248  lswccatn0lsw  13373  cshwidxmod  13549  cshwidxn  13555  absexpz  14045  climuni  14283  isercoll  14398  climcnds  14583  arisum  14592  trireciplem  14594  expcnv  14596  geo2sum  14604  geo2lim  14606  0.999...  14612  0.999...OLD  14613  geoihalfsum  14614  rpnnen2lem6  14948  rpnnen2lem9  14951  rpnnen2lem10  14952  dvdsval3  14987  nndivdvds  14989  modmulconst  15013  dvdsle  15032  dvdsssfz1  15040  fzm1ndvds  15044  dvdsfac  15048  oexpneg  15069  nnoddm1d2  15102  pwp1fsum  15114  divalg2  15128  divalgmod  15129  divalgmodOLD  15130  modremain  15132  ndvdsadd  15134  nndvdslegcd  15227  divgcdz  15233  divgcdnn  15236  divgcdnnr  15237  modgcd  15253  gcddiv  15268  gcdmultiple  15269  gcdmultiplez  15270  gcdzeq  15271  gcdeq  15272  rpmulgcd  15275  rplpwr  15276  rppwr  15277  sqgcd  15278  dvdssqlem  15279  dvdssq  15280  eucalginv  15297  lcmgcdlem  15319  lcmgcdnn  15324  lcmass  15327  lcmftp  15349  lcmfunsnlem2lem1  15351  coprmgcdb  15362  qredeq  15371  qredeu  15372  coprmprod  15375  coprmproddvdslem  15376  coprmproddvds  15377  cncongr1  15381  cncongr2  15382  1idssfct  15393  isprm2lem  15394  isprm3  15396  prmind2  15398  divgcdodd  15422  isprm6  15426  ncoprmlnprm  15436  divnumden  15456  divdenle  15457  nn0gcdsq  15460  phicl2  15473  phiprmpw  15481  eulerthlem2  15487  hashgcdlem  15493  hashgcdeq  15494  phisum  15495  nnoddn2prm  15516  pythagtriplem3  15523  pythagtriplem4  15524  pythagtriplem6  15526  pythagtriplem7  15527  pythagtriplem8  15528  pythagtriplem9  15529  pythagtriplem11  15530  pythagtriplem13  15532  pythagtriplem15  15534  pythagtriplem19  15538  pythagtrip  15539  iserodd  15540  pclem  15543  pccl  15554  pcdiv  15557  pcqcl  15561  pcdvds  15568  pcndvds  15570  pcndvds2  15572  pcelnn  15574  pcz  15585  pcmpt  15596  fldivp1  15601  pcfac  15603  infpnlem1  15614  prmunb  15618  prmreclem1  15620  1arith  15631  ram0  15726  prmdvdsprmo  15746  prmgaplem4  15758  prmgaplem6  15760  prmgaplem7  15761  cshwshashlem2  15803  setsstruct2  15896  setsstructOLD  15899  mulgnn  17547  mulgaddcom  17564  mulginvcom  17565  mulgmodid  17581  ghmmulg  17672  dfod2  17981  gexdvds  17999  gexnnod  18003  gexex  18256  mulgass2  18601  qsssubdrg  19805  prmirredlem  19841  znidomb  19910  znrrg  19914  chfacfisf  20659  chfacfisfcpmat  20660  chfacfscmul0  20663  chfacfpmmul0  20667  cayhamlem1  20671  cpmadugsumlemF  20681  lmmo  21184  1stckgenlem  21356  imasdsf1olem  22178  clmmulg  22901  cmetcaulem  23086  ovolunlem1a  23264  ovolicc2lem4  23288  mbfi1fseqlem6  23487  dvexp3  23741  dgreq0  24021  elqaalem2  24075  aaliou3lem1  24097  aaliou3lem2  24098  aaliou3lem3  24099  aaliou3lem9  24105  pserdvlem2  24182  logtayl2  24408  root1eq1  24496  root1cj  24497  atantayl2  24665  birthdaylem2  24679  birthdaylem3  24680  emcllem5  24726  basellem2  24808  basellem3  24809  basellem5  24811  issqf  24862  sgmnncl  24873  prmorcht  24904  mumullem1  24905  mumullem2  24906  sqff1o  24908  dvdsflsumcom  24914  muinv  24919  vmalelog  24930  chtublem  24936  vmasum  24941  logfac2  24942  logfaclbnd  24947  bclbnd  25005  bposlem5  25013  lgsval4a  25044  lgssq2  25063  lgsdchr  25080  gausslemma2dlem0c  25083  gausslemma2dlem0e  25085  gausslemma2dlem1a  25090  gausslemma2dlem5  25096  lgsquadlem1  25105  lgsquadlem2  25106  lgsquad3  25112  2lgslem1a1  25114  2lgslem3  25129  2lgsoddprm  25141  rplogsumlem1  25173  rplogsumlem2  25174  dchrisumlem2  25179  dchrmusumlema  25182  dchrmusum2  25183  dchrvmasumiflem1  25190  dchrvmaeq0  25193  dchrisum0flblem2  25198  dchrisum0re  25202  dchrisum0lema  25203  dchrisum0lem1b  25204  dchrisum0lem2a  25206  logdivbnd  25245  pntrsumbnd2  25256  ostth2lem1  25307  ostth2lem3  25324  ostth3  25327  axlowdimlem13  25834  crctcshwlkn0lem4  26705  crctcshwlkn0lem5  26706  crctcshwlkn0lem7  26708  wlkiswwlksupgr2  26763  clwwlkinwwlk  26905  clwwlksel  26914  clwwlksf  26915  clwwlksvbij  26922  wwlksubclwwlks  26925  clwwisshclwwslem  26927  eucrctshift  27103  eucrct2eupth  27105  numclwlk2lem2f  27236  bcm1n  29554  pnfinf  29737  isarchiofld  29817  rearchi  29842  submat1n  29871  lmatfvlem  29881  esumcvg  30148  oddpwdc  30416  fibp1  30463  chtvalz  30707  erdszelem7  31179  climuzcnv  31565  elfzm12  31569  bcprod  31624  nn0prpwlem  32317  knoppndvlem1  32503  knoppndvlem2  32504  knoppndvlem7  32509  knoppndvlem18  32520  poimirlem13  33422  poimirlem14  33423  mblfinlem2  33447  fzmul  33537  incsequz  33544  geomcau  33555  heibor1lem  33608  bfplem2  33622  fzsplit1nn0  37317  irrapxlem1  37386  pellexlem5  37397  rmynn  37523  jm2.24nn  37526  jm2.17c  37529  congrep  37540  congabseq  37541  acongrep  37547  acongeq  37550  jm2.18  37555  jm2.23  37563  jm2.20nn  37564  jm2.26lem3  37568  jm2.26  37569  jm2.15nn0  37570  jm2.16nn0  37571  jm2.27dlem2  37577  rmydioph  37581  jm3.1  37587  expdiophlem1  37588  expdioph  37590  idomodle  37774  proot1ex  37779  nznngen  38515  sumnnodd  39862  stoweidlem7  40224  stoweidlem17  40234  wallispilem4  40285  stirlinglem2  40292  stirlinglem3  40293  stirlinglem4  40294  stirlinglem12  40302  stirlinglem13  40303  stirlinglem14  40304  stirlinglem15  40305  stirlingr  40307  dirkertrigeqlem1  40315  fouriersw  40448  ovnsubaddlem1  40784  subsubelfzo0  41336  2ffzoeq  41338  iccpartres  41354  iccpartipre  41357  iccpartltu  41361  iccelpart  41369  odz2prm2pw  41475  fmtnoprmfac2lem1  41478  pwdif  41501  2pwp1prm  41503  lighneallem2  41523  lighneallem4  41527  lighneal  41528  proththd  41531  nneoALTV  41583  divgcdoddALTV  41593  gbowge7  41651  gbege6  41653  altgsumbc  42130  altgsumbcALT  42131  pw2m1lepw2m1  42310  nnpw2even  42323  nnlog2ge0lt1  42360  logbpw2m1  42361  blenpw2m1  42373  nnpw2blenfzo  42375  nnpw2pmod  42377  nnpw2p  42380  blengt1fldiv2p1  42387  dignn0fr  42395  dignn0flhalflem1  42409  dignn0flhalflem2  42410  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414