MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnz Structured version   Visualization version   GIF version

Theorem nnz 11999
Description: A positive integer is an integer. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
nnz (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

Proof of Theorem nnz
StepHypRef Expression
1 nnssz 11997 . 2 ℕ ⊆ ℤ
21sseli 3949 1 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2115  cn 11632  cz 11976
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7452  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-i2m1 10599  ax-1ne0 10600  ax-rrecex 10603  ax-cnre 10604
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 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4826  df-iun 4908  df-br 5054  df-opab 5116  df-mpt 5134  df-tr 5160  df-id 5448  df-eprel 5453  df-po 5462  df-so 5463  df-fr 5502  df-we 5504  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-pred 6136  df-ord 6182  df-on 6183  df-lim 6184  df-suc 6185  df-iota 6303  df-fun 6346  df-fn 6347  df-f 6348  df-f1 6349  df-fo 6350  df-f1o 6351  df-fv 6352  df-ov 7149  df-om 7572  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-neg 10867  df-nn 11633  df-z 11977
This theorem is referenced by:  elnnz1  12003  znegcl  12012  nnleltp1  12032  nnltp1le  12033  nnlem1lt  12043  nnltlem1  12044  nnm1ge0  12045  prime  12058  nneo  12061  zeo  12063  btwnz  12079  eluz2b2  12316  qaddcl  12359  qreccl  12363  elpqb  12370  elfz1end  12939  fznatpl1  12963  fznn  12977  elfz1b  12978  elfzo0  13080  elfzo0z  13081  elfzo1  13089  fzo1fzo0n0  13090  elfzom1p1elfzo  13119  ubmelm1fzo  13135  quoremz  13225  intfracq  13229  fznnfl  13232  zmodcl  13261  zmodfz  13263  zmodfzo  13264  zmodid2  13269  zmodidfzo  13270  modfzo0difsn  13313  expnnval  13435  mulexpz  13472  nnesq  13591  expnlbnd  13597  expnlbnd2  13598  digit2  13600  faclbnd  13653  bc0k  13674  bcval5  13681  fz1isolem  13822  seqcoll  13825  ccatval21sw  13937  lswccatn0lsw  13943  cshwidxmod  14163  cshwidxn  14169  absexpz  14663  climuni  14907  isercoll  15022  climcnds  15204  arisum  15213  trireciplem  15215  expcnv  15217  pwdif  15221  geo2sum  15227  geo2lim  15229  0.999...  15235  geoihalfsum  15236  rpnnen2lem6  15570  rpnnen2lem9  15573  rpnnen2lem10  15574  dvdsval3  15609  nndivdvds  15614  modmulconst  15639  dvdsle  15658  dvdsssfz1  15666  fzm1ndvds  15670  dvdsfac  15674  mulmoddvds  15677  oexpneg  15692  nnoddm1d2  15733  pwp1fsum  15738  divalg2  15752  divalgmod  15753  modremain  15755  ndvdsadd  15757  nndvdslegcd  15850  divgcdz  15856  divgcdnn  15859  divgcdnnr  15860  modgcd  15876  gcdmultiple  15880  gcddiv  15895  gcdmultipleOLD  15896  gcdmultiplezOLD  15897  gcdzeq  15898  gcdeq  15899  rpmulgcd  15902  rplpwr  15903  rppwr  15904  sqgcd  15905  dvdssqlem  15906  dvdssq  15907  eucalginv  15924  lcmgcdlem  15946  lcmgcdnn  15951  lcmass  15954  lcmftp  15976  lcmfunsnlem2lem1  15978  coprmgcdb  15989  qredeq  15997  qredeu  15998  coprmprod  16001  coprmproddvdslem  16002  coprmproddvds  16003  cncongr1  16007  cncongr2  16008  1idssfct  16020  isprm2lem  16021  isprm3  16023  prmind2  16025  ge2nprmge4  16041  divgcdodd  16050  isprm6  16054  ncoprmlnprm  16064  divnumden  16084  divdenle  16085  nn0gcdsq  16088  phicl2  16101  phiprmpw  16109  eulerthlem2  16115  hashgcdlem  16121  hashgcdeq  16122  phisum  16123  nnoddn2prm  16144  pythagtriplem3  16151  pythagtriplem4  16152  pythagtriplem6  16154  pythagtriplem7  16155  pythagtriplem8  16156  pythagtriplem9  16157  pythagtriplem11  16158  pythagtriplem13  16160  pythagtriplem15  16162  pythagtriplem19  16166  pythagtrip  16167  iserodd  16168  pclem  16171  pccl  16182  pcdiv  16185  pcqcl  16189  pcdvds  16196  pcndvds  16198  pcndvds2  16200  pcelnn  16202  pcz  16213  pcmpt  16224  fldivp1  16229  pcfac  16231  infpnlem1  16242  prmunb  16246  prmreclem1  16248  1arith  16259  ram0  16354  prmdvdsprmo  16374  prmgaplem4  16386  prmgaplem6  16388  prmgaplem7  16389  cshwshashlem2  16428  setsstruct2  16519  mulgnn  18230  mulgaddcom  18249  mulginvcom  18250  mulgmodid  18264  ghmmulg  18368  dfod2  18689  gexdvds  18707  gexnnod  18711  gexex  18971  mulgass2  19349  qsssubdrg  20599  prmirredlem  20635  znidomb  20703  znrrg  20707  chfacfisf  21457  chfacfisfcpmat  21458  chfacfscmul0  21461  chfacfpmmul0  21465  cayhamlem1  21469  cpmadugsumlemF  21479  lmmo  21983  1stckgenlem  22156  imasdsf1olem  22978  clmmulg  23704  cmetcaulem  23890  ovolunlem1a  24098  ovolicc2lem4  24122  mbfi1fseqlem6  24322  dvexp3  24579  dgreq0  24860  elqaalem2  24914  aaliou3lem1  24936  aaliou3lem2  24937  aaliou3lem3  24938  aaliou3lem9  24944  pserdvlem2  25021  logtayl2  25251  root1eq1  25342  root1cj  25343  logbgcd1irr  25378  atantayl2  25522  birthdaylem2  25536  birthdaylem3  25537  emcllem5  25583  basellem2  25665  basellem3  25666  basellem5  25668  issqf  25719  sgmnncl  25730  prmorcht  25761  mumullem1  25762  mumullem2  25763  sqff1o  25765  dvdsflsumcom  25771  muinv  25776  vmalelog  25787  chtublem  25793  vmasum  25798  logfac2  25799  logfaclbnd  25804  bclbnd  25862  bposlem5  25870  lgsval4a  25901  lgssq2  25920  lgsdchr  25937  gausslemma2dlem0c  25940  gausslemma2dlem0e  25942  gausslemma2dlem1a  25947  gausslemma2dlem5  25953  lgsquadlem1  25962  lgsquadlem2  25963  lgsquad3  25969  2lgslem1a1  25971  2lgslem3  25986  2lgsoddprm  25998  2sqnn  26021  2sqreunnltlem  26032  rplogsumlem1  26066  rplogsumlem2  26067  dchrisumlem2  26072  dchrmusumlema  26075  dchrmusum2  26076  dchrvmasumiflem1  26083  dchrvmaeq0  26086  dchrisum0flblem2  26091  dchrisum0re  26095  dchrisum0lema  26096  dchrisum0lem1b  26097  dchrisum0lem2a  26099  logdivbnd  26138  pntrsumbnd2  26149  ostth2lem1  26200  ostth2lem3  26217  ostth3  26220  axlowdimlem13  26746  crctcshwlkn0lem4  27597  crctcshwlkn0lem5  27598  crctcshwlkn0lem7  27600  wlkiswwlksupgr2  27661  clwwisshclwwslem  27797  clwwlkinwwlk  27823  clwwlkel  27829  clwwlkf  27830  wwlksubclwwlk  27841  clwwlkvbij  27896  eucrctshift  28026  eucrct2eupth  28028  numclwlk2lem2f  28160  bcm1n  30524  pnfinf  30839  isarchiofld  30917  rearchi  30942  submat1n  31100  lmatfvlem  31110  esumcvg  31372  oddpwdc  31639  fibp1  31686  chtvalz  31927  nnltp1ne  32376  erdszelem7  32471  climuzcnv  32941  elfzm12  32945  bcprod  32997  nn0prpwlem  33697  knoppndvlem1  33878  knoppndvlem2  33879  knoppndvlem7  33884  knoppndvlem18  33895  poimirlem13  34982  poimirlem14  34983  mblfinlem2  35007  fzmul  35091  incsequz  35098  geomcau  35109  heibor1lem  35159  bfplem2  35173  lcmfunnnd  39208  nn0rppwr  39364  nn0expgcd  39366  zrtdvds  39375  fzsplit1nn0  39551  irrapxlem1  39619  pellexlem5  39630  rmynn  39753  jm2.24nn  39756  jm2.17c  39759  congrep  39770  congabseq  39771  acongrep  39777  acongeq  39780  jm2.18  39785  jm2.23  39793  jm2.20nn  39794  jm2.26lem3  39798  jm2.26  39799  jm2.15nn0  39800  jm2.16nn0  39801  jm2.27dlem2  39807  rmydioph  39811  jm3.1  39817  expdiophlem1  39818  expdioph  39820  idomodle  39996  proot1ex  40001  nznngen  40880  sumnnodd  42138  stoweidlem7  42515  stoweidlem17  42525  wallispilem4  42576  stirlinglem2  42583  stirlinglem3  42584  stirlinglem4  42585  stirlinglem12  42593  stirlinglem13  42594  stirlinglem14  42595  stirlinglem15  42596  stirlingr  42598  dirkertrigeqlem1  42606  fouriersw  42739  ovnsubaddlem1  43075  subsubelfzo0  43749  2ffzoeq  43751  iccpartres  43801  iccpartipre  43804  iccpartltu  43808  iccelpart  43816  odz2prm2pw  43946  fmtnoprmfac2lem1  43949  2pwp1prm  43972  lighneallem2  43990  lighneallem4  43994  lighneal  43995  proththd  43998  nneoALTV  44056  divgcdoddALTV  44066  fpprmod  44111  fppr2odd  44115  dfwppr  44122  fpprwppr  44123  fpprwpprb  44124  gbowge7  44147  gbege6  44149  altgsumbc  44619  altgsumbcALT  44620  pw2m1lepw2m1  44794  nnpw2even  44808  nnlog2ge0lt1  44845  logbpw2m1  44846  blenpw2m1  44858  nnpw2blenfzo  44860  nnpw2pmod  44862  nnpw2p  44865  blengt1fldiv2p1  44872  dignn0fr  44880  dignn0flhalflem1  44894  dignn0flhalflem2  44895  nn0sumshdiglemA  44898  nn0sumshdiglemB  44899
  Copyright terms: Public domain W3C validator