Theorem nnz 12622

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

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1102   = wceq 1570   ∈ wcel 2146  ℝcr 11109  0cc0 11110  -cneg 11452  ℕcn 12243  ℤcz 12601

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5260  ax-nul 5272  ax-pr 5407  ax-un 7738  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-i2m1 11178  ax-1ne0 11179  ax-rrecex 11182  ax-cnre 11183

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 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4876  df-iun 4961  df-br 5113  df-opab 5177  df-mpt 5196  df-tr 5222  df-id 5559  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-we 5619  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7419  df-om 7865  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-neg 11454  df-nn 12244  df-z 12602

This theorem is used by:  nnssz  12623  elnnz1  12630  znegcl  12639  nnleltp1  12661  nnltp1le  12662  nnlem1lt  12672  nnltlem1  12673  nnm1ge0  12674  prime  12687  nneo  12690  zeo  12692  btwnz  12709  eluz2b2  12955  qaddcl  12999  qreccl  13003  elpqb  13010  elfz1end  13593  fznatpl1  13617  fznn  13631  elfz1b  13632  elfzo0  13740  elfzo0z  13741  elfzo1  13752  fzo1fzo0n0  13755  elfzom1p1elfzo  13785  ubmelm1fzo  13803  quoremz  13899  intfracq  13903  fznnfl  13906  zmodcl  13935  zmodfz  13937  zmodfzo  13938  zmodid2  13943  zmodidfzo  13944  modfzo0difsn  13990  expnnval  14111  mulexpz  14149  nnesq  14274  expnlbnd  14280  expnlbnd2  14281  digit2  14283  faclbnd  14337  bc0k  14358  bcval5  14365  fz1isolem  14509  seqcoll  14512  ccatval21sw  14634  lswccatn0lsw  14640  cshwidxmod  14851  cshwidxn  14857  absexpz  15367  climuni  15614  isercoll  15730  climcnds  15916  arisum  15925  trireciplem  15927  expcnv  15929  pwdif  15933  geo2sum  15938  geo2lim  15940  0.999...  15946  geoihalfsum  15947  rpnnen2lem6  16285  rpnnen2lem9  16288  rpnnen2lem10  16289  dvdsval3  16324  nndivdvds  16329  modmulconst  16356  dvdsle  16378  dvdsssfz1  16386  fzm1ndvds  16390  dvdsfac  16394  mulmoddvds  16398  oexpneg  16413  nnoddm1d2  16454  pwp1fsum  16459  divalg2  16473  divalgmod  16474  modremain  16476  ndvdsadd  16478  nndvdslegcd  16573  divgcdz  16579  divgcdnn  16583  divgcdnnr  16584  modgcd  16600  gcdmultiple  16604  gcddiv  16619  gcdzeq  16620  gcdeq  16621  rpmulgcd  16625  rplpwr  16626  rprpwr  16627  nn0rppwr  16629  sqgcd  16630  nn0expgcd  16632  dvdssqlem  16634  dvdssq  16635  eucalginv  16652  lcmgcdlem  16674  lcmgcdnn  16679  lcmass  16682  lcmftp  16704  lcmfunsnlem2lem1  16706  coprmgcdb  16717  qredeq  16725  qredeu  16726  coprmprod  16729  coprmproddvdslem  16730  coprmproddvds  16731  cncongr1  16735  cncongr2  16736  1idssfct  16748  isprm2lem  16749  isprm3  16751  prmind2  16753  ge2nprmge4  16770  divgcdodd  16779  isprm6  16783  ncoprmlnprm  16797  divnumden  16817  divdenle  16818  nn0gcdsq  16821  phicl2  16837  phiprmpw  16845  eulerthlem2  16851  hashgcdlem  16857  hashgcdeq  16859  phisum  16860  nnoddn2prm  16881  pythagtriplem3  16888  pythagtriplem4  16889  pythagtriplem6  16891  pythagtriplem7  16892  pythagtriplem8  16893  pythagtriplem9  16894  pythagtriplem11  16895  pythagtriplem13  16897  pythagtriplem15  16899  pythagtriplem19  16903  pythagtrip  16904  iserodd  16905  pclem  16908  pccl  16919  pcdiv  16922  pcqcl  16926  pcdvds  16934  pcndvds  16936  pcndvds2  16938  pcelnn  16940  pcz  16951  pcmpt  16962  fldivp1  16967  pcfac  16969  infpnlem1  16980  prmunb  16984  prmreclem1  16986  1arith  16997  ram0  17092  prmdvdsprmo  17112  prmgaplem4  17124  prmgaplem6  17126  prmgaplem7  17127  cshwshashlem2  17166  setsstruct2  17244  mulgnn  19151  mulgaddcom  19174  mulginvcom  19175  mulgmodid  19189  ghmmulg  19308  dfod2  19644  gexdvds  19664  gexnnod  19668  gexex  19933  mulgass2  20403  qsssubdrg  21591  prmirredlem  21637  znidomb  21726  znrrg  21730  chfacfisf  23026  chfacfisfcpmat  23027  chfacfscmul0  23030  chfacfpmmul0  23034  cayhamlem1  23038  cpmadugsumlemF  23048  lmmo  23552  1stckgenlem  23725  imasdsf1olem  24545  clmmulg  25275  cmetcaulem  25462  ovolunlem1a  25670  ovolicc2lem4  25694  mbfi1fseqlem6  25894  dvexp3  26152  dgreq0  26437  elqaalem2  26496  aaliou3lem1  26520  aaliou3lem2  26521  aaliou3lem3  26522  aaliou3lem9  26528  pserdvlem2  26606  logtayl2  26842  root1eq1  26935  root1cj  26936  zrtdvds  26939  logbgcd1irr  26974  atantayl2  27118  birthdaylem2  27132  birthdaylem3  27133  emcllem5  27179  basellem2  27261  basellem3  27262  basellem5  27264  issqf  27315  sgmnncl  27326  prmorcht  27357  mumullem1  27358  mumullem2  27359  sqff1o  27361  dvdsflsumcom  27367  muinv  27372  vmalelog  27384  chtublem  27390  vmasum  27395  logfac2  27396  logfaclbnd  27401  bclbnd  27459  bposlem5  27467  lgsval4a  27498  lgssq2  27517  lgsdchr  27534  gausslemma2dlem0c  27537  gausslemma2dlem0e  27539  gausslemma2dlem1a  27544  gausslemma2dlem5  27550  lgsquadlem1  27559  lgsquadlem2  27560  lgsquad3  27566  2lgslem1a1  27568  2lgslem3  27583  2lgsoddprm  27595  2sqnn  27618  2sqreunnltlem  27629  rplogsumlem1  27663  rplogsumlem2  27664  dchrisumlem2  27669  dchrmusumlema  27672  dchrmusum2  27673  dchrvmasumiflem1  27680  dchrvmaeq0  27683  dchrisum0flblem2  27688  dchrisum0re  27692  dchrisum0lema  27693  dchrisum0lem1b  27694  dchrisum0lem2a  27696  logdivbnd  27735  pntrsumbnd2  27746  ostth2lem1  27797  ostth2lem3  27814  ostth3  27817  axlowdimlem13  29319  crctcshwlkn0lem4  30177  crctcshwlkn0lem5  30178  crctcshwlkn0lem7  30180  wlkiswwlksupgr2  30241  clwwisshclwwslem  30380  clwwlkinwwlk  30406  clwwlkel  30412  clwwlkf  30413  wwlksubclwwlk  30424  clwwlkvbij  30479  eucrctshift  30609  eucrct2eupth  30611  numclwlk2lem2f  30743  bcm1n  33155  pnfinf  33516  isarchiofld  33532  1fldgenq  33656  rearchi  33679  submat1n  34208  lmatfvlem  34218  esumcvg  34489  oddpwdc  34757  fibp1  34804  chtvalz  35029  nnltp1ne  35614  erdszelem7  35701  climuzcnv  36175  elfzm12  36179  bcprod  36242  nn0prpwlem  36865  knoppndvlem1  37133  knoppndvlem2  37134  knoppndvlem7  37139  knoppndvlem18  37150  poimirlem13  38316  poimirlem14  38317  mblfinlem2  38341  fzmul  38424  incsequz  38431  geomcau  38442  heibor1lem  38492  bfplem2  38506  lcmfunnnd  42811  posbezout  42899  unitscyglem4  42997  dvdsexpnn  43126  dvdsexpnn0  43127  fimgmcyc  43334  fzsplit1nn0  43517  irrapxlem1  43581  pellexlem5  43592  rmynn  43715  jm2.24nn  43718  jm2.17c  43721  congrep  43732  congabseq  43733  acongrep  43739  acongeq  43742  jm2.18  43747  jm2.23  43755  jm2.20nn  43756  jm2.26lem3  43760  jm2.26  43761  jm2.15nn0  43762  jm2.16nn0  43763  jm2.27dlem2  43769  rmydioph  43773  jm3.1  43779  expdiophlem1  43780  expdioph  43782  idomodle  43950  proot1ex  43955  nznngen  45058  sumnnodd  46378  stoweidlem7  46753  stoweidlem17  46763  wallispilem4  46814  stirlinglem2  46821  stirlinglem3  46822  stirlinglem4  46823  stirlinglem12  46831  stirlinglem13  46832  stirlinglem14  46833  stirlinglem15  46834  stirlingr  46836  dirkertrigeqlem1  46844  fouriersw  46977  ovnsubaddlem1  47316  sqrtnnaa  47636  subsubelfzo0  48096  2ffzoeq  48097  nnmul2  48099  ceilhalfelfzo1  48103  2tceilhalfelfzo1  48105  difltmodne  48117  addmodne  48119  submodlt  48125  facnn0dvdsfac  48154  muldvdsfacgt  48155  iccpartres  48199  iccpartipre  48202  iccpartltu  48206  iccelpart  48214  odz2prm2pw  48347  fmtnoprmfac2lem1  48350  2pwp1prm  48373  lighneallem2  48390  lighneallem4  48394  lighneal  48395  proththd  48398  nneoALTV  48469  divgcdoddALTV  48479  fpprmod  48524  fppr2odd  48528  dfwppr  48535  fpprwppr  48536  fpprwpprb  48537  gbowge7  48560  gbege6  48562  gpg3kgrtriexlem2  48881  gpg3kgrtriexlem3  48882  gpg3kgrtriexlem5  48884  gpg3kgrtriexlem6  48885  altgsumbc  49164  altgsumbcALT  49165  pw2m1lepw2m1  49332  nnpw2even  49341  nnlog2ge0lt1  49378  logbpw2m1  49379  blenpw2m1  49391  nnpw2blenfzo  49393  nnpw2pmod  49395  nnpw2p  49398  blengt1fldiv2p1  49405  dignn0fr  49413  dignn0flhalflem1  49427  dignn0flhalflem2  49428  nn0sumshdiglemA  49431  nn0sumshdiglemB  49432