Theorem nnz 12509

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

Syntax hints:   → wi 4   ∨ w3o 1085   = wceq 1541   ∈ wcel 2113  ℝcr 11025  0cc0 11026  -cneg 11365  ℕcn 12145  ℤcz 12488

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 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-i2m1 11094  ax-1ne0 11095  ax-rrecex 11098  ax-cnre 11099

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-neg 11367  df-nn 12146  df-z 12489

This theorem is referenced by:  nnssz  12510  elnnz1  12517  znegcl  12526  nnleltp1  12547  nnltp1le  12548  nnlem1lt  12558  nnltlem1  12559  nnm1ge0  12560  prime  12573  nneo  12576  zeo  12578  btwnz  12595  eluz2b2  12834  qaddcl  12878  qreccl  12882  elpqb  12889  elfz1end  13470  fznatpl1  13494  fznn  13508  elfz1b  13509  elfzo0  13616  elfzo0z  13617  elfzo1  13628  fzo1fzo0n0  13631  elfzom1p1elfzo  13661  ubmelm1fzo  13679  quoremz  13775  intfracq  13779  fznnfl  13782  zmodcl  13811  zmodfz  13813  zmodfzo  13814  zmodid2  13819  zmodidfzo  13820  modfzo0difsn  13866  expnnval  13987  mulexpz  14025  nnesq  14150  expnlbnd  14156  expnlbnd2  14157  digit2  14159  faclbnd  14213  bc0k  14234  bcval5  14241  fz1isolem  14384  seqcoll  14387  ccatval21sw  14509  lswccatn0lsw  14515  cshwidxmod  14726  cshwidxn  14732  absexpz  15228  climuni  15475  isercoll  15591  climcnds  15774  arisum  15783  trireciplem  15785  expcnv  15787  pwdif  15791  geo2sum  15796  geo2lim  15798  0.999...  15804  geoihalfsum  15805  rpnnen2lem6  16144  rpnnen2lem9  16147  rpnnen2lem10  16148  dvdsval3  16183  nndivdvds  16188  modmulconst  16215  dvdsle  16237  dvdsssfz1  16245  fzm1ndvds  16249  dvdsfac  16253  mulmoddvds  16257  oexpneg  16272  nnoddm1d2  16313  pwp1fsum  16318  divalg2  16332  divalgmod  16333  modremain  16335  ndvdsadd  16337  nndvdslegcd  16432  divgcdz  16438  divgcdnn  16442  divgcdnnr  16443  modgcd  16459  gcdmultiple  16463  gcddiv  16478  gcdzeq  16479  gcdeq  16480  rpmulgcd  16484  rplpwr  16485  rprpwr  16486  nn0rppwr  16488  sqgcd  16489  nn0expgcd  16491  dvdssqlem  16493  dvdssq  16494  eucalginv  16511  lcmgcdlem  16533  lcmgcdnn  16538  lcmass  16541  lcmftp  16563  lcmfunsnlem2lem1  16565  coprmgcdb  16576  qredeq  16584  qredeu  16585  coprmprod  16588  coprmproddvdslem  16589  coprmproddvds  16590  cncongr1  16594  cncongr2  16595  1idssfct  16607  isprm2lem  16608  isprm3  16610  prmind2  16612  ge2nprmge4  16628  divgcdodd  16637  isprm6  16641  ncoprmlnprm  16655  divnumden  16675  divdenle  16676  nn0gcdsq  16679  phicl2  16695  phiprmpw  16703  eulerthlem2  16709  hashgcdlem  16715  hashgcdeq  16717  phisum  16718  nnoddn2prm  16739  pythagtriplem3  16746  pythagtriplem4  16747  pythagtriplem6  16749  pythagtriplem7  16750  pythagtriplem8  16751  pythagtriplem9  16752  pythagtriplem11  16753  pythagtriplem13  16755  pythagtriplem15  16757  pythagtriplem19  16761  pythagtrip  16762  iserodd  16763  pclem  16766  pccl  16777  pcdiv  16780  pcqcl  16784  pcdvds  16792  pcndvds  16794  pcndvds2  16796  pcelnn  16798  pcz  16809  pcmpt  16820  fldivp1  16825  pcfac  16827  infpnlem1  16838  prmunb  16842  prmreclem1  16844  1arith  16855  ram0  16950  prmdvdsprmo  16970  prmgaplem4  16982  prmgaplem6  16984  prmgaplem7  16985  cshwshashlem2  17024  setsstruct2  17101  mulgnn  19005  mulgaddcom  19028  mulginvcom  19029  mulgmodid  19043  ghmmulg  19157  dfod2  19493  gexdvds  19513  gexnnod  19517  gexex  19782  mulgass2  20244  qsssubdrg  21381  prmirredlem  21427  znidomb  21516  znrrg  21520  chfacfisf  22798  chfacfisfcpmat  22799  chfacfscmul0  22802  chfacfpmmul0  22806  cayhamlem1  22810  cpmadugsumlemF  22820  lmmo  23324  1stckgenlem  23497  imasdsf1olem  24317  clmmulg  25057  cmetcaulem  25244  ovolunlem1a  25453  ovolicc2lem4  25477  mbfi1fseqlem6  25677  dvexp3  25938  dgreq0  26227  elqaalem2  26284  aaliou3lem1  26306  aaliou3lem2  26307  aaliou3lem3  26308  aaliou3lem9  26314  pserdvlem2  26394  logtayl2  26627  root1eq1  26721  root1cj  26722  zrtdvds  26725  logbgcd1irr  26760  atantayl2  26904  birthdaylem2  26918  birthdaylem3  26919  emcllem5  26966  basellem2  27048  basellem3  27049  basellem5  27051  issqf  27102  sgmnncl  27113  prmorcht  27144  mumullem1  27145  mumullem2  27146  sqff1o  27148  dvdsflsumcom  27154  muinv  27159  vmalelog  27172  chtublem  27178  vmasum  27183  logfac2  27184  logfaclbnd  27189  bclbnd  27247  bposlem5  27255  lgsval4a  27286  lgssq2  27305  lgsdchr  27322  gausslemma2dlem0c  27325  gausslemma2dlem0e  27327  gausslemma2dlem1a  27332  gausslemma2dlem5  27338  lgsquadlem1  27347  lgsquadlem2  27348  lgsquad3  27354  2lgslem1a1  27356  2lgslem3  27371  2lgsoddprm  27383  2sqnn  27406  2sqreunnltlem  27417  rplogsumlem1  27451  rplogsumlem2  27452  dchrisumlem2  27457  dchrmusumlema  27460  dchrmusum2  27461  dchrvmasumiflem1  27468  dchrvmaeq0  27471  dchrisum0flblem2  27476  dchrisum0re  27480  dchrisum0lema  27481  dchrisum0lem1b  27482  dchrisum0lem2a  27484  logdivbnd  27523  pntrsumbnd2  27534  ostth2lem1  27585  ostth2lem3  27602  ostth3  27605  axlowdimlem13  29027  crctcshwlkn0lem4  29886  crctcshwlkn0lem5  29887  crctcshwlkn0lem7  29889  wlkiswwlksupgr2  29950  clwwisshclwwslem  30089  clwwlkinwwlk  30115  clwwlkel  30121  clwwlkf  30122  wwlksubclwwlk  30133  clwwlkvbij  30188  eucrctshift  30318  eucrct2eupth  30320  numclwlk2lem2f  30452  bcm1n  32875  pnfinf  33265  isarchiofld  33281  1fldgenq  33404  rearchi  33427  submat1n  33962  lmatfvlem  33972  esumcvg  34243  oddpwdc  34511  fibp1  34558  chtvalz  34786  nnltp1ne  35305  erdszelem7  35391  climuzcnv  35865  elfzm12  35869  bcprod  35932  nn0prpwlem  36516  knoppndvlem1  36712  knoppndvlem2  36713  knoppndvlem7  36718  knoppndvlem18  36729  poimirlem13  37830  poimirlem14  37831  mblfinlem2  37855  fzmul  37938  incsequz  37945  geomcau  37956  heibor1lem  38006  bfplem2  38020  lcmfunnnd  42262  posbezout  42350  unitscyglem4  42448  dvdsexpnn  42584  dvdsexpnn0  42585  fimgmcyc  42785  fzsplit1nn0  42992  irrapxlem1  43060  pellexlem5  43071  rmynn  43194  jm2.24nn  43197  jm2.17c  43200  congrep  43211  congabseq  43212  acongrep  43218  acongeq  43221  jm2.18  43226  jm2.23  43234  jm2.20nn  43235  jm2.26lem3  43239  jm2.26  43240  jm2.15nn0  43241  jm2.16nn0  43242  jm2.27dlem2  43248  rmydioph  43252  jm3.1  43258  expdiophlem1  43259  expdioph  43261  idomodle  43429  proot1ex  43434  nznngen  44553  sumnnodd  45872  stoweidlem7  46247  stoweidlem17  46257  wallispilem4  46308  stirlinglem2  46315  stirlinglem3  46316  stirlinglem4  46317  stirlinglem12  46325  stirlinglem13  46326  stirlinglem14  46327  stirlinglem15  46328  stirlingr  46330  dirkertrigeqlem1  46338  fouriersw  46471  ovnsubaddlem1  46810  nthrucw  47126  subsubelfzo0  47568  2ffzoeq  47569  ceilhalfelfzo1  47572  2tceilhalfelfzo1  47574  difltmodne  47584  addmodne  47586  submodlt  47592  iccpartres  47660  iccpartipre  47663  iccpartltu  47667  iccelpart  47675  odz2prm2pw  47805  fmtnoprmfac2lem1  47808  2pwp1prm  47831  lighneallem2  47848  lighneallem4  47852  lighneal  47853  proththd  47856  nneoALTV  47914  divgcdoddALTV  47924  fpprmod  47969  fppr2odd  47973  dfwppr  47980  fpprwppr  47981  fpprwpprb  47982  gbowge7  48005  gbege6  48007  gpg3kgrtriexlem2  48326  gpg3kgrtriexlem3  48327  gpg3kgrtriexlem5  48329  gpg3kgrtriexlem6  48330  altgsumbc  48594  altgsumbcALT  48595  pw2m1lepw2m1  48762  nnpw2even  48771  nnlog2ge0lt1  48808  logbpw2m1  48809  blenpw2m1  48821  nnpw2blenfzo  48823  nnpw2pmod  48825  nnpw2p  48828  blengt1fldiv2p1  48835  dignn0fr  48843  dignn0flhalflem1  48857  dignn0flhalflem2  48858  nn0sumshdiglemA  48861  nn0sumshdiglemB  48862