Theorem nnz 12586

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 12214	. 2 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
2		3mix2 1344	. 2 ⊢ (𝑁 ∈ ℕ → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
3		elz 12567	. 2 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
4	1, 2, 3	sylanbrc 592	1 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∨ w3o 1096   = wceq 1559   ∈ wcel 2141  ℝcr 11069  0cc0 11070  -cneg 11412  ℕcn 12207  ℤcz 12565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389  ax-un 7714  ax-1cn 11128  ax-icn 11129  ax-addcl 11130  ax-addrcl 11131  ax-mulcl 11132  ax-mulrcl 11133  ax-i2m1 11138  ax-1ne0 11139  ax-rrecex 11142  ax-cnre 11143

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5540  df-eprel 5545  df-po 5553  df-so 5554  df-fr 5598  df-we 5600  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-pred 6284  df-ord 6345  df-on 6346  df-lim 6347  df-suc 6348  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-fv 6525  df-ov 7395  df-om 7843  df-2nd 7967  df-frecs 8257  df-wrecs 8288  df-recs 8337  df-rdg 8376  df-neg 11414  df-nn 12208  df-z 12566

This theorem is referenced by:  nnssz  12587  elnnz1  12594  znegcl  12603  nnleltp1  12625  nnltp1le  12626  nnlem1lt  12636  nnltlem1  12637  nnm1ge0  12638  prime  12651  nneo  12654  zeo  12656  btwnz  12673  eluz2b2  12919  qaddcl  12963  qreccl  12967  elpqb  12974  elfz1end  13556  fznatpl1  13580  fznn  13594  elfz1b  13595  elfzo0  13703  elfzo0z  13704  elfzo1  13715  fzo1fzo0n0  13718  elfzom1p1elfzo  13748  ubmelm1fzo  13766  quoremz  13862  intfracq  13866  fznnfl  13869  zmodcl  13898  zmodfz  13900  zmodfzo  13901  zmodid2  13906  zmodidfzo  13907  modfzo0difsn  13953  expnnval  14074  mulexpz  14112  nnesq  14237  expnlbnd  14243  expnlbnd2  14244  digit2  14246  faclbnd  14300  bc0k  14321  bcval5  14328  fz1isolem  14471  seqcoll  14474  ccatval21sw  14596  lswccatn0lsw  14602  cshwidxmod  14813  cshwidxn  14819  absexpz  15315  climuni  15562  isercoll  15678  climcnds  15864  arisum  15873  trireciplem  15875  expcnv  15877  pwdif  15881  geo2sum  15886  geo2lim  15888  0.999...  15894  geoihalfsum  15895  rpnnen2lem6  16234  rpnnen2lem9  16237  rpnnen2lem10  16238  dvdsval3  16273  nndivdvds  16278  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  16719  divgcdodd  16728  isprm6  16732  ncoprmlnprm  16746  divnumden  16766  divdenle  16767  nn0gcdsq  16770  phicl2  16786  phiprmpw  16794  eulerthlem2  16800  hashgcdlem  16806  hashgcdeq  16808  phisum  16809  nnoddn2prm  16830  pythagtriplem3  16837  pythagtriplem4  16838  pythagtriplem6  16840  pythagtriplem7  16841  pythagtriplem8  16842  pythagtriplem9  16843  pythagtriplem11  16844  pythagtriplem13  16846  pythagtriplem15  16848  pythagtriplem19  16852  pythagtrip  16853  iserodd  16854  pclem  16857  pccl  16868  pcdiv  16871  pcqcl  16875  pcdvds  16883  pcndvds  16885  pcndvds2  16887  pcelnn  16889  pcz  16900  pcmpt  16911  fldivp1  16916  pcfac  16918  infpnlem1  16929  prmunb  16933  prmreclem1  16935  1arith  16946  ram0  17041  prmdvdsprmo  17061  prmgaplem4  17073  prmgaplem6  17075  prmgaplem7  17076  cshwshashlem2  17115  setsstruct2  17193  mulgnn  19100  mulgaddcom  19123  mulginvcom  19124  mulgmodid  19138  ghmmulg  19251  dfod2  19587  gexdvds  19607  gexnnod  19611  gexex  19876  mulgass2  20338  qsssubdrg  21458  prmirredlem  21504  znidomb  21593  znrrg  21597  chfacfisf  22894  chfacfisfcpmat  22895  chfacfscmul0  22898  chfacfpmmul0  22902  cayhamlem1  22906  cpmadugsumlemF  22916  lmmo  23420  1stckgenlem  23593  imasdsf1olem  24413  clmmulg  25143  cmetcaulem  25330  ovolunlem1a  25538  ovolicc2lem4  25562  mbfi1fseqlem6  25762  dvexp3  26020  dgreq0  26305  elqaalem2  26361  aaliou3lem1  26383  aaliou3lem2  26384  aaliou3lem3  26385  aaliou3lem9  26391  pserdvlem2  26468  logtayl2  26704  root1eq1  26797  root1cj  26798  zrtdvds  26801  logbgcd1irr  26836  atantayl2  26980  birthdaylem2  26994  birthdaylem3  26995  emcllem5  27041  basellem2  27123  basellem3  27124  basellem5  27126  issqf  27177  sgmnncl  27188  prmorcht  27219  mumullem1  27220  mumullem2  27221  sqff1o  27223  dvdsflsumcom  27229  muinv  27234  vmalelog  27246  chtublem  27252  vmasum  27257  logfac2  27258  logfaclbnd  27263  bclbnd  27321  bposlem5  27329  lgsval4a  27360  lgssq2  27379  lgsdchr  27396  gausslemma2dlem0c  27399  gausslemma2dlem0e  27401  gausslemma2dlem1a  27406  gausslemma2dlem5  27412  lgsquadlem1  27421  lgsquadlem2  27422  lgsquad3  27428  2lgslem1a1  27430  2lgslem3  27445  2lgsoddprm  27457  2sqnn  27480  2sqreunnltlem  27491  rplogsumlem1  27525  rplogsumlem2  27526  dchrisumlem2  27531  dchrmusumlema  27534  dchrmusum2  27535  dchrvmasumiflem1  27542  dchrvmaeq0  27545  dchrisum0flblem2  27550  dchrisum0re  27554  dchrisum0lema  27555  dchrisum0lem1b  27556  dchrisum0lem2a  27558  logdivbnd  27597  pntrsumbnd2  27608  ostth2lem1  27659  ostth2lem3  27676  ostth3  27679  axlowdimlem13  29101  crctcshwlkn0lem4  29959  crctcshwlkn0lem5  29960  crctcshwlkn0lem7  29962  wlkiswwlksupgr2  30023  clwwisshclwwslem  30162  clwwlkinwwlk  30188  clwwlkel  30194  clwwlkf  30195  wwlksubclwwlk  30206  clwwlkvbij  30261  eucrctshift  30391  eucrct2eupth  30393  numclwlk2lem2f  30525  bcm1n  32947  pnfinf  33324  isarchiofld  33340  1fldgenq  33470  rearchi  33493  submat1n  34063  lmatfvlem  34073  esumcvg  34344  oddpwdc  34612  fibp1  34659  chtvalz  34887  nnltp1ne  35425  erdszelem7  35511  climuzcnv  35985  elfzm12  35989  bcprod  36052  nn0prpwlem  36646  knoppndvlem1  36914  knoppndvlem2  36915  knoppndvlem7  36920  knoppndvlem18  36931  poimirlem13  38096  poimirlem14  38097  mblfinlem2  38121  fzmul  38204  incsequz  38211  geomcau  38222  heibor1lem  38272  bfplem2  38286  lcmfunnnd  42593  posbezout  42681  unitscyglem4  42779  dvdsexpnn  42906  dvdsexpnn0  42907  fimgmcyc  43116  fzsplit1nn0  43299  irrapxlem1  43363  pellexlem5  43374  rmynn  43497  jm2.24nn  43500  jm2.17c  43503  congrep  43514  congabseq  43515  acongrep  43521  acongeq  43524  jm2.18  43529  jm2.23  43537  jm2.20nn  43538  jm2.26lem3  43542  jm2.26  43543  jm2.15nn0  43544  jm2.16nn0  43545  jm2.27dlem2  43551  rmydioph  43555  jm3.1  43561  expdiophlem1  43562  expdioph  43564  idomodle  43732  proot1ex  43737  nznngen  44856  sumnnodd  46170  stoweidlem7  46545  stoweidlem17  46555  wallispilem4  46606  stirlinglem2  46613  stirlinglem3  46614  stirlinglem4  46615  stirlinglem12  46623  stirlinglem13  46624  stirlinglem14  46625  stirlinglem15  46626  stirlingr  46628  dirkertrigeqlem1  46636  fouriersw  46769  ovnsubaddlem1  47108  nthrucw  47426  subsubelfzo0  47885  2ffzoeq  47886  nnmul2  47888  ceilhalfelfzo1  47892  2tceilhalfelfzo1  47894  difltmodne  47906  addmodne  47908  submodlt  47914  facnn0dvdsfac  47943  muldvdsfacgt  47944  iccpartres  47988  iccpartipre  47991  iccpartltu  47995  iccelpart  48003  odz2prm2pw  48136  fmtnoprmfac2lem1  48139  2pwp1prm  48162  lighneallem2  48179  lighneallem4  48183  lighneal  48184  proththd  48187  nneoALTV  48258  divgcdoddALTV  48268  fpprmod  48313  fppr2odd  48317  dfwppr  48324  fpprwppr  48325  fpprwpprb  48326  gbowge7  48349  gbege6  48351  gpg3kgrtriexlem2  48670  gpg3kgrtriexlem3  48671  gpg3kgrtriexlem5  48673  gpg3kgrtriexlem6  48674  altgsumbc  48938  altgsumbcALT  48939  pw2m1lepw2m1  49106  nnpw2even  49115  nnlog2ge0lt1  49152  logbpw2m1  49153  blenpw2m1  49165  nnpw2blenfzo  49167  nnpw2pmod  49169  nnpw2p  49172  blengt1fldiv2p1  49179  dignn0fr  49187  dignn0flhalflem1  49201  dignn0flhalflem2  49202  nn0sumshdiglemA  49205  nn0sumshdiglemB  49206