Theorem nnz 12718

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

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1102   = wceq 1569   ∈ wcel 2144  ℝcr 11203  0cc0 11204   -cneg 11546  ℕcn 12339  ℤcz 12697

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7752  ax-1cn 11262  ax-icn 11263  ax-addcl 11264  ax-addrcl 11265  ax-mulcl 11266  ax-mulrcl 11267  ax-i2m1 11272  ax-1ne0 11273  ax-rrecex 11276  ax-cnre 11277

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-ov 7424  df-om 7879  df-2nd 8003  df-frecs 8303  df-wrecs 8334  df-recs 8383  df-rdg 8422  df-neg 11548  df-nn 12340  df-z 12698

This theorem is used by:  nnssz  12719  elnnz1  12726  znegcl  12735  nnleltp1  12758  nnltp1le  12759  nnlem1lt  12769  nnltlem1  12770  nnm1ge0  12771  prime  12784  nneo  12787  zeo  12789  btwnz  12806  eluz2b2  13052  qaddcl  13097  qreccl  13101  elpqb  13108  elfz1end  13692  fznatpl1  13716  fznn  13730  elfz1b  13731  elfzo0  13839  elfzo0z  13840  elfzo1  13851  fzo1fzo0n0  13854  elfzom1p1elfzo  13884  ubmelm1fzo  13902  quoremz  13999  intfracq  14003  fznnfl  14006  zmodcl  14035  zmodfz  14037  zmodfzo  14038  zmodid2  14043  zmodidfzo  14044  modfzo0difsn  14090  expnnval  14211  mulexpz  14249  nnesq  14375  expnlbnd  14381  expnlbnd2  14382  digit2  14384  faclbnd  14438  bc0k  14459  bcval5  14466  fz1isolem  14610  seqcoll  14613  ccatval21sw  14735  lswccatn0lsw  14742  cshwidxmod  14959  cshwidxn  14965  absexpz  15478  climuni  15725  isercoll  15841  climcnds  16026  arisum  16035  trireciplem  16037  expcnv  16039  pwdif  16043  geo2sum  16048  geo2lim  16050  0.999...  16056  geoihalfsum  16057  rpnnen2lem6  16393  rpnnen2lem9  16396  rpnnen2lem10  16397  dvdsval3  16432  nndivdvds  16437  modmulconst  16464  dvdsle  16486  dvdsssfz1  16494  fzm1ndvds  16498  dvdsfac  16502  mulmoddvds  16506  oexpneg  16521  nnoddm1d2  16562  pwp1fsum  16567  divalg2  16581  divalgmod  16582  modremain  16584  ndvdsadd  16586  nndvdslegcd  16681  divgcdz  16689  divgcdnn  16693  divgcdnnr  16694  modgcd  16711  gcdmultiple  16715  gcddiv  16730  gcdzeq  16731  gcdeq  16732  rpmulgcd  16737  rplpwr  16738  rprpwr  16739  nn0rppwr  16741  sqgcd  16742  nn0expgcd  16744  dvdsexpnn  16746  dvdssq  16748  eucalginv  16765  lcmgcdlem  16787  lcmgcdnn  16792  lcmass  16795  lcmftp  16817  lcmfunsnlem2lem1  16819  coprmgcdb  16830  qredeq  16838  qredeu  16839  coprmprod  16842  coprmproddvdslem  16843  coprmproddvds  16844  cncongr1  16848  cncongr2  16849  1idssfct  16861  isprm2lem  16862  isprm3  16864  prmind2  16866  ge2nprmge4  16883  divgcdodd  16892  isprm6  16896  ncoprmlnprm  16910  divnumden  16930  divdenle  16931  nn0gcdsq  16934  phicl2  16951  phiprmpw  16959  eulerthlem2  16965  hashgcdlem  16971  hashgcdeq  16973  phisum  16974  nnoddn2prm  16995  pythagtriplem3  17002  pythagtriplem4  17003  pythagtriplem6  17005  pythagtriplem7  17006  pythagtriplem8  17007  pythagtriplem9  17008  pythagtriplem11  17009  pythagtriplem13  17011  pythagtriplem15  17013  pythagtriplem19  17017  pythagtrip  17018  iserodd  17019  pclem  17022  pccl  17033  pcdiv  17036  pcqcl  17040  pcdvds  17048  pcndvds  17050  pcndvds2  17052  pcelnn  17054  pcz  17065  pcmpt  17076  fldivp1  17081  pcfac  17083  infpnlem1  17094  prmunb  17098  prmreclem1  17100  1arith  17111  ram0  17206  prmdvdsprmo  17226  prmgaplem4  17238  prmgaplem6  17240  prmgaplem7  17241  cshwshashlem2  17280  setsstruct2  17358  mulgnn  19291  mulgaddcom  19314  mulginvcom  19315  mulgmodid  19329  ghmmulg  19448  dfod2  19784  gexdvds  19804  gexnnod  19808  gexex  20073  mulgass2  20546  qsssubdrg  21738  prmirredlem  21784  znidomb  21873  znrrg  21877  chfacfisf  23178  chfacfisfcpmat  23179  chfacfscmul0  23182  chfacfpmmul0  23186  cayhamlem1  23190  cpmadugsumlemF  23200  lmmo  23704  1stckgenlem  23878  imasdsf1olem  24698  clmmulg  25428  cmetcaulem  25615  ovolunlem1a  25823  ovolicc2lem4  25847  mbfi1fseqlem6  26047  dvexp3  26304  dgreq0  26590  elqaalem2  26649  aaliou3lem1  26675  aaliou3lem2  26676  aaliou3lem3  26677  aaliou3lem9  26683  pserdvlem2  26761  logtayl2  26996  root1eq1  27089  root1cj  27090  zrtdvds  27093  logbgcd1irr  27128  atantayl2  27272  birthdaylem2  27286  birthdaylem3  27287  emcllem5  27333  basellem2  27415  basellem3  27416  basellem5  27418  issqf  27469  sgmnncl  27480  prmorcht  27511  mumullem1  27512  mumullem2  27513  sqff1o  27515  dvdsflsumcom  27521  muinv  27526  vmalelog  27538  chtublem  27544  vmasum  27549  logfac2  27550  logfaclbnd  27555  bclbnd  27613  bposlem5  27621  lgsval4a  27652  lgssq2  27671  lgsdchr  27688  gausslemma2dlem0c  27691  gausslemma2dlem0e  27693  gausslemma2dlem1a  27698  gausslemma2dlem5  27704  lgsquadlem1  27713  lgsquadlem2  27714  lgsquad3  27720  2lgslem1a1  27722  2lgslem3  27737  2lgsoddprm  27749  2sqnn  27772  2sqreunnltlem  27783  rplogsumlem1  27817  rplogsumlem2  27818  dchrisumlem2  27823  dchrmusumlema  27826  dchrmusum2  27827  dchrvmasumiflem1  27834  dchrvmaeq0  27837  dchrisum0flblem2  27842  dchrisum0re  27846  dchrisum0lema  27847  dchrisum0lem1b  27848  dchrisum0lem2a  27850  logdivbnd  27889  pntrsumbnd2  27900  ostth2lem1  27951  ostth2lem3  27968  ostth3  27971  axlowdimlem13  29538  crctcshwlkn0lem4  30408  crctcshwlkn0lem5  30409  crctcshwlkn0lem7  30411  wlkiswwlksupgr2  30472  clwwisshclwwslem  30611  clwwlkinwwlk  30637  clwwlkel  30643  clwwlkf  30644  wwlksubclwwlk  30655  clwwlkvbij  30710  eucrctshift  30850  eucrct2eupth  30852  numclwlk2lem2f  30984  bcm1n  33434  pnfinf  33791  isarchiofld  33807  1fldgenq  33931  rearchi  33954  submat1n  34484  lmatfvlem  34494  esumcvg  34765  oddpwdc  35033  fibp1  35080  chtvalz  35305  nnltp1ne  35978  erdszelem7  36049  climuzcnv  36523  elfzm12  36527  bcprod  36596  nn0prpwlem  37203  knoppndvlem1  37471  knoppndvlem2  37472  knoppndvlem7  37477  knoppndvlem18  37488  poimirlem13  38645  poimirlem14  38646  mblfinlem2  38670  fzmul  38769  incsequz  38776  geomcau  38787  heibor1lem  38837  bfplem2  38851  lcmfunnnd  43156  posbezout  43244  unitscyglem4  43342  dvdsexpnn0  43480  fimgmcyc  43692  fzsplit1nn0  43859  irrapxlem1  43923  pellexlem5  43934  rmynn  44057  jm2.24nn  44060  jm2.17c  44063  congrep  44074  congabseq  44075  acongrep  44081  acongeq  44084  jm2.18  44089  jm2.23  44097  jm2.20nn  44098  jm2.26lem3  44102  jm2.26  44103  jm2.15nn0  44104  jm2.16nn0  44105  jm2.27dlem2  44111  rmydioph  44115  jm3.1  44121  expdiophlem1  44122  expdioph  44124  idomodle  44287  proot1ex  44292  nznngen  45394  sumnnodd  46736  stoweidlem7  47111  stoweidlem17  47121  wallispilem4  47172  stirlinglem2  47179  stirlinglem3  47180  stirlinglem4  47181  stirlinglem12  47189  stirlinglem13  47190  stirlinglem14  47191  stirlinglem15  47192  stirlingr  47194  dirkertrigeqlem1  47202  fouriersw  47335  ovnsubaddlem1  47674  sqrtnnaa  48007  subsubelfzo0  48491  2ffzoeq  48492  nnmul2  48494  ceilhalfelfzo1  48498  2tceilhalfelfzo1  48500  difltmodne  48512  addmodne  48514  submodlt  48520  facnn0dvdsfac  48549  muldvdsfacgt  48550  iccpartres  48594  iccpartipre  48597  iccpartltu  48601  iccelpart  48609  odz2prm2pw  48742  fmtnoprmfac2lem1  48745  2pwp1prm  48768  lighneallem2  48785  lighneallem4  48789  lighneal  48790  proththd  48793  nneoALTV  48864  divgcdoddALTV  48874  fpprmod  48919  fppr2odd  48923  dfwppr  48930  fpprwppr  48931  fpprwpprb  48932  gbowge7  48955  gbege6  48957  gpg3kgrtriexlem2  49276  gpg3kgrtriexlem3  49277  gpg3kgrtriexlem5  49279  gpg3kgrtriexlem6  49280  altgsumbc  49558  altgsumbcALT  49559  pw2m1lepw2m1  49726  nnpw2even  49735  nnlog2ge0lt1  49772  logbpw2m1  49773  blenpw2m1  49785  nnpw2blenfzo  49787  nnpw2pmod  49789  nnpw2p  49792  blengt1fldiv2p1  49799  dignn0fr  49807  dignn0flhalflem1  49821  dignn0flhalflem2  49822  nn0sumshdiglemA  49825  nn0sumshdiglemB  49826