Theorem nnz 12521

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

Syntax hints:   → wi 4   ∨ w3o 1086   = wceq 1542   ∈ wcel 2114  ℝcr 11037  0cc0 11038  -cneg 11377  ℕcn 12157  ℤcz 12500

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 5243  ax-nul 5253  ax-pr 5379  ax-un 7690  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rrecex 11110  ax-cnre 11111

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 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-neg 11379  df-nn 12158  df-z 12501

This theorem is referenced by:  nnssz  12522  elnnz1  12529  znegcl  12538  nnleltp1  12559  nnltp1le  12560  nnlem1lt  12570  nnltlem1  12571  nnm1ge0  12572  prime  12585  nneo  12588  zeo  12590  btwnz  12607  eluz2b2  12846  qaddcl  12890  qreccl  12894  elpqb  12901  elfz1end  13482  fznatpl1  13506  fznn  13520  elfz1b  13521  elfzo0  13628  elfzo0z  13629  elfzo1  13640  fzo1fzo0n0  13643  elfzom1p1elfzo  13673  ubmelm1fzo  13691  quoremz  13787  intfracq  13791  fznnfl  13794  zmodcl  13823  zmodfz  13825  zmodfzo  13826  zmodid2  13831  zmodidfzo  13832  modfzo0difsn  13878  expnnval  13999  mulexpz  14037  nnesq  14162  expnlbnd  14168  expnlbnd2  14169  digit2  14171  faclbnd  14225  bc0k  14246  bcval5  14253  fz1isolem  14396  seqcoll  14399  ccatval21sw  14521  lswccatn0lsw  14527  cshwidxmod  14738  cshwidxn  14744  absexpz  15240  climuni  15487  isercoll  15603  climcnds  15786  arisum  15795  trireciplem  15797  expcnv  15799  pwdif  15803  geo2sum  15808  geo2lim  15810  0.999...  15816  geoihalfsum  15817  rpnnen2lem6  16156  rpnnen2lem9  16159  rpnnen2lem10  16160  dvdsval3  16195  nndivdvds  16200  modmulconst  16227  dvdsle  16249  dvdsssfz1  16257  fzm1ndvds  16261  dvdsfac  16265  mulmoddvds  16269  oexpneg  16284  nnoddm1d2  16325  pwp1fsum  16330  divalg2  16344  divalgmod  16345  modremain  16347  ndvdsadd  16349  nndvdslegcd  16444  divgcdz  16450  divgcdnn  16454  divgcdnnr  16455  modgcd  16471  gcdmultiple  16475  gcddiv  16490  gcdzeq  16491  gcdeq  16492  rpmulgcd  16496  rplpwr  16497  rprpwr  16498  nn0rppwr  16500  sqgcd  16501  nn0expgcd  16503  dvdssqlem  16505  dvdssq  16506  eucalginv  16523  lcmgcdlem  16545  lcmgcdnn  16550  lcmass  16553  lcmftp  16575  lcmfunsnlem2lem1  16577  coprmgcdb  16588  qredeq  16596  qredeu  16597  coprmprod  16600  coprmproddvdslem  16601  coprmproddvds  16602  cncongr1  16606  cncongr2  16607  1idssfct  16619  isprm2lem  16620  isprm3  16622  prmind2  16624  ge2nprmge4  16640  divgcdodd  16649  isprm6  16653  ncoprmlnprm  16667  divnumden  16687  divdenle  16688  nn0gcdsq  16691  phicl2  16707  phiprmpw  16715  eulerthlem2  16721  hashgcdlem  16727  hashgcdeq  16729  phisum  16730  nnoddn2prm  16751  pythagtriplem3  16758  pythagtriplem4  16759  pythagtriplem6  16761  pythagtriplem7  16762  pythagtriplem8  16763  pythagtriplem9  16764  pythagtriplem11  16765  pythagtriplem13  16767  pythagtriplem15  16769  pythagtriplem19  16773  pythagtrip  16774  iserodd  16775  pclem  16778  pccl  16789  pcdiv  16792  pcqcl  16796  pcdvds  16804  pcndvds  16806  pcndvds2  16808  pcelnn  16810  pcz  16821  pcmpt  16832  fldivp1  16837  pcfac  16839  infpnlem1  16850  prmunb  16854  prmreclem1  16856  1arith  16867  ram0  16962  prmdvdsprmo  16982  prmgaplem4  16994  prmgaplem6  16996  prmgaplem7  16997  cshwshashlem2  17036  setsstruct2  17113  mulgnn  19017  mulgaddcom  19040  mulginvcom  19041  mulgmodid  19055  ghmmulg  19169  dfod2  19505  gexdvds  19525  gexnnod  19529  gexex  19794  mulgass2  20256  qsssubdrg  21393  prmirredlem  21439  znidomb  21528  znrrg  21532  chfacfisf  22810  chfacfisfcpmat  22811  chfacfscmul0  22814  chfacfpmmul0  22818  cayhamlem1  22822  cpmadugsumlemF  22832  lmmo  23336  1stckgenlem  23509  imasdsf1olem  24329  clmmulg  25069  cmetcaulem  25256  ovolunlem1a  25465  ovolicc2lem4  25489  mbfi1fseqlem6  25689  dvexp3  25950  dgreq0  26239  elqaalem2  26296  aaliou3lem1  26318  aaliou3lem2  26319  aaliou3lem3  26320  aaliou3lem9  26326  pserdvlem2  26406  logtayl2  26639  root1eq1  26733  root1cj  26734  zrtdvds  26737  logbgcd1irr  26772  atantayl2  26916  birthdaylem2  26930  birthdaylem3  26931  emcllem5  26978  basellem2  27060  basellem3  27061  basellem5  27063  issqf  27114  sgmnncl  27125  prmorcht  27156  mumullem1  27157  mumullem2  27158  sqff1o  27160  dvdsflsumcom  27166  muinv  27171  vmalelog  27184  chtublem  27190  vmasum  27195  logfac2  27196  logfaclbnd  27201  bclbnd  27259  bposlem5  27267  lgsval4a  27298  lgssq2  27317  lgsdchr  27334  gausslemma2dlem0c  27337  gausslemma2dlem0e  27339  gausslemma2dlem1a  27344  gausslemma2dlem5  27350  lgsquadlem1  27359  lgsquadlem2  27360  lgsquad3  27366  2lgslem1a1  27368  2lgslem3  27383  2lgsoddprm  27395  2sqnn  27418  2sqreunnltlem  27429  rplogsumlem1  27463  rplogsumlem2  27464  dchrisumlem2  27469  dchrmusumlema  27472  dchrmusum2  27473  dchrvmasumiflem1  27480  dchrvmaeq0  27483  dchrisum0flblem2  27488  dchrisum0re  27492  dchrisum0lema  27493  dchrisum0lem1b  27494  dchrisum0lem2a  27496  logdivbnd  27535  pntrsumbnd2  27546  ostth2lem1  27597  ostth2lem3  27614  ostth3  27617  axlowdimlem13  29039  crctcshwlkn0lem4  29898  crctcshwlkn0lem5  29899  crctcshwlkn0lem7  29901  wlkiswwlksupgr2  29962  clwwisshclwwslem  30101  clwwlkinwwlk  30127  clwwlkel  30133  clwwlkf  30134  wwlksubclwwlk  30145  clwwlkvbij  30200  eucrctshift  30330  eucrct2eupth  30332  numclwlk2lem2f  30464  bcm1n  32885  pnfinf  33276  isarchiofld  33292  1fldgenq  33415  rearchi  33438  submat1n  33982  lmatfvlem  33992  esumcvg  34263  oddpwdc  34531  fibp1  34578  chtvalz  34806  nnltp1ne  35324  erdszelem7  35410  climuzcnv  35884  elfzm12  35888  bcprod  35951  nn0prpwlem  36535  knoppndvlem1  36731  knoppndvlem2  36732  knoppndvlem7  36737  knoppndvlem18  36748  poimirlem13  37878  poimirlem14  37879  mblfinlem2  37903  fzmul  37986  incsequz  37993  geomcau  38004  heibor1lem  38054  bfplem2  38068  lcmfunnnd  42376  posbezout  42464  unitscyglem4  42562  dvdsexpnn  42697  dvdsexpnn0  42698  fimgmcyc  42898  fzsplit1nn0  43105  irrapxlem1  43173  pellexlem5  43184  rmynn  43307  jm2.24nn  43310  jm2.17c  43313  congrep  43324  congabseq  43325  acongrep  43331  acongeq  43334  jm2.18  43339  jm2.23  43347  jm2.20nn  43348  jm2.26lem3  43352  jm2.26  43353  jm2.15nn0  43354  jm2.16nn0  43355  jm2.27dlem2  43361  rmydioph  43365  jm3.1  43371  expdiophlem1  43372  expdioph  43374  idomodle  43542  proot1ex  43547  nznngen  44666  sumnnodd  45984  stoweidlem7  46359  stoweidlem17  46369  wallispilem4  46420  stirlinglem2  46427  stirlinglem3  46428  stirlinglem4  46429  stirlinglem12  46437  stirlinglem13  46438  stirlinglem14  46439  stirlinglem15  46440  stirlingr  46442  dirkertrigeqlem1  46450  fouriersw  46583  ovnsubaddlem1  46922  nthrucw  47238  subsubelfzo0  47680  2ffzoeq  47681  ceilhalfelfzo1  47684  2tceilhalfelfzo1  47686  difltmodne  47696  addmodne  47698  submodlt  47704  iccpartres  47772  iccpartipre  47775  iccpartltu  47779  iccelpart  47787  odz2prm2pw  47917  fmtnoprmfac2lem1  47920  2pwp1prm  47943  lighneallem2  47960  lighneallem4  47964  lighneal  47965  proththd  47968  nneoALTV  48026  divgcdoddALTV  48036  fpprmod  48081  fppr2odd  48085  dfwppr  48092  fpprwppr  48093  fpprwpprb  48094  gbowge7  48117  gbege6  48119  gpg3kgrtriexlem2  48438  gpg3kgrtriexlem3  48439  gpg3kgrtriexlem5  48441  gpg3kgrtriexlem6  48442  altgsumbc  48706  altgsumbcALT  48707  pw2m1lepw2m1  48874  nnpw2even  48883  nnlog2ge0lt1  48920  logbpw2m1  48921  blenpw2m1  48933  nnpw2blenfzo  48935  nnpw2pmod  48937  nnpw2p  48940  blengt1fldiv2p1  48947  dignn0fr  48955  dignn0flhalflem1  48969  dignn0flhalflem2  48970  nn0sumshdiglemA  48973  nn0sumshdiglemB  48974