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

Theorem nnz 10259
Description: A natural number 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 10257 . 2  |-  NN  C_  ZZ
21sseli 3304 1  |-  ( N  e.  NN  ->  N  e.  ZZ )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   NNcn 9956   ZZcz 10238
This theorem is referenced by:  elnnz1  10263  znegcl  10269  nnleltp1  10285  nnltp1le  10286  nnlem1lt  10294  nnltlem1  10295  prime  10306  nneo  10309  zeo  10311  uzindOLD  10320  btwnz  10328  eluz2b2  10504  qaddcl  10546  qreccl  10550  elfz1end  11037  fznn  11070  elfzo0  11126  elfzo1  11128  quoremz  11191  intfracq  11195  fznnfl  11198  zmodcl  11221  zmodfz  11223  zmodfzo  11224  expnnval  11340  mulexpz  11375  nnesq  11458  expnlbnd  11464  expnlbnd2  11465  digit2  11467  faclbnd  11536  bc0k  11557  bcval5  11564  fz1isolem  11665  seqcoll  11667  absexpz  12065  climuni  12301  isercoll  12416  climcnds  12586  arisum  12594  trireciplem  12596  expcnv  12598  geo2sum  12605  geo2lim  12607  0.999...  12613  geoihalfsum  12614  rpnnen2lem6  12774  rpnnen2lem9  12777  rpnnen2lem10  12778  dvdsval3  12811  nndivdvds  12813  dvdsle  12850  dvdseq  12852  fzm1ndvds  12856  dvdsfac  12859  oexpneg  12866  divalg2  12880  divalgmod  12881  ndvdsadd  12883  modgcd  12991  gcddiv  13004  gcdmultiple  13005  gcdmultiplez  13006  gcdeq  13007  rpmulgcd  13010  rplpwr  13011  rppwr  13012  sqgcd  13013  dvdssqlem  13014  dvdssq  13015  eucalginv  13030  1idssfct  13040  isprm3  13043  prmind2  13045  qredeq  13061  qredeu  13062  isprm6  13064  divgcdodd  13074  divnumden  13095  divdenle  13096  nn0gcdsq  13099  phicl2  13112  phiprmpw  13120  eulerthlem2  13126  pythagtriplem3  13147  pythagtriplem4  13148  pythagtriplem6  13150  pythagtriplem7  13151  pythagtriplem8  13152  pythagtriplem9  13153  pythagtriplem11  13154  pythagtriplem13  13156  pythagtriplem15  13158  pythagtriplem19  13162  pythagtrip  13163  iserodd  13164  pclem  13167  pccl  13178  pcdiv  13181  pcqcl  13185  pcdvds  13192  pcndvds  13194  pcndvds2  13196  pcelnn  13198  pcz  13209  pcmpt  13216  fldivp1  13221  pcfac  13223  infpnlem1  13233  prmunb  13237  prmreclem1  13239  1arith  13250  ram0  13345  mulgnn  14851  ghmmulg  14973  dfod2  15155  gexdvds  15173  gexnnod  15177  gexex  15423  mulgass2  15665  qsssubdrg  16713  prmirredlem  16728  znidomb  16797  znrrg  16801  lmmo  17398  1stckgenlem  17538  imasdsf1olem  18356  clmmulg  19071  cmetcaulem  19194  ovolunlem1a  19345  ovolicc2lem4  19369  mbfi1fseqlem6  19565  dvexp3  19815  dgreq0  20136  elqaalem2  20190  aaliou3lem1  20212  aaliou3lem2  20213  aaliou3lem3  20214  aaliou3lem9  20220  pserdvlem2  20297  logtayl2  20506  root1eq1  20592  root1cj  20593  atantayl2  20731  birthdaylem2  20744  birthdaylem3  20745  emcllem5  20791  basellem2  20817  basellem3  20818  basellem5  20820  sgmss  20842  issqf  20872  sgmnncl  20883  prmorcht  20914  mumullem1  20915  mumullem2  20916  sqff1o  20918  dvdsdivcl  20919  dvdsflsumcom  20926  muinv  20931  vmalelog  20942  chtublem  20948  vmasum  20953  logfac2  20954  logfaclbnd  20959  bclbnd  21017  bposlem5  21025  lgsval4a  21055  lgssq  21072  lgssq2  21073  lgsdchr  21085  lgsquadlem1  21091  lgsquadlem2  21092  lgsquad3  21098  rplogsumlem1  21131  rplogsumlem2  21132  dchrisumlem2  21137  dchrmusumlema  21140  dchrmusum2  21141  dchrvmasumiflem1  21148  dchrvmaeq0  21151  dchrisum0flblem2  21156  dchrisum0re  21160  dchrisum0lema  21161  dchrisum0lem1b  21162  dchrisum0lem2a  21164  logdivbnd  21203  pntrsumbnd2  21214  ostth2lem1  21265  ostth2lem3  21282  ostth3  21285  gxpval  21800  gxcom  21810  gxinv  21811  gxid  21814  gxmodid  21820  gxdi  21837  bcm1n  24104  pnfinf  24206  esumcvg  24429  erdszelem7  24836  climuzcnv  25061  elfzm12  25065  zmodid2  25067  fznatpl1  25151  axlowdimlem13  25797  mblfinlem  26143  nn0prpwlem  26215  fzmul  26334  incsequz  26342  geomcau  26355  heibor1lem  26408  bfplem2  26422  fzsplit1nn0  26702  irrapxlem1  26775  pellexlem5  26786  rmynn  26911  jm2.24nn  26914  jm2.17c  26917  congrep  26928  congabseq  26929  acongrep  26935  acongeq  26938  jm2.18  26949  jm2.23  26957  jm2.20nn  26958  jm2.26lem3  26962  jm2.26  26963  jm2.15nn0  26964  jm2.16nn0  26965  jm2.27dlem2  26971  rmydioph  26975  jm3.1  26981  expdiophlem1  26982  expdioph  26984  idomodle  27380  hashgcdlem  27384  hashgcdeq  27385  phisum  27386  proot1ex  27388  stoweidlem7  27623  stoweidlem17  27633  wallispilem4  27684  stirlinglem2  27691  stirlinglem3  27692  stirlinglem4  27693  stirlinglem12  27701  stirlinglem13  27702  stirlinglem14  27703  stirlinglem15  27704  stirlingr  27706  ubmelfzo  27986  ubmelm1fzo  27987  fzo1fzo0n0  27988  swrdccatin12lem3a  28021  swrdccatin12lem3b  28022  swrdccatin12lem3c  28023  swrdccatin12lem3  28024  swrdccatin12  28026
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-riota 6508  df-recs 6592  df-rdg 6627  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-nn 9957  df-z 10239
  Copyright terms: Public domain W3C validator