Theorem nnz 12496

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

Syntax hints:   → wi 4   ∨ w3o 1085   = wceq 1541   ∈ wcel 2113  ℝcr 11012  0cc0 11013  -cneg 11352  ℕcn 12132  ℤcz 12475

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-un 7674  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-addrcl 11074  ax-mulcl 11075  ax-mulrcl 11076  ax-i2m1 11081  ax-1ne0 11082  ax-rrecex 11085  ax-cnre 11086

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-tr 5201  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7355  df-om 7803  df-2nd 7928  df-frecs 8217  df-wrecs 8248  df-recs 8297  df-rdg 8335  df-neg 11354  df-nn 12133  df-z 12476

This theorem is referenced by:  nnssz  12497  elnnz1  12504  znegcl  12513  nnleltp1  12534  nnltp1le  12535  nnlem1lt  12545  nnltlem1  12546  nnm1ge0  12547  prime  12560  nneo  12563  zeo  12565  btwnz  12582  eluz2b2  12821  qaddcl  12865  qreccl  12869  elpqb  12876  elfz1end  13456  fznatpl1  13480  fznn  13494  elfz1b  13495  elfzo0  13602  elfzo0z  13603  elfzo1  13614  fzo1fzo0n0  13617  elfzom1p1elfzo  13647  ubmelm1fzo  13665  quoremz  13761  intfracq  13765  fznnfl  13768  zmodcl  13797  zmodfz  13799  zmodfzo  13800  zmodid2  13805  zmodidfzo  13806  modfzo0difsn  13852  expnnval  13973  mulexpz  14011  nnesq  14136  expnlbnd  14142  expnlbnd2  14143  digit2  14145  faclbnd  14199  bc0k  14220  bcval5  14227  fz1isolem  14370  seqcoll  14373  ccatval21sw  14495  lswccatn0lsw  14501  cshwidxmod  14712  cshwidxn  14718  absexpz  15214  climuni  15461  isercoll  15577  climcnds  15760  arisum  15769  trireciplem  15771  expcnv  15773  pwdif  15777  geo2sum  15782  geo2lim  15784  0.999...  15790  geoihalfsum  15791  rpnnen2lem6  16130  rpnnen2lem9  16133  rpnnen2lem10  16134  dvdsval3  16169  nndivdvds  16174  modmulconst  16201  dvdsle  16223  dvdsssfz1  16231  fzm1ndvds  16235  dvdsfac  16239  mulmoddvds  16243  oexpneg  16258  nnoddm1d2  16299  pwp1fsum  16304  divalg2  16318  divalgmod  16319  modremain  16321  ndvdsadd  16323  nndvdslegcd  16418  divgcdz  16424  divgcdnn  16428  divgcdnnr  16429  modgcd  16445  gcdmultiple  16449  gcddiv  16464  gcdzeq  16465  gcdeq  16466  rpmulgcd  16470  rplpwr  16471  rprpwr  16472  nn0rppwr  16474  sqgcd  16475  nn0expgcd  16477  dvdssqlem  16479  dvdssq  16480  eucalginv  16497  lcmgcdlem  16519  lcmgcdnn  16524  lcmass  16527  lcmftp  16549  lcmfunsnlem2lem1  16551  coprmgcdb  16562  qredeq  16570  qredeu  16571  coprmprod  16574  coprmproddvdslem  16575  coprmproddvds  16576  cncongr1  16580  cncongr2  16581  1idssfct  16593  isprm2lem  16594  isprm3  16596  prmind2  16598  ge2nprmge4  16614  divgcdodd  16623  isprm6  16627  ncoprmlnprm  16641  divnumden  16661  divdenle  16662  nn0gcdsq  16665  phicl2  16681  phiprmpw  16689  eulerthlem2  16695  hashgcdlem  16701  hashgcdeq  16703  phisum  16704  nnoddn2prm  16725  pythagtriplem3  16732  pythagtriplem4  16733  pythagtriplem6  16735  pythagtriplem7  16736  pythagtriplem8  16737  pythagtriplem9  16738  pythagtriplem11  16739  pythagtriplem13  16741  pythagtriplem15  16743  pythagtriplem19  16747  pythagtrip  16748  iserodd  16749  pclem  16752  pccl  16763  pcdiv  16766  pcqcl  16770  pcdvds  16778  pcndvds  16780  pcndvds2  16782  pcelnn  16784  pcz  16795  pcmpt  16806  fldivp1  16811  pcfac  16813  infpnlem1  16824  prmunb  16828  prmreclem1  16830  1arith  16841  ram0  16936  prmdvdsprmo  16956  prmgaplem4  16968  prmgaplem6  16970  prmgaplem7  16971  cshwshashlem2  17010  setsstruct2  17087  mulgnn  18990  mulgaddcom  19013  mulginvcom  19014  mulgmodid  19028  ghmmulg  19142  dfod2  19478  gexdvds  19498  gexnnod  19502  gexex  19767  mulgass2  20229  qsssubdrg  21365  prmirredlem  21411  znidomb  21500  znrrg  21504  chfacfisf  22770  chfacfisfcpmat  22771  chfacfscmul0  22774  chfacfpmmul0  22778  cayhamlem1  22782  cpmadugsumlemF  22792  lmmo  23296  1stckgenlem  23469  imasdsf1olem  24289  clmmulg  25029  cmetcaulem  25216  ovolunlem1a  25425  ovolicc2lem4  25449  mbfi1fseqlem6  25649  dvexp3  25910  dgreq0  26199  elqaalem2  26256  aaliou3lem1  26278  aaliou3lem2  26279  aaliou3lem3  26280  aaliou3lem9  26286  pserdvlem2  26366  logtayl2  26599  root1eq1  26693  root1cj  26694  zrtdvds  26697  logbgcd1irr  26732  atantayl2  26876  birthdaylem2  26890  birthdaylem3  26891  emcllem5  26938  basellem2  27020  basellem3  27021  basellem5  27023  issqf  27074  sgmnncl  27085  prmorcht  27116  mumullem1  27117  mumullem2  27118  sqff1o  27120  dvdsflsumcom  27126  muinv  27131  vmalelog  27144  chtublem  27150  vmasum  27155  logfac2  27156  logfaclbnd  27161  bclbnd  27219  bposlem5  27227  lgsval4a  27258  lgssq2  27277  lgsdchr  27294  gausslemma2dlem0c  27297  gausslemma2dlem0e  27299  gausslemma2dlem1a  27304  gausslemma2dlem5  27310  lgsquadlem1  27319  lgsquadlem2  27320  lgsquad3  27326  2lgslem1a1  27328  2lgslem3  27343  2lgsoddprm  27355  2sqnn  27378  2sqreunnltlem  27389  rplogsumlem1  27423  rplogsumlem2  27424  dchrisumlem2  27429  dchrmusumlema  27432  dchrmusum2  27433  dchrvmasumiflem1  27440  dchrvmaeq0  27443  dchrisum0flblem2  27448  dchrisum0re  27452  dchrisum0lema  27453  dchrisum0lem1b  27454  dchrisum0lem2a  27456  logdivbnd  27495  pntrsumbnd2  27506  ostth2lem1  27557  ostth2lem3  27574  ostth3  27577  axlowdimlem13  28934  crctcshwlkn0lem4  29793  crctcshwlkn0lem5  29794  crctcshwlkn0lem7  29796  wlkiswwlksupgr2  29857  clwwisshclwwslem  29996  clwwlkinwwlk  30022  clwwlkel  30028  clwwlkf  30029  wwlksubclwwlk  30040  clwwlkvbij  30095  eucrctshift  30225  eucrct2eupth  30227  numclwlk2lem2f  30359  bcm1n  32782  pnfinf  33159  isarchiofld  33175  1fldgenq  33295  rearchi  33318  submat1n  33839  lmatfvlem  33849  esumcvg  34120  oddpwdc  34388  fibp1  34435  chtvalz  34663  nnltp1ne  35176  erdszelem7  35262  climuzcnv  35736  elfzm12  35740  bcprod  35803  nn0prpwlem  36387  knoppndvlem1  36577  knoppndvlem2  36578  knoppndvlem7  36583  knoppndvlem18  36594  poimirlem13  37694  poimirlem14  37695  mblfinlem2  37719  fzmul  37802  incsequz  37809  geomcau  37820  heibor1lem  37870  bfplem2  37884  lcmfunnnd  42126  posbezout  42214  unitscyglem4  42312  dvdsexpnn  42452  dvdsexpnn0  42453  fimgmcyc  42653  fzsplit1nn0  42872  irrapxlem1  42940  pellexlem5  42951  rmynn  43074  jm2.24nn  43077  jm2.17c  43080  congrep  43091  congabseq  43092  acongrep  43098  acongeq  43101  jm2.18  43106  jm2.23  43114  jm2.20nn  43115  jm2.26lem3  43119  jm2.26  43120  jm2.15nn0  43121  jm2.16nn0  43122  jm2.27dlem2  43128  rmydioph  43132  jm3.1  43138  expdiophlem1  43139  expdioph  43141  idomodle  43309  proot1ex  43314  nznngen  44434  sumnnodd  45755  stoweidlem7  46130  stoweidlem17  46140  wallispilem4  46191  stirlinglem2  46198  stirlinglem3  46199  stirlinglem4  46200  stirlinglem12  46208  stirlinglem13  46209  stirlinglem14  46210  stirlinglem15  46211  stirlingr  46213  dirkertrigeqlem1  46221  fouriersw  46354  ovnsubaddlem1  46693  nthrucw  47009  subsubelfzo0  47451  2ffzoeq  47452  ceilhalfelfzo1  47455  2tceilhalfelfzo1  47457  difltmodne  47467  addmodne  47469  submodlt  47475  iccpartres  47543  iccpartipre  47546  iccpartltu  47550  iccelpart  47558  odz2prm2pw  47688  fmtnoprmfac2lem1  47691  2pwp1prm  47714  lighneallem2  47731  lighneallem4  47735  lighneal  47736  proththd  47739  nneoALTV  47797  divgcdoddALTV  47807  fpprmod  47852  fppr2odd  47856  dfwppr  47863  fpprwppr  47864  fpprwpprb  47865  gbowge7  47888  gbege6  47890  gpg3kgrtriexlem2  48209  gpg3kgrtriexlem3  48210  gpg3kgrtriexlem5  48212  gpg3kgrtriexlem6  48213  altgsumbc  48477  altgsumbcALT  48478  pw2m1lepw2m1  48646  nnpw2even  48655  nnlog2ge0lt1  48692  logbpw2m1  48693  blenpw2m1  48705  nnpw2blenfzo  48707  nnpw2pmod  48709  nnpw2p  48712  blengt1fldiv2p1  48719  dignn0fr  48727  dignn0flhalflem1  48741  dignn0flhalflem2  48742  nn0sumshdiglemA  48745  nn0sumshdiglemB  48746