Theorem nnz 12005

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℕcn 11638  ℤcz 11982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-i2m1 10605  ax-1ne0 10606  ax-rrecex 10609  ax-cnre 10610

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-ov 7159  df-om 7581  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-neg 10873  df-nn 11639  df-z 11983

This theorem is referenced by:  elnnz1  12009  znegcl  12018  nnleltp1  12038  nnltp1le  12039  nnlem1lt  12049  nnltlem1  12050  nnm1ge0  12051  prime  12064  nneo  12067  zeo  12069  btwnz  12085  eluz2b2  12322  qaddcl  12365  qreccl  12369  elpqb  12376  elfz1end  12938  fznatpl1  12962  fznn  12976  elfz1b  12977  elfzo0  13079  elfzo0z  13080  elfzo1  13088  fzo1fzo0n0  13089  elfzom1p1elfzo  13118  ubmelm1fzo  13134  quoremz  13224  intfracq  13228  fznnfl  13231  zmodcl  13260  zmodfz  13262  zmodfzo  13263  zmodid2  13268  zmodidfzo  13269  modfzo0difsn  13312  expnnval  13433  mulexpz  13470  nnesq  13589  expnlbnd  13595  expnlbnd2  13596  digit2  13598  faclbnd  13651  bc0k  13672  bcval5  13679  fz1isolem  13820  seqcoll  13823  ccatval21sw  13939  lswccatn0lsw  13945  cshwidxmod  14165  cshwidxn  14171  absexpz  14665  climuni  14909  isercoll  15024  climcnds  15206  arisum  15215  trireciplem  15217  expcnv  15219  pwdif  15223  geo2sum  15229  geo2lim  15231  0.999...  15237  geoihalfsum  15238  rpnnen2lem6  15572  rpnnen2lem9  15575  rpnnen2lem10  15576  dvdsval3  15611  nndivdvds  15616  modmulconst  15641  dvdsle  15660  dvdsssfz1  15668  fzm1ndvds  15672  dvdsfac  15676  mulmoddvds  15679  oexpneg  15694  nnoddm1d2  15737  pwp1fsum  15742  divalg2  15756  divalgmod  15757  modremain  15759  ndvdsadd  15761  nndvdslegcd  15854  divgcdz  15860  divgcdnn  15863  divgcdnnr  15864  modgcd  15880  gcdmultiple  15884  gcddiv  15899  gcdmultipleOLD  15900  gcdmultiplezOLD  15901  gcdzeq  15902  gcdeq  15903  rpmulgcd  15906  rplpwr  15907  rppwr  15908  sqgcd  15909  dvdssqlem  15910  dvdssq  15911  eucalginv  15928  lcmgcdlem  15950  lcmgcdnn  15955  lcmass  15958  lcmftp  15980  lcmfunsnlem2lem1  15982  coprmgcdb  15993  qredeq  16001  qredeu  16002  coprmprod  16005  coprmproddvdslem  16006  coprmproddvds  16007  cncongr1  16011  cncongr2  16012  1idssfct  16024  isprm2lem  16025  isprm3  16027  prmind2  16029  ge2nprmge4  16045  divgcdodd  16054  isprm6  16058  ncoprmlnprm  16068  divnumden  16088  divdenle  16089  nn0gcdsq  16092  phicl2  16105  phiprmpw  16113  eulerthlem2  16119  hashgcdlem  16125  hashgcdeq  16126  phisum  16127  nnoddn2prm  16148  pythagtriplem3  16155  pythagtriplem4  16156  pythagtriplem6  16158  pythagtriplem7  16159  pythagtriplem8  16160  pythagtriplem9  16161  pythagtriplem11  16162  pythagtriplem13  16164  pythagtriplem15  16166  pythagtriplem19  16170  pythagtrip  16171  iserodd  16172  pclem  16175  pccl  16186  pcdiv  16189  pcqcl  16193  pcdvds  16200  pcndvds  16202  pcndvds2  16204  pcelnn  16206  pcz  16217  pcmpt  16228  fldivp1  16233  pcfac  16235  infpnlem1  16246  prmunb  16250  prmreclem1  16252  1arith  16263  ram0  16358  prmdvdsprmo  16378  prmgaplem4  16390  prmgaplem6  16392  prmgaplem7  16393  cshwshashlem2  16430  setsstruct2  16521  mulgnn  18232  mulgaddcom  18251  mulginvcom  18252  mulgmodid  18266  ghmmulg  18370  dfod2  18691  gexdvds  18709  gexnnod  18713  gexex  18973  mulgass2  19351  qsssubdrg  20604  prmirredlem  20640  znidomb  20708  znrrg  20712  chfacfisf  21462  chfacfisfcpmat  21463  chfacfscmul0  21466  chfacfpmmul0  21470  cayhamlem1  21474  cpmadugsumlemF  21484  lmmo  21988  1stckgenlem  22161  imasdsf1olem  22983  clmmulg  23705  cmetcaulem  23891  ovolunlem1a  24097  ovolicc2lem4  24121  mbfi1fseqlem6  24321  dvexp3  24575  dgreq0  24855  elqaalem2  24909  aaliou3lem1  24931  aaliou3lem2  24932  aaliou3lem3  24933  aaliou3lem9  24939  pserdvlem2  25016  logtayl2  25245  root1eq1  25336  root1cj  25337  logbgcd1irr  25372  atantayl2  25516  birthdaylem2  25530  birthdaylem3  25531  emcllem5  25577  basellem2  25659  basellem3  25660  basellem5  25662  issqf  25713  sgmnncl  25724  prmorcht  25755  mumullem1  25756  mumullem2  25757  sqff1o  25759  dvdsflsumcom  25765  muinv  25770  vmalelog  25781  chtublem  25787  vmasum  25792  logfac2  25793  logfaclbnd  25798  bclbnd  25856  bposlem5  25864  lgsval4a  25895  lgssq2  25914  lgsdchr  25931  gausslemma2dlem0c  25934  gausslemma2dlem0e  25936  gausslemma2dlem1a  25941  gausslemma2dlem5  25947  lgsquadlem1  25956  lgsquadlem2  25957  lgsquad3  25963  2lgslem1a1  25965  2lgslem3  25980  2lgsoddprm  25992  2sqnn  26015  2sqreunnltlem  26026  rplogsumlem1  26060  rplogsumlem2  26061  dchrisumlem2  26066  dchrmusumlema  26069  dchrmusum2  26070  dchrvmasumiflem1  26077  dchrvmaeq0  26080  dchrisum0flblem2  26085  dchrisum0re  26089  dchrisum0lema  26090  dchrisum0lem1b  26091  dchrisum0lem2a  26093  logdivbnd  26132  pntrsumbnd2  26143  ostth2lem1  26194  ostth2lem3  26211  ostth3  26214  axlowdimlem13  26740  crctcshwlkn0lem4  27591  crctcshwlkn0lem5  27592  crctcshwlkn0lem7  27594  wlkiswwlksupgr2  27655  clwwisshclwwslem  27792  clwwlkinwwlk  27818  clwwlkel  27825  clwwlkf  27826  wwlksubclwwlk  27837  clwwlkvbij  27892  eucrctshift  28022  eucrct2eupth  28024  numclwlk2lem2f  28156  bcm1n  30518  pnfinf  30812  isarchiofld  30890  rearchi  30915  submat1n  31070  lmatfvlem  31080  esumcvg  31345  oddpwdc  31612  fibp1  31659  chtvalz  31900  nnltp1ne  32349  erdszelem7  32444  climuzcnv  32914  elfzm12  32918  bcprod  32970  nn0prpwlem  33670  knoppndvlem1  33851  knoppndvlem2  33852  knoppndvlem7  33857  knoppndvlem18  33868  poimirlem13  34920  poimirlem14  34921  mblfinlem2  34945  fzmul  35031  incsequz  35038  geomcau  35049  heibor1lem  35102  bfplem2  35116  lcmfunnnd  39133  nn0rppwr  39231  nn0expgcd  39233  zrtdvds  39242  fzsplit1nn0  39400  irrapxlem1  39468  pellexlem5  39479  rmynn  39602  jm2.24nn  39605  jm2.17c  39608  congrep  39619  congabseq  39620  acongrep  39626  acongeq  39629  jm2.18  39634  jm2.23  39642  jm2.20nn  39643  jm2.26lem3  39647  jm2.26  39648  jm2.15nn0  39649  jm2.16nn0  39650  jm2.27dlem2  39656  rmydioph  39660  jm3.1  39666  expdiophlem1  39667  expdioph  39669  idomodle  39845  proot1ex  39850  nznngen  40697  sumnnodd  41960  stoweidlem7  42341  stoweidlem17  42351  wallispilem4  42402  stirlinglem2  42409  stirlinglem3  42410  stirlinglem4  42411  stirlinglem12  42419  stirlinglem13  42420  stirlinglem14  42421  stirlinglem15  42422  stirlingr  42424  dirkertrigeqlem1  42432  fouriersw  42565  ovnsubaddlem1  42901  subsubelfzo0  43575  2ffzoeq  43577  iccpartres  43627  iccpartipre  43630  iccpartltu  43634  iccelpart  43642  odz2prm2pw  43774  fmtnoprmfac2lem1  43777  2pwp1prm  43800  lighneallem2  43820  lighneallem4  43824  lighneal  43825  proththd  43828  nneoALTV  43886  divgcdoddALTV  43896  fpprmod  43941  fppr2odd  43945  dfwppr  43952  fpprwppr  43953  fpprwpprb  43954  gbowge7  43977  gbege6  43979  altgsumbc  44449  altgsumbcALT  44450  pw2m1lepw2m1  44624  nnpw2even  44638  nnlog2ge0lt1  44675  logbpw2m1  44676  blenpw2m1  44688  nnpw2blenfzo  44690  nnpw2pmod  44692  nnpw2p  44695  blengt1fldiv2p1  44702  dignn0fr  44710  dignn0flhalflem1  44724  dignn0flhalflem2  44725  nn0sumshdiglemA  44728  nn0sumshdiglemB  44729