Theorem nnz 12612

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 12252	. 2 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
2		3mix2 1328	. 2 ⊢ (𝑁 ∈ ℕ → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
3		elz 12593	. 2 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
4	1, 2, 3	sylanbrc 581	1 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∨ w3o 1083   = wceq 1533   ∈ wcel 2098  ℝcr 11139  0cc0 11140  -cneg 11477  ℕcn 12245  ℤcz 12591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429  ax-un 7741  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-i2m1 11208  ax-1ne0 11209  ax-rrecex 11212  ax-cnre 11213

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-ov 7422  df-om 7872  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-neg 11479  df-nn 12246  df-z 12592

This theorem is referenced by:  nnssz  12613  elnnz1  12621  znegcl  12630  nnleltp1  12650  nnltp1le  12651  nnlem1lt  12661  nnltlem1  12662  nnm1ge0  12663  prime  12676  nneo  12679  zeo  12681  btwnz  12698  eluz2b2  12938  qaddcl  12982  qreccl  12986  elpqb  12993  elfz1end  13566  fznatpl1  13590  fznn  13604  elfz1b  13605  elfzo0  13708  elfzo0z  13709  elfzo1  13717  fzo1fzo0n0  13718  elfzom1p1elfzo  13747  ubmelm1fzo  13764  quoremz  13856  intfracq  13860  fznnfl  13863  zmodcl  13892  zmodfz  13894  zmodfzo  13895  zmodid2  13900  zmodidfzo  13901  modfzo0difsn  13944  expnnval  14065  mulexpz  14103  nnesq  14225  expnlbnd  14231  expnlbnd2  14232  digit2  14234  faclbnd  14285  bc0k  14306  bcval5  14313  fz1isolem  14458  seqcoll  14461  ccatval21sw  14571  lswccatn0lsw  14577  cshwidxmod  14789  cshwidxn  14795  absexpz  15288  climuni  15532  isercoll  15650  climcnds  15833  arisum  15842  trireciplem  15844  expcnv  15846  pwdif  15850  geo2sum  15855  geo2lim  15857  0.999...  15863  geoihalfsum  15864  rpnnen2lem6  16199  rpnnen2lem9  16202  rpnnen2lem10  16203  dvdsval3  16238  nndivdvds  16243  modmulconst  16268  dvdsle  16290  dvdsssfz1  16298  fzm1ndvds  16302  dvdsfac  16306  mulmoddvds  16310  oexpneg  16325  nnoddm1d2  16366  pwp1fsum  16371  divalg2  16385  divalgmod  16386  modremain  16388  ndvdsadd  16390  nndvdslegcd  16483  divgcdz  16489  divgcdnn  16493  divgcdnnr  16494  modgcd  16511  gcdmultiple  16515  gcddiv  16530  gcdzeq  16531  gcdeq  16532  rpmulgcd  16535  rplpwr  16536  rprpwr  16537  sqgcd  16539  dvdssqlem  16540  dvdssq  16541  eucalginv  16558  lcmgcdlem  16580  lcmgcdnn  16585  lcmass  16588  lcmftp  16610  lcmfunsnlem2lem1  16612  coprmgcdb  16623  qredeq  16631  qredeu  16632  coprmprod  16635  coprmproddvdslem  16636  coprmproddvds  16637  cncongr1  16641  cncongr2  16642  1idssfct  16654  isprm2lem  16655  isprm3  16657  prmind2  16659  ge2nprmge4  16675  divgcdodd  16684  isprm6  16688  ncoprmlnprm  16703  divnumden  16723  divdenle  16724  nn0gcdsq  16727  phicl2  16740  phiprmpw  16748  eulerthlem2  16754  hashgcdlem  16760  hashgcdeq  16761  phisum  16762  nnoddn2prm  16783  pythagtriplem3  16790  pythagtriplem4  16791  pythagtriplem6  16793  pythagtriplem7  16794  pythagtriplem8  16795  pythagtriplem9  16796  pythagtriplem11  16797  pythagtriplem13  16799  pythagtriplem15  16801  pythagtriplem19  16805  pythagtrip  16806  iserodd  16807  pclem  16810  pccl  16821  pcdiv  16824  pcqcl  16828  pcdvds  16836  pcndvds  16838  pcndvds2  16840  pcelnn  16842  pcz  16853  pcmpt  16864  fldivp1  16869  pcfac  16871  infpnlem1  16882  prmunb  16886  prmreclem1  16888  1arith  16899  ram0  16994  prmdvdsprmo  17014  prmgaplem4  17026  prmgaplem6  17028  prmgaplem7  17029  cshwshashlem2  17069  setsstruct2  17146  mulgnn  19039  mulgaddcom  19061  mulginvcom  19062  mulgmodid  19076  ghmmulg  19191  dfod2  19531  gexdvds  19551  gexnnod  19555  gexex  19820  mulgass2  20257  qsssubdrg  21376  prmirredlem  21415  znidomb  21512  znrrg  21516  chfacfisf  22800  chfacfisfcpmat  22801  chfacfscmul0  22804  chfacfpmmul0  22808  cayhamlem1  22812  cpmadugsumlemF  22822  lmmo  23328  1stckgenlem  23501  imasdsf1olem  24323  clmmulg  25072  cmetcaulem  25260  ovolunlem1a  25469  ovolicc2lem4  25493  mbfi1fseqlem6  25694  dvexp3  25954  dgreq0  26245  elqaalem2  26300  aaliou3lem1  26322  aaliou3lem2  26323  aaliou3lem3  26324  aaliou3lem9  26330  pserdvlem2  26410  logtayl2  26641  root1eq1  26735  root1cj  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  27183  chtublem  27189  vmasum  27194  logfac2  27195  logfaclbnd  27200  bclbnd  27258  bposlem5  27266  lgsval4a  27297  lgssq2  27316  lgsdchr  27333  gausslemma2dlem0c  27336  gausslemma2dlem0e  27338  gausslemma2dlem1a  27343  gausslemma2dlem5  27349  lgsquadlem1  27358  lgsquadlem2  27359  lgsquad3  27365  2lgslem1a1  27367  2lgslem3  27382  2lgsoddprm  27394  2sqnn  27417  2sqreunnltlem  27428  rplogsumlem1  27462  rplogsumlem2  27463  dchrisumlem2  27468  dchrmusumlema  27471  dchrmusum2  27472  dchrvmasumiflem1  27479  dchrvmaeq0  27482  dchrisum0flblem2  27487  dchrisum0re  27491  dchrisum0lema  27492  dchrisum0lem1b  27493  dchrisum0lem2a  27495  logdivbnd  27534  pntrsumbnd2  27545  ostth2lem1  27596  ostth2lem3  27613  ostth3  27616  axlowdimlem13  28837  crctcshwlkn0lem4  29696  crctcshwlkn0lem5  29697  crctcshwlkn0lem7  29699  wlkiswwlksupgr2  29760  clwwisshclwwslem  29896  clwwlkinwwlk  29922  clwwlkel  29928  clwwlkf  29929  wwlksubclwwlk  29940  clwwlkvbij  29995  eucrctshift  30125  eucrct2eupth  30127  numclwlk2lem2f  30259  bcm1n  32645  pnfinf  32983  1fldgenq  33108  isarchiofld  33131  rearchi  33157  submat1n  33537  lmatfvlem  33547  esumcvg  33836  oddpwdc  34105  fibp1  34152  chtvalz  34392  nnltp1ne  34851  erdszelem7  34938  climuzcnv  35406  elfzm12  35410  bcprod  35463  nn0prpwlem  35937  knoppndvlem1  36118  knoppndvlem2  36119  knoppndvlem7  36124  knoppndvlem18  36135  poimirlem13  37237  poimirlem14  37238  mblfinlem2  37262  fzmul  37345  incsequz  37352  geomcau  37363  heibor1lem  37413  bfplem2  37427  lcmfunnnd  41615  posbezout  41703  metakunt16  41806  metakunt26  41816  nn0rppwr  42028  nn0expgcd  42030  dvdsexpnn  42035  dvdsexpnn0  42036  zrtdvds  42040  fzsplit1nn0  42316  irrapxlem1  42384  pellexlem5  42395  rmynn  42519  jm2.24nn  42522  jm2.17c  42525  congrep  42536  congabseq  42537  acongrep  42543  acongeq  42546  jm2.18  42551  jm2.23  42559  jm2.20nn  42560  jm2.26lem3  42564  jm2.26  42565  jm2.15nn0  42566  jm2.16nn0  42567  jm2.27dlem2  42573  rmydioph  42577  jm3.1  42583  expdiophlem1  42584  expdioph  42586  idomodle  42761  proot1ex  42766  nznngen  43895  sumnnodd  45156  stoweidlem7  45533  stoweidlem17  45543  wallispilem4  45594  stirlinglem2  45601  stirlinglem3  45602  stirlinglem4  45603  stirlinglem12  45611  stirlinglem13  45612  stirlinglem14  45613  stirlinglem15  45614  stirlingr  45616  dirkertrigeqlem1  45624  fouriersw  45757  ovnsubaddlem1  46096  subsubelfzo0  46844  2ffzoeq  46845  iccpartres  46895  iccpartipre  46898  iccpartltu  46902  iccelpart  46910  odz2prm2pw  47040  fmtnoprmfac2lem1  47043  2pwp1prm  47066  lighneallem2  47083  lighneallem4  47087  lighneal  47088  proththd  47091  nneoALTV  47149  divgcdoddALTV  47159  fpprmod  47204  fppr2odd  47208  dfwppr  47215  fpprwppr  47216  fpprwpprb  47217  gbowge7  47240  gbege6  47242  altgsumbc  47602  altgsumbcALT  47603  pw2m1lepw2m1  47774  nnpw2even  47788  nnlog2ge0lt1  47825  logbpw2m1  47826  blenpw2m1  47838  nnpw2blenfzo  47840  nnpw2pmod  47842  nnpw2p  47845  blengt1fldiv2p1  47852  dignn0fr  47860  dignn0flhalflem1  47874  dignn0flhalflem2  47875  nn0sumshdiglemA  47878  nn0sumshdiglemB  47879