Theorem nnz 12603

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 12231	. 2 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
2		3mix2 1348	. 2 ⊢ (𝑁 ∈ ℕ → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
3		elz 12584	. 2 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
4	1, 2, 3	sylanbrc 594	1 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∨ w3o 1100   = wceq 1563   ∈ wcel 2145  ℝcr 11087  0cc0 11088  -cneg 11430  ℕcn 12224  ℤcz 12582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395  ax-un 7722  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-i2m1 11156  ax-1ne0 11157  ax-rrecex 11160  ax-cnre 11161

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-ov 7403  df-om 7851  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-neg 11432  df-nn 12225  df-z 12583

This theorem is referenced by:  nnssz  12604  elnnz1  12611  znegcl  12620  nnleltp1  12642  nnltp1le  12643  nnlem1lt  12653  nnltlem1  12654  nnm1ge0  12655  prime  12668  nneo  12671  zeo  12673  btwnz  12690  eluz2b2  12936  qaddcl  12980  qreccl  12984  elpqb  12991  elfz1end  13573  fznatpl1  13597  fznn  13611  elfz1b  13612  elfzo0  13720  elfzo0z  13721  elfzo1  13732  fzo1fzo0n0  13735  elfzom1p1elfzo  13765  ubmelm1fzo  13783  quoremz  13879  intfracq  13883  fznnfl  13886  zmodcl  13915  zmodfz  13917  zmodfzo  13918  zmodid2  13923  zmodidfzo  13924  modfzo0difsn  13970  expnnval  14091  mulexpz  14129  nnesq  14254  expnlbnd  14260  expnlbnd2  14261  digit2  14263  faclbnd  14317  bc0k  14338  bcval5  14345  fz1isolem  14488  seqcoll  14491  ccatval21sw  14613  lswccatn0lsw  14619  cshwidxmod  14830  cshwidxn  14836  absexpz  15346  climuni  15593  isercoll  15709  climcnds  15895  arisum  15904  trireciplem  15906  expcnv  15908  pwdif  15912  geo2sum  15917  geo2lim  15919  0.999...  15925  geoihalfsum  15926  rpnnen2lem6  16265  rpnnen2lem9  16268  rpnnen2lem10  16269  dvdsval3  16304  nndivdvds  16309  modmulconst  16336  dvdsle  16358  dvdsssfz1  16366  fzm1ndvds  16370  dvdsfac  16374  mulmoddvds  16378  oexpneg  16393  nnoddm1d2  16434  pwp1fsum  16439  divalg2  16453  divalgmod  16454  modremain  16456  ndvdsadd  16458  nndvdslegcd  16553  divgcdz  16559  divgcdnn  16563  divgcdnnr  16564  modgcd  16580  gcdmultiple  16584  gcddiv  16599  gcdzeq  16600  gcdeq  16601  rpmulgcd  16605  rplpwr  16606  rprpwr  16607  nn0rppwr  16609  sqgcd  16610  nn0expgcd  16612  dvdssqlem  16614  dvdssq  16615  eucalginv  16632  lcmgcdlem  16654  lcmgcdnn  16659  lcmass  16662  lcmftp  16684  lcmfunsnlem2lem1  16686  coprmgcdb  16697  qredeq  16705  qredeu  16706  coprmprod  16709  coprmproddvdslem  16710  coprmproddvds  16711  cncongr1  16715  cncongr2  16716  1idssfct  16728  isprm2lem  16729  isprm3  16731  prmind2  16733  ge2nprmge4  16750  divgcdodd  16759  isprm6  16763  ncoprmlnprm  16777  divnumden  16797  divdenle  16798  nn0gcdsq  16801  phicl2  16817  phiprmpw  16825  eulerthlem2  16831  hashgcdlem  16837  hashgcdeq  16839  phisum  16840  nnoddn2prm  16861  pythagtriplem3  16868  pythagtriplem4  16869  pythagtriplem6  16871  pythagtriplem7  16872  pythagtriplem8  16873  pythagtriplem9  16874  pythagtriplem11  16875  pythagtriplem13  16877  pythagtriplem15  16879  pythagtriplem19  16883  pythagtrip  16884  iserodd  16885  pclem  16888  pccl  16899  pcdiv  16902  pcqcl  16906  pcdvds  16914  pcndvds  16916  pcndvds2  16918  pcelnn  16920  pcz  16931  pcmpt  16942  fldivp1  16947  pcfac  16949  infpnlem1  16960  prmunb  16964  prmreclem1  16966  1arith  16977  ram0  17072  prmdvdsprmo  17092  prmgaplem4  17104  prmgaplem6  17106  prmgaplem7  17107  cshwshashlem2  17146  setsstruct2  17224  mulgnn  19132  mulgaddcom  19155  mulginvcom  19156  mulgmodid  19170  ghmmulg  19289  dfod2  19625  gexdvds  19645  gexnnod  19649  gexex  19914  mulgass2  20383  qsssubdrg  21536  prmirredlem  21582  znidomb  21671  znrrg  21675  chfacfisf  22972  chfacfisfcpmat  22973  chfacfscmul0  22976  chfacfpmmul0  22980  cayhamlem1  22984  cpmadugsumlemF  22994  lmmo  23498  1stckgenlem  23671  imasdsf1olem  24491  clmmulg  25221  cmetcaulem  25408  ovolunlem1a  25616  ovolicc2lem4  25640  mbfi1fseqlem6  25840  dvexp3  26098  dgreq0  26383  elqaalem2  26442  aaliou3lem1  26464  aaliou3lem2  26465  aaliou3lem3  26466  aaliou3lem9  26472  pserdvlem2  26549  logtayl2  26785  root1eq1  26878  root1cj  26879  zrtdvds  26882  logbgcd1irr  26917  atantayl2  27061  birthdaylem2  27075  birthdaylem3  27076  emcllem5  27122  basellem2  27204  basellem3  27205  basellem5  27207  issqf  27258  sgmnncl  27269  prmorcht  27300  mumullem1  27301  mumullem2  27302  sqff1o  27304  dvdsflsumcom  27310  muinv  27315  vmalelog  27327  chtublem  27333  vmasum  27338  logfac2  27339  logfaclbnd  27344  bclbnd  27402  bposlem5  27410  lgsval4a  27441  lgssq2  27460  lgsdchr  27477  gausslemma2dlem0c  27480  gausslemma2dlem0e  27482  gausslemma2dlem1a  27487  gausslemma2dlem5  27493  lgsquadlem1  27502  lgsquadlem2  27503  lgsquad3  27509  2lgslem1a1  27511  2lgslem3  27526  2lgsoddprm  27538  2sqnn  27561  2sqreunnltlem  27572  rplogsumlem1  27606  rplogsumlem2  27607  dchrisumlem2  27612  dchrmusumlema  27615  dchrmusum2  27616  dchrvmasumiflem1  27623  dchrvmaeq0  27626  dchrisum0flblem2  27631  dchrisum0re  27635  dchrisum0lema  27636  dchrisum0lem1b  27637  dchrisum0lem2a  27639  logdivbnd  27678  pntrsumbnd2  27689  ostth2lem1  27740  ostth2lem3  27757  ostth3  27760  axlowdimlem13  29213  crctcshwlkn0lem4  30071  crctcshwlkn0lem5  30072  crctcshwlkn0lem7  30074  wlkiswwlksupgr2  30135  clwwisshclwwslem  30274  clwwlkinwwlk  30300  clwwlkel  30306  clwwlkf  30307  wwlksubclwwlk  30318  clwwlkvbij  30373  eucrctshift  30503  eucrct2eupth  30505  numclwlk2lem2f  30637  bcm1n  33052  pnfinf  33416  isarchiofld  33432  1fldgenq  33558  rearchi  33581  submat1n  34112  lmatfvlem  34122  esumcvg  34393  oddpwdc  34661  fibp1  34708  chtvalz  34933  nnltp1ne  35473  erdszelem7  35560  climuzcnv  36034  elfzm12  36038  bcprod  36101  nn0prpwlem  36695  knoppndvlem1  36963  knoppndvlem2  36964  knoppndvlem7  36969  knoppndvlem18  36980  poimirlem13  38144  poimirlem14  38145  mblfinlem2  38169  fzmul  38252  incsequz  38259  geomcau  38270  heibor1lem  38320  bfplem2  38334  lcmfunnnd  42641  posbezout  42729  unitscyglem4  42827  dvdsexpnn  42954  dvdsexpnn0  42955  fimgmcyc  43164  fzsplit1nn0  43347  irrapxlem1  43411  pellexlem5  43422  rmynn  43545  jm2.24nn  43548  jm2.17c  43551  congrep  43562  congabseq  43563  acongrep  43569  acongeq  43572  jm2.18  43577  jm2.23  43585  jm2.20nn  43586  jm2.26lem3  43590  jm2.26  43591  jm2.15nn0  43592  jm2.16nn0  43593  jm2.27dlem2  43599  rmydioph  43603  jm3.1  43609  expdiophlem1  43610  expdioph  43612  idomodle  43780  proot1ex  43785  nznngen  44890  sumnnodd  46204  stoweidlem7  46579  stoweidlem17  46589  wallispilem4  46640  stirlinglem2  46647  stirlinglem3  46648  stirlinglem4  46649  stirlinglem12  46657  stirlinglem13  46658  stirlinglem14  46659  stirlinglem15  46660  stirlingr  46662  dirkertrigeqlem1  46670  fouriersw  46803  ovnsubaddlem1  47142  nthrucw  47460  subsubelfzo0  47919  2ffzoeq  47920  nnmul2  47922  ceilhalfelfzo1  47926  2tceilhalfelfzo1  47928  difltmodne  47940  addmodne  47942  submodlt  47948  facnn0dvdsfac  47977  muldvdsfacgt  47978  iccpartres  48022  iccpartipre  48025  iccpartltu  48029  iccelpart  48037  odz2prm2pw  48170  fmtnoprmfac2lem1  48173  2pwp1prm  48196  lighneallem2  48213  lighneallem4  48217  lighneal  48218  proththd  48221  nneoALTV  48292  divgcdoddALTV  48302  fpprmod  48347  fppr2odd  48351  dfwppr  48358  fpprwppr  48359  fpprwpprb  48360  gbowge7  48383  gbege6  48385  gpg3kgrtriexlem2  48704  gpg3kgrtriexlem3  48705  gpg3kgrtriexlem5  48707  gpg3kgrtriexlem6  48708  altgsumbc  48983  altgsumbcALT  48984  pw2m1lepw2m1  49151  nnpw2even  49160  nnlog2ge0lt1  49197  logbpw2m1  49198  blenpw2m1  49210  nnpw2blenfzo  49212  nnpw2pmod  49214  nnpw2p  49217  blengt1fldiv2p1  49224  dignn0fr  49232  dignn0flhalflem1  49246  dignn0flhalflem2  49247  nn0sumshdiglemA  49250  nn0sumshdiglemB  49251