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

Theorem nnz 10882
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 10880 . 2  |-  NN  C_  ZZ
21sseli 3485 1  |-  ( N  e.  NN  ->  N  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1823   NNcn 10531   ZZcz 10860
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-om 6674  df-recs 7034  df-rdg 7068  df-er 7303  df-en 7510  df-dom 7511  df-sdom 7512  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9798  df-neg 9799  df-nn 10532  df-z 10861
This theorem is referenced by:  elnnz1  10886  znegcl  10895  nnleltp1  10914  nnltp1le  10915  nnlem1lt  10925  nnltlem1  10926  nnm1ge0  10927  prime  10939  nneo  10942  zeo  10944  uzindOLD  10953  btwnz  10962  eluz2b2  11155  qaddcl  11199  qreccl  11203  elfz1end  11718  fznatpl1  11738  fznn  11751  elfz1b  11752  elfzo0  11840  fzo1fzo0n0  11841  elfzo0z  11842  elfzo1  11848  ubmelm1fzo  11889  quoremz  11964  intfracq  11968  fznnfl  11971  zmodcl  11998  zmodfz  12000  zmodfzo  12001  modidmul0OLD  12005  zmodid2  12007  zmodidfzo  12008  expnnval  12154  mulexpz  12191  nnesq  12275  expnlbnd  12281  expnlbnd2  12282  digit2  12284  faclbnd  12353  bc0k  12374  bcval5  12381  fz1isolem  12497  seqcoll  12499  lswccatn0lsw  12599  cshwidxmod  12768  cshwidxn  12773  absexpz  13223  climuni  13460  isercoll  13575  climcnds  13748  arisum  13756  trireciplem  13758  expcnv  13760  geo2sum  13767  geo2lim  13769  0.999...  13775  geoihalfsum  13776  rpnnen2lem6  14040  rpnnen2lem9  14043  rpnnen2lem10  14044  dvdsval3  14077  nndivdvds  14079  dvdsle  14118  dvdseq  14120  fzm1ndvds  14125  dvdsfac  14128  oexpneg  14136  divalg2  14150  divalgmod  14151  ndvdsadd  14153  modgcd  14261  gcddiv  14274  gcdmultiple  14275  gcdmultiplez  14276  gcdeq  14277  rpmulgcd  14280  rplpwr  14281  rppwr  14282  sqgcd  14283  dvdssqlem  14284  dvdssq  14285  eucalginv  14300  1idssfct  14310  isprm3  14313  prmind2  14315  qredeq  14334  qredeu  14335  isprm6  14337  divgcdodd  14347  divnumden  14368  divdenle  14369  nn0gcdsq  14372  phicl2  14385  phiprmpw  14393  eulerthlem2  14399  pythagtriplem3  14429  pythagtriplem4  14430  pythagtriplem6  14432  pythagtriplem7  14433  pythagtriplem8  14434  pythagtriplem9  14435  pythagtriplem11  14436  pythagtriplem13  14438  pythagtriplem15  14440  pythagtriplem19  14444  pythagtrip  14445  iserodd  14446  pclem  14449  pccl  14460  pcdiv  14463  pcqcl  14467  pcdvds  14474  pcndvds  14476  pcndvds2  14478  pcelnn  14480  pcz  14491  pcmpt  14498  fldivp1  14503  pcfac  14505  infpnlem1  14515  prmunb  14519  prmreclem1  14521  1arith  14532  ram0  14627  cshwshashlem2  14668  mulgnn  16350  ghmmulg  16481  dfod2  16788  gexdvds  16806  gexnnod  16810  gexex  17061  mulgass2  17445  qsssubdrg  18675  prmirredlem  18708  znidomb  18776  znrrg  18780  chfacfisf  19525  chfacfisfcpmat  19526  chfacfscmul0  19529  chfacfpmmul0  19533  cayhamlem1  19537  cpmadugsumlemF  19547  lmmo  20051  1stckgenlem  20223  imasdsf1olem  21045  clmmulg  21762  cmetcaulem  21896  ovolunlem1a  22076  ovolicc2lem4  22100  mbfi1fseqlem6  22296  dvexp3  22548  dgreq0  22831  elqaalem2  22885  aaliou3lem1  22907  aaliou3lem2  22908  aaliou3lem3  22909  aaliou3lem9  22915  pserdvlem2  22992  logtayl2  23214  root1eq1  23300  root1cj  23301  atantayl2  23469  birthdaylem2  23483  birthdaylem3  23484  emcllem5  23530  basellem2  23556  basellem3  23557  basellem5  23559  sgmss  23581  issqf  23611  sgmnncl  23622  prmorcht  23653  mumullem1  23654  mumullem2  23655  sqff1o  23657  dvdsdivcl  23658  dvdsflsumcom  23665  muinv  23670  vmalelog  23681  chtublem  23687  vmasum  23692  logfac2  23693  logfaclbnd  23698  bclbnd  23756  bposlem5  23764  lgsval4a  23794  lgssq  23811  lgssq2  23812  lgsdchr  23824  lgsquadlem1  23830  lgsquadlem2  23831  lgsquad3  23837  rplogsumlem1  23870  rplogsumlem2  23871  dchrisumlem2  23876  dchrmusumlema  23879  dchrmusum2  23880  dchrvmasumiflem1  23887  dchrvmaeq0  23890  dchrisum0flblem2  23895  dchrisum0re  23899  dchrisum0lema  23900  dchrisum0lem1b  23901  dchrisum0lem2a  23903  logdivbnd  23942  pntrsumbnd2  23953  ostth2lem1  24004  ostth2lem3  24021  ostth3  24024  axlowdimlem13  24462  clwwlkel  24998  clwwlkf  24999  clwwlkvbij  25006  wwlksubclwwlk  25009  clwwisshclwwlem  25011  clwwisshclww  25012  numclwlk2lem2f  25308  gxpval  25462  gxcom  25472  gxinv  25473  gxid  25476  gxmodid  25482  gxdi  25499  bcm1n  27837  pnfinf  27964  isarchiofld  28045  rearchi  28070  esumcvg  28318  oddpwdc  28560  fibp1  28607  erdszelem7  28908  climuzcnv  29304  elfzm12  29308  mblfinlem2  30295  nn0prpwlem  30383  fzmul  30476  incsequz  30484  geomcau  30495  heibor1lem  30548  bfplem2  30562  fzsplit1nn0  30929  irrapxlem1  31000  pellexlem5  31011  rmynn  31136  jm2.24nn  31139  jm2.17c  31142  congrep  31153  congabseq  31154  acongrep  31160  acongeq  31163  jm2.18  31172  jm2.23  31180  jm2.20nn  31181  jm2.26lem3  31185  jm2.26  31186  jm2.15nn0  31187  jm2.16nn0  31188  jm2.27dlem2  31194  rmydioph  31198  jm3.1  31204  expdiophlem1  31205  expdioph  31207  idomodle  31397  hashgcdlem  31401  hashgcdeq  31402  phisum  31403  proot1ex  31405  lcmgcdlem  31456  lcmass  31462  nznngen  31465  sumnnodd  31878  stoweidlem7  32031  stoweidlem17  32041  wallispilem4  32092  stirlinglem2  32099  stirlinglem3  32100  stirlinglem4  32101  stirlinglem12  32109  stirlinglem13  32110  stirlinglem14  32111  stirlinglem15  32112  stirlingr  32114  dirkertrigeqlem1  32122  fouriersw  32256  gcdzeq  32578  nneoALTV  32586  divgcdoddALTV  32596  subsubelfzo0  32731  2ffzoeq  32734  altgsumbc  33214  altgsumbcALT  33215  pw2m1lepw2m1  33400  nnpw2even  33419  nnlog2ge0lt1  33460  logbpw2m1  33461  blenpw2m1  33473  nnpw2blenfzo  33475  nnpw2pmod  33477  nnpw2p  33480  blengt1fldiv2p1  33487  dignn0fr  33495  dignn0flhalflem1  33509  dignn0flhalflem2  33510  nn0sumshdiglemA  33513  nn0sumshdiglemB  33514
  Copyright terms: Public domain W3C validator