Theorem nnz 12557

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

Syntax hints:   → wi 4   ∨ w3o 1085   = wceq 1540   ∈ wcel 2109  ℝcr 11074  0cc0 11075  -cneg 11413  ℕcn 12193  ℤcz 12536

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-i2m1 11143  ax-1ne0 11144  ax-rrecex 11147  ax-cnre 11148

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 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-neg 11415  df-nn 12194  df-z 12537

This theorem is referenced by:  nnssz  12558  elnnz1  12566  znegcl  12575  nnleltp1  12596  nnltp1le  12597  nnlem1lt  12607  nnltlem1  12608  nnm1ge0  12609  prime  12622  nneo  12625  zeo  12627  btwnz  12644  eluz2b2  12887  qaddcl  12931  qreccl  12935  elpqb  12942  elfz1end  13522  fznatpl1  13546  fznn  13560  elfz1b  13561  elfzo0  13668  elfzo0z  13669  elfzo1  13680  fzo1fzo0n0  13683  elfzom1p1elfzo  13713  ubmelm1fzo  13731  quoremz  13824  intfracq  13828  fznnfl  13831  zmodcl  13860  zmodfz  13862  zmodfzo  13863  zmodid2  13868  zmodidfzo  13869  modfzo0difsn  13915  expnnval  14036  mulexpz  14074  nnesq  14199  expnlbnd  14205  expnlbnd2  14206  digit2  14208  faclbnd  14262  bc0k  14283  bcval5  14290  fz1isolem  14433  seqcoll  14436  ccatval21sw  14557  lswccatn0lsw  14563  cshwidxmod  14775  cshwidxn  14781  absexpz  15278  climuni  15525  isercoll  15641  climcnds  15824  arisum  15833  trireciplem  15835  expcnv  15837  pwdif  15841  geo2sum  15846  geo2lim  15848  0.999...  15854  geoihalfsum  15855  rpnnen2lem6  16194  rpnnen2lem9  16197  rpnnen2lem10  16198  dvdsval3  16233  nndivdvds  16238  modmulconst  16265  dvdsle  16287  dvdsssfz1  16295  fzm1ndvds  16299  dvdsfac  16303  mulmoddvds  16307  oexpneg  16322  nnoddm1d2  16363  pwp1fsum  16368  divalg2  16382  divalgmod  16383  modremain  16385  ndvdsadd  16387  nndvdslegcd  16482  divgcdz  16488  divgcdnn  16492  divgcdnnr  16493  modgcd  16509  gcdmultiple  16513  gcddiv  16528  gcdzeq  16529  gcdeq  16530  rpmulgcd  16534  rplpwr  16535  rprpwr  16536  nn0rppwr  16538  sqgcd  16539  nn0expgcd  16541  dvdssqlem  16543  dvdssq  16544  eucalginv  16561  lcmgcdlem  16583  lcmgcdnn  16588  lcmass  16591  lcmftp  16613  lcmfunsnlem2lem1  16615  coprmgcdb  16626  qredeq  16634  qredeu  16635  coprmprod  16638  coprmproddvdslem  16639  coprmproddvds  16640  cncongr1  16644  cncongr2  16645  1idssfct  16657  isprm2lem  16658  isprm3  16660  prmind2  16662  ge2nprmge4  16678  divgcdodd  16687  isprm6  16691  ncoprmlnprm  16705  divnumden  16725  divdenle  16726  nn0gcdsq  16729  phicl2  16745  phiprmpw  16753  eulerthlem2  16759  hashgcdlem  16765  hashgcdeq  16767  phisum  16768  nnoddn2prm  16789  pythagtriplem3  16796  pythagtriplem4  16797  pythagtriplem6  16799  pythagtriplem7  16800  pythagtriplem8  16801  pythagtriplem9  16802  pythagtriplem11  16803  pythagtriplem13  16805  pythagtriplem15  16807  pythagtriplem19  16811  pythagtrip  16812  iserodd  16813  pclem  16816  pccl  16827  pcdiv  16830  pcqcl  16834  pcdvds  16842  pcndvds  16844  pcndvds2  16846  pcelnn  16848  pcz  16859  pcmpt  16870  fldivp1  16875  pcfac  16877  infpnlem1  16888  prmunb  16892  prmreclem1  16894  1arith  16905  ram0  17000  prmdvdsprmo  17020  prmgaplem4  17032  prmgaplem6  17034  prmgaplem7  17035  cshwshashlem2  17074  setsstruct2  17151  mulgnn  19014  mulgaddcom  19037  mulginvcom  19038  mulgmodid  19052  ghmmulg  19167  dfod2  19501  gexdvds  19521  gexnnod  19525  gexex  19790  mulgass2  20225  qsssubdrg  21350  prmirredlem  21389  znidomb  21478  znrrg  21482  chfacfisf  22748  chfacfisfcpmat  22749  chfacfscmul0  22752  chfacfpmmul0  22756  cayhamlem1  22760  cpmadugsumlemF  22770  lmmo  23274  1stckgenlem  23447  imasdsf1olem  24268  clmmulg  25008  cmetcaulem  25195  ovolunlem1a  25404  ovolicc2lem4  25428  mbfi1fseqlem6  25628  dvexp3  25889  dgreq0  26178  elqaalem2  26235  aaliou3lem1  26257  aaliou3lem2  26258  aaliou3lem3  26259  aaliou3lem9  26265  pserdvlem2  26345  logtayl2  26578  root1eq1  26672  root1cj  26673  zrtdvds  26676  logbgcd1irr  26711  atantayl2  26855  birthdaylem2  26869  birthdaylem3  26870  emcllem5  26917  basellem2  26999  basellem3  27000  basellem5  27002  issqf  27053  sgmnncl  27064  prmorcht  27095  mumullem1  27096  mumullem2  27097  sqff1o  27099  dvdsflsumcom  27105  muinv  27110  vmalelog  27123  chtublem  27129  vmasum  27134  logfac2  27135  logfaclbnd  27140  bclbnd  27198  bposlem5  27206  lgsval4a  27237  lgssq2  27256  lgsdchr  27273  gausslemma2dlem0c  27276  gausslemma2dlem0e  27278  gausslemma2dlem1a  27283  gausslemma2dlem5  27289  lgsquadlem1  27298  lgsquadlem2  27299  lgsquad3  27305  2lgslem1a1  27307  2lgslem3  27322  2lgsoddprm  27334  2sqnn  27357  2sqreunnltlem  27368  rplogsumlem1  27402  rplogsumlem2  27403  dchrisumlem2  27408  dchrmusumlema  27411  dchrmusum2  27412  dchrvmasumiflem1  27419  dchrvmaeq0  27422  dchrisum0flblem2  27427  dchrisum0re  27431  dchrisum0lema  27432  dchrisum0lem1b  27433  dchrisum0lem2a  27435  logdivbnd  27474  pntrsumbnd2  27485  ostth2lem1  27536  ostth2lem3  27553  ostth3  27556  axlowdimlem13  28888  crctcshwlkn0lem4  29750  crctcshwlkn0lem5  29751  crctcshwlkn0lem7  29753  wlkiswwlksupgr2  29814  clwwisshclwwslem  29950  clwwlkinwwlk  29976  clwwlkel  29982  clwwlkf  29983  wwlksubclwwlk  29994  clwwlkvbij  30049  eucrctshift  30179  eucrct2eupth  30181  numclwlk2lem2f  30313  bcm1n  32725  pnfinf  33144  1fldgenq  33279  isarchiofld  33302  rearchi  33324  submat1n  33802  lmatfvlem  33812  esumcvg  34083  oddpwdc  34352  fibp1  34399  chtvalz  34627  nnltp1ne  35105  erdszelem7  35191  climuzcnv  35665  elfzm12  35669  bcprod  35732  nn0prpwlem  36317  knoppndvlem1  36507  knoppndvlem2  36508  knoppndvlem7  36513  knoppndvlem18  36524  poimirlem13  37634  poimirlem14  37635  mblfinlem2  37659  fzmul  37742  incsequz  37749  geomcau  37760  heibor1lem  37810  bfplem2  37824  lcmfunnnd  42007  posbezout  42095  unitscyglem4  42193  dvdsexpnn  42328  dvdsexpnn0  42329  fimgmcyc  42529  fzsplit1nn0  42749  irrapxlem1  42817  pellexlem5  42828  rmynn  42952  jm2.24nn  42955  jm2.17c  42958  congrep  42969  congabseq  42970  acongrep  42976  acongeq  42979  jm2.18  42984  jm2.23  42992  jm2.20nn  42993  jm2.26lem3  42997  jm2.26  42998  jm2.15nn0  42999  jm2.16nn0  43000  jm2.27dlem2  43006  rmydioph  43010  jm3.1  43016  expdiophlem1  43017  expdioph  43019  idomodle  43187  proot1ex  43192  nznngen  44312  sumnnodd  45635  stoweidlem7  46012  stoweidlem17  46022  wallispilem4  46073  stirlinglem2  46080  stirlinglem3  46081  stirlinglem4  46082  stirlinglem12  46090  stirlinglem13  46091  stirlinglem14  46092  stirlinglem15  46093  stirlingr  46095  dirkertrigeqlem1  46103  fouriersw  46236  ovnsubaddlem1  46575  subsubelfzo0  47331  2ffzoeq  47332  ceilhalfelfzo1  47335  2tceilhalfelfzo1  47337  difltmodne  47347  addmodne  47349  submodlt  47355  iccpartres  47423  iccpartipre  47426  iccpartltu  47430  iccelpart  47438  odz2prm2pw  47568  fmtnoprmfac2lem1  47571  2pwp1prm  47594  lighneallem2  47611  lighneallem4  47615  lighneal  47616  proththd  47619  nneoALTV  47677  divgcdoddALTV  47687  fpprmod  47732  fppr2odd  47736  dfwppr  47743  fpprwppr  47744  fpprwpprb  47745  gbowge7  47768  gbege6  47770  gpg3kgrtriexlem2  48079  gpg3kgrtriexlem3  48080  gpg3kgrtriexlem5  48082  gpg3kgrtriexlem6  48083  altgsumbc  48344  altgsumbcALT  48345  pw2m1lepw2m1  48513  nnpw2even  48522  nnlog2ge0lt1  48559  logbpw2m1  48560  blenpw2m1  48572  nnpw2blenfzo  48574  nnpw2pmod  48576  nnpw2p  48579  blengt1fldiv2p1  48586  dignn0fr  48594  dignn0flhalflem1  48608  dignn0flhalflem2  48609  nn0sumshdiglemA  48612  nn0sumshdiglemB  48613