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

Theorem nnz 11993
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 11991 . 2 ℕ ⊆ ℤ
21sseli 3962 1 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  cn 11627  cz 11970
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-i2m1 10594  ax-1ne0 10595  ax-rrecex 10598  ax-cnre 10599
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  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 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-ov 7148  df-om 7569  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-neg 10862  df-nn 11628  df-z 11971
This theorem is referenced by:  elnnz1  11997  znegcl  12006  nnleltp1  12026  nnltp1le  12027  nnlem1lt  12037  nnltlem1  12038  nnm1ge0  12039  prime  12052  nneo  12055  zeo  12057  btwnz  12073  eluz2b2  12310  qaddcl  12354  qreccl  12358  elpqb  12365  elfz1end  12927  fznatpl1  12951  fznn  12965  elfz1b  12966  elfzo0  13068  elfzo0z  13069  elfzo1  13077  fzo1fzo0n0  13078  elfzom1p1elfzo  13107  ubmelm1fzo  13123  quoremz  13213  intfracq  13217  fznnfl  13220  zmodcl  13249  zmodfz  13251  zmodfzo  13252  zmodid2  13257  zmodidfzo  13258  modfzo0difsn  13301  expnnval  13422  mulexpz  13459  nnesq  13578  expnlbnd  13584  expnlbnd2  13585  digit2  13587  faclbnd  13640  bc0k  13661  bcval5  13668  fz1isolem  13809  seqcoll  13812  ccatval21sw  13929  lswccatn0lsw  13935  cshwidxmod  14155  cshwidxn  14161  absexpz  14655  climuni  14899  isercoll  15014  climcnds  15196  arisum  15205  trireciplem  15207  expcnv  15209  pwdif  15213  geo2sum  15219  geo2lim  15221  0.999...  15227  geoihalfsum  15228  rpnnen2lem6  15562  rpnnen2lem9  15565  rpnnen2lem10  15566  dvdsval3  15601  nndivdvds  15606  modmulconst  15631  dvdsle  15650  dvdsssfz1  15658  fzm1ndvds  15662  dvdsfac  15666  mulmoddvds  15669  oexpneg  15684  nnoddm1d2  15727  pwp1fsum  15732  divalg2  15746  divalgmod  15747  modremain  15749  ndvdsadd  15751  nndvdslegcd  15844  divgcdz  15850  divgcdnn  15853  divgcdnnr  15854  modgcd  15870  gcdmultiple  15874  gcddiv  15889  gcdmultipleOLD  15890  gcdmultiplezOLD  15891  gcdzeq  15892  gcdeq  15893  rpmulgcd  15896  rplpwr  15897  rppwr  15898  sqgcd  15899  dvdssqlem  15900  dvdssq  15901  eucalginv  15918  lcmgcdlem  15940  lcmgcdnn  15945  lcmass  15948  lcmftp  15970  lcmfunsnlem2lem1  15972  coprmgcdb  15983  qredeq  15991  qredeu  15992  coprmprod  15995  coprmproddvdslem  15996  coprmproddvds  15997  cncongr1  16001  cncongr2  16002  1idssfct  16014  isprm2lem  16015  isprm3  16017  prmind2  16019  ge2nprmge4  16035  divgcdodd  16044  isprm6  16048  ncoprmlnprm  16058  divnumden  16078  divdenle  16079  nn0gcdsq  16082  phicl2  16095  phiprmpw  16103  eulerthlem2  16109  hashgcdlem  16115  hashgcdeq  16116  phisum  16117  nnoddn2prm  16138  pythagtriplem3  16145  pythagtriplem4  16146  pythagtriplem6  16148  pythagtriplem7  16149  pythagtriplem8  16150  pythagtriplem9  16151  pythagtriplem11  16152  pythagtriplem13  16154  pythagtriplem15  16156  pythagtriplem19  16160  pythagtrip  16161  iserodd  16162  pclem  16165  pccl  16176  pcdiv  16179  pcqcl  16183  pcdvds  16190  pcndvds  16192  pcndvds2  16194  pcelnn  16196  pcz  16207  pcmpt  16218  fldivp1  16223  pcfac  16225  infpnlem1  16236  prmunb  16240  prmreclem1  16242  1arith  16253  ram0  16348  prmdvdsprmo  16368  prmgaplem4  16380  prmgaplem6  16382  prmgaplem7  16383  cshwshashlem2  16420  setsstruct2  16511  mulgnn  18172  mulgaddcom  18191  mulginvcom  18192  mulgmodid  18206  ghmmulg  18310  dfod2  18622  gexdvds  18640  gexnnod  18644  gexex  18904  mulgass2  19282  qsssubdrg  20534  prmirredlem  20570  znidomb  20638  znrrg  20642  chfacfisf  21392  chfacfisfcpmat  21393  chfacfscmul0  21396  chfacfpmmul0  21400  cayhamlem1  21404  cpmadugsumlemF  21414  lmmo  21918  1stckgenlem  22091  imasdsf1olem  22912  clmmulg  23634  cmetcaulem  23820  ovolunlem1a  24026  ovolicc2lem4  24050  mbfi1fseqlem6  24250  dvexp3  24504  dgreq0  24784  elqaalem2  24838  aaliou3lem1  24860  aaliou3lem2  24861  aaliou3lem3  24862  aaliou3lem9  24868  pserdvlem2  24945  logtayl2  25172  root1eq1  25263  root1cj  25264  logbgcd1irr  25299  atantayl2  25443  birthdaylem2  25458  birthdaylem3  25459  emcllem5  25505  basellem2  25587  basellem3  25588  basellem5  25590  issqf  25641  sgmnncl  25652  prmorcht  25683  mumullem1  25684  mumullem2  25685  sqff1o  25687  dvdsflsumcom  25693  muinv  25698  vmalelog  25709  chtublem  25715  vmasum  25720  logfac2  25721  logfaclbnd  25726  bclbnd  25784  bposlem5  25792  lgsval4a  25823  lgssq2  25842  lgsdchr  25859  gausslemma2dlem0c  25862  gausslemma2dlem0e  25864  gausslemma2dlem1a  25869  gausslemma2dlem5  25875  lgsquadlem1  25884  lgsquadlem2  25885  lgsquad3  25891  2lgslem1a1  25893  2lgslem3  25908  2lgsoddprm  25920  2sqnn  25943  2sqreunnltlem  25954  rplogsumlem1  25988  rplogsumlem2  25989  dchrisumlem2  25994  dchrmusumlema  25997  dchrmusum2  25998  dchrvmasumiflem1  26005  dchrvmaeq0  26008  dchrisum0flblem2  26013  dchrisum0re  26017  dchrisum0lema  26018  dchrisum0lem1b  26019  dchrisum0lem2a  26021  logdivbnd  26060  pntrsumbnd2  26071  ostth2lem1  26122  ostth2lem3  26139  ostth3  26142  axlowdimlem13  26668  crctcshwlkn0lem4  27519  crctcshwlkn0lem5  27520  crctcshwlkn0lem7  27522  wlkiswwlksupgr2  27583  clwwisshclwwslem  27720  clwwlkinwwlk  27746  clwwlkel  27753  clwwlkf  27754  wwlksubclwwlk  27765  clwwlkvbij  27820  eucrctshift  27950  eucrct2eupth  27952  numclwlk2lem2f  28084  bcm1n  30445  pnfinf  30740  isarchiofld  30818  rearchi  30843  submat1n  30970  lmatfvlem  30980  esumcvg  31245  oddpwdc  31512  fibp1  31559  chtvalz  31800  nnltp1ne  32247  erdszelem7  32342  climuzcnv  32812  elfzm12  32816  bcprod  32868  nn0prpwlem  33568  knoppndvlem1  33749  knoppndvlem2  33750  knoppndvlem7  33755  knoppndvlem18  33766  poimirlem13  34787  poimirlem14  34788  mblfinlem2  34812  fzmul  34899  incsequz  34906  geomcau  34917  heibor1lem  34970  bfplem2  34984  nn0rppwr  39062  nn0expgcd  39064  zrtdvds  39073  fzsplit1nn0  39231  irrapxlem1  39299  pellexlem5  39310  rmynn  39433  jm2.24nn  39436  jm2.17c  39439  congrep  39450  congabseq  39451  acongrep  39457  acongeq  39460  jm2.18  39465  jm2.23  39473  jm2.20nn  39474  jm2.26lem3  39478  jm2.26  39479  jm2.15nn0  39480  jm2.16nn0  39481  jm2.27dlem2  39487  rmydioph  39491  jm3.1  39497  expdiophlem1  39498  expdioph  39500  idomodle  39676  proot1ex  39681  nznngen  40528  sumnnodd  41791  stoweidlem7  42173  stoweidlem17  42183  wallispilem4  42234  stirlinglem2  42241  stirlinglem3  42242  stirlinglem4  42243  stirlinglem12  42251  stirlinglem13  42252  stirlinglem14  42253  stirlinglem15  42254  stirlingr  42256  dirkertrigeqlem1  42264  fouriersw  42397  ovnsubaddlem1  42733  subsubelfzo0  43407  2ffzoeq  43409  iccpartres  43425  iccpartipre  43428  iccpartltu  43432  iccelpart  43440  odz2prm2pw  43572  fmtnoprmfac2lem1  43575  2pwp1prm  43598  lighneallem2  43618  lighneallem4  43622  lighneal  43623  proththd  43626  nneoALTV  43684  divgcdoddALTV  43694  fpprmod  43739  fppr2odd  43743  dfwppr  43750  fpprwppr  43751  fpprwpprb  43752  gbowge7  43775  gbege6  43777  altgsumbc  44298  altgsumbcALT  44299  pw2m1lepw2m1  44473  nnpw2even  44487  nnlog2ge0lt1  44524  logbpw2m1  44525  blenpw2m1  44537  nnpw2blenfzo  44539  nnpw2pmod  44541  nnpw2p  44544  blengt1fldiv2p1  44551  dignn0fr  44559  dignn0flhalflem1  44573  dignn0flhalflem2  44574  nn0sumshdiglemA  44577  nn0sumshdiglemB  44578
  Copyright terms: Public domain W3C validator