Theorem nnz 12634

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

Syntax hints:   → wi 4   ∨ w3o 1086   = wceq 1540   ∈ wcel 2108  ℝcr 11154  0cc0 11155  -cneg 11493  ℕcn 12266  ℤcz 12613

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-i2m1 11223  ax-1ne0 11224  ax-rrecex 11227  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-neg 11495  df-nn 12267  df-z 12614

This theorem is referenced by:  nnssz  12635  elnnz1  12643  znegcl  12652  nnleltp1  12673  nnltp1le  12674  nnlem1lt  12684  nnltlem1  12685  nnm1ge0  12686  prime  12699  nneo  12702  zeo  12704  btwnz  12721  eluz2b2  12963  qaddcl  13007  qreccl  13011  elpqb  13018  elfz1end  13594  fznatpl1  13618  fznn  13632  elfz1b  13633  elfzo0  13740  elfzo0z  13741  elfzo1  13752  fzo1fzo0n0  13754  elfzom1p1elfzo  13784  ubmelm1fzo  13802  quoremz  13895  intfracq  13899  fznnfl  13902  zmodcl  13931  zmodfz  13933  zmodfzo  13934  zmodid2  13939  zmodidfzo  13940  modfzo0difsn  13984  expnnval  14105  mulexpz  14143  nnesq  14266  expnlbnd  14272  expnlbnd2  14273  digit2  14275  faclbnd  14329  bc0k  14350  bcval5  14357  fz1isolem  14500  seqcoll  14503  ccatval21sw  14623  lswccatn0lsw  14629  cshwidxmod  14841  cshwidxn  14847  absexpz  15344  climuni  15588  isercoll  15704  climcnds  15887  arisum  15896  trireciplem  15898  expcnv  15900  pwdif  15904  geo2sum  15909  geo2lim  15911  0.999...  15917  geoihalfsum  15918  rpnnen2lem6  16255  rpnnen2lem9  16258  rpnnen2lem10  16259  dvdsval3  16294  nndivdvds  16299  modmulconst  16325  dvdsle  16347  dvdsssfz1  16355  fzm1ndvds  16359  dvdsfac  16363  mulmoddvds  16367  oexpneg  16382  nnoddm1d2  16423  pwp1fsum  16428  divalg2  16442  divalgmod  16443  modremain  16445  ndvdsadd  16447  nndvdslegcd  16542  divgcdz  16548  divgcdnn  16552  divgcdnnr  16553  modgcd  16569  gcdmultiple  16573  gcddiv  16588  gcdzeq  16589  gcdeq  16590  rpmulgcd  16594  rplpwr  16595  rprpwr  16596  nn0rppwr  16598  sqgcd  16599  nn0expgcd  16601  dvdssqlem  16603  dvdssq  16604  eucalginv  16621  lcmgcdlem  16643  lcmgcdnn  16648  lcmass  16651  lcmftp  16673  lcmfunsnlem2lem1  16675  coprmgcdb  16686  qredeq  16694  qredeu  16695  coprmprod  16698  coprmproddvdslem  16699  coprmproddvds  16700  cncongr1  16704  cncongr2  16705  1idssfct  16717  isprm2lem  16718  isprm3  16720  prmind2  16722  ge2nprmge4  16738  divgcdodd  16747  isprm6  16751  ncoprmlnprm  16765  divnumden  16785  divdenle  16786  nn0gcdsq  16789  phicl2  16805  phiprmpw  16813  eulerthlem2  16819  hashgcdlem  16825  hashgcdeq  16827  phisum  16828  nnoddn2prm  16849  pythagtriplem3  16856  pythagtriplem4  16857  pythagtriplem6  16859  pythagtriplem7  16860  pythagtriplem8  16861  pythagtriplem9  16862  pythagtriplem11  16863  pythagtriplem13  16865  pythagtriplem15  16867  pythagtriplem19  16871  pythagtrip  16872  iserodd  16873  pclem  16876  pccl  16887  pcdiv  16890  pcqcl  16894  pcdvds  16902  pcndvds  16904  pcndvds2  16906  pcelnn  16908  pcz  16919  pcmpt  16930  fldivp1  16935  pcfac  16937  infpnlem1  16948  prmunb  16952  prmreclem1  16954  1arith  16965  ram0  17060  prmdvdsprmo  17080  prmgaplem4  17092  prmgaplem6  17094  prmgaplem7  17095  cshwshashlem2  17134  setsstruct2  17211  mulgnn  19093  mulgaddcom  19116  mulginvcom  19117  mulgmodid  19131  ghmmulg  19246  dfod2  19582  gexdvds  19602  gexnnod  19606  gexex  19871  mulgass2  20306  qsssubdrg  21444  prmirredlem  21483  znidomb  21580  znrrg  21584  chfacfisf  22860  chfacfisfcpmat  22861  chfacfscmul0  22864  chfacfpmmul0  22868  cayhamlem1  22872  cpmadugsumlemF  22882  lmmo  23388  1stckgenlem  23561  imasdsf1olem  24383  clmmulg  25134  cmetcaulem  25322  ovolunlem1a  25531  ovolicc2lem4  25555  mbfi1fseqlem6  25755  dvexp3  26016  dgreq0  26305  elqaalem2  26362  aaliou3lem1  26384  aaliou3lem2  26385  aaliou3lem3  26386  aaliou3lem9  26392  pserdvlem2  26472  logtayl2  26704  root1eq1  26798  root1cj  26799  zrtdvds  26802  logbgcd1irr  26837  atantayl2  26981  birthdaylem2  26995  birthdaylem3  26996  emcllem5  27043  basellem2  27125  basellem3  27126  basellem5  27128  issqf  27179  sgmnncl  27190  prmorcht  27221  mumullem1  27222  mumullem2  27223  sqff1o  27225  dvdsflsumcom  27231  muinv  27236  vmalelog  27249  chtublem  27255  vmasum  27260  logfac2  27261  logfaclbnd  27266  bclbnd  27324  bposlem5  27332  lgsval4a  27363  lgssq2  27382  lgsdchr  27399  gausslemma2dlem0c  27402  gausslemma2dlem0e  27404  gausslemma2dlem1a  27409  gausslemma2dlem5  27415  lgsquadlem1  27424  lgsquadlem2  27425  lgsquad3  27431  2lgslem1a1  27433  2lgslem3  27448  2lgsoddprm  27460  2sqnn  27483  2sqreunnltlem  27494  rplogsumlem1  27528  rplogsumlem2  27529  dchrisumlem2  27534  dchrmusumlema  27537  dchrmusum2  27538  dchrvmasumiflem1  27545  dchrvmaeq0  27548  dchrisum0flblem2  27553  dchrisum0re  27557  dchrisum0lema  27558  dchrisum0lem1b  27559  dchrisum0lem2a  27561  logdivbnd  27600  pntrsumbnd2  27611  ostth2lem1  27662  ostth2lem3  27679  ostth3  27682  axlowdimlem13  28969  crctcshwlkn0lem4  29833  crctcshwlkn0lem5  29834  crctcshwlkn0lem7  29836  wlkiswwlksupgr2  29897  clwwisshclwwslem  30033  clwwlkinwwlk  30059  clwwlkel  30065  clwwlkf  30066  wwlksubclwwlk  30077  clwwlkvbij  30132  eucrctshift  30262  eucrct2eupth  30264  numclwlk2lem2f  30396  bcm1n  32797  pnfinf  33190  1fldgenq  33324  isarchiofld  33347  rearchi  33374  submat1n  33804  lmatfvlem  33814  esumcvg  34087  oddpwdc  34356  fibp1  34403  chtvalz  34644  nnltp1ne  35116  erdszelem7  35202  climuzcnv  35676  elfzm12  35680  bcprod  35738  nn0prpwlem  36323  knoppndvlem1  36513  knoppndvlem2  36514  knoppndvlem7  36519  knoppndvlem18  36530  poimirlem13  37640  poimirlem14  37641  mblfinlem2  37665  fzmul  37748  incsequz  37755  geomcau  37766  heibor1lem  37816  bfplem2  37830  lcmfunnnd  42013  posbezout  42101  unitscyglem4  42199  metakunt16  42221  metakunt26  42231  dvdsexpnn  42368  dvdsexpnn0  42369  fimgmcyc  42544  fzsplit1nn0  42765  irrapxlem1  42833  pellexlem5  42844  rmynn  42968  jm2.24nn  42971  jm2.17c  42974  congrep  42985  congabseq  42986  acongrep  42992  acongeq  42995  jm2.18  43000  jm2.23  43008  jm2.20nn  43009  jm2.26lem3  43013  jm2.26  43014  jm2.15nn0  43015  jm2.16nn0  43016  jm2.27dlem2  43022  rmydioph  43026  jm3.1  43032  expdiophlem1  43033  expdioph  43035  idomodle  43203  proot1ex  43208  nznngen  44335  sumnnodd  45645  stoweidlem7  46022  stoweidlem17  46032  wallispilem4  46083  stirlinglem2  46090  stirlinglem3  46091  stirlinglem4  46092  stirlinglem12  46100  stirlinglem13  46101  stirlinglem14  46102  stirlinglem15  46103  stirlingr  46105  dirkertrigeqlem1  46113  fouriersw  46246  ovnsubaddlem1  46585  subsubelfzo0  47338  2ffzoeq  47339  difltmodne  47344  addmodne  47346  submodlt  47352  iccpartres  47405  iccpartipre  47408  iccpartltu  47412  iccelpart  47420  odz2prm2pw  47550  fmtnoprmfac2lem1  47553  2pwp1prm  47576  lighneallem2  47593  lighneallem4  47597  lighneal  47598  proththd  47601  nneoALTV  47659  divgcdoddALTV  47669  fpprmod  47714  fppr2odd  47718  dfwppr  47725  fpprwppr  47726  fpprwpprb  47727  gbowge7  47750  gbege6  47752  ceilhalfelfzo1  48016  2tceilhalfelfzo1  48018  gpg3kgrtriexlem2  48040  gpg3kgrtriexlem3  48041  gpg3kgrtriexlem5  48043  gpg3kgrtriexlem6  48044  altgsumbc  48268  altgsumbcALT  48269  pw2m1lepw2m1  48437  nnpw2even  48450  nnlog2ge0lt1  48487  logbpw2m1  48488  blenpw2m1  48500  nnpw2blenfzo  48502  nnpw2pmod  48504  nnpw2p  48507  blengt1fldiv2p1  48514  dignn0fr  48522  dignn0flhalflem1  48536  dignn0flhalflem2  48537  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541