Theorem nnz 12550

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

Syntax hints:   → wi 4   ∨ w3o 1085   = wceq 1540   ∈ wcel 2109  ℝcr 11067  0cc0 11068  -cneg 11406  ℕcn 12186  ℤcz 12529

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rrecex 11140  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-neg 11408  df-nn 12187  df-z 12530

This theorem is referenced by:  nnssz  12551  elnnz1  12559  znegcl  12568  nnleltp1  12589  nnltp1le  12590  nnlem1lt  12600  nnltlem1  12601  nnm1ge0  12602  prime  12615  nneo  12618  zeo  12620  btwnz  12637  eluz2b2  12880  qaddcl  12924  qreccl  12928  elpqb  12935  elfz1end  13515  fznatpl1  13539  fznn  13553  elfz1b  13554  elfzo0  13661  elfzo0z  13662  elfzo1  13673  fzo1fzo0n0  13676  elfzom1p1elfzo  13706  ubmelm1fzo  13724  quoremz  13817  intfracq  13821  fznnfl  13824  zmodcl  13853  zmodfz  13855  zmodfzo  13856  zmodid2  13861  zmodidfzo  13862  modfzo0difsn  13908  expnnval  14029  mulexpz  14067  nnesq  14192  expnlbnd  14198  expnlbnd2  14199  digit2  14201  faclbnd  14255  bc0k  14276  bcval5  14283  fz1isolem  14426  seqcoll  14429  ccatval21sw  14550  lswccatn0lsw  14556  cshwidxmod  14768  cshwidxn  14774  absexpz  15271  climuni  15518  isercoll  15634  climcnds  15817  arisum  15826  trireciplem  15828  expcnv  15830  pwdif  15834  geo2sum  15839  geo2lim  15841  0.999...  15847  geoihalfsum  15848  rpnnen2lem6  16187  rpnnen2lem9  16190  rpnnen2lem10  16191  dvdsval3  16226  nndivdvds  16231  modmulconst  16258  dvdsle  16280  dvdsssfz1  16288  fzm1ndvds  16292  dvdsfac  16296  mulmoddvds  16300  oexpneg  16315  nnoddm1d2  16356  pwp1fsum  16361  divalg2  16375  divalgmod  16376  modremain  16378  ndvdsadd  16380  nndvdslegcd  16475  divgcdz  16481  divgcdnn  16485  divgcdnnr  16486  modgcd  16502  gcdmultiple  16506  gcddiv  16521  gcdzeq  16522  gcdeq  16523  rpmulgcd  16527  rplpwr  16528  rprpwr  16529  nn0rppwr  16531  sqgcd  16532  nn0expgcd  16534  dvdssqlem  16536  dvdssq  16537  eucalginv  16554  lcmgcdlem  16576  lcmgcdnn  16581  lcmass  16584  lcmftp  16606  lcmfunsnlem2lem1  16608  coprmgcdb  16619  qredeq  16627  qredeu  16628  coprmprod  16631  coprmproddvdslem  16632  coprmproddvds  16633  cncongr1  16637  cncongr2  16638  1idssfct  16650  isprm2lem  16651  isprm3  16653  prmind2  16655  ge2nprmge4  16671  divgcdodd  16680  isprm6  16684  ncoprmlnprm  16698  divnumden  16718  divdenle  16719  nn0gcdsq  16722  phicl2  16738  phiprmpw  16746  eulerthlem2  16752  hashgcdlem  16758  hashgcdeq  16760  phisum  16761  nnoddn2prm  16782  pythagtriplem3  16789  pythagtriplem4  16790  pythagtriplem6  16792  pythagtriplem7  16793  pythagtriplem8  16794  pythagtriplem9  16795  pythagtriplem11  16796  pythagtriplem13  16798  pythagtriplem15  16800  pythagtriplem19  16804  pythagtrip  16805  iserodd  16806  pclem  16809  pccl  16820  pcdiv  16823  pcqcl  16827  pcdvds  16835  pcndvds  16837  pcndvds2  16839  pcelnn  16841  pcz  16852  pcmpt  16863  fldivp1  16868  pcfac  16870  infpnlem1  16881  prmunb  16885  prmreclem1  16887  1arith  16898  ram0  16993  prmdvdsprmo  17013  prmgaplem4  17025  prmgaplem6  17027  prmgaplem7  17028  cshwshashlem2  17067  setsstruct2  17144  mulgnn  19007  mulgaddcom  19030  mulginvcom  19031  mulgmodid  19045  ghmmulg  19160  dfod2  19494  gexdvds  19514  gexnnod  19518  gexex  19783  mulgass2  20218  qsssubdrg  21343  prmirredlem  21382  znidomb  21471  znrrg  21475  chfacfisf  22741  chfacfisfcpmat  22742  chfacfscmul0  22745  chfacfpmmul0  22749  cayhamlem1  22753  cpmadugsumlemF  22763  lmmo  23267  1stckgenlem  23440  imasdsf1olem  24261  clmmulg  25001  cmetcaulem  25188  ovolunlem1a  25397  ovolicc2lem4  25421  mbfi1fseqlem6  25621  dvexp3  25882  dgreq0  26171  elqaalem2  26228  aaliou3lem1  26250  aaliou3lem2  26251  aaliou3lem3  26252  aaliou3lem9  26258  pserdvlem2  26338  logtayl2  26571  root1eq1  26665  root1cj  26666  zrtdvds  26669  logbgcd1irr  26704  atantayl2  26848  birthdaylem2  26862  birthdaylem3  26863  emcllem5  26910  basellem2  26992  basellem3  26993  basellem5  26995  issqf  27046  sgmnncl  27057  prmorcht  27088  mumullem1  27089  mumullem2  27090  sqff1o  27092  dvdsflsumcom  27098  muinv  27103  vmalelog  27116  chtublem  27122  vmasum  27127  logfac2  27128  logfaclbnd  27133  bclbnd  27191  bposlem5  27199  lgsval4a  27230  lgssq2  27249  lgsdchr  27266  gausslemma2dlem0c  27269  gausslemma2dlem0e  27271  gausslemma2dlem1a  27276  gausslemma2dlem5  27282  lgsquadlem1  27291  lgsquadlem2  27292  lgsquad3  27298  2lgslem1a1  27300  2lgslem3  27315  2lgsoddprm  27327  2sqnn  27350  2sqreunnltlem  27361  rplogsumlem1  27395  rplogsumlem2  27396  dchrisumlem2  27401  dchrmusumlema  27404  dchrmusum2  27405  dchrvmasumiflem1  27412  dchrvmaeq0  27415  dchrisum0flblem2  27420  dchrisum0re  27424  dchrisum0lema  27425  dchrisum0lem1b  27426  dchrisum0lem2a  27428  logdivbnd  27467  pntrsumbnd2  27478  ostth2lem1  27529  ostth2lem3  27546  ostth3  27549  axlowdimlem13  28881  crctcshwlkn0lem4  29743  crctcshwlkn0lem5  29744  crctcshwlkn0lem7  29746  wlkiswwlksupgr2  29807  clwwisshclwwslem  29943  clwwlkinwwlk  29969  clwwlkel  29975  clwwlkf  29976  wwlksubclwwlk  29987  clwwlkvbij  30042  eucrctshift  30172  eucrct2eupth  30174  numclwlk2lem2f  30306  bcm1n  32718  pnfinf  33137  1fldgenq  33272  isarchiofld  33295  rearchi  33317  submat1n  33795  lmatfvlem  33805  esumcvg  34076  oddpwdc  34345  fibp1  34392  chtvalz  34620  nnltp1ne  35098  erdszelem7  35184  climuzcnv  35658  elfzm12  35662  bcprod  35725  nn0prpwlem  36310  knoppndvlem1  36500  knoppndvlem2  36501  knoppndvlem7  36506  knoppndvlem18  36517  poimirlem13  37627  poimirlem14  37628  mblfinlem2  37652  fzmul  37735  incsequz  37742  geomcau  37753  heibor1lem  37803  bfplem2  37817  lcmfunnnd  42000  posbezout  42088  unitscyglem4  42186  dvdsexpnn  42321  dvdsexpnn0  42322  fimgmcyc  42522  fzsplit1nn0  42742  irrapxlem1  42810  pellexlem5  42821  rmynn  42945  jm2.24nn  42948  jm2.17c  42951  congrep  42962  congabseq  42963  acongrep  42969  acongeq  42972  jm2.18  42977  jm2.23  42985  jm2.20nn  42986  jm2.26lem3  42990  jm2.26  42991  jm2.15nn0  42992  jm2.16nn0  42993  jm2.27dlem2  42999  rmydioph  43003  jm3.1  43009  expdiophlem1  43010  expdioph  43012  idomodle  43180  proot1ex  43185  nznngen  44305  sumnnodd  45628  stoweidlem7  46005  stoweidlem17  46015  wallispilem4  46066  stirlinglem2  46073  stirlinglem3  46074  stirlinglem4  46075  stirlinglem12  46083  stirlinglem13  46084  stirlinglem14  46085  stirlinglem15  46086  stirlingr  46088  dirkertrigeqlem1  46096  fouriersw  46229  ovnsubaddlem1  46568  subsubelfzo0  47327  2ffzoeq  47328  ceilhalfelfzo1  47331  2tceilhalfelfzo1  47333  difltmodne  47343  addmodne  47345  submodlt  47351  iccpartres  47419  iccpartipre  47422  iccpartltu  47426  iccelpart  47434  odz2prm2pw  47564  fmtnoprmfac2lem1  47567  2pwp1prm  47590  lighneallem2  47607  lighneallem4  47611  lighneal  47612  proththd  47615  nneoALTV  47673  divgcdoddALTV  47683  fpprmod  47728  fppr2odd  47732  dfwppr  47739  fpprwppr  47740  fpprwpprb  47741  gbowge7  47764  gbege6  47766  gpg3kgrtriexlem2  48075  gpg3kgrtriexlem3  48076  gpg3kgrtriexlem5  48078  gpg3kgrtriexlem6  48079  altgsumbc  48340  altgsumbcALT  48341  pw2m1lepw2m1  48509  nnpw2even  48518  nnlog2ge0lt1  48555  logbpw2m1  48556  blenpw2m1  48568  nnpw2blenfzo  48570  nnpw2pmod  48572  nnpw2p  48575  blengt1fldiv2p1  48582  dignn0fr  48590  dignn0flhalflem1  48604  dignn0flhalflem2  48605  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609