Theorem nnz 12536

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 12172	. 2 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
2		3mix2 1333	. 2 ⊢ (𝑁 ∈ ℕ → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
3		elz 12517	. 2 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
4	1, 2, 3	sylanbrc 584	1 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∨ w3o 1086   = wceq 1542   ∈ wcel 2114  ℝcr 11028  0cc0 11029  -cneg 11369  ℕcn 12165  ℤcz 12515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-i2m1 11097  ax-1ne0 11098  ax-rrecex 11101  ax-cnre 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7363  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-neg 11371  df-nn 12166  df-z 12516

This theorem is referenced by:  nnssz  12537  elnnz1  12544  znegcl  12553  nnleltp1  12575  nnltp1le  12576  nnlem1lt  12586  nnltlem1  12587  nnm1ge0  12588  prime  12601  nneo  12604  zeo  12606  btwnz  12623  eluz2b2  12862  qaddcl  12906  qreccl  12910  elpqb  12917  elfz1end  13499  fznatpl1  13523  fznn  13537  elfz1b  13538  elfzo0  13646  elfzo0z  13647  elfzo1  13658  fzo1fzo0n0  13661  elfzom1p1elfzo  13691  ubmelm1fzo  13709  quoremz  13805  intfracq  13809  fznnfl  13812  zmodcl  13841  zmodfz  13843  zmodfzo  13844  zmodid2  13849  zmodidfzo  13850  modfzo0difsn  13896  expnnval  14017  mulexpz  14055  nnesq  14180  expnlbnd  14186  expnlbnd2  14187  digit2  14189  faclbnd  14243  bc0k  14264  bcval5  14271  fz1isolem  14414  seqcoll  14417  ccatval21sw  14539  lswccatn0lsw  14545  cshwidxmod  14756  cshwidxn  14762  absexpz  15258  climuni  15505  isercoll  15621  climcnds  15807  arisum  15816  trireciplem  15818  expcnv  15820  pwdif  15824  geo2sum  15829  geo2lim  15831  0.999...  15837  geoihalfsum  15838  rpnnen2lem6  16177  rpnnen2lem9  16180  rpnnen2lem10  16181  dvdsval3  16216  nndivdvds  16221  modmulconst  16248  dvdsle  16270  dvdsssfz1  16278  fzm1ndvds  16282  dvdsfac  16286  mulmoddvds  16290  oexpneg  16305  nnoddm1d2  16346  pwp1fsum  16351  divalg2  16365  divalgmod  16366  modremain  16368  ndvdsadd  16370  nndvdslegcd  16465  divgcdz  16471  divgcdnn  16475  divgcdnnr  16476  modgcd  16492  gcdmultiple  16496  gcddiv  16511  gcdzeq  16512  gcdeq  16513  rpmulgcd  16517  rplpwr  16518  rprpwr  16519  nn0rppwr  16521  sqgcd  16522  nn0expgcd  16524  dvdssqlem  16526  dvdssq  16527  eucalginv  16544  lcmgcdlem  16566  lcmgcdnn  16571  lcmass  16574  lcmftp  16596  lcmfunsnlem2lem1  16598  coprmgcdb  16609  qredeq  16617  qredeu  16618  coprmprod  16621  coprmproddvdslem  16622  coprmproddvds  16623  cncongr1  16627  cncongr2  16628  1idssfct  16640  isprm2lem  16641  isprm3  16643  prmind2  16645  ge2nprmge4  16662  divgcdodd  16671  isprm6  16675  ncoprmlnprm  16689  divnumden  16709  divdenle  16710  nn0gcdsq  16713  phicl2  16729  phiprmpw  16737  eulerthlem2  16743  hashgcdlem  16749  hashgcdeq  16751  phisum  16752  nnoddn2prm  16773  pythagtriplem3  16780  pythagtriplem4  16781  pythagtriplem6  16783  pythagtriplem7  16784  pythagtriplem8  16785  pythagtriplem9  16786  pythagtriplem11  16787  pythagtriplem13  16789  pythagtriplem15  16791  pythagtriplem19  16795  pythagtrip  16796  iserodd  16797  pclem  16800  pccl  16811  pcdiv  16814  pcqcl  16818  pcdvds  16826  pcndvds  16828  pcndvds2  16830  pcelnn  16832  pcz  16843  pcmpt  16854  fldivp1  16859  pcfac  16861  infpnlem1  16872  prmunb  16876  prmreclem1  16878  1arith  16889  ram0  16984  prmdvdsprmo  17004  prmgaplem4  17016  prmgaplem6  17018  prmgaplem7  17019  cshwshashlem2  17058  setsstruct2  17135  mulgnn  19042  mulgaddcom  19065  mulginvcom  19066  mulgmodid  19080  ghmmulg  19194  dfod2  19530  gexdvds  19550  gexnnod  19554  gexex  19819  mulgass2  20281  qsssubdrg  21416  prmirredlem  21462  znidomb  21551  znrrg  21555  chfacfisf  22829  chfacfisfcpmat  22830  chfacfscmul0  22833  chfacfpmmul0  22837  cayhamlem1  22841  cpmadugsumlemF  22851  lmmo  23355  1stckgenlem  23528  imasdsf1olem  24348  clmmulg  25078  cmetcaulem  25265  ovolunlem1a  25473  ovolicc2lem4  25497  mbfi1fseqlem6  25697  dvexp3  25955  dgreq0  26240  elqaalem2  26297  aaliou3lem1  26319  aaliou3lem2  26320  aaliou3lem3  26321  aaliou3lem9  26327  pserdvlem2  26406  logtayl2  26639  root1eq1  26732  root1cj  26733  zrtdvds  26736  logbgcd1irr  26771  atantayl2  26915  birthdaylem2  26929  birthdaylem3  26930  emcllem5  26977  basellem2  27059  basellem3  27060  basellem5  27062  issqf  27113  sgmnncl  27124  prmorcht  27155  mumullem1  27156  mumullem2  27157  sqff1o  27159  dvdsflsumcom  27165  muinv  27170  vmalelog  27182  chtublem  27188  vmasum  27193  logfac2  27194  logfaclbnd  27199  bclbnd  27257  bposlem5  27265  lgsval4a  27296  lgssq2  27315  lgsdchr  27332  gausslemma2dlem0c  27335  gausslemma2dlem0e  27337  gausslemma2dlem1a  27342  gausslemma2dlem5  27348  lgsquadlem1  27357  lgsquadlem2  27358  lgsquad3  27364  2lgslem1a1  27366  2lgslem3  27381  2lgsoddprm  27393  2sqnn  27416  2sqreunnltlem  27427  rplogsumlem1  27461  rplogsumlem2  27462  dchrisumlem2  27467  dchrmusumlema  27470  dchrmusum2  27471  dchrvmasumiflem1  27478  dchrvmaeq0  27481  dchrisum0flblem2  27486  dchrisum0re  27490  dchrisum0lema  27491  dchrisum0lem1b  27492  dchrisum0lem2a  27494  logdivbnd  27533  pntrsumbnd2  27544  ostth2lem1  27595  ostth2lem3  27612  ostth3  27615  axlowdimlem13  29037  crctcshwlkn0lem4  29896  crctcshwlkn0lem5  29897  crctcshwlkn0lem7  29899  wlkiswwlksupgr2  29960  clwwisshclwwslem  30099  clwwlkinwwlk  30125  clwwlkel  30131  clwwlkf  30132  wwlksubclwwlk  30143  clwwlkvbij  30198  eucrctshift  30328  eucrct2eupth  30330  numclwlk2lem2f  30462  bcm1n  32883  pnfinf  33259  isarchiofld  33275  1fldgenq  33398  rearchi  33421  submat1n  33965  lmatfvlem  33975  esumcvg  34246  oddpwdc  34514  fibp1  34561  chtvalz  34789  nnltp1ne  35309  erdszelem7  35395  climuzcnv  35869  elfzm12  35873  bcprod  35936  nn0prpwlem  36520  knoppndvlem1  36788  knoppndvlem2  36789  knoppndvlem7  36794  knoppndvlem18  36805  poimirlem13  37968  poimirlem14  37969  mblfinlem2  37993  fzmul  38076  incsequz  38083  geomcau  38094  heibor1lem  38144  bfplem2  38158  lcmfunnnd  42465  posbezout  42553  unitscyglem4  42651  dvdsexpnn  42779  dvdsexpnn0  42780  fimgmcyc  42993  fzsplit1nn0  43200  irrapxlem1  43268  pellexlem5  43279  rmynn  43402  jm2.24nn  43405  jm2.17c  43408  congrep  43419  congabseq  43420  acongrep  43426  acongeq  43429  jm2.18  43434  jm2.23  43442  jm2.20nn  43443  jm2.26lem3  43447  jm2.26  43448  jm2.15nn0  43449  jm2.16nn0  43450  jm2.27dlem2  43456  rmydioph  43460  jm3.1  43466  expdiophlem1  43467  expdioph  43469  idomodle  43637  proot1ex  43642  nznngen  44761  sumnnodd  46078  stoweidlem7  46453  stoweidlem17  46463  wallispilem4  46514  stirlinglem2  46521  stirlinglem3  46522  stirlinglem4  46523  stirlinglem12  46531  stirlinglem13  46532  stirlinglem14  46533  stirlinglem15  46534  stirlingr  46536  dirkertrigeqlem1  46544  fouriersw  46677  ovnsubaddlem1  47016  nthrucw  47332  subsubelfzo0  47787  2ffzoeq  47788  nnmul2  47790  ceilhalfelfzo1  47794  2tceilhalfelfzo1  47796  difltmodne  47808  addmodne  47810  submodlt  47816  facnn0dvdsfac  47845  muldvdsfacgt  47846  iccpartres  47890  iccpartipre  47893  iccpartltu  47897  iccelpart  47905  odz2prm2pw  48038  fmtnoprmfac2lem1  48041  2pwp1prm  48064  lighneallem2  48081  lighneallem4  48085  lighneal  48086  proththd  48089  nneoALTV  48160  divgcdoddALTV  48170  fpprmod  48215  fppr2odd  48219  dfwppr  48226  fpprwppr  48227  fpprwpprb  48228  gbowge7  48251  gbege6  48253  gpg3kgrtriexlem2  48572  gpg3kgrtriexlem3  48573  gpg3kgrtriexlem5  48575  gpg3kgrtriexlem6  48576  altgsumbc  48840  altgsumbcALT  48841  pw2m1lepw2m1  49008  nnpw2even  49017  nnlog2ge0lt1  49054  logbpw2m1  49055  blenpw2m1  49067  nnpw2blenfzo  49069  nnpw2pmod  49071  nnpw2p  49074  blengt1fldiv2p1  49081  dignn0fr  49089  dignn0flhalflem1  49103  dignn0flhalflem2  49104  nn0sumshdiglemA  49107  nn0sumshdiglemB  49108