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

Theorem nnz 10304
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 10302 . 2  |-  NN  C_  ZZ
21sseli 3345 1  |-  ( N  e.  NN  ->  N  e.  ZZ )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   NNcn 10001   ZZcz 10283
This theorem is referenced by:  elnnz1  10308  znegcl  10314  nnleltp1  10330  nnltp1le  10331  nnlem1lt  10339  nnltlem1  10340  prime  10351  nneo  10354  zeo  10356  uzindOLD  10365  btwnz  10373  eluz2b2  10549  qaddcl  10591  qreccl  10595  elfz1end  11082  fznn  11116  elfzo0  11172  elfzo1  11174  quoremz  11237  intfracq  11241  fznnfl  11244  zmodcl  11267  zmodfz  11269  zmodfzo  11270  expnnval  11386  mulexpz  11421  nnesq  11504  expnlbnd  11510  expnlbnd2  11511  digit2  11513  faclbnd  11582  bc0k  11603  bcval5  11610  fz1isolem  11711  seqcoll  11713  absexpz  12111  climuni  12347  isercoll  12462  climcnds  12632  arisum  12640  trireciplem  12642  expcnv  12644  geo2sum  12651  geo2lim  12653  0.999...  12659  geoihalfsum  12660  rpnnen2lem6  12820  rpnnen2lem9  12823  rpnnen2lem10  12824  dvdsval3  12857  nndivdvds  12859  dvdsle  12896  dvdseq  12898  fzm1ndvds  12902  dvdsfac  12905  oexpneg  12912  divalg2  12926  divalgmod  12927  ndvdsadd  12929  modgcd  13037  gcddiv  13050  gcdmultiple  13051  gcdmultiplez  13052  gcdeq  13053  rpmulgcd  13056  rplpwr  13057  rppwr  13058  sqgcd  13059  dvdssqlem  13060  dvdssq  13061  eucalginv  13076  1idssfct  13086  isprm3  13089  prmind2  13091  qredeq  13107  qredeu  13108  isprm6  13110  divgcdodd  13120  divnumden  13141  divdenle  13142  nn0gcdsq  13145  phicl2  13158  phiprmpw  13166  eulerthlem2  13172  pythagtriplem3  13193  pythagtriplem4  13194  pythagtriplem6  13196  pythagtriplem7  13197  pythagtriplem8  13198  pythagtriplem9  13199  pythagtriplem11  13200  pythagtriplem13  13202  pythagtriplem15  13204  pythagtriplem19  13208  pythagtrip  13209  iserodd  13210  pclem  13213  pccl  13224  pcdiv  13227  pcqcl  13231  pcdvds  13238  pcndvds  13240  pcndvds2  13242  pcelnn  13244  pcz  13255  pcmpt  13262  fldivp1  13267  pcfac  13269  infpnlem1  13279  prmunb  13283  prmreclem1  13285  1arith  13296  ram0  13391  mulgnn  14897  ghmmulg  15019  dfod2  15201  gexdvds  15219  gexnnod  15223  gexex  15469  mulgass2  15711  qsssubdrg  16759  prmirredlem  16774  znidomb  16843  znrrg  16847  lmmo  17445  1stckgenlem  17586  imasdsf1olem  18404  clmmulg  19119  cmetcaulem  19242  ovolunlem1a  19393  ovolicc2lem4  19417  mbfi1fseqlem6  19613  dvexp3  19863  dgreq0  20184  elqaalem2  20238  aaliou3lem1  20260  aaliou3lem2  20261  aaliou3lem3  20262  aaliou3lem9  20268  pserdvlem2  20345  logtayl2  20554  root1eq1  20640  root1cj  20641  atantayl2  20779  birthdaylem2  20792  birthdaylem3  20793  emcllem5  20839  basellem2  20865  basellem3  20866  basellem5  20868  sgmss  20890  issqf  20920  sgmnncl  20931  prmorcht  20962  mumullem1  20963  mumullem2  20964  sqff1o  20966  dvdsdivcl  20967  dvdsflsumcom  20974  muinv  20979  vmalelog  20990  chtublem  20996  vmasum  21001  logfac2  21002  logfaclbnd  21007  bclbnd  21065  bposlem5  21073  lgsval4a  21103  lgssq  21120  lgssq2  21121  lgsdchr  21133  lgsquadlem1  21139  lgsquadlem2  21140  lgsquad3  21146  rplogsumlem1  21179  rplogsumlem2  21180  dchrisumlem2  21185  dchrmusumlema  21188  dchrmusum2  21189  dchrvmasumiflem1  21196  dchrvmaeq0  21199  dchrisum0flblem2  21204  dchrisum0re  21208  dchrisum0lema  21209  dchrisum0lem1b  21210  dchrisum0lem2a  21212  logdivbnd  21251  pntrsumbnd2  21262  ostth2lem1  21313  ostth2lem3  21330  ostth3  21333  gxpval  21848  gxcom  21858  gxinv  21859  gxid  21862  gxmodid  21868  gxdi  21885  bcm1n  24152  pnfinf  24254  esumcvg  24477  erdszelem7  24884  climuzcnv  25109  elfzm12  25113  zmodid2  25115  fznatpl1  25199  axlowdimlem13  25894  mblfinlem2  26245  nn0prpwlem  26326  fzmul  26445  incsequz  26453  geomcau  26466  heibor1lem  26519  bfplem2  26533  fzsplit1nn0  26813  irrapxlem1  26886  pellexlem5  26897  rmynn  27022  jm2.24nn  27025  jm2.17c  27028  congrep  27039  congabseq  27040  acongrep  27046  acongeq  27049  jm2.18  27060  jm2.23  27068  jm2.20nn  27069  jm2.26lem3  27073  jm2.26  27074  jm2.15nn0  27075  jm2.16nn0  27076  jm2.27dlem2  27082  rmydioph  27086  jm3.1  27092  expdiophlem1  27093  expdioph  27095  idomodle  27490  hashgcdlem  27494  hashgcdeq  27495  phisum  27496  proot1ex  27498  stoweidlem7  27733  stoweidlem17  27743  wallispilem4  27794  stirlinglem2  27801  stirlinglem3  27802  stirlinglem4  27803  stirlinglem12  27811  stirlinglem13  27812  stirlinglem14  27813  stirlinglem15  27814  stirlingr  27816  ubmelfzo  28127  ubmelm1fzo  28128  fzo1fzo0n0  28129  subsubelfzo0  28136  2ffzoeq  28141  modidmul0  28161  cshwidx  28243  cshwssizelem4a  28284
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-sep 4331  ax-nul 4339  ax-pow 4378  ax-pr 4404  ax-un 4702  ax-resscn 9048  ax-1cn 9049  ax-icn 9050  ax-addcl 9051  ax-addrcl 9052  ax-mulcl 9053  ax-mulrcl 9054  ax-mulcom 9055  ax-addass 9056  ax-mulass 9057  ax-distr 9058  ax-i2m1 9059  ax-1ne0 9060  ax-1rid 9061  ax-rnegex 9062  ax-rrecex 9063  ax-cnre 9064  ax-pre-lttri 9065  ax-pre-lttrn 9066  ax-pre-ltadd 9067  ax-pre-mulgt0 9068
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2711  df-rex 2712  df-reu 2713  df-rab 2715  df-v 2959  df-sbc 3163  df-csb 3253  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3630  df-if 3741  df-pw 3802  df-sn 3821  df-pr 3822  df-tp 3823  df-op 3824  df-uni 4017  df-iun 4096  df-br 4214  df-opab 4268  df-mpt 4269  df-tr 4304  df-eprel 4495  df-id 4499  df-po 4504  df-so 4505  df-fr 4542  df-we 4544  df-ord 4585  df-on 4586  df-lim 4587  df-suc 4588  df-om 4847  df-xp 4885  df-rel 4886  df-cnv 4887  df-co 4888  df-dm 4889  df-rn 4890  df-res 4891  df-ima 4892  df-iota 5419  df-fun 5457  df-fn 5458  df-f 5459  df-f1 5460  df-fo 5461  df-f1o 5462  df-fv 5463  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-riota 6550  df-recs 6634  df-rdg 6669  df-er 6906  df-en 7111  df-dom 7112  df-sdom 7113  df-pnf 9123  df-mnf 9124  df-xr 9125  df-ltxr 9126  df-le 9127  df-sub 9294  df-neg 9295  df-nn 10002  df-z 10284
  Copyright terms: Public domain W3C validator