Theorem nnz 12486

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

Syntax hints:   → wi 4   ∨ w3o 1085   = wceq 1541   ∈ wcel 2111  ℝcr 11002  0cc0 11003  -cneg 11342  ℕcn 12122  ℤcz 12465

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370  ax-un 7668  ax-1cn 11061  ax-icn 11062  ax-addcl 11063  ax-addrcl 11064  ax-mulcl 11065  ax-mulrcl 11066  ax-i2m1 11071  ax-1ne0 11072  ax-rrecex 11075  ax-cnre 11076

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-iun 4943  df-br 5092  df-opab 5154  df-mpt 5173  df-tr 5199  df-id 5511  df-eprel 5516  df-po 5524  df-so 5525  df-fr 5569  df-we 5571  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-om 7797  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-neg 11344  df-nn 12123  df-z 12466

This theorem is referenced by:  nnssz  12487  elnnz1  12495  znegcl  12504  nnleltp1  12525  nnltp1le  12526  nnlem1lt  12536  nnltlem1  12537  nnm1ge0  12538  prime  12551  nneo  12554  zeo  12556  btwnz  12573  eluz2b2  12816  qaddcl  12860  qreccl  12864  elpqb  12871  elfz1end  13451  fznatpl1  13475  fznn  13489  elfz1b  13490  elfzo0  13597  elfzo0z  13598  elfzo1  13609  fzo1fzo0n0  13612  elfzom1p1elfzo  13642  ubmelm1fzo  13660  quoremz  13756  intfracq  13760  fznnfl  13763  zmodcl  13792  zmodfz  13794  zmodfzo  13795  zmodid2  13800  zmodidfzo  13801  modfzo0difsn  13847  expnnval  13968  mulexpz  14006  nnesq  14131  expnlbnd  14137  expnlbnd2  14138  digit2  14140  faclbnd  14194  bc0k  14215  bcval5  14222  fz1isolem  14365  seqcoll  14368  ccatval21sw  14490  lswccatn0lsw  14496  cshwidxmod  14707  cshwidxn  14713  absexpz  15209  climuni  15456  isercoll  15572  climcnds  15755  arisum  15764  trireciplem  15766  expcnv  15768  pwdif  15772  geo2sum  15777  geo2lim  15779  0.999...  15785  geoihalfsum  15786  rpnnen2lem6  16125  rpnnen2lem9  16128  rpnnen2lem10  16129  dvdsval3  16164  nndivdvds  16169  modmulconst  16196  dvdsle  16218  dvdsssfz1  16226  fzm1ndvds  16230  dvdsfac  16234  mulmoddvds  16238  oexpneg  16253  nnoddm1d2  16294  pwp1fsum  16299  divalg2  16313  divalgmod  16314  modremain  16316  ndvdsadd  16318  nndvdslegcd  16413  divgcdz  16419  divgcdnn  16423  divgcdnnr  16424  modgcd  16440  gcdmultiple  16444  gcddiv  16459  gcdzeq  16460  gcdeq  16461  rpmulgcd  16465  rplpwr  16466  rprpwr  16467  nn0rppwr  16469  sqgcd  16470  nn0expgcd  16472  dvdssqlem  16474  dvdssq  16475  eucalginv  16492  lcmgcdlem  16514  lcmgcdnn  16519  lcmass  16522  lcmftp  16544  lcmfunsnlem2lem1  16546  coprmgcdb  16557  qredeq  16565  qredeu  16566  coprmprod  16569  coprmproddvdslem  16570  coprmproddvds  16571  cncongr1  16575  cncongr2  16576  1idssfct  16588  isprm2lem  16589  isprm3  16591  prmind2  16593  ge2nprmge4  16609  divgcdodd  16618  isprm6  16622  ncoprmlnprm  16636  divnumden  16656  divdenle  16657  nn0gcdsq  16660  phicl2  16676  phiprmpw  16684  eulerthlem2  16690  hashgcdlem  16696  hashgcdeq  16698  phisum  16699  nnoddn2prm  16720  pythagtriplem3  16727  pythagtriplem4  16728  pythagtriplem6  16730  pythagtriplem7  16731  pythagtriplem8  16732  pythagtriplem9  16733  pythagtriplem11  16734  pythagtriplem13  16736  pythagtriplem15  16738  pythagtriplem19  16742  pythagtrip  16743  iserodd  16744  pclem  16747  pccl  16758  pcdiv  16761  pcqcl  16765  pcdvds  16773  pcndvds  16775  pcndvds2  16777  pcelnn  16779  pcz  16790  pcmpt  16801  fldivp1  16806  pcfac  16808  infpnlem1  16819  prmunb  16823  prmreclem1  16825  1arith  16836  ram0  16931  prmdvdsprmo  16951  prmgaplem4  16963  prmgaplem6  16965  prmgaplem7  16966  cshwshashlem2  17005  setsstruct2  17082  mulgnn  18985  mulgaddcom  19008  mulginvcom  19009  mulgmodid  19023  ghmmulg  19138  dfod2  19474  gexdvds  19494  gexnnod  19498  gexex  19763  mulgass2  20225  qsssubdrg  21361  prmirredlem  21407  znidomb  21496  znrrg  21500  chfacfisf  22767  chfacfisfcpmat  22768  chfacfscmul0  22771  chfacfpmmul0  22775  cayhamlem1  22779  cpmadugsumlemF  22789  lmmo  23293  1stckgenlem  23466  imasdsf1olem  24286  clmmulg  25026  cmetcaulem  25213  ovolunlem1a  25422  ovolicc2lem4  25446  mbfi1fseqlem6  25646  dvexp3  25907  dgreq0  26196  elqaalem2  26253  aaliou3lem1  26275  aaliou3lem2  26276  aaliou3lem3  26277  aaliou3lem9  26283  pserdvlem2  26363  logtayl2  26596  root1eq1  26690  root1cj  26691  zrtdvds  26694  logbgcd1irr  26729  atantayl2  26873  birthdaylem2  26887  birthdaylem3  26888  emcllem5  26935  basellem2  27017  basellem3  27018  basellem5  27020  issqf  27071  sgmnncl  27082  prmorcht  27113  mumullem1  27114  mumullem2  27115  sqff1o  27117  dvdsflsumcom  27123  muinv  27128  vmalelog  27141  chtublem  27147  vmasum  27152  logfac2  27153  logfaclbnd  27158  bclbnd  27216  bposlem5  27224  lgsval4a  27255  lgssq2  27274  lgsdchr  27291  gausslemma2dlem0c  27294  gausslemma2dlem0e  27296  gausslemma2dlem1a  27301  gausslemma2dlem5  27307  lgsquadlem1  27316  lgsquadlem2  27317  lgsquad3  27323  2lgslem1a1  27325  2lgslem3  27340  2lgsoddprm  27352  2sqnn  27375  2sqreunnltlem  27386  rplogsumlem1  27420  rplogsumlem2  27421  dchrisumlem2  27426  dchrmusumlema  27429  dchrmusum2  27430  dchrvmasumiflem1  27437  dchrvmaeq0  27440  dchrisum0flblem2  27445  dchrisum0re  27449  dchrisum0lema  27450  dchrisum0lem1b  27451  dchrisum0lem2a  27453  logdivbnd  27492  pntrsumbnd2  27503  ostth2lem1  27554  ostth2lem3  27571  ostth3  27574  axlowdimlem13  28930  crctcshwlkn0lem4  29789  crctcshwlkn0lem5  29790  crctcshwlkn0lem7  29792  wlkiswwlksupgr2  29853  clwwisshclwwslem  29989  clwwlkinwwlk  30015  clwwlkel  30021  clwwlkf  30022  wwlksubclwwlk  30033  clwwlkvbij  30088  eucrctshift  30218  eucrct2eupth  30220  numclwlk2lem2f  30352  bcm1n  32772  pnfinf  33147  isarchiofld  33163  1fldgenq  33283  rearchi  33306  submat1n  33813  lmatfvlem  33823  esumcvg  34094  oddpwdc  34362  fibp1  34409  chtvalz  34637  nnltp1ne  35143  erdszelem7  35229  climuzcnv  35703  elfzm12  35707  bcprod  35770  nn0prpwlem  36355  knoppndvlem1  36545  knoppndvlem2  36546  knoppndvlem7  36551  knoppndvlem18  36562  poimirlem13  37672  poimirlem14  37673  mblfinlem2  37697  fzmul  37780  incsequz  37787  geomcau  37798  heibor1lem  37848  bfplem2  37862  lcmfunnnd  42044  posbezout  42132  unitscyglem4  42230  dvdsexpnn  42365  dvdsexpnn0  42366  fimgmcyc  42566  fzsplit1nn0  42786  irrapxlem1  42854  pellexlem5  42865  rmynn  42988  jm2.24nn  42991  jm2.17c  42994  congrep  43005  congabseq  43006  acongrep  43012  acongeq  43015  jm2.18  43020  jm2.23  43028  jm2.20nn  43029  jm2.26lem3  43033  jm2.26  43034  jm2.15nn0  43035  jm2.16nn0  43036  jm2.27dlem2  43042  rmydioph  43046  jm3.1  43052  expdiophlem1  43053  expdioph  43055  idomodle  43223  proot1ex  43228  nznngen  44348  sumnnodd  45669  stoweidlem7  46044  stoweidlem17  46054  wallispilem4  46105  stirlinglem2  46112  stirlinglem3  46113  stirlinglem4  46114  stirlinglem12  46122  stirlinglem13  46123  stirlinglem14  46124  stirlinglem15  46125  stirlingr  46127  dirkertrigeqlem1  46135  fouriersw  46268  ovnsubaddlem1  46607  subsubelfzo0  47356  2ffzoeq  47357  ceilhalfelfzo1  47360  2tceilhalfelfzo1  47362  difltmodne  47372  addmodne  47374  submodlt  47380  iccpartres  47448  iccpartipre  47451  iccpartltu  47455  iccelpart  47463  odz2prm2pw  47593  fmtnoprmfac2lem1  47596  2pwp1prm  47619  lighneallem2  47636  lighneallem4  47640  lighneal  47641  proththd  47644  nneoALTV  47702  divgcdoddALTV  47712  fpprmod  47757  fppr2odd  47761  dfwppr  47768  fpprwppr  47769  fpprwpprb  47770  gbowge7  47793  gbege6  47795  gpg3kgrtriexlem2  48114  gpg3kgrtriexlem3  48115  gpg3kgrtriexlem5  48117  gpg3kgrtriexlem6  48118  altgsumbc  48382  altgsumbcALT  48383  pw2m1lepw2m1  48551  nnpw2even  48560  nnlog2ge0lt1  48597  logbpw2m1  48598  blenpw2m1  48610  nnpw2blenfzo  48612  nnpw2pmod  48614  nnpw2p  48617  blengt1fldiv2p1  48624  dignn0fr  48632  dignn0flhalflem1  48646  dignn0flhalflem2  48647  nn0sumshdiglemA  48650  nn0sumshdiglemB  48651