Theorem nnz 12744

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 12372	. 2 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
2		3mix2 1350	. 2 ⊢ (𝑁 ∈ ℕ → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
3		elz 12725	. 2 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
4	1, 2, 3	sylanbrc 595	1 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1102   = wceq 1570   ∈ wcel 2147  ℝcr 11229  0cc0 11230   -cneg 11572  ℕcn 12365  ℤcz 12723

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pr 5396  ax-un 7778  ax-1cn 11288  ax-icn 11289  ax-addcl 11290  ax-addrcl 11291  ax-mulcl 11292  ax-mulrcl 11293  ax-i2m1 11298  ax-1ne0 11299  ax-rrecex 11302  ax-cnre 11303

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5551  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-we 5611  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-pred 6325  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7449  df-om 7905  df-2nd 8029  df-frecs 8330  df-wrecs 8361  df-recs 8410  df-rdg 8449  df-neg 11574  df-nn 12366  df-z 12724

This theorem is used by:  nnssz  12745  elnnz1  12752  znegcl  12761  nnleltp1  12784  nnltp1le  12785  nnlem1lt  12795  nnltlem1  12796  nnm1ge0  12797  prime  12810  nneo  12813  zeo  12815  btwnz  12832  eluz2b2  13078  qaddcl  13123  qreccl  13127  elpqb  13134  elfz1end  13718  fznatpl1  13742  fznn  13756  elfz1b  13757  elfzo0  13865  elfzo0z  13866  elfzo1  13877  fzo1fzo0n0  13880  elfzom1p1elfzo  13910  ubmelm1fzo  13928  quoremz  14025  intfracq  14029  fznnfl  14032  zmodcl  14061  zmodfz  14063  zmodfzo  14064  zmodid2  14069  zmodidfzo  14070  modfzo0difsn  14116  expnnval  14237  mulexpz  14275  nnesq  14401  expnlbnd  14407  expnlbnd2  14408  digit2  14410  faclbnd  14464  bc0k  14485  bcval5  14492  fz1isolem  14636  seqcoll  14639  ccatval21sw  14761  lswccatn0lsw  14768  cshwidxmod  14985  cshwidxn  14991  absexpz  15504  climuni  15751  isercoll  15867  climcnds  16052  arisum  16061  trireciplem  16063  expcnv  16065  pwdif  16069  geo2sum  16074  geo2lim  16076  0.999...  16082  geoihalfsum  16083  rpnnen2lem6  16419  rpnnen2lem9  16422  rpnnen2lem10  16423  dvdsval3  16458  nndivdvds  16463  modmulconst  16490  dvdsle  16512  dvdsssfz1  16520  fzm1ndvds  16524  dvdsfac  16528  mulmoddvds  16532  oexpneg  16547  nnoddm1d2  16588  pwp1fsum  16593  divalg2  16607  divalgmod  16608  modremain  16610  ndvdsadd  16612  nndvdslegcd  16707  divgcdz  16715  divgcdnn  16719  divgcdnnr  16720  modgcd  16737  gcdmultiple  16741  gcddiv  16756  gcdzeq  16757  gcdeq  16758  rpmulgcd  16763  rplpwr  16764  rprpwr  16765  nn0rppwr  16767  sqgcd  16768  nn0expgcd  16770  dvdsexpnn  16772  dvdssq  16774  eucalginv  16791  lcmgcdlem  16813  lcmgcdnn  16818  lcmass  16821  lcmftp  16843  lcmfunsnlem2lem1  16845  coprmgcdb  16856  qredeq  16864  qredeu  16865  coprmprod  16868  coprmproddvdslem  16869  coprmproddvds  16870  cncongr1  16874  cncongr2  16875  1idssfct  16887  isprm2lem  16888  isprm3  16890  prmind2  16892  ge2nprmge4  16909  divgcdodd  16918  isprm6  16922  ncoprmlnprm  16936  divnumden  16956  divdenle  16957  nn0gcdsq  16960  phicl2  16977  phiprmpw  16985  eulerthlem2  16991  hashgcdlem  16997  hashgcdeq  16999  phisum  17000  nnoddn2prm  17021  pythagtriplem3  17028  pythagtriplem4  17029  pythagtriplem6  17031  pythagtriplem7  17032  pythagtriplem8  17033  pythagtriplem9  17034  pythagtriplem11  17035  pythagtriplem13  17037  pythagtriplem15  17039  pythagtriplem19  17043  pythagtrip  17044  iserodd  17045  pclem  17048  pccl  17059  pcdiv  17062  pcqcl  17066  pcdvds  17074  pcndvds  17076  pcndvds2  17078  pcelnn  17080  pcz  17091  pcmpt  17102  fldivp1  17107  pcfac  17109  infpnlem1  17120  prmunb  17124  prmreclem1  17126  1arith  17137  ram0  17232  prmdvdsprmo  17252  prmgaplem4  17264  prmgaplem6  17266  prmgaplem7  17267  cshwshashlem2  17306  setsstruct2  17384  mulgnn  19317  mulgaddcom  19340  mulginvcom  19341  mulgmodid  19355  ghmmulg  19474  dfod2  19811  gexdvds  19831  gexnnod  19835  gexex  20100  mulgass2  20573  qsssubdrg  21765  prmirredlem  21811  znidomb  21900  znrrg  21904  chfacfisf  23205  chfacfisfcpmat  23206  chfacfscmul0  23209  chfacfpmmul0  23213  cayhamlem1  23217  cpmadugsumlemF  23227  lmmo  23731  1stckgenlem  23905  imasdsf1olem  24725  clmmulg  25455  cmetcaulem  25642  ovolunlem1a  25850  ovolicc2lem4  25874  mbfi1fseqlem6  26074  dvexp3  26331  dgreq0  26617  elqaalem2  26676  aaliou3lem1  26702  aaliou3lem2  26703  aaliou3lem3  26704  aaliou3lem9  26710  pserdvlem2  26788  logtayl2  27023  root1eq1  27116  root1cj  27117  zrtdvds  27120  logbgcd1irr  27155  atantayl2  27299  birthdaylem2  27313  birthdaylem3  27314  emcllem5  27360  basellem2  27442  basellem3  27443  basellem5  27445  issqf  27496  sgmnncl  27507  prmorcht  27538  mumullem1  27539  mumullem2  27540  sqff1o  27542  dvdsflsumcom  27548  muinv  27553  vmalelog  27565  chtublem  27571  vmasum  27576  logfac2  27577  logfaclbnd  27582  bclbnd  27640  bposlem5  27648  lgsval4a  27679  lgssq2  27698  lgsdchr  27715  gausslemma2dlem0c  27718  gausslemma2dlem0e  27720  gausslemma2dlem1a  27725  gausslemma2dlem5  27731  lgsquadlem1  27740  lgsquadlem2  27741  lgsquad3  27747  2lgslem1a1  27749  2lgslem3  27764  2lgsoddprm  27776  2sqnn  27799  2sqreunnltlem  27810  rplogsumlem1  27844  rplogsumlem2  27845  dchrisumlem2  27850  dchrmusumlema  27853  dchrmusum2  27854  dchrvmasumiflem1  27861  dchrvmaeq0  27864  dchrisum0flblem2  27869  dchrisum0re  27873  dchrisum0lema  27874  dchrisum0lem1b  27875  dchrisum0lem2a  27877  logdivbnd  27916  pntrsumbnd2  27927  ostth2lem1  27978  ostth2lem3  27995  ostth3  27998  axlowdimlem13  29565  crctcshwlkn0lem4  30435  crctcshwlkn0lem5  30436  crctcshwlkn0lem7  30438  wlkiswwlksupgr2  30499  clwwisshclwwslem  30638  clwwlkinwwlk  30664  clwwlkel  30670  clwwlkf  30671  wwlksubclwwlk  30682  clwwlkvbij  30737  eucrctshift  30877  eucrct2eupth  30879  numclwlk2lem2f  31011  bcm1n  33460  pnfinf  33820  isarchiofld  33836  1fldgenq  33968  rearchi  33991  submat1n  34520  lmatfvlem  34530  esumcvg  34801  oddpwdc  35069  fibp1  35116  chtvalz  35341  nnltp1ne  36071  erdszelem7  36142  climuzcnv  36616  elfzm12  36620  bcprod  36694  nn0prpwlem  37301  knoppndvlem1  37569  knoppndvlem2  37570  knoppndvlem7  37575  knoppndvlem18  37586  poimirlem13  38756  poimirlem14  38757  mblfinlem2  38781  fzmul  38878  incsequz  38885  geomcau  38896  heibor1lem  38946  bfplem2  38960  lcmfunnnd  43265  posbezout  43353  unitscyglem4  43451  dvdsexpnn0  43590  fimgmcyc  43802  fzsplit1nn0  43969  irrapxlem1  44033  pellexlem5  44044  rmynn  44167  jm2.24nn  44170  jm2.17c  44173  congrep  44184  congabseq  44185  acongrep  44191  acongeq  44194  jm2.18  44199  jm2.23  44207  jm2.20nn  44208  jm2.26lem3  44212  jm2.26  44213  jm2.15nn0  44214  jm2.16nn0  44215  jm2.27dlem2  44221  rmydioph  44225  jm3.1  44231  expdiophlem1  44232  expdioph  44234  idomodle  44396  proot1ex  44401  nznngen  45503  sumnnodd  46857  stoweidlem7  47232  stoweidlem17  47242  wallispilem4  47293  stirlinglem2  47300  stirlinglem3  47301  stirlinglem4  47302  stirlinglem12  47310  stirlinglem13  47311  stirlinglem14  47312  stirlinglem15  47313  stirlingr  47315  dirkertrigeqlem1  47323  fouriersw  47456  ovnsubaddlem1  47795  sqrtnnaa  48128  subsubelfzo0  48612  2ffzoeq  48613  nnmul2  48615  ceilhalfelfzo1  48619  2tceilhalfelfzo1  48621  difltmodne  48633  addmodne  48635  submodlt  48641  facnn0dvdsfac  48670  muldvdsfacgt  48671  iccpartres  48715  iccpartipre  48718  iccpartltu  48722  iccelpart  48730  odz2prm2pw  48863  fmtnoprmfac2lem1  48866  2pwp1prm  48889  lighneallem2  48906  lighneallem4  48910  lighneal  48911  proththd  48914  nneoALTV  48985  divgcdoddALTV  48995  fpprmod  49040  fppr2odd  49044  dfwppr  49051  fpprwppr  49052  fpprwpprb  49053  gbowge7  49076  gbege6  49078  gpg3kgrtriexlem2  49397  gpg3kgrtriexlem3  49398  gpg3kgrtriexlem5  49400  gpg3kgrtriexlem6  49401  altgsumbc  49679  altgsumbcALT  49680  pw2m1lepw2m1  49847  nnpw2even  49856  nnlog2ge0lt1  49893  logbpw2m1  49894  blenpw2m1  49906  nnpw2blenfzo  49908  nnpw2pmod  49910  nnpw2p  49913  blengt1fldiv2p1  49920  dignn0fr  49928  dignn0flhalflem1  49942  dignn0flhalflem2  49943  nn0sumshdiglemA  49946  nn0sumshdiglemB  49947