Theorem nnz 12340

Description: A positive integer is an integer. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nnz	⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

Proof of Theorem nnz

Step	Hyp	Ref	Expression
1		nnssz 12338	. 2 ⊢ ℕ ⊆ ℤ
2	1	sseli 3922	1 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2110  ℕcn 11971  ℤcz 12317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356  ax-un 7580  ax-1cn 10928  ax-icn 10929  ax-addcl 10930  ax-addrcl 10931  ax-mulcl 10932  ax-mulrcl 10933  ax-i2m1 10938  ax-1ne0 10939  ax-rrecex 10942  ax-cnre 10943

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-ral 3071  df-rex 3072  df-reu 3073  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-tr 5197  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6200  df-ord 6267  df-on 6268  df-lim 6269  df-suc 6270  df-iota 6389  df-fun 6433  df-fn 6434  df-f 6435  df-f1 6436  df-fo 6437  df-f1o 6438  df-fv 6439  df-ov 7272  df-om 7705  df-2nd 7823  df-frecs 8086  df-wrecs 8117  df-recs 8191  df-rdg 8230  df-neg 11206  df-nn 11972  df-z 12318

This theorem is referenced by:  elnnz1  12344  znegcl  12353  nnleltp1  12373  nnltp1le  12374  nnlem1lt  12384  nnltlem1  12385  nnm1ge0  12386  prime  12399  nneo  12402  zeo  12404  btwnz  12420  eluz2b2  12658  qaddcl  12702  qreccl  12706  elpqb  12713  elfz1end  13283  fznatpl1  13307  fznn  13321  elfz1b  13322  elfzo0  13424  elfzo0z  13425  elfzo1  13433  fzo1fzo0n0  13434  elfzom1p1elfzo  13463  ubmelm1fzo  13479  quoremz  13571  intfracq  13575  fznnfl  13578  zmodcl  13607  zmodfz  13609  zmodfzo  13610  zmodid2  13615  zmodidfzo  13616  modfzo0difsn  13659  expnnval  13781  mulexpz  13819  nnesq  13938  expnlbnd  13944  expnlbnd2  13945  digit2  13947  faclbnd  14000  bc0k  14021  bcval5  14028  fz1isolem  14171  seqcoll  14174  ccatval21sw  14286  lswccatn0lsw  14292  cshwidxmod  14512  cshwidxn  14518  absexpz  15013  climuni  15257  isercoll  15375  climcnds  15559  arisum  15568  trireciplem  15570  expcnv  15572  pwdif  15576  geo2sum  15581  geo2lim  15583  0.999...  15589  geoihalfsum  15590  rpnnen2lem6  15924  rpnnen2lem9  15927  rpnnen2lem10  15928  dvdsval3  15963  nndivdvds  15968  modmulconst  15993  dvdsle  16015  dvdsssfz1  16023  fzm1ndvds  16027  dvdsfac  16031  mulmoddvds  16035  oexpneg  16050  nnoddm1d2  16091  pwp1fsum  16096  divalg2  16110  divalgmod  16111  modremain  16113  ndvdsadd  16115  nndvdslegcd  16208  divgcdz  16214  divgcdnn  16218  divgcdnnr  16219  modgcd  16236  gcdmultiple  16240  gcddiv  16255  gcdmultipleOLD  16256  gcdmultiplezOLD  16257  gcdzeq  16258  gcdeq  16259  rpmulgcd  16262  rplpwr  16263  rprpwr  16264  sqgcd  16266  dvdssqlem  16267  dvdssq  16268  eucalginv  16285  lcmgcdlem  16307  lcmgcdnn  16312  lcmass  16315  lcmftp  16337  lcmfunsnlem2lem1  16339  coprmgcdb  16350  qredeq  16358  qredeu  16359  coprmprod  16362  coprmproddvdslem  16363  coprmproddvds  16364  cncongr1  16368  cncongr2  16369  1idssfct  16381  isprm2lem  16382  isprm3  16384  prmind2  16386  ge2nprmge4  16402  divgcdodd  16411  isprm6  16415  ncoprmlnprm  16428  divnumden  16448  divdenle  16449  nn0gcdsq  16452  phicl2  16465  phiprmpw  16473  eulerthlem2  16479  hashgcdlem  16485  hashgcdeq  16486  phisum  16487  nnoddn2prm  16508  pythagtriplem3  16515  pythagtriplem4  16516  pythagtriplem6  16518  pythagtriplem7  16519  pythagtriplem8  16520  pythagtriplem9  16521  pythagtriplem11  16522  pythagtriplem13  16524  pythagtriplem15  16526  pythagtriplem19  16530  pythagtrip  16531  iserodd  16532  pclem  16535  pccl  16546  pcdiv  16549  pcqcl  16553  pcdvds  16561  pcndvds  16563  pcndvds2  16565  pcelnn  16567  pcz  16578  pcmpt  16589  fldivp1  16594  pcfac  16596  infpnlem1  16607  prmunb  16611  prmreclem1  16613  1arith  16624  ram0  16719  prmdvdsprmo  16739  prmgaplem4  16751  prmgaplem6  16753  prmgaplem7  16754  cshwshashlem2  16794  setsstruct2  16871  mulgnn  18704  mulgaddcom  18723  mulginvcom  18724  mulgmodid  18738  ghmmulg  18842  dfod2  19167  gexdvds  19185  gexnnod  19189  gexex  19450  mulgass2  19836  qsssubdrg  20653  prmirredlem  20690  znidomb  20765  znrrg  20769  chfacfisf  21999  chfacfisfcpmat  22000  chfacfscmul0  22003  chfacfpmmul0  22007  cayhamlem1  22011  cpmadugsumlemF  22021  lmmo  22527  1stckgenlem  22700  imasdsf1olem  23522  clmmulg  24260  cmetcaulem  24448  ovolunlem1a  24656  ovolicc2lem4  24680  mbfi1fseqlem6  24881  dvexp3  25138  dgreq0  25422  elqaalem2  25476  aaliou3lem1  25498  aaliou3lem2  25499  aaliou3lem3  25500  aaliou3lem9  25506  pserdvlem2  25583  logtayl2  25813  root1eq1  25904  root1cj  25905  logbgcd1irr  25940  atantayl2  26084  birthdaylem2  26098  birthdaylem3  26099  emcllem5  26145  basellem2  26227  basellem3  26228  basellem5  26230  issqf  26281  sgmnncl  26292  prmorcht  26323  mumullem1  26324  mumullem2  26325  sqff1o  26327  dvdsflsumcom  26333  muinv  26338  vmalelog  26349  chtublem  26355  vmasum  26360  logfac2  26361  logfaclbnd  26366  bclbnd  26424  bposlem5  26432  lgsval4a  26463  lgssq2  26482  lgsdchr  26499  gausslemma2dlem0c  26502  gausslemma2dlem0e  26504  gausslemma2dlem1a  26509  gausslemma2dlem5  26515  lgsquadlem1  26524  lgsquadlem2  26525  lgsquad3  26531  2lgslem1a1  26533  2lgslem3  26548  2lgsoddprm  26560  2sqnn  26583  2sqreunnltlem  26594  rplogsumlem1  26628  rplogsumlem2  26629  dchrisumlem2  26634  dchrmusumlema  26637  dchrmusum2  26638  dchrvmasumiflem1  26645  dchrvmaeq0  26648  dchrisum0flblem2  26653  dchrisum0re  26657  dchrisum0lema  26658  dchrisum0lem1b  26659  dchrisum0lem2a  26661  logdivbnd  26700  pntrsumbnd2  26711  ostth2lem1  26762  ostth2lem3  26779  ostth3  26782  axlowdimlem13  27318  crctcshwlkn0lem4  28172  crctcshwlkn0lem5  28173  crctcshwlkn0lem7  28175  wlkiswwlksupgr2  28236  clwwisshclwwslem  28372  clwwlkinwwlk  28398  clwwlkel  28404  clwwlkf  28405  wwlksubclwwlk  28416  clwwlkvbij  28471  eucrctshift  28601  eucrct2eupth  28603  numclwlk2lem2f  28735  bcm1n  31110  pnfinf  31431  isarchiofld  31510  rearchi  31540  submat1n  31749  lmatfvlem  31759  esumcvg  32048  oddpwdc  32315  fibp1  32362  chtvalz  32603  nnltp1ne  33063  erdszelem7  33153  climuzcnv  33623  elfzm12  33627  bcprod  33698  nn0prpwlem  34505  knoppndvlem1  34686  knoppndvlem2  34687  knoppndvlem7  34692  knoppndvlem18  34703  poimirlem13  35784  poimirlem14  35785  mblfinlem2  35809  fzmul  35893  incsequz  35900  geomcau  35911  heibor1lem  35961  bfplem2  35975  lcmfunnnd  40015  metakunt16  40135  metakunt26  40145  nn0rppwr  40328  nn0expgcd  40330  dvdsexpnn  40335  dvdsexpnn0  40336  zrtdvds  40341  fzsplit1nn0  40571  irrapxlem1  40639  pellexlem5  40650  rmynn  40773  jm2.24nn  40776  jm2.17c  40779  congrep  40790  congabseq  40791  acongrep  40797  acongeq  40800  jm2.18  40805  jm2.23  40813  jm2.20nn  40814  jm2.26lem3  40818  jm2.26  40819  jm2.15nn0  40820  jm2.16nn0  40821  jm2.27dlem2  40827  rmydioph  40831  jm3.1  40837  expdiophlem1  40838  expdioph  40840  idomodle  41016  proot1ex  41021  nznngen  41902  sumnnodd  43140  stoweidlem7  43517  stoweidlem17  43527  wallispilem4  43578  stirlinglem2  43585  stirlinglem3  43586  stirlinglem4  43587  stirlinglem12  43595  stirlinglem13  43596  stirlinglem14  43597  stirlinglem15  43598  stirlingr  43600  dirkertrigeqlem1  43608  fouriersw  43741  ovnsubaddlem1  44077  subsubelfzo0  44785  2ffzoeq  44787  iccpartres  44837  iccpartipre  44840  iccpartltu  44844  iccelpart  44852  odz2prm2pw  44982  fmtnoprmfac2lem1  44985  2pwp1prm  45008  lighneallem2  45025  lighneallem4  45029  lighneal  45030  proththd  45033  nneoALTV  45091  divgcdoddALTV  45101  fpprmod  45146  fppr2odd  45150  dfwppr  45157  fpprwppr  45158  fpprwpprb  45159  gbowge7  45182  gbege6  45184  altgsumbc  45655  altgsumbcALT  45656  pw2m1lepw2m1  45828  nnpw2even  45842  nnlog2ge0lt1  45879  logbpw2m1  45880  blenpw2m1  45892  nnpw2blenfzo  45894  nnpw2pmod  45896  nnpw2p  45899  blengt1fldiv2p1  45906  dignn0fr  45914  dignn0flhalflem1  45928  dignn0flhalflem2  45929  nn0sumshdiglemA  45932  nn0sumshdiglemB  45933