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

Theorem nnz 10655
Description: A positive integer is an integer. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
nnz  |-  ( N  e.  NN  ->  N  e.  ZZ )

Proof of Theorem nnz
StepHypRef Expression
1 nnssz 10653 . 2  |-  NN  C_  ZZ
21sseli 3340 1  |-  ( N  e.  NN  ->  N  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   NNcn 10309   ZZcz 10633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-resscn 9326  ax-1cn 9327  ax-icn 9328  ax-addcl 9329  ax-addrcl 9330  ax-mulcl 9331  ax-mulrcl 9332  ax-mulcom 9333  ax-addass 9334  ax-mulass 9335  ax-distr 9336  ax-i2m1 9337  ax-1ne0 9338  ax-1rid 9339  ax-rnegex 9340  ax-rrecex 9341  ax-cnre 9342  ax-pre-lttri 9343  ax-pre-lttrn 9344  ax-pre-ltadd 9345  ax-pre-mulgt0 9346
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-reu 2712  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-riota 6039  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-om 6466  df-recs 6818  df-rdg 6852  df-er 7089  df-en 7299  df-dom 7300  df-sdom 7301  df-pnf 9407  df-mnf 9408  df-xr 9409  df-ltxr 9410  df-le 9411  df-sub 9584  df-neg 9585  df-nn 10310  df-z 10634
This theorem is referenced by:  elnnz1  10659  znegcl  10667  nnleltp1  10686  nnltp1le  10687  nnlem1lt  10695  nnltlem1  10696  nnm1ge0  10697  prime  10709  nneo  10712  zeo  10714  uzindOLD  10723  btwnz  10731  eluz2b2  10914  qaddcl  10956  qreccl  10960  elfz1end  11465  fznatpl1  11494  fznn  11509  elfz1b  11510  elfzo0  11570  fzo1fzo0n0  11571  elfzo0z  11572  elfzo1  11578  ubmelm1fzo  11606  quoremz  11677  intfracq  11681  fznnfl  11684  zmodcl  11710  zmodfz  11712  zmodfzo  11713  modidmul0  11717  zmodid2  11719  zmodidfzo  11720  expnnval  11851  mulexpz  11887  nnesq  11971  expnlbnd  11977  expnlbnd2  11978  digit2  11980  faclbnd  12049  bc0k  12070  bcval5  12077  fz1isolem  12197  seqcoll  12199  cshwidxmod  12423  cshwidxn  12428  absexpz  12777  climuni  13013  isercoll  13128  climcnds  13296  arisum  13304  trireciplem  13306  expcnv  13308  geo2sum  13315  geo2lim  13317  0.999...  13323  geoihalfsum  13324  rpnnen2lem6  13484  rpnnen2lem9  13487  rpnnen2lem10  13488  dvdsval3  13521  nndivdvds  13523  dvdsle  13560  dvdseq  13562  fzm1ndvds  13567  dvdsfac  13570  oexpneg  13577  divalg2  13591  divalgmod  13592  ndvdsadd  13594  modgcd  13702  gcddiv  13715  gcdmultiple  13716  gcdmultiplez  13717  gcdeq  13718  rpmulgcd  13721  rplpwr  13722  rppwr  13723  sqgcd  13724  dvdssqlem  13725  dvdssq  13726  eucalginv  13741  1idssfct  13751  isprm3  13754  prmind2  13756  qredeq  13774  qredeu  13775  isprm6  13777  divgcdodd  13787  divnumden  13808  divdenle  13809  nn0gcdsq  13812  phicl2  13825  phiprmpw  13833  eulerthlem2  13839  pythagtriplem3  13867  pythagtriplem4  13868  pythagtriplem6  13870  pythagtriplem7  13871  pythagtriplem8  13872  pythagtriplem9  13873  pythagtriplem11  13874  pythagtriplem13  13876  pythagtriplem15  13878  pythagtriplem19  13882  pythagtrip  13883  iserodd  13884  pclem  13887  pccl  13898  pcdiv  13901  pcqcl  13905  pcdvds  13912  pcndvds  13914  pcndvds2  13916  pcelnn  13918  pcz  13929  pcmpt  13936  fldivp1  13941  pcfac  13943  infpnlem1  13953  prmunb  13957  prmreclem1  13959  1arith  13970  ram0  14065  cshwshashlem2  14105  mulgnn  15612  ghmmulg  15738  dfod2  16044  gexdvds  16062  gexnnod  16066  gexex  16314  mulgass2  16626  qsssubdrg  17715  prmirredlem  17758  prmirredlemOLD  17761  znidomb  17835  znrrg  17839  lmmo  18825  1stckgenlem  18967  imasdsf1olem  19789  clmmulg  20506  cmetcaulem  20640  ovolunlem1a  20820  ovolicc2lem4  20844  mbfi1fseqlem6  21039  dvexp3  21291  dgreq0  21616  elqaalem2  21670  aaliou3lem1  21692  aaliou3lem2  21693  aaliou3lem3  21694  aaliou3lem9  21700  pserdvlem2  21777  logtayl2  21991  root1eq1  22077  root1cj  22078  atantayl2  22217  birthdaylem2  22230  birthdaylem3  22231  emcllem5  22277  basellem2  22303  basellem3  22304  basellem5  22306  sgmss  22328  issqf  22358  sgmnncl  22369  prmorcht  22400  mumullem1  22401  mumullem2  22402  sqff1o  22404  dvdsdivcl  22405  dvdsflsumcom  22412  muinv  22417  vmalelog  22428  chtublem  22434  vmasum  22439  logfac2  22440  logfaclbnd  22445  bclbnd  22503  bposlem5  22511  lgsval4a  22541  lgssq  22558  lgssq2  22559  lgsdchr  22571  lgsquadlem1  22577  lgsquadlem2  22578  lgsquad3  22584  rplogsumlem1  22617  rplogsumlem2  22618  dchrisumlem2  22623  dchrmusumlema  22626  dchrmusum2  22627  dchrvmasumiflem1  22634  dchrvmaeq0  22637  dchrisum0flblem2  22642  dchrisum0re  22646  dchrisum0lema  22647  dchrisum0lem1b  22648  dchrisum0lem2a  22650  logdivbnd  22689  pntrsumbnd2  22700  ostth2lem1  22751  ostth2lem3  22768  ostth3  22771  axlowdimlem13  23022  gxpval  23568  gxcom  23578  gxinv  23579  gxid  23582  gxmodid  23588  gxdi  23605  bcm1n  25901  pnfinf  26023  isarchiofld  26137  rearchi  26163  esumcvg  26388  oddpwdc  26584  fibp1  26631  erdszelem7  26932  climuzcnv  27162  elfzm12  27166  mblfinlem2  28270  nn0prpwlem  28358  fzmul  28477  incsequz  28485  geomcau  28496  heibor1lem  28549  bfplem2  28563  fzsplit1nn0  28934  irrapxlem1  29005  pellexlem5  29016  rmynn  29141  jm2.24nn  29144  jm2.17c  29147  congrep  29158  congabseq  29159  acongrep  29165  acongeq  29168  jm2.18  29179  jm2.23  29187  jm2.20nn  29188  jm2.26lem3  29192  jm2.26  29193  jm2.15nn0  29194  jm2.16nn0  29195  jm2.27dlem2  29201  rmydioph  29205  jm3.1  29211  expdiophlem1  29212  expdioph  29214  idomodle  29403  hashgcdlem  29407  hashgcdeq  29408  phisum  29409  proot1ex  29411  stoweidlem7  29645  stoweidlem17  29655  wallispilem4  29706  stirlinglem2  29713  stirlinglem3  29714  stirlinglem4  29715  stirlinglem12  29723  stirlinglem13  29724  stirlinglem14  29725  stirlinglem15  29726  stirlingr  29728  subsubelfzo0  30053  2ffzoeq  30057  clwwlkel  30298  clwwlkf  30299  clwwlkvbij  30306  wwlksubclwwlk  30309  clwwisshclwwlem  30313  clwwisshclww  30314  numclwlk2lem2f  30539
  Copyright terms: Public domain W3C validator