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

Theorem nnz 10893
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 10891 . 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 1804   NNcn 10543   ZZcz 10871
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570  ax-pre-ltadd 9571  ax-pre-mulgt0 9572
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-riota 6242  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-om 6686  df-recs 7044  df-rdg 7078  df-er 7313  df-en 7519  df-dom 7520  df-sdom 7521  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637  df-sub 9812  df-neg 9813  df-nn 10544  df-z 10872
This theorem is referenced by:  elnnz1  10897  znegcl  10906  nnleltp1  10925  nnltp1le  10926  nnlem1lt  10936  nnltlem1  10937  nnm1ge0  10938  prime  10950  nneo  10953  zeo  10955  uzindOLD  10964  btwnz  10972  eluz2b2  11164  qaddcl  11208  qreccl  11212  elfz1end  11725  fznatpl1  11744  fznn  11757  elfz1b  11758  elfzo0  11844  fzo1fzo0n0  11845  elfzo0z  11846  elfzo1  11852  ubmelm1fzo  11889  quoremz  11963  intfracq  11967  fznnfl  11970  zmodcl  11996  zmodfz  11998  zmodfzo  11999  modidmul0  12003  zmodid2  12005  zmodidfzo  12006  expnnval  12150  mulexpz  12187  nnesq  12271  expnlbnd  12277  expnlbnd2  12278  digit2  12280  faclbnd  12349  bc0k  12370  bcval5  12377  fz1isolem  12491  seqcoll  12493  cshwidxmod  12755  cshwidxn  12760  absexpz  13119  climuni  13356  isercoll  13471  climcnds  13644  arisum  13652  trireciplem  13654  expcnv  13656  geo2sum  13663  geo2lim  13665  0.999...  13671  geoihalfsum  13672  rpnnen2lem6  13934  rpnnen2lem9  13937  rpnnen2lem10  13938  dvdsval3  13971  nndivdvds  13973  dvdsle  14012  dvdseq  14014  fzm1ndvds  14019  dvdsfac  14022  oexpneg  14030  divalg2  14044  divalgmod  14045  ndvdsadd  14047  modgcd  14155  gcddiv  14168  gcdmultiple  14169  gcdmultiplez  14170  gcdeq  14171  rpmulgcd  14174  rplpwr  14175  rppwr  14176  sqgcd  14177  dvdssqlem  14178  dvdssq  14179  eucalginv  14194  1idssfct  14204  isprm3  14207  prmind2  14209  qredeq  14228  qredeu  14229  isprm6  14231  divgcdodd  14241  divnumden  14262  divdenle  14263  nn0gcdsq  14266  phicl2  14279  phiprmpw  14287  eulerthlem2  14293  pythagtriplem3  14323  pythagtriplem4  14324  pythagtriplem6  14326  pythagtriplem7  14327  pythagtriplem8  14328  pythagtriplem9  14329  pythagtriplem11  14330  pythagtriplem13  14332  pythagtriplem15  14334  pythagtriplem19  14338  pythagtrip  14339  iserodd  14340  pclem  14343  pccl  14354  pcdiv  14357  pcqcl  14361  pcdvds  14368  pcndvds  14370  pcndvds2  14372  pcelnn  14374  pcz  14385  pcmpt  14392  fldivp1  14397  pcfac  14399  infpnlem1  14409  prmunb  14413  prmreclem1  14415  1arith  14426  ram0  14521  cshwshashlem2  14562  mulgnn  16126  ghmmulg  16257  dfod2  16564  gexdvds  16582  gexnnod  16586  gexex  16837  mulgass2  17225  qsssubdrg  18455  prmirredlem  18500  prmirredlemOLD  18503  znidomb  18577  znrrg  18581  chfacfisf  19332  chfacfisfcpmat  19333  chfacfscmul0  19336  chfacfpmmul0  19340  cayhamlem1  19344  cpmadugsumlemF  19354  lmmo  19858  1stckgenlem  20031  imasdsf1olem  20853  clmmulg  21570  cmetcaulem  21704  ovolunlem1a  21884  ovolicc2lem4  21908  mbfi1fseqlem6  22104  dvexp3  22356  dgreq0  22638  elqaalem2  22692  aaliou3lem1  22714  aaliou3lem2  22715  aaliou3lem3  22716  aaliou3lem9  22722  pserdvlem2  22799  logtayl2  23019  root1eq1  23105  root1cj  23106  atantayl2  23245  birthdaylem2  23258  birthdaylem3  23259  emcllem5  23305  basellem2  23331  basellem3  23332  basellem5  23334  sgmss  23356  issqf  23386  sgmnncl  23397  prmorcht  23428  mumullem1  23429  mumullem2  23430  sqff1o  23432  dvdsdivcl  23433  dvdsflsumcom  23440  muinv  23445  vmalelog  23456  chtublem  23462  vmasum  23467  logfac2  23468  logfaclbnd  23473  bclbnd  23531  bposlem5  23539  lgsval4a  23569  lgssq  23586  lgssq2  23587  lgsdchr  23599  lgsquadlem1  23605  lgsquadlem2  23606  lgsquad3  23612  rplogsumlem1  23645  rplogsumlem2  23646  dchrisumlem2  23651  dchrmusumlema  23654  dchrmusum2  23655  dchrvmasumiflem1  23662  dchrvmaeq0  23665  dchrisum0flblem2  23670  dchrisum0re  23674  dchrisum0lema  23675  dchrisum0lem1b  23676  dchrisum0lem2a  23678  logdivbnd  23717  pntrsumbnd2  23728  ostth2lem1  23779  ostth2lem3  23796  ostth3  23799  axlowdimlem13  24233  clwwlkel  24769  clwwlkf  24770  clwwlkvbij  24777  wwlksubclwwlk  24780  clwwisshclwwlem  24782  clwwisshclww  24783  numclwlk2lem2f  25079  gxpval  25237  gxcom  25247  gxinv  25248  gxid  25251  gxmodid  25257  gxdi  25274  bcm1n  27576  pnfinf  27704  isarchiofld  27784  rearchi  27809  esumcvg  28069  oddpwdc  28270  fibp1  28317  erdszelem7  28618  climuzcnv  29014  elfzm12  29018  mblfinlem2  30027  nn0prpwlem  30115  fzmul  30208  incsequz  30216  geomcau  30227  heibor1lem  30280  bfplem2  30294  fzsplit1nn0  30662  irrapxlem1  30733  pellexlem5  30744  rmynn  30869  jm2.24nn  30872  jm2.17c  30875  congrep  30886  congabseq  30887  acongrep  30893  acongeq  30896  jm2.18  30905  jm2.23  30913  jm2.20nn  30914  jm2.26lem3  30918  jm2.26  30919  jm2.15nn0  30920  jm2.16nn0  30921  jm2.27dlem2  30927  rmydioph  30931  jm3.1  30937  expdiophlem1  30938  expdioph  30940  idomodle  31129  hashgcdlem  31133  hashgcdeq  31134  phisum  31135  proot1ex  31137  lcmgcdlem  31188  lcmass  31194  nznngen  31197  sumnnodd  31544  stoweidlem7  31678  stoweidlem17  31688  wallispilem4  31739  stirlinglem2  31746  stirlinglem3  31747  stirlinglem4  31748  stirlinglem12  31756  stirlinglem13  31757  stirlinglem14  31758  stirlinglem15  31759  stirlingr  31761  dirkertrigeqlem1  31769  fouriersw  31903  subsubelfzo0  32176  2ffzoeq  32179  altgsumbc  32674  altgsumbcALT  32675
  Copyright terms: Public domain W3C validator