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

Theorem nnz 11232
Description: A positive integer is an integer. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
nnz (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

Proof of Theorem nnz
StepHypRef Expression
1 nnssz 11230 . 2 ℕ ⊆ ℤ
21sseli 3563 1 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  cn 10867  cz 11210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-er 7606  df-en 7819  df-dom 7820  df-sdom 7821  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-nn 10868  df-z 11211
This theorem is referenced by:  elnnz1  11236  znegcl  11245  nnleltp1  11265  nnltp1le  11266  nnlem1lt  11275  nnltlem1  11276  nnm1ge0  11277  prime  11290  nneo  11293  zeo  11295  btwnz  11311  eluz2b2  11593  qaddcl  11636  qreccl  11640  elfz1end  12197  fznatpl1  12220  fznn  12233  elfz1b  12234  elfzo0  12331  elfzo0z  12332  elfzo1  12340  fzo1fzo0n0  12341  ubmelm1fzo  12385  quoremz  12471  intfracq  12475  fznnfl  12478  zmodcl  12507  zmodfz  12509  zmodfzo  12510  zmodid2  12515  zmodidfzo  12516  modfzo0difsn  12559  expnnval  12680  mulexpz  12717  nnesq  12805  expnlbnd  12811  expnlbnd2  12812  digit2  12814  faclbnd  12894  bc0k  12915  bcval5  12922  fz1isolem  13054  seqcoll  13057  lswccatn0lsw  13172  cshwidxmod  13346  cshwidxn  13352  absexpz  13839  climuni  14077  isercoll  14192  climcnds  14368  arisum  14377  trireciplem  14379  expcnv  14381  geo2sum  14389  geo2lim  14391  0.999...  14397  0.999...OLD  14398  geoihalfsum  14399  rpnnen2lem6  14733  rpnnen2lem9  14736  rpnnen2lem10  14737  dvdsval3  14771  nndivdvds  14773  modmulconst  14797  dvdsle  14816  dvdsssfz1  14824  fzm1ndvds  14828  dvdsfac  14832  oexpneg  14853  nnoddm1d2  14886  pwp1fsum  14898  divalg2  14912  divalgmod  14913  divalgmodOLD  14914  modremain  14916  ndvdsadd  14918  nndvdslegcd  15011  divgcdz  15017  divgcdnn  15020  divgcdnnr  15021  modgcd  15037  gcddiv  15052  gcdmultiple  15053  gcdmultiplez  15054  gcdzeq  15055  gcdeq  15056  rpmulgcd  15059  rplpwr  15060  rppwr  15061  sqgcd  15062  dvdssqlem  15063  dvdssq  15064  eucalginv  15081  lcmgcdlem  15103  lcmgcdnn  15108  lcmass  15111  lcmftp  15133  lcmfunsnlem2lem1  15135  coprmgcdb  15146  qredeq  15155  qredeu  15156  coprmprod  15159  coprmproddvdslem  15160  coprmproddvds  15161  cncongr1  15165  cncongr2  15166  1idssfct  15177  isprm3  15180  prmind2  15182  divgcdodd  15206  isprm6  15210  ncoprmlnprm  15220  divnumden  15240  divdenle  15241  nn0gcdsq  15244  phicl2  15257  phiprmpw  15265  eulerthlem2  15271  hashgcdlem  15277  hashgcdeq  15278  phisum  15279  nnoddn2prm  15300  pythagtriplem3  15307  pythagtriplem4  15308  pythagtriplem6  15310  pythagtriplem7  15311  pythagtriplem8  15312  pythagtriplem9  15313  pythagtriplem11  15314  pythagtriplem13  15316  pythagtriplem15  15318  pythagtriplem19  15322  pythagtrip  15323  iserodd  15324  pclem  15327  pccl  15338  pcdiv  15341  pcqcl  15345  pcdvds  15352  pcndvds  15354  pcndvds2  15356  pcelnn  15358  pcz  15369  pcmpt  15380  fldivp1  15385  pcfac  15387  infpnlem1  15398  prmunb  15402  prmreclem1  15404  1arith  15415  ram0  15510  prmdvdsprmo  15530  prmgaplem4  15542  prmgaplem6  15544  prmgaplem7  15545  cshwshashlem2  15587  setsstruct  15673  mulgnn  17316  mulgaddcom  17333  mulginvcom  17334  mulgmodid  17350  ghmmulg  17441  dfod2  17750  gexdvds  17768  gexnnod  17772  gexex  18025  mulgass2  18370  qsssubdrg  19570  prmirredlem  19605  znidomb  19674  znrrg  19678  chfacfisf  20420  chfacfisfcpmat  20421  chfacfscmul0  20424  chfacfpmmul0  20428  cayhamlem1  20432  cpmadugsumlemF  20442  lmmo  20936  1stckgenlem  21108  imasdsf1olem  21929  clmmulg  22640  cmetcaulem  22812  ovolunlem1a  22988  ovolicc2lem4  23012  mbfi1fseqlem6  23210  dvexp3  23462  dgreq0  23742  elqaalem2  23796  aaliou3lem1  23818  aaliou3lem2  23819  aaliou3lem3  23820  aaliou3lem9  23826  pserdvlem2  23903  logtayl2  24125  root1eq1  24213  root1cj  24214  atantayl2  24382  birthdaylem2  24396  birthdaylem3  24397  emcllem5  24443  basellem2  24525  basellem3  24526  basellem5  24528  issqf  24579  sgmnncl  24590  prmorcht  24621  mumullem1  24622  mumullem2  24623  sqff1o  24625  dvdsflsumcom  24631  muinv  24636  vmalelog  24647  chtublem  24653  vmasum  24658  logfac2  24659  logfaclbnd  24664  bclbnd  24722  bposlem5  24730  lgsval4a  24761  lgssq2  24780  lgsdchr  24797  gausslemma2dlem0c  24800  gausslemma2dlem0e  24802  gausslemma2dlem1a  24807  gausslemma2dlem5  24813  lgsquadlem1  24822  lgsquadlem2  24823  lgsquad3  24829  2lgslem1a1  24831  2lgslem3  24846  2lgsoddprm  24858  rplogsumlem1  24890  rplogsumlem2  24891  dchrisumlem2  24896  dchrmusumlema  24899  dchrmusum2  24900  dchrvmasumiflem1  24907  dchrvmaeq0  24910  dchrisum0flblem2  24915  dchrisum0re  24919  dchrisum0lema  24920  dchrisum0lem1b  24921  dchrisum0lem2a  24923  logdivbnd  24962  pntrsumbnd2  24973  ostth2lem1  25024  ostth2lem3  25041  ostth3  25044  axlowdimlem13  25552  clwwlkel  26087  clwwlkf  26088  clwwlkvbij  26095  wwlksubclwwlk  26098  clwwisshclwwlem  26100  clwwisshclww  26101  numclwlk2lem2f  26396  bcm1n  28747  pnfinf  28874  isarchiofld  28954  rearchi  28979  submat1n  29005  lmatfvlem  29015  esumcvg  29281  oddpwdc  29549  fibp1  29596  erdszelem7  30239  climuzcnv  30625  elfzm12  30629  bcprod  30683  nn0prpwlem  31293  knoppndvlem1  31479  knoppndvlem2  31480  knoppndvlem7  31485  knoppndvlem18  31496  poimirlem13  32388  poimirlem14  32389  mblfinlem2  32413  fzmul  32503  incsequz  32510  geomcau  32521  heibor1lem  32574  bfplem2  32588  fzsplit1nn0  36131  irrapxlem1  36200  pellexlem5  36211  rmynn  36337  jm2.24nn  36340  jm2.17c  36343  congrep  36354  congabseq  36355  acongrep  36361  acongeq  36364  jm2.18  36369  jm2.23  36377  jm2.20nn  36378  jm2.26lem3  36382  jm2.26  36383  jm2.15nn0  36384  jm2.16nn0  36385  jm2.27dlem2  36391  rmydioph  36395  jm3.1  36401  expdiophlem1  36402  expdioph  36404  idomodle  36589  proot1ex  36594  nznngen  37333  sumnnodd  38494  stoweidlem7  38697  stoweidlem17  38707  wallispilem4  38758  stirlinglem2  38765  stirlinglem3  38766  stirlinglem4  38767  stirlinglem12  38775  stirlinglem13  38776  stirlinglem14  38777  stirlinglem15  38778  stirlingr  38780  dirkertrigeqlem1  38788  fouriersw  38921  ovnsubaddlem1  39257  iccpartres  39754  iccpartipre  39757  iccpartltu  39761  iccelpart  39769  odz2prm2pw  39811  fmtnoprmfac2lem1  39814  pwdif  39837  2pwp1prm  39839  lighneallem2  39859  lighneallem4  39863  lighneal  39864  proththd  39867  nneoALTV  39919  divgcdoddALTV  39929  gboge7  39983  gbege6  39985  subsubelfzo0  40179  2ffzoeq  40181  crctcsh1wlkn0lem4  41011  crctcsh1wlkn0lem5  41012  crctcsh1wlkn0lem7  41014  1wlkiswwlksupgr2  41069  clwwlksel  41216  clwwlksf  41217  clwwlksvbij  41224  wwlksubclwwlks  41227  clwwisshclwwslem  41229  eucrctshift  41406  eucrct2eupth  41408  av-numclwlk2lem2f  41528  altgsumbc  41918  altgsumbcALT  41919  pw2m1lepw2m1  42099  nnpw2even  42112  nnlog2ge0lt1  42153  logbpw2m1  42154  blenpw2m1  42166  nnpw2blenfzo  42168  nnpw2pmod  42170  nnpw2p  42173  blengt1fldiv2p1  42180  dignn0fr  42188  dignn0flhalflem1  42202  dignn0flhalflem2  42203  nn0sumshdiglemA  42206  nn0sumshdiglemB  42207
  Copyright terms: Public domain W3C validator