Theorem nnz 12695

Description: A positive integer is an integer. (Contributed by NM, 9-May-2004.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 29-Nov-2022.)

Assertion

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

Proof of Theorem nnz

Step	Hyp	Ref	Expression
1		nnre 12323	. 2 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
2		3mix2 1350	. 2 ⊢ (𝑁 ∈ ℕ → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
3		elz 12676	. 2 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
4	1, 2, 3	sylanbrc 595	1 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1102   = wceq 1570   ∈ wcel 2145  ℝcr 11180  0cc0 11181  -cneg 11523  ℕcn 12316  ℤcz 12674

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7740  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-addrcl 11242  ax-mulcl 11243  ax-mulrcl 11244  ax-i2m1 11249  ax-1ne0 11250  ax-rrecex 11253  ax-cnre 11254

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6297  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7415  df-om 7867  df-2nd 7991  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-neg 11525  df-nn 12317  df-z 12675

This theorem is used by:  nnssz  12696  elnnz1  12703  znegcl  12712  nnleltp1  12735  nnltp1le  12736  nnlem1lt  12746  nnltlem1  12747  nnm1ge0  12748  prime  12761  nneo  12764  zeo  12766  btwnz  12783  eluz2b2  13029  qaddcl  13074  qreccl  13078  elpqb  13085  elfz1end  13668  fznatpl1  13692  fznn  13706  elfz1b  13707  elfzo0  13815  elfzo0z  13816  elfzo1  13827  fzo1fzo0n0  13830  elfzom1p1elfzo  13860  ubmelm1fzo  13878  quoremz  13975  intfracq  13979  fznnfl  13982  zmodcl  14011  zmodfz  14013  zmodfzo  14014  zmodid2  14019  zmodidfzo  14020  modfzo0difsn  14066  expnnval  14187  mulexpz  14225  nnesq  14351  expnlbnd  14357  expnlbnd2  14358  digit2  14360  faclbnd  14414  bc0k  14435  bcval5  14442  fz1isolem  14586  seqcoll  14589  ccatval21sw  14711  lswccatn0lsw  14718  cshwidxmod  14934  cshwidxn  14940  absexpz  15452  climuni  15699  isercoll  15815  climcnds  16000  arisum  16009  trireciplem  16011  expcnv  16013  pwdif  16017  geo2sum  16022  geo2lim  16024  0.999...  16030  geoihalfsum  16031  rpnnen2lem6  16367  rpnnen2lem9  16370  rpnnen2lem10  16371  dvdsval3  16406  nndivdvds  16411  modmulconst  16438  dvdsle  16460  dvdsssfz1  16468  fzm1ndvds  16472  dvdsfac  16476  mulmoddvds  16480  oexpneg  16495  nnoddm1d2  16536  pwp1fsum  16541  divalg2  16555  divalgmod  16556  modremain  16558  ndvdsadd  16560  nndvdslegcd  16655  divgcdz  16663  divgcdnn  16667  divgcdnnr  16668  modgcd  16685  gcdmultiple  16689  gcddiv  16704  gcdzeq  16705  gcdeq  16706  rpmulgcd  16711  rplpwr  16712  rprpwr  16713  nn0rppwr  16715  sqgcd  16716  nn0expgcd  16718  dvdsexpnn  16720  dvdssq  16722  eucalginv  16739  lcmgcdlem  16761  lcmgcdnn  16766  lcmass  16769  lcmftp  16791  lcmfunsnlem2lem1  16793  coprmgcdb  16804  qredeq  16812  qredeu  16813  coprmprod  16816  coprmproddvdslem  16817  coprmproddvds  16818  cncongr1  16822  cncongr2  16823  1idssfct  16835  isprm2lem  16836  isprm3  16838  prmind2  16840  ge2nprmge4  16857  divgcdodd  16866  isprm6  16870  ncoprmlnprm  16884  divnumden  16904  divdenle  16905  nn0gcdsq  16908  phicl2  16925  phiprmpw  16933  eulerthlem2  16939  hashgcdlem  16945  hashgcdeq  16947  phisum  16948  nnoddn2prm  16969  pythagtriplem3  16976  pythagtriplem4  16977  pythagtriplem6  16979  pythagtriplem7  16980  pythagtriplem8  16981  pythagtriplem9  16982  pythagtriplem11  16983  pythagtriplem13  16985  pythagtriplem15  16987  pythagtriplem19  16991  pythagtrip  16992  iserodd  16993  pclem  16996  pccl  17007  pcdiv  17010  pcqcl  17014  pcdvds  17022  pcndvds  17024  pcndvds2  17026  pcelnn  17028  pcz  17039  pcmpt  17050  fldivp1  17055  pcfac  17057  infpnlem1  17068  prmunb  17072  prmreclem1  17074  1arith  17085  ram0  17180  prmdvdsprmo  17200  prmgaplem4  17212  prmgaplem6  17214  prmgaplem7  17215  cshwshashlem2  17254  setsstruct2  17332  mulgnn  19265  mulgaddcom  19288  mulginvcom  19289  mulgmodid  19303  ghmmulg  19422  dfod2  19758  gexdvds  19778  gexnnod  19782  gexex  20047  mulgass2  20520  qsssubdrg  21712  prmirredlem  21758  znidomb  21847  znrrg  21851  chfacfisf  23152  chfacfisfcpmat  23153  chfacfscmul0  23156  chfacfpmmul0  23160  cayhamlem1  23164  cpmadugsumlemF  23174  lmmo  23678  1stckgenlem  23852  imasdsf1olem  24672  clmmulg  25402  cmetcaulem  25589  ovolunlem1a  25797  ovolicc2lem4  25821  mbfi1fseqlem6  26021  dvexp3  26278  dgreq0  26564  elqaalem2  26625  aaliou3lem1  26651  aaliou3lem2  26652  aaliou3lem3  26653  aaliou3lem9  26659  pserdvlem2  26737  logtayl2  26972  root1eq1  27065  root1cj  27066  zrtdvds  27069  logbgcd1irr  27104  atantayl2  27248  birthdaylem2  27262  birthdaylem3  27263  emcllem5  27309  basellem2  27391  basellem3  27392  basellem5  27394  issqf  27445  sgmnncl  27456  prmorcht  27487  mumullem1  27488  mumullem2  27489  sqff1o  27491  dvdsflsumcom  27497  muinv  27502  vmalelog  27514  chtublem  27520  vmasum  27525  logfac2  27526  logfaclbnd  27531  bclbnd  27589  bposlem5  27597  lgsval4a  27628  lgssq2  27647  lgsdchr  27664  gausslemma2dlem0c  27667  gausslemma2dlem0e  27669  gausslemma2dlem1a  27674  gausslemma2dlem5  27680  lgsquadlem1  27689  lgsquadlem2  27690  lgsquad3  27696  2lgslem1a1  27698  2lgslem3  27713  2lgsoddprm  27725  2sqnn  27748  2sqreunnltlem  27759  rplogsumlem1  27793  rplogsumlem2  27794  dchrisumlem2  27799  dchrmusumlema  27802  dchrmusum2  27803  dchrvmasumiflem1  27810  dchrvmaeq0  27813  dchrisum0flblem2  27818  dchrisum0re  27822  dchrisum0lema  27823  dchrisum0lem1b  27824  dchrisum0lem2a  27826  logdivbnd  27865  pntrsumbnd2  27876  ostth2lem1  27927  ostth2lem3  27944  ostth3  27947  axlowdimlem13  29514  crctcshwlkn0lem4  30384  crctcshwlkn0lem5  30385  crctcshwlkn0lem7  30387  wlkiswwlksupgr2  30448  clwwisshclwwslem  30587  clwwlkinwwlk  30613  clwwlkel  30619  clwwlkf  30620  wwlksubclwwlk  30631  clwwlkvbij  30686  eucrctshift  30826  eucrct2eupth  30828  numclwlk2lem2f  30960  bcm1n  33369  pnfinf  33726  isarchiofld  33742  1fldgenq  33866  rearchi  33889  submat1n  34419  lmatfvlem  34429  esumcvg  34700  oddpwdc  34969  fibp1  35016  chtvalz  35241  nnltp1ne  35870  erdszelem7  35931  climuzcnv  36405  elfzm12  36409  bcprod  36472  nn0prpwlem  37080  knoppndvlem1  37348  knoppndvlem2  37349  knoppndvlem7  37354  knoppndvlem18  37365  poimirlem13  38519  poimirlem14  38520  mblfinlem2  38544  fzmul  38643  incsequz  38650  geomcau  38661  heibor1lem  38711  bfplem2  38725  lcmfunnnd  43030  posbezout  43118  unitscyglem4  43216  dvdsexpnn0  43354  fimgmcyc  43560  fzsplit1nn0  43718  irrapxlem1  43782  pellexlem5  43793  rmynn  43916  jm2.24nn  43919  jm2.17c  43922  congrep  43933  congabseq  43934  acongrep  43940  acongeq  43943  jm2.18  43948  jm2.23  43956  jm2.20nn  43957  jm2.26lem3  43961  jm2.26  43962  jm2.15nn0  43963  jm2.16nn0  43964  jm2.27dlem2  43970  rmydioph  43974  jm3.1  43980  expdiophlem1  43981  expdioph  43983  idomodle  44151  proot1ex  44156  nznngen  45259  sumnnodd  46586  stoweidlem7  46961  stoweidlem17  46971  wallispilem4  47022  stirlinglem2  47029  stirlinglem3  47030  stirlinglem4  47031  stirlinglem12  47039  stirlinglem13  47040  stirlinglem14  47041  stirlinglem15  47042  stirlingr  47044  dirkertrigeqlem1  47052  fouriersw  47185  ovnsubaddlem1  47524  sqrtnnaa  47857  subsubelfzo0  48341  2ffzoeq  48342  nnmul2  48344  ceilhalfelfzo1  48348  2tceilhalfelfzo1  48350  difltmodne  48362  addmodne  48364  submodlt  48370  facnn0dvdsfac  48399  muldvdsfacgt  48400  iccpartres  48444  iccpartipre  48447  iccpartltu  48451  iccelpart  48459  odz2prm2pw  48592  fmtnoprmfac2lem1  48595  2pwp1prm  48618  lighneallem2  48635  lighneallem4  48639  lighneal  48640  proththd  48643  nneoALTV  48714  divgcdoddALTV  48724  fpprmod  48769  fppr2odd  48773  dfwppr  48780  fpprwppr  48781  fpprwpprb  48782  gbowge7  48805  gbege6  48807  gpg3kgrtriexlem2  49126  gpg3kgrtriexlem3  49127  gpg3kgrtriexlem5  49129  gpg3kgrtriexlem6  49130  altgsumbc  49408  altgsumbcALT  49409  pw2m1lepw2m1  49576  nnpw2even  49585  nnlog2ge0lt1  49622  logbpw2m1  49623  blenpw2m1  49635  nnpw2blenfzo  49637  nnpw2pmod  49639  nnpw2p  49642  blengt1fldiv2p1  49649  dignn0fr  49657  dignn0flhalflem1  49671  dignn0flhalflem2  49672  nn0sumshdiglemA  49675  nn0sumshdiglemB  49676