Theorem nnz 12630

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

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1102   = wceq 1570   ∈ wcel 2146  ℝcr 11117  0cc0 11118  -cneg 11460  ℕcn 12251  ℤcz 12609

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 5262  ax-nul 5274  ax-pr 5409  ax-un 7745  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-addrcl 11179  ax-mulcl 11180  ax-mulrcl 11181  ax-i2m1 11186  ax-1ne0 11187  ax-rrecex 11190  ax-cnre 11191

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 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7426  df-om 7872  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-neg 11462  df-nn 12252  df-z 12610

This theorem is used by:  nnssz  12631  elnnz1  12638  znegcl  12647  nnleltp1  12669  nnltp1le  12670  nnlem1lt  12680  nnltlem1  12681  nnm1ge0  12682  prime  12695  nneo  12698  zeo  12700  btwnz  12717  eluz2b2  12963  qaddcl  13007  qreccl  13011  elpqb  13018  elfz1end  13601  fznatpl1  13625  fznn  13639  elfz1b  13640  elfzo0  13748  elfzo0z  13749  elfzo1  13760  fzo1fzo0n0  13763  elfzom1p1elfzo  13793  ubmelm1fzo  13811  quoremz  13908  intfracq  13912  fznnfl  13915  zmodcl  13944  zmodfz  13946  zmodfzo  13947  zmodid2  13952  zmodidfzo  13953  modfzo0difsn  13999  expnnval  14120  mulexpz  14158  nnesq  14283  expnlbnd  14289  expnlbnd2  14290  digit2  14292  faclbnd  14346  bc0k  14367  bcval5  14374  fz1isolem  14518  seqcoll  14521  ccatval21sw  14643  lswccatn0lsw  14650  cshwidxmod  14866  cshwidxn  14872  absexpz  15382  climuni  15629  isercoll  15745  climcnds  15931  arisum  15940  trireciplem  15942  expcnv  15944  pwdif  15948  geo2sum  15953  geo2lim  15955  0.999...  15961  geoihalfsum  15962  rpnnen2lem6  16300  rpnnen2lem9  16303  rpnnen2lem10  16304  dvdsval3  16339  nndivdvds  16344  modmulconst  16371  dvdsle  16393  dvdsssfz1  16401  fzm1ndvds  16405  dvdsfac  16409  mulmoddvds  16413  oexpneg  16428  nnoddm1d2  16469  pwp1fsum  16474  divalg2  16488  divalgmod  16489  modremain  16491  ndvdsadd  16493  nndvdslegcd  16588  divgcdz  16594  divgcdnn  16598  divgcdnnr  16599  modgcd  16615  gcdmultiple  16619  gcddiv  16634  gcdzeq  16635  gcdeq  16636  rpmulgcd  16640  rplpwr  16641  rprpwr  16642  nn0rppwr  16644  sqgcd  16645  nn0expgcd  16647  dvdssqlem  16649  dvdssq  16650  eucalginv  16667  lcmgcdlem  16689  lcmgcdnn  16694  lcmass  16697  lcmftp  16719  lcmfunsnlem2lem1  16721  coprmgcdb  16732  qredeq  16740  qredeu  16741  coprmprod  16744  coprmproddvdslem  16745  coprmproddvds  16746  cncongr1  16750  cncongr2  16751  1idssfct  16763  isprm2lem  16764  isprm3  16766  prmind2  16768  ge2nprmge4  16785  divgcdodd  16794  isprm6  16798  ncoprmlnprm  16812  divnumden  16832  divdenle  16833  nn0gcdsq  16836  phicl2  16852  phiprmpw  16860  eulerthlem2  16866  hashgcdlem  16872  hashgcdeq  16874  phisum  16875  nnoddn2prm  16896  pythagtriplem3  16903  pythagtriplem4  16904  pythagtriplem6  16906  pythagtriplem7  16907  pythagtriplem8  16908  pythagtriplem9  16909  pythagtriplem11  16910  pythagtriplem13  16912  pythagtriplem15  16914  pythagtriplem19  16918  pythagtrip  16919  iserodd  16920  pclem  16923  pccl  16934  pcdiv  16937  pcqcl  16941  pcdvds  16949  pcndvds  16951  pcndvds2  16953  pcelnn  16955  pcz  16966  pcmpt  16977  fldivp1  16982  pcfac  16984  infpnlem1  16995  prmunb  16999  prmreclem1  17001  1arith  17012  ram0  17107  prmdvdsprmo  17127  prmgaplem4  17139  prmgaplem6  17141  prmgaplem7  17142  cshwshashlem2  17181  setsstruct2  17259  mulgnn  19172  mulgaddcom  19195  mulginvcom  19196  mulgmodid  19210  ghmmulg  19329  dfod2  19665  gexdvds  19685  gexnnod  19689  gexex  19954  mulgass2  20425  qsssubdrg  21613  prmirredlem  21659  znidomb  21748  znrrg  21752  chfacfisf  23048  chfacfisfcpmat  23049  chfacfscmul0  23052  chfacfpmmul0  23056  cayhamlem1  23060  cpmadugsumlemF  23070  lmmo  23574  1stckgenlem  23747  imasdsf1olem  24567  clmmulg  25297  cmetcaulem  25484  ovolunlem1a  25692  ovolicc2lem4  25716  mbfi1fseqlem6  25916  dvexp3  26174  dgreq0  26459  elqaalem2  26518  aaliou3lem1  26542  aaliou3lem2  26543  aaliou3lem3  26544  aaliou3lem9  26550  pserdvlem2  26628  logtayl2  26864  root1eq1  26957  root1cj  26958  zrtdvds  26961  logbgcd1irr  26996  atantayl2  27140  birthdaylem2  27154  birthdaylem3  27155  emcllem5  27201  basellem2  27283  basellem3  27284  basellem5  27286  issqf  27337  sgmnncl  27348  prmorcht  27379  mumullem1  27380  mumullem2  27381  sqff1o  27383  dvdsflsumcom  27389  muinv  27394  vmalelog  27406  chtublem  27412  vmasum  27417  logfac2  27418  logfaclbnd  27423  bclbnd  27481  bposlem5  27489  lgsval4a  27520  lgssq2  27539  lgsdchr  27556  gausslemma2dlem0c  27559  gausslemma2dlem0e  27561  gausslemma2dlem1a  27566  gausslemma2dlem5  27572  lgsquadlem1  27581  lgsquadlem2  27582  lgsquad3  27588  2lgslem1a1  27590  2lgslem3  27605  2lgsoddprm  27617  2sqnn  27640  2sqreunnltlem  27651  rplogsumlem1  27685  rplogsumlem2  27686  dchrisumlem2  27691  dchrmusumlema  27694  dchrmusum2  27695  dchrvmasumiflem1  27702  dchrvmaeq0  27705  dchrisum0flblem2  27710  dchrisum0re  27714  dchrisum0lema  27715  dchrisum0lem1b  27716  dchrisum0lem2a  27718  logdivbnd  27757  pntrsumbnd2  27768  ostth2lem1  27819  ostth2lem3  27836  ostth3  27839  axlowdimlem13  29341  crctcshwlkn0lem4  30199  crctcshwlkn0lem5  30200  crctcshwlkn0lem7  30202  wlkiswwlksupgr2  30263  clwwisshclwwslem  30402  clwwlkinwwlk  30428  clwwlkel  30434  clwwlkf  30435  wwlksubclwwlk  30446  clwwlkvbij  30501  eucrctshift  30631  eucrct2eupth  30633  numclwlk2lem2f  30765  bcm1n  33177  pnfinf  33534  isarchiofld  33550  1fldgenq  33674  rearchi  33697  submat1n  34226  lmatfvlem  34236  esumcvg  34507  oddpwdc  34776  fibp1  34823  chtvalz  35048  nnltp1ne  35626  erdszelem7  35710  climuzcnv  36184  elfzm12  36188  bcprod  36251  nn0prpwlem  36874  knoppndvlem1  37142  knoppndvlem2  37143  knoppndvlem7  37148  knoppndvlem18  37159  poimirlem13  38325  poimirlem14  38326  mblfinlem2  38350  fzmul  38433  incsequz  38440  geomcau  38451  heibor1lem  38501  bfplem2  38515  lcmfunnnd  42820  posbezout  42908  unitscyglem4  43006  dvdsexpnn  43135  dvdsexpnn0  43136  fimgmcyc  43343  fzsplit1nn0  43526  irrapxlem1  43590  pellexlem5  43601  rmynn  43724  jm2.24nn  43727  jm2.17c  43730  congrep  43741  congabseq  43742  acongrep  43748  acongeq  43751  jm2.18  43756  jm2.23  43764  jm2.20nn  43765  jm2.26lem3  43769  jm2.26  43770  jm2.15nn0  43771  jm2.16nn0  43772  jm2.27dlem2  43778  rmydioph  43782  jm3.1  43788  expdiophlem1  43789  expdioph  43791  idomodle  43959  proot1ex  43964  nznngen  45067  sumnnodd  46387  stoweidlem7  46762  stoweidlem17  46772  wallispilem4  46823  stirlinglem2  46830  stirlinglem3  46831  stirlinglem4  46832  stirlinglem12  46840  stirlinglem13  46841  stirlinglem14  46842  stirlinglem15  46843  stirlingr  46845  dirkertrigeqlem1  46853  fouriersw  46986  ovnsubaddlem1  47325  sqrtnnaa  47645  subsubelfzo0  48105  2ffzoeq  48106  nnmul2  48108  ceilhalfelfzo1  48112  2tceilhalfelfzo1  48114  difltmodne  48126  addmodne  48128  submodlt  48134  facnn0dvdsfac  48163  muldvdsfacgt  48164  iccpartres  48208  iccpartipre  48211  iccpartltu  48215  iccelpart  48223  odz2prm2pw  48356  fmtnoprmfac2lem1  48359  2pwp1prm  48382  lighneallem2  48399  lighneallem4  48403  lighneal  48404  proththd  48407  nneoALTV  48478  divgcdoddALTV  48488  fpprmod  48533  fppr2odd  48537  dfwppr  48544  fpprwppr  48545  fpprwpprb  48546  gbowge7  48569  gbege6  48571  gpg3kgrtriexlem2  48890  gpg3kgrtriexlem3  48891  gpg3kgrtriexlem5  48893  gpg3kgrtriexlem6  48894  altgsumbc  49173  altgsumbcALT  49174  pw2m1lepw2m1  49341  nnpw2even  49350  nnlog2ge0lt1  49387  logbpw2m1  49388  blenpw2m1  49400  nnpw2blenfzo  49402  nnpw2pmod  49404  nnpw2p  49407  blengt1fldiv2p1  49414  dignn0fr  49422  dignn0flhalflem1  49436  dignn0flhalflem2  49437  nn0sumshdiglemA  49440  nn0sumshdiglemB  49441