Theorem nnz 12607

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 12245	. 2 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
2		3mix2 1332	. 2 ⊢ (𝑁 ∈ ℕ → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
3		elz 12588	. 2 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
4	1, 2, 3	sylanbrc 583	1 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∨ w3o 1085   = wceq 1540   ∈ wcel 2108  ℝcr 11126  0cc0 11127  -cneg 11465  ℕcn 12238  ℤcz 12586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7727  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-i2m1 11195  ax-1ne0 11196  ax-rrecex 11199  ax-cnre 11200

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-ov 7406  df-om 7860  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-neg 11467  df-nn 12239  df-z 12587

This theorem is referenced by:  nnssz  12608  elnnz1  12616  znegcl  12625  nnleltp1  12646  nnltp1le  12647  nnlem1lt  12657  nnltlem1  12658  nnm1ge0  12659  prime  12672  nneo  12675  zeo  12677  btwnz  12694  eluz2b2  12935  qaddcl  12979  qreccl  12983  elpqb  12990  elfz1end  13569  fznatpl1  13593  fznn  13607  elfz1b  13608  elfzo0  13715  elfzo0z  13716  elfzo1  13727  fzo1fzo0n0  13729  elfzom1p1elfzo  13759  ubmelm1fzo  13777  quoremz  13870  intfracq  13874  fznnfl  13877  zmodcl  13906  zmodfz  13908  zmodfzo  13909  zmodid2  13914  zmodidfzo  13915  modfzo0difsn  13959  expnnval  14080  mulexpz  14118  nnesq  14243  expnlbnd  14249  expnlbnd2  14250  digit2  14252  faclbnd  14306  bc0k  14327  bcval5  14334  fz1isolem  14477  seqcoll  14480  ccatval21sw  14601  lswccatn0lsw  14607  cshwidxmod  14819  cshwidxn  14825  absexpz  15322  climuni  15566  isercoll  15682  climcnds  15865  arisum  15874  trireciplem  15876  expcnv  15878  pwdif  15882  geo2sum  15887  geo2lim  15889  0.999...  15895  geoihalfsum  15896  rpnnen2lem6  16235  rpnnen2lem9  16238  rpnnen2lem10  16239  dvdsval3  16274  nndivdvds  16279  modmulconst  16305  dvdsle  16327  dvdsssfz1  16335  fzm1ndvds  16339  dvdsfac  16343  mulmoddvds  16347  oexpneg  16362  nnoddm1d2  16403  pwp1fsum  16408  divalg2  16422  divalgmod  16423  modremain  16425  ndvdsadd  16427  nndvdslegcd  16522  divgcdz  16528  divgcdnn  16532  divgcdnnr  16533  modgcd  16549  gcdmultiple  16553  gcddiv  16568  gcdzeq  16569  gcdeq  16570  rpmulgcd  16574  rplpwr  16575  rprpwr  16576  nn0rppwr  16578  sqgcd  16579  nn0expgcd  16581  dvdssqlem  16583  dvdssq  16584  eucalginv  16601  lcmgcdlem  16623  lcmgcdnn  16628  lcmass  16631  lcmftp  16653  lcmfunsnlem2lem1  16655  coprmgcdb  16666  qredeq  16674  qredeu  16675  coprmprod  16678  coprmproddvdslem  16679  coprmproddvds  16680  cncongr1  16684  cncongr2  16685  1idssfct  16697  isprm2lem  16698  isprm3  16700  prmind2  16702  ge2nprmge4  16718  divgcdodd  16727  isprm6  16731  ncoprmlnprm  16745  divnumden  16765  divdenle  16766  nn0gcdsq  16769  phicl2  16785  phiprmpw  16793  eulerthlem2  16799  hashgcdlem  16805  hashgcdeq  16807  phisum  16808  nnoddn2prm  16829  pythagtriplem3  16836  pythagtriplem4  16837  pythagtriplem6  16839  pythagtriplem7  16840  pythagtriplem8  16841  pythagtriplem9  16842  pythagtriplem11  16843  pythagtriplem13  16845  pythagtriplem15  16847  pythagtriplem19  16851  pythagtrip  16852  iserodd  16853  pclem  16856  pccl  16867  pcdiv  16870  pcqcl  16874  pcdvds  16882  pcndvds  16884  pcndvds2  16886  pcelnn  16888  pcz  16899  pcmpt  16910  fldivp1  16915  pcfac  16917  infpnlem1  16928  prmunb  16932  prmreclem1  16934  1arith  16945  ram0  17040  prmdvdsprmo  17060  prmgaplem4  17072  prmgaplem6  17074  prmgaplem7  17075  cshwshashlem2  17114  setsstruct2  17191  mulgnn  19056  mulgaddcom  19079  mulginvcom  19080  mulgmodid  19094  ghmmulg  19209  dfod2  19543  gexdvds  19563  gexnnod  19567  gexex  19832  mulgass2  20267  qsssubdrg  21392  prmirredlem  21431  znidomb  21520  znrrg  21524  chfacfisf  22790  chfacfisfcpmat  22791  chfacfscmul0  22794  chfacfpmmul0  22798  cayhamlem1  22802  cpmadugsumlemF  22812  lmmo  23316  1stckgenlem  23489  imasdsf1olem  24310  clmmulg  25050  cmetcaulem  25238  ovolunlem1a  25447  ovolicc2lem4  25471  mbfi1fseqlem6  25671  dvexp3  25932  dgreq0  26221  elqaalem2  26278  aaliou3lem1  26300  aaliou3lem2  26301  aaliou3lem3  26302  aaliou3lem9  26308  pserdvlem2  26388  logtayl2  26621  root1eq1  26715  root1cj  26716  zrtdvds  26719  logbgcd1irr  26754  atantayl2  26898  birthdaylem2  26912  birthdaylem3  26913  emcllem5  26960  basellem2  27042  basellem3  27043  basellem5  27045  issqf  27096  sgmnncl  27107  prmorcht  27138  mumullem1  27139  mumullem2  27140  sqff1o  27142  dvdsflsumcom  27148  muinv  27153  vmalelog  27166  chtublem  27172  vmasum  27177  logfac2  27178  logfaclbnd  27183  bclbnd  27241  bposlem5  27249  lgsval4a  27280  lgssq2  27299  lgsdchr  27316  gausslemma2dlem0c  27319  gausslemma2dlem0e  27321  gausslemma2dlem1a  27326  gausslemma2dlem5  27332  lgsquadlem1  27341  lgsquadlem2  27342  lgsquad3  27348  2lgslem1a1  27350  2lgslem3  27365  2lgsoddprm  27377  2sqnn  27400  2sqreunnltlem  27411  rplogsumlem1  27445  rplogsumlem2  27446  dchrisumlem2  27451  dchrmusumlema  27454  dchrmusum2  27455  dchrvmasumiflem1  27462  dchrvmaeq0  27465  dchrisum0flblem2  27470  dchrisum0re  27474  dchrisum0lema  27475  dchrisum0lem1b  27476  dchrisum0lem2a  27478  logdivbnd  27517  pntrsumbnd2  27528  ostth2lem1  27579  ostth2lem3  27596  ostth3  27599  axlowdimlem13  28879  crctcshwlkn0lem4  29741  crctcshwlkn0lem5  29742  crctcshwlkn0lem7  29744  wlkiswwlksupgr2  29805  clwwisshclwwslem  29941  clwwlkinwwlk  29967  clwwlkel  29973  clwwlkf  29974  wwlksubclwwlk  29985  clwwlkvbij  30040  eucrctshift  30170  eucrct2eupth  30172  numclwlk2lem2f  30304  bcm1n  32718  pnfinf  33127  1fldgenq  33262  isarchiofld  33285  rearchi  33307  submat1n  33782  lmatfvlem  33792  esumcvg  34063  oddpwdc  34332  fibp1  34379  chtvalz  34607  nnltp1ne  35079  erdszelem7  35165  climuzcnv  35639  elfzm12  35643  bcprod  35701  nn0prpwlem  36286  knoppndvlem1  36476  knoppndvlem2  36477  knoppndvlem7  36482  knoppndvlem18  36493  poimirlem13  37603  poimirlem14  37604  mblfinlem2  37628  fzmul  37711  incsequz  37718  geomcau  37729  heibor1lem  37779  bfplem2  37793  lcmfunnnd  41971  posbezout  42059  unitscyglem4  42157  metakunt16  42179  metakunt26  42189  dvdsexpnn  42329  dvdsexpnn0  42330  fimgmcyc  42504  fzsplit1nn0  42724  irrapxlem1  42792  pellexlem5  42803  rmynn  42927  jm2.24nn  42930  jm2.17c  42933  congrep  42944  congabseq  42945  acongrep  42951  acongeq  42954  jm2.18  42959  jm2.23  42967  jm2.20nn  42968  jm2.26lem3  42972  jm2.26  42973  jm2.15nn0  42974  jm2.16nn0  42975  jm2.27dlem2  42981  rmydioph  42985  jm3.1  42991  expdiophlem1  42992  expdioph  42994  idomodle  43162  proot1ex  43167  nznngen  44288  sumnnodd  45607  stoweidlem7  45984  stoweidlem17  45994  wallispilem4  46045  stirlinglem2  46052  stirlinglem3  46053  stirlinglem4  46054  stirlinglem12  46062  stirlinglem13  46063  stirlinglem14  46064  stirlinglem15  46065  stirlingr  46067  dirkertrigeqlem1  46075  fouriersw  46208  ovnsubaddlem1  46547  subsubelfzo0  47303  2ffzoeq  47304  ceilhalfelfzo1  47307  2tceilhalfelfzo1  47309  difltmodne  47319  addmodne  47321  submodlt  47327  iccpartres  47380  iccpartipre  47383  iccpartltu  47387  iccelpart  47395  odz2prm2pw  47525  fmtnoprmfac2lem1  47528  2pwp1prm  47551  lighneallem2  47568  lighneallem4  47572  lighneal  47573  proththd  47576  nneoALTV  47634  divgcdoddALTV  47644  fpprmod  47689  fppr2odd  47693  dfwppr  47700  fpprwppr  47701  fpprwpprb  47702  gbowge7  47725  gbege6  47727  gpg3kgrtriexlem2  48034  gpg3kgrtriexlem3  48035  gpg3kgrtriexlem5  48037  gpg3kgrtriexlem6  48038  altgsumbc  48275  altgsumbcALT  48276  pw2m1lepw2m1  48444  nnpw2even  48457  nnlog2ge0lt1  48494  logbpw2m1  48495  blenpw2m1  48507  nnpw2blenfzo  48509  nnpw2pmod  48511  nnpw2p  48514  blengt1fldiv2p1  48521  dignn0fr  48529  dignn0flhalflem1  48543  dignn0flhalflem2  48544  nn0sumshdiglemA  48547  nn0sumshdiglemB  48548