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

Theorem nnz 11359
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 11357 . 2 ℕ ⊆ ℤ
21sseli 3584 1 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  cn 10980  cz 11337
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-om 7028  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-er 7702  df-en 7916  df-dom 7917  df-sdom 7918  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-nn 10981  df-z 11338
This theorem is referenced by:  elnnz1  11363  znegcl  11372  nnleltp1  11392  nnltp1le  11393  nnlem1lt  11403  nnltlem1  11404  nnm1ge0  11405  prime  11418  nneo  11421  zeo  11423  btwnz  11439  eluz2b2  11721  qaddcl  11764  qreccl  11768  elfz1end  12329  fznatpl1  12353  fznn  12366  elfz1b  12367  elfzo0  12465  elfzo0z  12466  elfzo1  12474  fzo1fzo0n0  12475  ubmelm1fzo  12521  quoremz  12610  intfracq  12614  fznnfl  12617  zmodcl  12646  zmodfz  12648  zmodfzo  12649  zmodid2  12654  zmodidfzo  12655  modfzo0difsn  12698  expnnval  12819  mulexpz  12856  nnesq  12944  expnlbnd  12950  expnlbnd2  12951  digit2  12953  faclbnd  13033  bc0k  13054  bcval5  13061  fz1isolem  13199  seqcoll  13202  lswccatn0lsw  13328  cshwidxmod  13502  cshwidxn  13508  absexpz  13995  climuni  14233  isercoll  14348  climcnds  14527  arisum  14536  trireciplem  14538  expcnv  14540  geo2sum  14548  geo2lim  14550  0.999...  14556  0.999...OLD  14557  geoihalfsum  14558  rpnnen2lem6  14892  rpnnen2lem9  14895  rpnnen2lem10  14896  dvdsval3  14930  nndivdvds  14932  modmulconst  14956  dvdsle  14975  dvdsssfz1  14983  fzm1ndvds  14987  dvdsfac  14991  oexpneg  15012  nnoddm1d2  15045  pwp1fsum  15057  divalg2  15071  divalgmod  15072  divalgmodOLD  15073  modremain  15075  ndvdsadd  15077  nndvdslegcd  15170  divgcdz  15176  divgcdnn  15179  divgcdnnr  15180  modgcd  15196  gcddiv  15211  gcdmultiple  15212  gcdmultiplez  15213  gcdzeq  15214  gcdeq  15215  rpmulgcd  15218  rplpwr  15219  rppwr  15220  sqgcd  15221  dvdssqlem  15222  dvdssq  15223  eucalginv  15240  lcmgcdlem  15262  lcmgcdnn  15267  lcmass  15270  lcmftp  15292  lcmfunsnlem2lem1  15294  coprmgcdb  15305  qredeq  15314  qredeu  15315  coprmprod  15318  coprmproddvdslem  15319  coprmproddvds  15320  cncongr1  15324  cncongr2  15325  1idssfct  15336  isprm3  15339  prmind2  15341  divgcdodd  15365  isprm6  15369  ncoprmlnprm  15379  divnumden  15399  divdenle  15400  nn0gcdsq  15403  phicl2  15416  phiprmpw  15424  eulerthlem2  15430  hashgcdlem  15436  hashgcdeq  15437  phisum  15438  nnoddn2prm  15459  pythagtriplem3  15466  pythagtriplem4  15467  pythagtriplem6  15469  pythagtriplem7  15470  pythagtriplem8  15471  pythagtriplem9  15472  pythagtriplem11  15473  pythagtriplem13  15475  pythagtriplem15  15477  pythagtriplem19  15481  pythagtrip  15482  iserodd  15483  pclem  15486  pccl  15497  pcdiv  15500  pcqcl  15504  pcdvds  15511  pcndvds  15513  pcndvds2  15515  pcelnn  15517  pcz  15528  pcmpt  15539  fldivp1  15544  pcfac  15546  infpnlem1  15557  prmunb  15561  prmreclem1  15563  1arith  15574  ram0  15669  prmdvdsprmo  15689  prmgaplem4  15701  prmgaplem6  15703  prmgaplem7  15704  cshwshashlem2  15746  setsstruct2  15836  setsstructOLD  15839  mulgnn  17487  mulgaddcom  17504  mulginvcom  17505  mulgmodid  17521  ghmmulg  17612  dfod2  17921  gexdvds  17939  gexnnod  17943  gexex  18196  mulgass2  18541  qsssubdrg  19745  prmirredlem  19781  znidomb  19850  znrrg  19854  chfacfisf  20599  chfacfisfcpmat  20600  chfacfscmul0  20603  chfacfpmmul0  20607  cayhamlem1  20611  cpmadugsumlemF  20621  lmmo  21124  1stckgenlem  21296  imasdsf1olem  22118  clmmulg  22841  cmetcaulem  23026  ovolunlem1a  23204  ovolicc2lem4  23228  mbfi1fseqlem6  23427  dvexp3  23679  dgreq0  23959  elqaalem2  24013  aaliou3lem1  24035  aaliou3lem2  24036  aaliou3lem3  24037  aaliou3lem9  24043  pserdvlem2  24120  logtayl2  24342  root1eq1  24430  root1cj  24431  atantayl2  24599  birthdaylem2  24613  birthdaylem3  24614  emcllem5  24660  basellem2  24742  basellem3  24743  basellem5  24745  issqf  24796  sgmnncl  24807  prmorcht  24838  mumullem1  24839  mumullem2  24840  sqff1o  24842  dvdsflsumcom  24848  muinv  24853  vmalelog  24864  chtublem  24870  vmasum  24875  logfac2  24876  logfaclbnd  24881  bclbnd  24939  bposlem5  24947  lgsval4a  24978  lgssq2  24997  lgsdchr  25014  gausslemma2dlem0c  25017  gausslemma2dlem0e  25019  gausslemma2dlem1a  25024  gausslemma2dlem5  25030  lgsquadlem1  25039  lgsquadlem2  25040  lgsquad3  25046  2lgslem1a1  25048  2lgslem3  25063  2lgsoddprm  25075  rplogsumlem1  25107  rplogsumlem2  25108  dchrisumlem2  25113  dchrmusumlema  25116  dchrmusum2  25117  dchrvmasumiflem1  25124  dchrvmaeq0  25127  dchrisum0flblem2  25132  dchrisum0re  25136  dchrisum0lema  25137  dchrisum0lem1b  25138  dchrisum0lem2a  25140  logdivbnd  25179  pntrsumbnd2  25190  ostth2lem1  25241  ostth2lem3  25258  ostth3  25261  axlowdimlem13  25768  crctcshwlkn0lem4  26608  crctcshwlkn0lem5  26609  crctcshwlkn0lem7  26611  wlkiswwlksupgr2  26666  clwwlksel  26814  clwwlksf  26815  clwwlksvbij  26822  wwlksubclwwlks  26825  clwwisshclwwslem  26827  eucrctshift  27003  eucrct2eupth  27005  numclwlk2lem2f  27125  bcm1n  29437  pnfinf  29564  isarchiofld  29644  rearchi  29669  submat1n  29695  lmatfvlem  29705  esumcvg  29971  oddpwdc  30239  fibp1  30286  erdszelem7  30940  climuzcnv  31326  elfzm12  31330  bcprod  31385  nn0prpwlem  32012  knoppndvlem1  32198  knoppndvlem2  32199  knoppndvlem7  32204  knoppndvlem18  32215  poimirlem13  33093  poimirlem14  33094  mblfinlem2  33118  fzmul  33208  incsequz  33215  geomcau  33226  heibor1lem  33279  bfplem2  33293  fzsplit1nn0  36836  irrapxlem1  36905  pellexlem5  36916  rmynn  37042  jm2.24nn  37045  jm2.17c  37048  congrep  37059  congabseq  37060  acongrep  37066  acongeq  37069  jm2.18  37074  jm2.23  37082  jm2.20nn  37083  jm2.26lem3  37087  jm2.26  37088  jm2.15nn0  37089  jm2.16nn0  37090  jm2.27dlem2  37096  rmydioph  37100  jm3.1  37106  expdiophlem1  37107  expdioph  37109  idomodle  37294  proot1ex  37299  nznngen  38036  sumnnodd  39298  stoweidlem7  39561  stoweidlem17  39571  wallispilem4  39622  stirlinglem2  39629  stirlinglem3  39630  stirlinglem4  39631  stirlinglem12  39639  stirlinglem13  39640  stirlinglem14  39641  stirlinglem15  39642  stirlingr  39644  dirkertrigeqlem1  39652  fouriersw  39785  ovnsubaddlem1  40121  subsubelfzo0  40663  2ffzoeq  40665  iccpartres  40682  iccpartipre  40685  iccpartltu  40689  iccelpart  40697  odz2prm2pw  40804  fmtnoprmfac2lem1  40807  pwdif  40830  2pwp1prm  40832  lighneallem2  40852  lighneallem4  40856  lighneal  40857  proththd  40860  nneoALTV  40912  divgcdoddALTV  40922  gboge7  40976  gbege6  40978  altgsumbc  41448  altgsumbcALT  41449  pw2m1lepw2m1  41628  nnpw2even  41641  nnlog2ge0lt1  41682  logbpw2m1  41683  blenpw2m1  41695  nnpw2blenfzo  41697  nnpw2pmod  41699  nnpw2p  41702  blengt1fldiv2p1  41709  dignn0fr  41717  dignn0flhalflem1  41731  dignn0flhalflem2  41732  nn0sumshdiglemA  41735  nn0sumshdiglemB  41736
  Copyright terms: Public domain W3C validator