Theorem nnz 11276

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 11274	. 2 ⊢ ℕ ⊆ ℤ
2	1	sseli 3564	1 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 1977  ℕcn 10897  ℤcz 11254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-z 11255

This theorem is referenced by:  elnnz1  11280  znegcl  11289  nnleltp1  11309  nnltp1le  11310  nnlem1lt  11319  nnltlem1  11320  nnm1ge0  11321  prime  11334  nneo  11337  zeo  11339  btwnz  11355  eluz2b2  11637  qaddcl  11680  qreccl  11684  elfz1end  12242  fznatpl1  12265  fznn  12278  elfz1b  12279  elfzo0  12376  elfzo0z  12377  elfzo1  12385  fzo1fzo0n0  12386  ubmelm1fzo  12430  quoremz  12516  intfracq  12520  fznnfl  12523  zmodcl  12552  zmodfz  12554  zmodfzo  12555  zmodid2  12560  zmodidfzo  12561  modfzo0difsn  12604  expnnval  12725  mulexpz  12762  nnesq  12850  expnlbnd  12856  expnlbnd2  12857  digit2  12859  faclbnd  12939  bc0k  12960  bcval5  12967  fz1isolem  13102  seqcoll  13105  lswccatn0lsw  13226  cshwidxmod  13400  cshwidxn  13406  absexpz  13893  climuni  14131  isercoll  14246  climcnds  14422  arisum  14431  trireciplem  14433  expcnv  14435  geo2sum  14443  geo2lim  14445  0.999...  14451  0.999...OLD  14452  geoihalfsum  14453  rpnnen2lem6  14787  rpnnen2lem9  14790  rpnnen2lem10  14791  dvdsval3  14825  nndivdvds  14827  modmulconst  14851  dvdsle  14870  dvdsssfz1  14878  fzm1ndvds  14882  dvdsfac  14886  oexpneg  14907  nnoddm1d2  14940  pwp1fsum  14952  divalg2  14966  divalgmod  14967  divalgmodOLD  14968  modremain  14970  ndvdsadd  14972  nndvdslegcd  15065  divgcdz  15071  divgcdnn  15074  divgcdnnr  15075  modgcd  15091  gcddiv  15106  gcdmultiple  15107  gcdmultiplez  15108  gcdzeq  15109  gcdeq  15110  rpmulgcd  15113  rplpwr  15114  rppwr  15115  sqgcd  15116  dvdssqlem  15117  dvdssq  15118  eucalginv  15135  lcmgcdlem  15157  lcmgcdnn  15162  lcmass  15165  lcmftp  15187  lcmfunsnlem2lem1  15189  coprmgcdb  15200  qredeq  15209  qredeu  15210  coprmprod  15213  coprmproddvdslem  15214  coprmproddvds  15215  cncongr1  15219  cncongr2  15220  1idssfct  15231  isprm3  15234  prmind2  15236  divgcdodd  15260  isprm6  15264  ncoprmlnprm  15274  divnumden  15294  divdenle  15295  nn0gcdsq  15298  phicl2  15311  phiprmpw  15319  eulerthlem2  15325  hashgcdlem  15331  hashgcdeq  15332  phisum  15333  nnoddn2prm  15354  pythagtriplem3  15361  pythagtriplem4  15362  pythagtriplem6  15364  pythagtriplem7  15365  pythagtriplem8  15366  pythagtriplem9  15367  pythagtriplem11  15368  pythagtriplem13  15370  pythagtriplem15  15372  pythagtriplem19  15376  pythagtrip  15377  iserodd  15378  pclem  15381  pccl  15392  pcdiv  15395  pcqcl  15399  pcdvds  15406  pcndvds  15408  pcndvds2  15410  pcelnn  15412  pcz  15423  pcmpt  15434  fldivp1  15439  pcfac  15441  infpnlem1  15452  prmunb  15456  prmreclem1  15458  1arith  15469  ram0  15564  prmdvdsprmo  15584  prmgaplem4  15596  prmgaplem6  15598  prmgaplem7  15599  cshwshashlem2  15641  setsstruct  15727  mulgnn  17370  mulgaddcom  17387  mulginvcom  17388  mulgmodid  17404  ghmmulg  17495  dfod2  17804  gexdvds  17822  gexnnod  17826  gexex  18079  mulgass2  18424  qsssubdrg  19624  prmirredlem  19660  znidomb  19729  znrrg  19733  chfacfisf  20478  chfacfisfcpmat  20479  chfacfscmul0  20482  chfacfpmmul0  20486  cayhamlem1  20490  cpmadugsumlemF  20500  lmmo  20994  1stckgenlem  21166  imasdsf1olem  21988  clmmulg  22709  cmetcaulem  22894  ovolunlem1a  23071  ovolicc2lem4  23095  mbfi1fseqlem6  23293  dvexp3  23545  dgreq0  23825  elqaalem2  23879  aaliou3lem1  23901  aaliou3lem2  23902  aaliou3lem3  23903  aaliou3lem9  23909  pserdvlem2  23986  logtayl2  24208  root1eq1  24296  root1cj  24297  atantayl2  24465  birthdaylem2  24479  birthdaylem3  24480  emcllem5  24526  basellem2  24608  basellem3  24609  basellem5  24611  issqf  24662  sgmnncl  24673  prmorcht  24704  mumullem1  24705  mumullem2  24706  sqff1o  24708  dvdsflsumcom  24714  muinv  24719  vmalelog  24730  chtublem  24736  vmasum  24741  logfac2  24742  logfaclbnd  24747  bclbnd  24805  bposlem5  24813  lgsval4a  24844  lgssq2  24863  lgsdchr  24880  gausslemma2dlem0c  24883  gausslemma2dlem0e  24885  gausslemma2dlem1a  24890  gausslemma2dlem5  24896  lgsquadlem1  24905  lgsquadlem2  24906  lgsquad3  24912  2lgslem1a1  24914  2lgslem3  24929  2lgsoddprm  24941  rplogsumlem1  24973  rplogsumlem2  24974  dchrisumlem2  24979  dchrmusumlema  24982  dchrmusum2  24983  dchrvmasumiflem1  24990  dchrvmaeq0  24993  dchrisum0flblem2  24998  dchrisum0re  25002  dchrisum0lema  25003  dchrisum0lem1b  25004  dchrisum0lem2a  25006  logdivbnd  25045  pntrsumbnd2  25056  ostth2lem1  25107  ostth2lem3  25124  ostth3  25127  axlowdimlem13  25634  clwwlkel  26321  clwwlkf  26322  clwwlkvbij  26329  wwlksubclwwlk  26332  clwwisshclwwlem  26334  clwwisshclww  26335  numclwlk2lem2f  26630  bcm1n  28941  pnfinf  29068  isarchiofld  29148  rearchi  29173  submat1n  29199  lmatfvlem  29209  esumcvg  29475  oddpwdc  29743  fibp1  29790  erdszelem7  30433  climuzcnv  30819  elfzm12  30823  bcprod  30877  nn0prpwlem  31487  knoppndvlem1  31673  knoppndvlem2  31674  knoppndvlem7  31679  knoppndvlem18  31690  poimirlem13  32592  poimirlem14  32593  mblfinlem2  32617  fzmul  32707  incsequz  32714  geomcau  32725  heibor1lem  32778  bfplem2  32792  fzsplit1nn0  36335  irrapxlem1  36404  pellexlem5  36415  rmynn  36541  jm2.24nn  36544  jm2.17c  36547  congrep  36558  congabseq  36559  acongrep  36565  acongeq  36568  jm2.18  36573  jm2.23  36581  jm2.20nn  36582  jm2.26lem3  36586  jm2.26  36587  jm2.15nn0  36588  jm2.16nn0  36589  jm2.27dlem2  36595  rmydioph  36599  jm3.1  36605  expdiophlem1  36606  expdioph  36608  idomodle  36793  proot1ex  36798  nznngen  37537  sumnnodd  38697  stoweidlem7  38900  stoweidlem17  38910  wallispilem4  38961  stirlinglem2  38968  stirlinglem3  38969  stirlinglem4  38970  stirlinglem12  38978  stirlinglem13  38979  stirlinglem14  38980  stirlinglem15  38981  stirlingr  38983  dirkertrigeqlem1  38991  fouriersw  39124  ovnsubaddlem1  39460  iccpartres  39956  iccpartipre  39959  iccpartltu  39963  iccelpart  39971  odz2prm2pw  40013  fmtnoprmfac2lem1  40016  pwdif  40039  2pwp1prm  40041  lighneallem2  40061  lighneallem4  40065  lighneal  40066  proththd  40069  nneoALTV  40121  divgcdoddALTV  40131  gboge7  40185  gbege6  40187  subsubelfzo0  40359  2ffzoeq  40361  crctcsh1wlkn0lem4  41016  crctcsh1wlkn0lem5  41017  crctcsh1wlkn0lem7  41019  1wlkiswwlksupgr2  41074  clwwlksel  41221  clwwlksf  41222  clwwlksvbij  41229  wwlksubclwwlks  41232  clwwisshclwwslem  41234  eucrctshift  41411  eucrct2eupth  41413  av-numclwlk2lem2f  41533  altgsumbc  41923  altgsumbcALT  41924  pw2m1lepw2m1  42104  nnpw2even  42117  nnlog2ge0lt1  42158  logbpw2m1  42159  blenpw2m1  42171  nnpw2blenfzo  42173  nnpw2pmod  42175  nnpw2p  42178  blengt1fldiv2p1  42185  dignn0fr  42193  dignn0flhalflem1  42207  dignn0flhalflem2  42208  nn0sumshdiglemA  42211  nn0sumshdiglemB  42212