Theorem nnz 12613

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

Syntax hints:   → wi 4   ∨ w3o 1102   = wceq 1570   ∈ wcel 2143  ℝcr 11100  0cc0 11101  -cneg 11443  ℕcn 12234  ℤcz 12592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406  ax-un 7734  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-i2m1 11169  ax-1ne0 11170  ax-rrecex 11173  ax-cnre 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7415  df-om 7864  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-neg 11445  df-nn 12235  df-z 12593

This theorem is referenced by:  nnssz  12614  elnnz1  12621  znegcl  12630  nnleltp1  12652  nnltp1le  12653  nnlem1lt  12663  nnltlem1  12664  nnm1ge0  12665  prime  12678  nneo  12681  zeo  12683  btwnz  12700  eluz2b2  12946  qaddcl  12990  qreccl  12994  elpqb  13001  elfz1end  13584  fznatpl1  13608  fznn  13622  elfz1b  13623  elfzo0  13731  elfzo0z  13732  elfzo1  13743  fzo1fzo0n0  13746  elfzom1p1elfzo  13776  ubmelm1fzo  13794  quoremz  13890  intfracq  13894  fznnfl  13897  zmodcl  13926  zmodfz  13928  zmodfzo  13929  zmodid2  13934  zmodidfzo  13935  modfzo0difsn  13981  expnnval  14102  mulexpz  14140  nnesq  14265  expnlbnd  14271  expnlbnd2  14272  digit2  14274  faclbnd  14328  bc0k  14349  bcval5  14356  fz1isolem  14500  seqcoll  14503  ccatval21sw  14625  lswccatn0lsw  14631  cshwidxmod  14842  cshwidxn  14848  absexpz  15358  climuni  15605  isercoll  15721  climcnds  15907  arisum  15916  trireciplem  15918  expcnv  15920  pwdif  15924  geo2sum  15929  geo2lim  15931  0.999...  15937  geoihalfsum  15938  rpnnen2lem6  16276  rpnnen2lem9  16279  rpnnen2lem10  16280  dvdsval3  16315  nndivdvds  16320  modmulconst  16347  dvdsle  16369  dvdsssfz1  16377  fzm1ndvds  16381  dvdsfac  16385  mulmoddvds  16389  oexpneg  16404  nnoddm1d2  16445  pwp1fsum  16450  divalg2  16464  divalgmod  16465  modremain  16467  ndvdsadd  16469  nndvdslegcd  16564  divgcdz  16570  divgcdnn  16574  divgcdnnr  16575  modgcd  16591  gcdmultiple  16595  gcddiv  16610  gcdzeq  16611  gcdeq  16612  rpmulgcd  16616  rplpwr  16617  rprpwr  16618  nn0rppwr  16620  sqgcd  16621  nn0expgcd  16623  dvdssqlem  16625  dvdssq  16626  eucalginv  16643  lcmgcdlem  16665  lcmgcdnn  16670  lcmass  16673  lcmftp  16695  lcmfunsnlem2lem1  16697  coprmgcdb  16708  qredeq  16716  qredeu  16717  coprmprod  16720  coprmproddvdslem  16721  coprmproddvds  16722  cncongr1  16726  cncongr2  16727  1idssfct  16739  isprm2lem  16740  isprm3  16742  prmind2  16744  ge2nprmge4  16761  divgcdodd  16770  isprm6  16774  ncoprmlnprm  16788  divnumden  16808  divdenle  16809  nn0gcdsq  16812  phicl2  16828  phiprmpw  16836  eulerthlem2  16842  hashgcdlem  16848  hashgcdeq  16850  phisum  16851  nnoddn2prm  16872  pythagtriplem3  16879  pythagtriplem4  16880  pythagtriplem6  16882  pythagtriplem7  16883  pythagtriplem8  16884  pythagtriplem9  16885  pythagtriplem11  16886  pythagtriplem13  16888  pythagtriplem15  16890  pythagtriplem19  16894  pythagtrip  16895  iserodd  16896  pclem  16899  pccl  16910  pcdiv  16913  pcqcl  16917  pcdvds  16925  pcndvds  16927  pcndvds2  16929  pcelnn  16931  pcz  16942  pcmpt  16953  fldivp1  16958  pcfac  16960  infpnlem1  16971  prmunb  16975  prmreclem1  16977  1arith  16988  ram0  17083  prmdvdsprmo  17103  prmgaplem4  17115  prmgaplem6  17117  prmgaplem7  17118  cshwshashlem2  17157  setsstruct2  17235  mulgnn  19142  mulgaddcom  19165  mulginvcom  19166  mulgmodid  19180  ghmmulg  19299  dfod2  19635  gexdvds  19655  gexnnod  19659  gexex  19924  mulgass2  20393  qsssubdrg  21557  prmirredlem  21603  znidomb  21692  znrrg  21696  chfacfisf  22992  chfacfisfcpmat  22993  chfacfscmul0  22996  chfacfpmmul0  23000  cayhamlem1  23004  cpmadugsumlemF  23014  lmmo  23518  1stckgenlem  23691  imasdsf1olem  24511  clmmulg  25241  cmetcaulem  25428  ovolunlem1a  25636  ovolicc2lem4  25660  mbfi1fseqlem6  25860  dvexp3  26118  dgreq0  26403  elqaalem2  26462  aaliou3lem1  26486  aaliou3lem2  26487  aaliou3lem3  26488  aaliou3lem9  26494  pserdvlem2  26572  logtayl2  26808  root1eq1  26901  root1cj  26902  zrtdvds  26905  logbgcd1irr  26940  atantayl2  27084  birthdaylem2  27098  birthdaylem3  27099  emcllem5  27145  basellem2  27227  basellem3  27228  basellem5  27230  issqf  27281  sgmnncl  27292  prmorcht  27323  mumullem1  27324  mumullem2  27325  sqff1o  27327  dvdsflsumcom  27333  muinv  27338  vmalelog  27350  chtublem  27356  vmasum  27361  logfac2  27362  logfaclbnd  27367  bclbnd  27425  bposlem5  27433  lgsval4a  27464  lgssq2  27483  lgsdchr  27500  gausslemma2dlem0c  27503  gausslemma2dlem0e  27505  gausslemma2dlem1a  27510  gausslemma2dlem5  27516  lgsquadlem1  27525  lgsquadlem2  27526  lgsquad3  27532  2lgslem1a1  27534  2lgslem3  27549  2lgsoddprm  27561  2sqnn  27584  2sqreunnltlem  27595  rplogsumlem1  27629  rplogsumlem2  27630  dchrisumlem2  27635  dchrmusumlema  27638  dchrmusum2  27639  dchrvmasumiflem1  27646  dchrvmaeq0  27649  dchrisum0flblem2  27654  dchrisum0re  27658  dchrisum0lema  27659  dchrisum0lem1b  27660  dchrisum0lem2a  27662  logdivbnd  27701  pntrsumbnd2  27712  ostth2lem1  27763  ostth2lem3  27780  ostth3  27783  axlowdimlem13  29285  crctcshwlkn0lem4  30143  crctcshwlkn0lem5  30144  crctcshwlkn0lem7  30146  wlkiswwlksupgr2  30207  clwwisshclwwslem  30346  clwwlkinwwlk  30372  clwwlkel  30378  clwwlkf  30379  wwlksubclwwlk  30390  clwwlkvbij  30445  eucrctshift  30575  eucrct2eupth  30577  numclwlk2lem2f  30709  bcm1n  33121  pnfinf  33484  isarchiofld  33500  1fldgenq  33624  rearchi  33647  submat1n  34176  lmatfvlem  34186  esumcvg  34457  oddpwdc  34725  fibp1  34772  chtvalz  34997  nnltp1ne  35583  erdszelem7  35670  climuzcnv  36144  elfzm12  36148  bcprod  36211  nn0prpwlem  36814  knoppndvlem1  37082  knoppndvlem2  37083  knoppndvlem7  37088  knoppndvlem18  37099  poimirlem13  38265  poimirlem14  38266  mblfinlem2  38290  fzmul  38373  incsequz  38380  geomcau  38391  heibor1lem  38441  bfplem2  38455  lcmfunnnd  42760  posbezout  42848  unitscyglem4  42946  dvdsexpnn  43075  dvdsexpnn0  43076  fimgmcyc  43285  fzsplit1nn0  43468  irrapxlem1  43532  pellexlem5  43543  rmynn  43666  jm2.24nn  43669  jm2.17c  43672  congrep  43683  congabseq  43684  acongrep  43690  acongeq  43693  jm2.18  43698  jm2.23  43706  jm2.20nn  43707  jm2.26lem3  43711  jm2.26  43712  jm2.15nn0  43713  jm2.16nn0  43714  jm2.27dlem2  43720  rmydioph  43724  jm3.1  43730  expdiophlem1  43731  expdioph  43733  idomodle  43901  proot1ex  43906  nznngen  45009  sumnnodd  46329  stoweidlem7  46704  stoweidlem17  46714  wallispilem4  46765  stirlinglem2  46772  stirlinglem3  46773  stirlinglem4  46774  stirlinglem12  46782  stirlinglem13  46783  stirlinglem14  46784  stirlinglem15  46785  stirlingr  46787  dirkertrigeqlem1  46795  fouriersw  46928  ovnsubaddlem1  47267  sqrtnnaa  47587  subsubelfzo0  48047  2ffzoeq  48048  nnmul2  48050  ceilhalfelfzo1  48054  2tceilhalfelfzo1  48056  difltmodne  48068  addmodne  48070  submodlt  48076  facnn0dvdsfac  48105  muldvdsfacgt  48106  iccpartres  48150  iccpartipre  48153  iccpartltu  48157  iccelpart  48165  odz2prm2pw  48298  fmtnoprmfac2lem1  48301  2pwp1prm  48324  lighneallem2  48341  lighneallem4  48345  lighneal  48346  proththd  48349  nneoALTV  48420  divgcdoddALTV  48430  fpprmod  48475  fppr2odd  48479  dfwppr  48486  fpprwppr  48487  fpprwpprb  48488  gbowge7  48511  gbege6  48513  gpg3kgrtriexlem2  48832  gpg3kgrtriexlem3  48833  gpg3kgrtriexlem5  48835  gpg3kgrtriexlem6  48836  altgsumbc  49115  altgsumbcALT  49116  pw2m1lepw2m1  49283  nnpw2even  49292  nnlog2ge0lt1  49329  logbpw2m1  49330  blenpw2m1  49342  nnpw2blenfzo  49344  nnpw2pmod  49346  nnpw2p  49349  blengt1fldiv2p1  49356  dignn0fr  49364  dignn0flhalflem1  49378  dignn0flhalflem2  49379  nn0sumshdiglemA  49382  nn0sumshdiglemB  49383