Theorem nnz 12481

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

Syntax hints:   → wi 4   ∨ w3o 1085   = wceq 1541   ∈ wcel 2110  ℝcr 10997  0cc0 10998  -cneg 11337  ℕcn 12117  ℤcz 12460

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 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7663  ax-1cn 11056  ax-icn 11057  ax-addcl 11058  ax-addrcl 11059  ax-mulcl 11060  ax-mulrcl 11061  ax-i2m1 11066  ax-1ne0 11067  ax-rrecex 11070  ax-cnre 11071

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 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3345  df-rab 3394  df-v 3436  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-pss 3920  df-nul 4282  df-if 4474  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6244  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6433  df-fun 6479  df-fn 6480  df-f 6481  df-f1 6482  df-fo 6483  df-f1o 6484  df-fv 6485  df-ov 7344  df-om 7792  df-2nd 7917  df-frecs 8206  df-wrecs 8237  df-recs 8286  df-rdg 8324  df-neg 11339  df-nn 12118  df-z 12461

This theorem is referenced by:  nnssz  12482  elnnz1  12490  znegcl  12499  nnleltp1  12520  nnltp1le  12521  nnlem1lt  12531  nnltlem1  12532  nnm1ge0  12533  prime  12546  nneo  12549  zeo  12551  btwnz  12568  eluz2b2  12811  qaddcl  12855  qreccl  12859  elpqb  12866  elfz1end  13446  fznatpl1  13470  fznn  13484  elfz1b  13485  elfzo0  13592  elfzo0z  13593  elfzo1  13604  fzo1fzo0n0  13607  elfzom1p1elfzo  13637  ubmelm1fzo  13655  quoremz  13751  intfracq  13755  fznnfl  13758  zmodcl  13787  zmodfz  13789  zmodfzo  13790  zmodid2  13795  zmodidfzo  13796  modfzo0difsn  13842  expnnval  13963  mulexpz  14001  nnesq  14126  expnlbnd  14132  expnlbnd2  14133  digit2  14135  faclbnd  14189  bc0k  14210  bcval5  14217  fz1isolem  14360  seqcoll  14363  ccatval21sw  14485  lswccatn0lsw  14491  cshwidxmod  14702  cshwidxn  14708  absexpz  15204  climuni  15451  isercoll  15567  climcnds  15750  arisum  15759  trireciplem  15761  expcnv  15763  pwdif  15767  geo2sum  15772  geo2lim  15774  0.999...  15780  geoihalfsum  15781  rpnnen2lem6  16120  rpnnen2lem9  16123  rpnnen2lem10  16124  dvdsval3  16159  nndivdvds  16164  modmulconst  16191  dvdsle  16213  dvdsssfz1  16221  fzm1ndvds  16225  dvdsfac  16229  mulmoddvds  16233  oexpneg  16248  nnoddm1d2  16289  pwp1fsum  16294  divalg2  16308  divalgmod  16309  modremain  16311  ndvdsadd  16313  nndvdslegcd  16408  divgcdz  16414  divgcdnn  16418  divgcdnnr  16419  modgcd  16435  gcdmultiple  16439  gcddiv  16454  gcdzeq  16455  gcdeq  16456  rpmulgcd  16460  rplpwr  16461  rprpwr  16462  nn0rppwr  16464  sqgcd  16465  nn0expgcd  16467  dvdssqlem  16469  dvdssq  16470  eucalginv  16487  lcmgcdlem  16509  lcmgcdnn  16514  lcmass  16517  lcmftp  16539  lcmfunsnlem2lem1  16541  coprmgcdb  16552  qredeq  16560  qredeu  16561  coprmprod  16564  coprmproddvdslem  16565  coprmproddvds  16566  cncongr1  16570  cncongr2  16571  1idssfct  16583  isprm2lem  16584  isprm3  16586  prmind2  16588  ge2nprmge4  16604  divgcdodd  16613  isprm6  16617  ncoprmlnprm  16631  divnumden  16651  divdenle  16652  nn0gcdsq  16655  phicl2  16671  phiprmpw  16679  eulerthlem2  16685  hashgcdlem  16691  hashgcdeq  16693  phisum  16694  nnoddn2prm  16715  pythagtriplem3  16722  pythagtriplem4  16723  pythagtriplem6  16725  pythagtriplem7  16726  pythagtriplem8  16727  pythagtriplem9  16728  pythagtriplem11  16729  pythagtriplem13  16731  pythagtriplem15  16733  pythagtriplem19  16737  pythagtrip  16738  iserodd  16739  pclem  16742  pccl  16753  pcdiv  16756  pcqcl  16760  pcdvds  16768  pcndvds  16770  pcndvds2  16772  pcelnn  16774  pcz  16785  pcmpt  16796  fldivp1  16801  pcfac  16803  infpnlem1  16814  prmunb  16818  prmreclem1  16820  1arith  16831  ram0  16926  prmdvdsprmo  16946  prmgaplem4  16958  prmgaplem6  16960  prmgaplem7  16961  cshwshashlem2  17000  setsstruct2  17077  mulgnn  18980  mulgaddcom  19003  mulginvcom  19004  mulgmodid  19018  ghmmulg  19133  dfod2  19469  gexdvds  19489  gexnnod  19493  gexex  19758  mulgass2  20220  qsssubdrg  21356  prmirredlem  21402  znidomb  21491  znrrg  21495  chfacfisf  22762  chfacfisfcpmat  22763  chfacfscmul0  22766  chfacfpmmul0  22770  cayhamlem1  22774  cpmadugsumlemF  22784  lmmo  23288  1stckgenlem  23461  imasdsf1olem  24281  clmmulg  25021  cmetcaulem  25208  ovolunlem1a  25417  ovolicc2lem4  25441  mbfi1fseqlem6  25641  dvexp3  25902  dgreq0  26191  elqaalem2  26248  aaliou3lem1  26270  aaliou3lem2  26271  aaliou3lem3  26272  aaliou3lem9  26278  pserdvlem2  26358  logtayl2  26591  root1eq1  26685  root1cj  26686  zrtdvds  26689  logbgcd1irr  26724  atantayl2  26868  birthdaylem2  26882  birthdaylem3  26883  emcllem5  26930  basellem2  27012  basellem3  27013  basellem5  27015  issqf  27066  sgmnncl  27077  prmorcht  27108  mumullem1  27109  mumullem2  27110  sqff1o  27112  dvdsflsumcom  27118  muinv  27123  vmalelog  27136  chtublem  27142  vmasum  27147  logfac2  27148  logfaclbnd  27153  bclbnd  27211  bposlem5  27219  lgsval4a  27250  lgssq2  27269  lgsdchr  27286  gausslemma2dlem0c  27289  gausslemma2dlem0e  27291  gausslemma2dlem1a  27296  gausslemma2dlem5  27302  lgsquadlem1  27311  lgsquadlem2  27312  lgsquad3  27318  2lgslem1a1  27320  2lgslem3  27335  2lgsoddprm  27347  2sqnn  27370  2sqreunnltlem  27381  rplogsumlem1  27415  rplogsumlem2  27416  dchrisumlem2  27421  dchrmusumlema  27424  dchrmusum2  27425  dchrvmasumiflem1  27432  dchrvmaeq0  27435  dchrisum0flblem2  27440  dchrisum0re  27444  dchrisum0lema  27445  dchrisum0lem1b  27446  dchrisum0lem2a  27448  logdivbnd  27487  pntrsumbnd2  27498  ostth2lem1  27549  ostth2lem3  27566  ostth3  27569  axlowdimlem13  28925  crctcshwlkn0lem4  29784  crctcshwlkn0lem5  29785  crctcshwlkn0lem7  29787  wlkiswwlksupgr2  29848  clwwisshclwwslem  29984  clwwlkinwwlk  30010  clwwlkel  30016  clwwlkf  30017  wwlksubclwwlk  30028  clwwlkvbij  30083  eucrctshift  30213  eucrct2eupth  30215  numclwlk2lem2f  30347  bcm1n  32767  pnfinf  33142  isarchiofld  33158  1fldgenq  33278  rearchi  33301  submat1n  33808  lmatfvlem  33818  esumcvg  34089  oddpwdc  34357  fibp1  34404  chtvalz  34632  nnltp1ne  35123  erdszelem7  35209  climuzcnv  35683  elfzm12  35687  bcprod  35750  nn0prpwlem  36335  knoppndvlem1  36525  knoppndvlem2  36526  knoppndvlem7  36531  knoppndvlem18  36542  poimirlem13  37652  poimirlem14  37653  mblfinlem2  37677  fzmul  37760  incsequz  37767  geomcau  37778  heibor1lem  37828  bfplem2  37842  lcmfunnnd  42024  posbezout  42112  unitscyglem4  42210  dvdsexpnn  42345  dvdsexpnn0  42346  fimgmcyc  42546  fzsplit1nn0  42766  irrapxlem1  42834  pellexlem5  42845  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  44328  sumnnodd  45649  stoweidlem7  46024  stoweidlem17  46034  wallispilem4  46085  stirlinglem2  46092  stirlinglem3  46093  stirlinglem4  46094  stirlinglem12  46102  stirlinglem13  46103  stirlinglem14  46104  stirlinglem15  46105  stirlingr  46107  dirkertrigeqlem1  46115  fouriersw  46248  ovnsubaddlem1  46587  subsubelfzo0  47336  2ffzoeq  47337  ceilhalfelfzo1  47340  2tceilhalfelfzo1  47342  difltmodne  47352  addmodne  47354  submodlt  47360  iccpartres  47428  iccpartipre  47431  iccpartltu  47435  iccelpart  47443  odz2prm2pw  47573  fmtnoprmfac2lem1  47576  2pwp1prm  47599  lighneallem2  47616  lighneallem4  47620  lighneal  47621  proththd  47624  nneoALTV  47682  divgcdoddALTV  47692  fpprmod  47737  fppr2odd  47741  dfwppr  47748  fpprwppr  47749  fpprwpprb  47750  gbowge7  47773  gbege6  47775  gpg3kgrtriexlem2  48094  gpg3kgrtriexlem3  48095  gpg3kgrtriexlem5  48097  gpg3kgrtriexlem6  48098  altgsumbc  48362  altgsumbcALT  48363  pw2m1lepw2m1  48531  nnpw2even  48540  nnlog2ge0lt1  48577  logbpw2m1  48578  blenpw2m1  48590  nnpw2blenfzo  48592  nnpw2pmod  48594  nnpw2p  48597  blengt1fldiv2p1  48604  dignn0fr  48612  dignn0flhalflem1  48626  dignn0flhalflem2  48627  nn0sumshdiglemA  48630  nn0sumshdiglemB  48631